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