1structure Canon_Port :> Canon_Port = 2struct 3 4open HolKernel Parse boolLib liteLib Ho_Rewrite tautLib; 5 6(* Fix the grammar used by this file *) 7val ambient_grammars = Parse.current_grammars(); 8val _ = Parse.temp_set_grammars combinTheory.combin_grammars; 9 10val RIGHT_AND_EXISTS_THM = GSYM RIGHT_EXISTS_AND_THM; 11val LEFT_AND_EXISTS_THM = GSYM LEFT_EXISTS_AND_THM; 12val OR_EXISTS_THM = GSYM EXISTS_OR_THM; 13val AND_FORALL_THM = GSYM FORALL_AND_THM; 14val LEFT_OR_FORALL_THM = GSYM LEFT_FORALL_OR_THM; 15val RIGHT_OR_FORALL_THM = GSYM RIGHT_FORALL_OR_THM; 16val LEFT_IMP_FORALL_THM = GSYM LEFT_EXISTS_IMP_THM; 17val RIGHT_IMP_FORALL_THM = GSYM RIGHT_FORALL_IMP_THM; 18val LEFT_IMP_EXISTS_THM = boolTheory.LEFT_EXISTS_IMP_THM; 19val RIGHT_IMP_EXISTS_THM = GSYM RIGHT_EXISTS_IMP_THM; 20 21fun freesl tml = itlist (union o free_vars) tml [];; 22 23fun is_eqc tm = same_const equality tm 24 25local fun get_heads lconsts tm (sofar as (cheads,vheads)) = 26 let val (v,bod) = dest_forall tm 27 in get_heads (subtract lconsts [v]) bod sofar 28 end 29 handle HOL_ERR _ => 30 let val (l,r) = dest_conj tm handle HOL_ERR _ => dest_disj tm 31 in get_heads lconsts l (get_heads lconsts r sofar) 32 end 33 handle HOL_ERR _ => 34 let val tm' = dest_neg tm 35 in get_heads lconsts tm' sofar 36 end 37 handle HOL_ERR _ => 38 let val (hop,args) = strip_comb tm 39 val len = length args 40 val newheads = 41 if is_const hop orelse mem hop lconsts 42 then (insert (hop,len) cheads, vheads) 43 else if len > 0 44 then (cheads,insert (hop,len) vheads) 45 else sofar 46 in 47 itlist (get_heads lconsts) args newheads 48 end 49in 50 fun get_thm_heads th sofar = get_heads (freesl(hyp th)) (concl th) sofar; 51end; 52 53 54local 55 val APP_CONV = 56 let val eq = ``!f:'a->'b. !x. f x = I f x`` 57 in REWR_CONV (prove (eq, REWRITE_TAC[combinTheory.I_THM])) 58 end 59 60 fun APP_N_CONV n tm = 61 if n = 1 then APP_CONV tm 62 else (RATOR_CONV (APP_N_CONV (n - 1)) THENC APP_CONV) tm 63 64 fun FOL_CONV hddata tm = 65 if is_forall tm then 66 BINDER_CONV (FOL_CONV hddata) tm 67 else 68 if is_conj tm orelse is_disj tm then 69 BINOP_CONV (FOL_CONV hddata) tm 70 else 71 let 72 val (opn,args) = strip_comb tm 73 val th = rev_itlist (C (curry MK_COMB)) 74 (map (FOL_CONV hddata) args) (REFL opn) 75 val tm' = rand(concl th) 76 val n = length args - assoc opn hddata 77 handle HOL_ERR _ => 0 78 in 79 if n = 0 then th 80 else TRANS th (APP_N_CONV n tm') 81 end 82in 83 fun GEN_FOL_CONV (cheads,vheads) = 84 let val hddata = 85 if vheads = [] 86 then let val hops = mk_set (map fst cheads) 87 fun getmin h = 88 let val ns = mapfilter 89 (fn (k,n) => if k=h then n else fail()) cheads 90 in (if length ns < 2 then fail() else h, 91 end_itlist (curry Int.min) ns) 92 end 93 in mapfilter getmin hops 94 end 95 else map (fn t => if is_eqc t then (t,2) else (t,0)) 96 (mk_set (map fst (vheads @ cheads))) 97 in FOL_CONV hddata 98 end 99end 100 101 102local 103 val NOT_EXISTS_UNIQUE_THM = Tactical.prove( 104 ``~(?!x:'a. P x) = (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')``, 105 REWRITE_TAC [EXISTS_UNIQUE_THM, DE_MORGAN_THM,NOT_EXISTS_THM] 106 THEN CONV_TAC (REDEPTH_CONV NOT_FORALL_CONV) 107 THEN REWRITE_TAC [NOT_IMP, CONJ_ASSOC]) 108 val common_tauts = 109 [TAUT `~~p:bool = p`, 110 TAUT `~(p /\ q) = ~p \/ ~q`, 111 TAUT `~(p \/ q) = ~p /\ ~q`, 112 TAUT `~(p ==> q) = p /\ ~q`, 113 TAUT `p ==> q = ~p \/ q`, 114 NOT_FORALL_THM, 115 NOT_EXISTS_THM, 116 EXISTS_UNIQUE_THM, 117 NOT_EXISTS_UNIQUE_THM] 118 and dnf_tauts = 119 map TAUT [`~(p = q) = (p /\ ~q) \/ (~p /\ q)`, 120 `(p = q) = (p /\ q) \/ (~p /\ ~q)`] 121 and cnf_tauts = 122 map TAUT [`~(p = q) = (p \/ q) /\ (~p \/ ~q)`, 123 `(p = q) = (p \/ ~q) /\ (~p \/ q)`] 124 val NNFC_CONV0 = 125 GEN_REWRITE_CONV TOP_SWEEP_CONV (common_tauts @ cnf_tauts) 126in 127val NNFC_CONV = let 128 fun SINGLE_SWEEP_CONV conv tm = let 129 fun continue tm = if is_abs tm then NNFC_CONV0 tm 130 else SUB_CONV (SINGLE_SWEEP_CONV conv) tm 131 in 132 (conv THENC continue) ORELSEC continue 133 end tm 134in 135 SINGLE_SWEEP_CONV (GEN_REWRITE_CONV I (common_tauts @ dnf_tauts)) 136end 137end (* local *) 138 139 140fun has_abs tm = 141 case dest_term tm 142 of LAMB _ => true 143 | COMB(M,N) => if is_const M andalso is_abs N (* binder *) 144 then has_abs (body N) 145 else has_abs N orelse has_abs M 146 | other => false 147 148val DELAMB_CONV = 149 let val pth = prove( 150 ``(((\x. s x) = t) = (!x:'a. s x:'b = t x)) /\ 151 ((s = \x. t x) = (!x. s x = t x))``, 152 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN 153 REWRITE_TAC []) 154 val qconv = 155 TOP_DEPTH_CONV BETA_CONV THENC 156 REPEATC (QCHANGED_CONV (GEN_REWRITE_CONV ONCE_DEPTH_CONV [pth]) THENC 157 TOP_DEPTH_CONV BETA_CONV) 158 159 (* used to be: 160 THENQC (TOP_DEPTH_QCONV BETA_CONV, 161 REPEATQC (THENCQC 162 (GEN_REWRITE_CONV ONCE_DEPTH_QCONV [pth], 163 TRY_CONV(TOP_DEPTH_QCONV BETA_CONV)))) 164 using the liteLib converionals. Here's the argument as to why the 165 replacement has the right effect, and fixes a bug when UNCHANGED 166 exceptions might be flying around 167 168 THENQC(c1, c2) raises a HOL_ERR iff c1 and c2 both raise errors 169 THENCQC(c1, c2) raises a HOL_ERR iff c1 raises an error 170 171 so 172 173 if TOP_DEPTH_QCONV raises a HOL_ERR it will be because it 174 hasn't managed to change the input term at all. The outermost 175 THENQC traps this and moves onto its second argument, which is a 176 REPEATQC. This will raise an error if its argument fails 177 immediately. Its argument will fail iff the GEN_REWRITE_CONV 178 fails, which will happen only if it doesn't change the argument. 179 180 This suggests that the TRY_CONV is redundant. Not only is it 181 redundant, but when it introduces UNCHANGED, it causes the 182 whole conversion to raise UNCHANGED, even though the rewriting 183 has actually done some good. 184 185 so 186 187 the replacement drops the TRY_CONV, and replaces THENQC with 188 THENC, and THENCQC with (QCHANGED_CONV ... THENC ...) This 189 is not always valid, because THENC only traps UNCHANGED, whereas 190 THENQC traps everything, but here the only exceptions coming out 191 of the first argument to THENC will be caused by the input term 192 not changing. 193 *) 194 in 195 fn tm => if has_abs tm then TRY_CONV qconv tm else ALL_CONV tm 196 end; 197 198val PROP_CNF_CONV = 199 GEN_REWRITE_CONV REDEPTH_CONV 200 [TAUT `a \/ (b /\ c) = (a \/ b) /\ (a \/ c)`, 201 TAUT `(a /\ b) \/ c = (a \/ c) /\ (b \/ c)`, 202 GSYM CONJ_ASSOC, GSYM DISJ_ASSOC];; 203 204 205val PRESIMP_CONV = 206 GEN_REWRITE_CONV DEPTH_CONV 207 [NOT_CLAUSES, AND_CLAUSES, OR_CLAUSES, IMP_CLAUSES, EQ_CLAUSES, 208 FORALL_SIMP, EXISTS_SIMP, EXISTS_OR_THM, FORALL_AND_THM, 209 LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM, 210 LEFT_FORALL_OR_THM, RIGHT_FORALL_OR_THM]; 211 212 213val REFUTE_THEN = 214 let val conv = REWR_CONV(TAUT `p = ~p ==> F`) 215 in fn ttac => CONV_TAC conv THEN DISCH_THEN ttac 216 end;; 217 218val SKOLEM_CONV = 219 GEN_REWRITE_CONV REDEPTH_CONV 220 [RIGHT_AND_EXISTS_THM, 221 LEFT_AND_EXISTS_THM, 222 OR_EXISTS_THM, 223 RIGHT_OR_EXISTS_THM, 224 LEFT_OR_EXISTS_THM, 225 SKOLEM_THM]; 226 227local fun STRIP conv tm opt = 228 let val (vlist,M) = strip_binder opt tm 229 in GEN_ABS opt vlist (conv M) 230 end 231in 232fun STRIP_BINDER_CONV conv tm = 233 let val Z = STRIP conv tm 234 in if is_abs tm then Z NONE else 235 if is_forall tm then Z (SOME boolSyntax.universal) else 236 if is_exists tm then Z (SOME boolSyntax.existential) else 237 if is_select tm then Z (SOME boolSyntax.select) else 238 if is_exists1 tm then Z (SOME boolSyntax.exists1) 239 else failwith "STRIP_BINDER_CONV" 240 end 241end; 242 243val PRENEX_CONV = 244 let val PRENEX1_QCONV = GEN_REWRITE_CONV I 245 [NOT_FORALL_THM, NOT_EXISTS_THM, 246 AND_FORALL_THM, LEFT_AND_FORALL_THM, RIGHT_AND_FORALL_THM, 247 LEFT_OR_FORALL_THM, RIGHT_OR_FORALL_THM, 248 LEFT_IMP_FORALL_THM, RIGHT_IMP_FORALL_THM, 249 LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM, 250 OR_EXISTS_THM, LEFT_OR_EXISTS_THM, RIGHT_OR_EXISTS_THM, 251 LEFT_IMP_EXISTS_THM, RIGHT_IMP_EXISTS_THM] 252 fun PRENEX2_QCONV tm = THENCQC(PRENEX1_QCONV,BINDER_CONV PRENEX2_QCONV) tm 253 fun PRENEX_QCONV tm = 254 let val (lop,r) = dest_comb tm 255 in if is_const lop 256 then if same_const lop boolSyntax.universal orelse 257 same_const lop boolSyntax.existential 258 then STRIP_BINDER_CONV PRENEX_QCONV tm 259(* then AP_TERM lop (ABS_CONV PRENEX_QCONV r) *) 260 else if same_const lop boolSyntax.negation 261 then THENQC (RAND_CONV PRENEX_QCONV, PRENEX2_QCONV) tm 262 else failwith "unchanged" 263 else let val (oper,l) = dest_comb lop 264 in if same_const oper boolSyntax.conjunction orelse 265 same_const oper boolSyntax.disjunction orelse 266 same_const oper boolSyntax.implication 267 then let val th = 268 (let val lth = PRENEX_QCONV l 269 in let val rth = PRENEX_QCONV r 270 in MK_COMB(AP_TERM oper lth,rth) 271 end handle HOL_ERR _ => AP_THM(AP_TERM oper lth) r 272 end handle HOL_ERR _ => AP_TERM lop (PRENEX_QCONV r) 273 ) handle HOL_ERR _ => REFL tm 274 in 275 TRANS th (PRENEX2_QCONV (rand(concl th))) 276 end 277 else failwith "unchanged" 278 end 279 end 280 in 281 fn tm => TRY_CONV PRENEX_QCONV tm 282 end; 283 284val _ = Parse.temp_set_grammars ambient_grammars; 285 286end 287