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