1(* ========================================================================= *) 2(* DEFINITIONAL CNF IN HOL. *) 3(* Created by Joe Hurd, February 2002. *) 4(* ========================================================================= *) 5 6(* 7app load ["simpLib", "combinTheory", "boolSimps", "numLib", "normalForms", 8 "defCNFTheory"]; 9guessing_tyvars := false; 10*) 11 12(* 13*) 14structure defCNF :> defCNF = 15struct 16 17open HolKernel Parse boolLib simpLib numLib normalForms defCNFTheory; 18 19(* ------------------------------------------------------------------------- *) 20(* Helper functions. *) 21(* ------------------------------------------------------------------------- *) 22 23fun ERR f s = 24 HOL_ERR {message = s, origin_function = f, origin_structure = "defCNF"}; 25 26fun distinct [] = true 27 | distinct (x :: rest) = not (mem x rest) andalso distinct rest; 28 29val zero = numSyntax.zero_tm 30val suc = numSyntax.suc_tm 31 32val beq = mk_thy_const{Name = "=", Ty = bool --> bool --> bool, Thy = "min"} 33 34fun dest_beq tm = 35 let val (a, b, ty) = dest_eq_ty tm 36 in if ty = bool then (a, b) else raise ERR "dest_beq" "not a bool" 37 end; 38 39val is_beq = can dest_beq; 40 41val OKDEF = prim_mk_const{Thy = "defCNF", Name = "OKDEF"}; 42 43(* ------------------------------------------------------------------------- *) 44(* Definitional Conjunctive Normal Form using variable vectors *) 45(* *) 46(* Example: *) 47(* (~(p = ~(q = r)) = ~(~(p = q) = r)) *) 48(* = *) 49(* ?v. *) 50(* (v 0 = (q = r)) /\ (v 1 = (p = v 0)) /\ (v 2 = (p = ~q)) /\ *) 51(* (v 3 = (v 2 = ~r)) /\ (v 4 = (v 1 = v 3)) /\ v 4 *) 52(* ------------------------------------------------------------------------- *) 53 54 55fun sub_cnf f con defs (a, b) = 56 let 57 val (defs, a) = f defs a 58 val (defs, b) = f defs b 59 val tm = mk_comb (mk_comb (con, a), b) 60 in 61 (defs, tm) 62 end; 63 64fun def_step (defs as (vec, n, ds), tm) = 65 case List.find (fn (_, b) => b = tm) ds of NONE => 66 let 67 val g = mk_comb (vec, n) 68 val n = rhs (concl (REDUCE_CONV (mk_comb (suc, n)))) 69 in 70 ((vec, n, (g, tm) :: ds), g) 71 end 72 | SOME (v, _) => (defs, v); 73 74fun gen_cnf defs tm = 75 if is_conj tm then 76 def_step (sub_cnf gen_cnf conjunction defs (dest_conj tm)) 77 else if is_disj tm then 78 def_step (sub_cnf gen_cnf disjunction defs (dest_disj tm)) 79 else if is_beq tm then 80 def_step (sub_cnf gen_cnf beq defs (dest_beq tm)) 81 else 82 (defs, tm); 83 84fun disj_cnf defs tm = 85 if is_disj tm then sub_cnf disj_cnf disjunction defs (dest_disj tm) 86 else gen_cnf defs tm; 87 88fun conj_cnf defs tm = 89 if is_conj tm then sub_cnf conj_cnf conjunction defs (dest_conj tm) 90 else disj_cnf defs tm; 91 92val DISCH_CONJ = CONV_RULE (REWR_CONV AND_IMP_INTRO) o uncurry DISCH; 93 94val UNIQUE_CONV = let 95 val v = mk_var("v", numSyntax.num --> bool) 96in 97 FIRST_CONV (map (REWR_CONV o GEN v o SYM) (CONJUNCTS UNIQUE_def)) 98end 99 100val DEF_CONV = (REWR_CONV o GSYM o CONJUNCT2) DEF_def; 101 102val FINAL_DEF_CONV = 103 REWR_CONV FINAL_DEF THENC 104 RAND_CONV (RATOR_CONV (RAND_CONV REDUCE_CONV)); 105 106fun TODEF_CONV tm = 107 ((if is_conj tm then RAND_CONV TODEF_CONV else FINAL_DEF_CONV) THENC 108 LAND_CONV UNIQUE_CONV THENC 109 RAND_CONV (RATOR_CONV (RAND_CONV num_CONV)) THENC 110 DEF_CONV) tm; 111 112val AND_TRUEL_CONV = REWR_CONV (CONJUNCT1 (SPEC_ALL AND_CLAUSES)); 113 114local 115 val OKDEF1_CONV = REWR_CONV (CONJUNCT1 OKDEF_def); 116 val OKDEF2_CONV = REWR_CONV (CONJUNCT2 OKDEF_def); 117in 118 fun OKDEF_CONV tm = 119 (OKDEF1_CONV ORELSEC 120 (OKDEF2_CONV THENC 121 LAND_CONV (REWRITE_CONV [OK_def] THENC REDUCE_CONV) THENC 122 AND_TRUEL_CONV THENC 123 RATOR_CONV (RAND_CONV REDUCE_CONV) THENC 124 OKDEF_CONV)) tm; 125end; 126 127fun ELIM_DEFS tm = 128 let 129 val th1 = SYM (QUANT_CONV TODEF_CONV tm) 130 val l = rand (snd (dest_exists (lhs (concl th1)))) 131 val th2 = OKDEF_CONV (mk_comb (mk_comb (OKDEF, zero), l)) 132 in 133 EQ_MP th1 (MATCH_MP CONSISTENCY (EQT_ELIM th2)) 134 end; 135 136val ELIM_DEFS_CONV = EQT_INTRO o ELIM_DEFS; 137 138val pure_def_cnf_cleanup = 139 CONV_RULE (LAND_CONV ((LAND_CONV ELIM_DEFS_CONV) THENC AND_TRUEL_CONV)); 140 141val dcnfgv = ref (K (genvar (num --> bool))) 142val ndefs = ref T 143 144fun PURE_DEF_CNF_VECTOR_CONV tm = 145 let 146 (*val (defs, tm') = conj_cnf (genvar (num --> bool), zero, []) tm*) 147 val (defs, tm') = conj_cnf ((!dcnfgv)(), zero, []) tm 148 val (vec, n, ds) = defs 149 val _ = (ndefs:=n) 150 val eqs = map mk_eq ds 151 val th1 = SYM (REWRITE_CONV (map ASSUME eqs) tm') 152 in 153 case eqs of [] => th1 154 | eq :: rest => 155 let 156 val th2 = GEN vec (foldl DISCH_CONJ (DISCH eq th1) rest) 157 val th3 = HO_MATCH_MP BIGSTEP th2 158 in 159 pure_def_cnf_cleanup th3 160 end 161 end; 162 163val DEF_CNF_VECTOR_CONV = 164 DEF_NNF_CONV THENC PURE_DEF_CNF_VECTOR_CONV THENC CLEANUP_DEF_CNF_CONV; 165 166(* Quick testing 167val Term = Parse.Term; 168val Type = Parse.Type; 169show_assums := true; 170Globals.guessing_tyvars := true; 171app load ["normalFormsTest", "numLib", "arithmeticTheory", "bossLib"]; 172open normalFormsTest numLib arithmeticTheory bossLib; 173Parse.reveal "C"; 174val DEF_CNF_CONV' = 175 time DEF_NNF_CONV THENC 176 time PURE_DEF_CNF_VECTOR_CONV THENC 177 time CLEANUP_DEF_CNF_CONV; 178 179val th = DEF_CNF_CONV' ``~(p = q) ==> q /\ r``; 180PRETTIFY_VARS_CONV (rhs (concl th)); 181 182try DEF_NNF_CONV ``~(p = ~(q = r)) = ~(~(p = q) = r)``; 183try (DEF_CNF_CONV' THENC PRETTIFY_VARS_CONV) 184 ``~(p = ~(q = r)) = ~(~(p = q) = r)``; 185try DEF_CNF_CONV ``(p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s)``; 186 187(* Large formulas *) 188 189val valid1 = time (mk_neg o Term) valid_1; 190 191val _ = time DEF_CNF_CONV' valid1; 192 193(* The pigeon-hole principle *) 194 195fun test n = (((time DEF_CNF_CONV') o time (mk_neg o var_pigeon)) n; n); 196 197test 8; 198test 9; 199test 10; 200test 11; 201test 12; 202test 13; 203test 14; 204test 15; 205test 16; 206test 17; 207test 18; 208test 19; 209test 20; 210 211*) 212 213end 214