1structure QbfConv :> QbfConv = struct 2 3 open Canon Conv Feedback boolSyntax 4 5 local open Tactical bossLib simpLib boolSimps boolTheory Thm 6 val QMETIS_TAC = Feedback.trace ("metis", 0) (METIS_TAC []) 7 val th1 = Tactical.prove(``(!x. (x \/ P)) = P``, QMETIS_TAC) 8 val th2 = prove(``(!x. (~x \/ P)) = P``,SIMP_TAC bool_ss []) 9 val th3 = SYM F_DEF 10 val th4 = prove(``(!x. ~x) = F``,SIMP_TAC bool_ss []) 11 val th5 = AC DISJ_COMM DISJ_ASSOC 12 val th6 = AC CONJ_COMM CONJ_ASSOC 13 in 14 val simp_clauses = SIMP_CONV bool_ss [th1,th2,th3,th4,th5,th6] 15 end 16 17 local 18 open boolSyntax boolTheory markerLib 19 fun literal x t = t = x orelse dest_neg t = x handle HOL_ERR _ => false 20 in 21 val remove_forall = 22 Ho_Rewrite.PURE_REWRITE_CONV [FORALL_AND_THM] THENC 23 EVERY_CONJ_CONV (fn t => 24 let val (x,_) = dest_forall t in 25 CHANGED_CONV (Rewrite.PURE_REWRITE_CONV [FORALL_SIMP]) 26 ORELSEC 27 QUANT_CONV (move_disj_left (literal x)) 28 end t) THENC 29 simp_clauses 30 end 31 32 fun last_quant_conv c = let 33 exception Innermost 34 fun f t = 35 QUANT_CONV f t handle 36 HOL_ERR {origin_function="RAND_CONV",...} => raise Innermost 37 | Innermost => c t 38 in f end 39 40 fun strip_prefix_conv c = let 41 fun f tm = 42 (if is_forall tm orelse is_exists tm 43 then STRIP_QUANT_CONV f 44 else c) tm 45 in f end 46 47 fun last_quant_seq_conv cq cb = let 48 fun f t = 49 (QUANT_CONV f THENC cq) t handle 50 HOL_ERR {origin_function="RAND_CONV",...} => cb t 51 in f end 52 53 fun last_forall_seq_conv cq cb = let 54 exception Innermost 55 fun f tm = 56 if is_exists tm then STRIP_QUANT_CONV f tm 57 else if is_forall tm then 58 STRIP_QUANT_CONV 59 (fn t => if is_exists t then f t else raise Innermost) 60 tm 61 handle Innermost => last_quant_seq_conv cq cb tm 62 else cb tm 63 in f end 64 65 val qbf_prenex_conv = 66 (* remove equalities THENC *) 67 PRENEX_CONV THENC 68 (last_forall_seq_conv 69 remove_forall 70 (NNF_CONV NO_CONV true THENC 71 PROP_CNF_CONV THENC 72 simp_clauses)) 73 74end 75