defCNFScript.sml
1Theory defCNF[bare]
2Ancestors
3 rich_list arithmetic
4Libs
5 HolKernel Parse boolLib simpLib numLib TotalDefn BasicProvers
6
7val _ = ParseExtras.temp_loose_equality()
8
9
10(* ------------------------------------------------------------------------- *)
11(* Definitions. *)
12(* ------------------------------------------------------------------------- *)
13
14Definition UNIQUE_def:
15 (UNIQUE (v:num->bool) n (conn, INL i, INL j) = (v n = conn (v i) (v j))) /\
16 (UNIQUE v n (conn, INL i, INR b) = (v n = conn (v i) b)) /\
17 (UNIQUE v n (conn, INR a, INL j) = (v n = conn a (v j))) /\
18 (UNIQUE v n (conn, INR a, INR b) = (v n = conn a b))
19End
20
21Definition DEF_def:
22 (DEF (v:num->bool) n [] = T) /\
23 (DEF v n (x :: xs) = UNIQUE v n x /\ DEF v (SUC n) xs)
24End
25
26Definition OK_def:
27 (OK n ((conn:bool->bool->bool), INL i, INL j) = i < n /\ j < n) /\
28 (OK n (conn, INL i, INR (b:bool)) = i < n) /\
29 (OK n (conn, INR (a:bool), INL j) = j < n) /\
30 (OK n (conn, INR a, INR b) = T)
31End
32
33Definition OKDEF_def:
34 (OKDEF n [] = T) /\
35 (OKDEF n (x :: xs) = OK n x /\ OKDEF (SUC n) xs)
36End
37
38(* ------------------------------------------------------------------------- *)
39(* Theorems. *)
40(* ------------------------------------------------------------------------- *)
41
42Theorem DEF_SNOC:
43 !n x l v. DEF v n (SNOC x l) = DEF v n l /\ UNIQUE v (n + LENGTH l) x
44Proof
45 (Induct_on `l` THEN1 RW_TAC arith_ss [SNOC, DEF_def, LENGTH]) THEN
46 RW_TAC std_ss [SNOC, LENGTH, DEF_def, ADD_CLAUSES, CONJ_ASSOC]
47QED
48
49Theorem OKDEF_SNOC:
50 !n x l. OKDEF n (SNOC x l) = OKDEF n l /\ OK (n + LENGTH l) x
51Proof
52 (Induct_on `l` THEN1 RW_TAC arith_ss [SNOC, OKDEF_def, LENGTH]) THEN
53 RW_TAC std_ss [SNOC, LENGTH, OKDEF_def, ADD_CLAUSES, CONJ_ASSOC]
54QED
55
56Theorem CONSISTENCY:
57 !n l. OKDEF n l ==> ?v. DEF v n l
58Proof
59 REPEAT GEN_TAC THEN
60 Q.SPEC_TAC (`n`, `n`) THEN
61 Q.SPEC_TAC (`l`, `l`) THEN
62 HO_MATCH_MP_TAC SNOC_INDUCT THEN
63 (CONJ_TAC THEN1 RW_TAC std_ss [DEF_def]) THEN
64 RW_TAC std_ss [OKDEF_SNOC, DEF_SNOC] THEN
65 Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`) THEN
66 RW_TAC std_ss [] THEN
67 (Q_TAC SUFF_TAC
68 `(!w. (!m. m < n + LENGTH l ==> (w m = v m)) ==> DEF w n l) /\
69 ?w. (!m. m < n + LENGTH l ==> (w m = v m)) /\ UNIQUE w (n + LENGTH l) x`
70 THEN1 PROVE_TAC []) THEN
71 CONJ_TAC THENL
72 [STRIP_TAC THEN
73 POP_ASSUM MP_TAC THEN
74 POP_ASSUM (K ALL_TAC) THEN
75 POP_ASSUM MP_TAC THEN
76 Q.SPEC_TAC (`n`, `n`) THEN
77 (Induct_on `l` THEN1 RW_TAC std_ss [DEF_def]) THEN
78 RW_TAC std_ss [LENGTH, ADD_CLAUSES, DEF_def, OKDEF_def] THEN
79 Q.PAT_X_ASSUM `UNIQUE P Q R` MP_TAC THEN
80 Q.PAT_X_ASSUM `OK P Q` MP_TAC THEN
81 Q.PAT_X_ASSUM `!n. OKDEF P Q ==> X` (K ALL_TAC) THEN
82 Q.PAT_X_ASSUM `DEF P Q R` (K ALL_TAC) THEN
83 Q.PAT_X_ASSUM `OKDEF P Q` (K ALL_TAC) THEN
84 (Cases_on `h` THEN
85 Cases_on `r` THEN
86 Cases_on `q'` THEN
87 Cases_on `r'` THEN
88 RW_TAC std_ss [UNIQUE_def, OK_def]) THENL
89 [Q.PAT_X_ASSUM `!m. P m`
90 (fn th =>
91 MP_TAC (Q.SPEC `n` th) THEN
92 MP_TAC (Q.SPEC `x` th) THEN
93 MP_TAC (Q.SPEC `x'` th)) THEN
94 RW_TAC arith_ss [],
95 Q.PAT_X_ASSUM `!m. P m`
96 (fn th =>
97 MP_TAC (Q.SPEC `n` th) THEN
98 MP_TAC (Q.SPEC `x` th)) THEN
99 RW_TAC arith_ss [],
100 Q.PAT_X_ASSUM `!m. P m`
101 (fn th =>
102 MP_TAC (Q.SPEC `n` th) THEN
103 MP_TAC (Q.SPEC `x` th)) THEN
104 RW_TAC arith_ss [],
105 Q.PAT_X_ASSUM `!m. P m`
106 (fn th =>
107 MP_TAC (Q.SPEC `n` th)) THEN
108 RW_TAC arith_ss []],
109 Q.PAT_X_ASSUM `OK P Q` MP_TAC THEN
110 POP_ASSUM_LIST (K ALL_TAC) THEN
111 (Cases_on `x` THEN
112 Cases_on `r` THEN
113 Cases_on `q'` THEN
114 Cases_on `r'` THEN
115 RW_TAC std_ss [UNIQUE_def, OK_def]) THENL
116 [Q.EXISTS_TAC `\m. if m = n + LENGTH l then q (v x) (v x') else v m` THEN
117 RW_TAC arith_ss [],
118 Q.EXISTS_TAC `\m. if m = n + LENGTH l then q (v x) y else v m` THEN
119 RW_TAC arith_ss [],
120 Q.EXISTS_TAC `\m. if m = n + LENGTH l then q y (v x) else v m` THEN
121 RW_TAC arith_ss [],
122 Q.EXISTS_TAC `\m. if m = n + LENGTH l then q y y' else v m` THEN
123 RW_TAC arith_ss []]]
124QED
125
126Theorem BIGSTEP:
127 !P Q R.
128 (!v:num->bool. P v ==> (Q = R v)) ==>
129 ((?v. P v) /\ Q = (?v. P v /\ R v))
130Proof
131 REPEAT STRIP_TAC THEN
132 EQ_TAC THENL [
133 STRIP_TAC THEN
134 EXISTS_TAC ``v:num->bool`` THEN
135 Q.PAT_X_ASSUM `!v:num->bool. A v` (MP_TAC o Q.SPEC `v`) THEN
136 ASM_REWRITE_TAC [],
137 STRIP_TAC THEN
138 Q.PAT_X_ASSUM `!v:num->bool. A v` (MP_TAC o Q.SPEC `v`) THEN
139 ASM_REWRITE_TAC [] THEN
140 STRIP_TAC THEN
141 ASM_REWRITE_TAC [] THEN
142 EXISTS_TAC ``v:num->bool`` THEN
143 ASM_REWRITE_TAC []
144 ]
145QED
146
147Theorem FINAL_DEF:
148 !v n x. (v n = x) = (v n = x) /\ DEF v (SUC n) []
149Proof
150 SIMP_TAC boolSimps.bool_ss [DEF_def]
151QED
152
153val _ = app
154 (fn s => remove_ovl_mapping s {Thy = "defCNF", Name = s})
155 ["OKDEF", "DEF", "UNIQUE", "OK"]
156