1 2(* Non-logical definitional CNF, due to John Harrison. *) 3(* Ported from HOL Light by Hasan Amjad, with HOL4 specific mods. *) 4 5structure def_cnf = 6struct 7 8local 9 10open Lib boolLib Globals Parse Term Type Thm Drule Psyntax Conv Feedback boolSyntax 11 12open satCommonTools satTheory 13 14val dpfx = "dcnf_" 15 16in 17 18val presimp_conv = QCONV (GEN_REWRITE_CONV REDEPTH_CONV empty_rewrites 19 [NOT_CLAUSES, AND_CLAUSES, OR_CLAUSES, IMP_CLAUSES, EQ_CLAUSES, COND_EXPAND, 20 COND_CLAUSES]) 21 22(* ------------------------------------------------------------------------- *) 23(* Split up a theorem according to conjuncts, in a general sense. *) 24(* ------------------------------------------------------------------------- *) 25local 26val p_tm = mk_var("p",bool) 27val q_tm = mk_var("q",bool) 28fun is_literal tm = is_var tm orelse (is_neg tm andalso is_var(rand tm)) 29val spine_disj = HolKernel.spine_binop (total dest_disj) (*FIXME: fold is_lit check into this *) 30fun is_clausal tm = 31 let val djs = spine_disj tm 32 in all is_literal djs end 33in 34val GCONJUNCTS = 35 let fun GCONJUNCTS' th acc = 36 let val (opr,args) = strip_comb (concl th) 37 in if not (is_const opr) then th::acc else 38 case fst (dest_const opr) of 39 "~" => 40 let val (opr,args) = strip_comb (hd args) 41 in if not (is_const opr) then th::acc else 42 (case fst (dest_const opr) of 43 "==>" => 44 let val (p,q) = (hd args,last args) 45 in GCONJUNCTS' (MP (INST [p_tm|->p,q_tm|->q] pth_ni1) th) 46 (GCONJUNCTS' (MP (INST [p_tm|->p,q_tm|->q] pth_ni2) th) acc) end 47 | "\\/" => 48 let val (p,q) = (hd args,last args) 49 in GCONJUNCTS' (MP (INST [p_tm|->p,q_tm|->q] pth_no1) th) 50 (GCONJUNCTS' (MP (INST [p_tm|->p,q_tm|->q] pth_no2) th) acc) end 51 | "~" => 52 GCONJUNCTS' (MP (INST [p_tm|->hd args] pth_nn) th) acc 53 | _ => th::acc) 54 end 55 | "/\\" => 56 let val (p,q) = (hd args,last args) 57 in GCONJUNCTS' (CONJUNCT1 th) (GCONJUNCTS' (CONJUNCT2 th) acc) end 58 | _ => th::acc 59 end 60 fun findTF tm = total (HolKernel.find_term (fn t => is_T t orelse is_F t)) tm 61 fun GCONJUNCTS'' th = GCONJUNCTS' th [] 62 in fn tm => fn th => 63 let val ths0 = if is_neg tm andalso is_neg (rand tm) 64 then CONJUNCTSR (CONV_RULE NOT_NOT_CONV th) else [th] 65 val ths1 = List.map GCONJUNCTS'' ths0 66 val is_cnf = ref true 67 val ths2 = List.map (fn th => 68 if is_clausal (concl th) then (true,th) 69 else (is_cnf:=false;(false,th))) (List.concat ths1) 70 val ths3 = if !is_cnf then ths2 else 71 List.map (fn (is_c,th) => 72 if isSome (findTF (concl th)) 73 then (is_c,CONV_RULE presimp_conv th) else (is_c,th)) ths2 74 in (!is_cnf,ths3) end 75 end 76end 77 78(* ------------------------------------------------------------------------- *) 79(* Generate fresh variable names (could just use genvars). *) 80(* ------------------------------------------------------------------------- *) 81 82fun propvar cnfv i = mk_var(cnfv^(int_to_string i),bool) 83 84(* ------------------------------------------------------------------------- *) 85(* Set up the basic definitional arrangement. *) 86(* ------------------------------------------------------------------------- *) 87 88fun localdefs cnfv tm (n,defs,lfn) = 89 if is_neg tm then 90 let val (n1,v1,defs1,lfn1) = localdefs cnfv (rand tm) (n,defs,lfn) 91 val tm' = mk_neg v1 92 in (n1,rbapply defs1 tm',defs1,lfn1) 93 handle NotFound => let val n2 = n1 + 1 94 val v2 = propvar cnfv n2 95 in (n2,v2,RBM.insert(defs1,tm',v2),RBM.insert(lfn1,v2,tm)) end 96 end 97 else if is_conj tm orelse is_disj tm orelse is_imp tm orelse is_eq tm then 98 let val (n1,v1,defs1,lfn1) = localdefs cnfv (land tm) (n,defs,lfn) 99 val (n2,v2,defs2,lfn2) = localdefs cnfv (rand tm) (n1,defs1,lfn1) 100 val tm' = mk_comb(mk_comb(rator(rator tm),v1),v2) 101 in (n2,rbapply defs2 tm',defs2,lfn2) 102 handle NotFound => let val n3 = n2 + 1 103 val v3 = propvar cnfv n3 104 in (n3,v3,RBM.insert(defs2,tm',v3),RBM.insert(lfn2,v3,tm)) end 105 end 106 else if is_cond tm then 107 let val (opr,args) = strip_comb tm 108 val (n1,v1,defs1,lfn1) = localdefs cnfv (List.nth(args,0)) (n,defs,lfn) 109 val (n2,v2,defs2,lfn2) = localdefs cnfv (List.nth(args,1)) (n1,defs1,lfn1) 110 val (n3,v3,defs3,lfn3) = localdefs cnfv (List.nth(args,2)) (n2,defs2,lfn2) 111 val tm' = mk_comb(mk_comb(mk_comb(opr,v1),v2),v3) 112 in (n3,rbapply defs3 tm',defs2,lfn3) 113 handle NotFound => let val n4 = n3 + 1 114 val v4 = propvar cnfv n4 115 in (n4,v4,RBM.insert(defs3,tm',v4),RBM.insert(lfn3,v4,tm)) end 116 end 117 else (n,rbapply defs tm,defs,lfn) 118 handle NotFound => let val n1 = n + 1 119 val v1 = propvar cnfv n1 120 in (n1,v1,RBM.insert(defs,tm,v1),RBM.insert(lfn,v1,tm)) end 121 122(* ------------------------------------------------------------------------- *) 123(* Just translate to fresh variables, but otherwise leave unchanged. *) 124(* ------------------------------------------------------------------------- *) 125 126fun transvar_var cnfv (n,tm,vdefs,lfn) = 127 (n,rbapply vdefs tm,vdefs,lfn) 128 handle NotFound => let val n1 = n + 1 129 val v1 = propvar cnfv n1 130 in (n1,v1,RBM.insert(vdefs,tm,v1),RBM.insert(lfn,v1,tm)) end 131 132fun transvar_lit cnfv (n,tm,vdefs,lfn) = 133 if is_neg tm then 134 let val (n1,tm1,vdefs1,lfn1) = transvar_var cnfv (n,rand tm,vdefs,lfn) 135 in (n1,mk_neg tm1,vdefs1,lfn1) end 136 else transvar_var cnfv (n,tm,vdefs,lfn) 137 138fun transvar_clause cnfv (n,tm,vdefs,lfn) = 139 let val lits = List.rev (strip_disj tm) 140 val (h,t) = (hd lits,tl lits) 141 val (n,tm,vdefs,lfn) = 142 List.foldl 143 (fn (p,(n,tm,vdefs,lfn)) => 144 let val (n1,p1,vdefs1,lfn1) = transvar_lit cnfv (n,p,vdefs,lfn) 145 in (n1,mk_disj(p1,tm),vdefs1,lfn1) end) 146 (transvar_lit cnfv (n,h,vdefs,lfn)) t 147 in (n,tm,vdefs,lfn) end 148 149(* ------------------------------------------------------------------------- *) 150(* Check if something is clausal (slightly stupid). *) 151(* ------------------------------------------------------------------------- *) 152 153(* convert tm to CNF, assuming that it is of the form v = v' op v'' *) 154(* where all the v's are vars, and op is one of [~,\/,/\,==>,=] *) 155(* of course when op is ~, there is only one argument *) 156exception To_cnf_false 157local 158val p_tm = mk_var("p",bool) 159val q_tm = mk_var("q",bool) 160val r_tm = mk_var("r",bool) 161val s_tm = mk_var("s",bool) 162in 163fun to_cnf' tm = 164 let val (l,r) = dest_eq tm 165 val (opr,args) = strip_comb r 166 in case fst (dest_const opr) of 167 "~" => INST [p_tm |-> l, q_tm |-> (hd args)] dc_neg 168 | "\\/" => INST [p_tm |-> l, q_tm |-> (hd args),r_tm |-> (last args)] dc_disj 169 | "/\\" => INST [p_tm |-> l, q_tm |-> (hd args),r_tm |-> (last args)] dc_conj 170 | "==>" => INST [p_tm |-> l, q_tm |-> (hd args),r_tm |-> (last args)] dc_imp 171 | "=" => INST [p_tm |-> l, q_tm |-> (hd args),r_tm |-> (last args)] dc_eq 172 | "COND" => INST [p_tm |-> l, q_tm |-> (hd args), r_tm |-> (hd (tl args)), 173 s_tm |-> (last args)] dc_cond 174 | _ => failwith("to_cnf': "^(fst (dest_const opr))) 175 end 176end 177 178val cnfv_ref = ref "SP" 179 180fun clausify tm lfn eq cls = 181 let val fvs = free_vars eq 182 val eth = to_cnf' eq 183 val tth = INST (map (fn v => v |-> rbapply lfn v) fvs) eth 184 val xth = ADD_ASSUM tm (EQ_MP tth (REFL(rbapply lfn (land eq)))) 185 in zip (strip_conj(rand(concl eth))) (CONJUNCTS xth) @ cls end 186 187fun to_cnf is_cnf tm = 188 if is_cnf then 189 (NONE,HOLset.numItems(FVL[tm](HOLset.empty Term.var_compare)),RBM.mkDict Term.var_compare, 190 Array.fromList (zip (strip_conj(dest_neg tm)) (CONJUNCTSR (ASSUME (dest_neg tm))))) else 191 let 192 val th = ASSUME tm 193 val (is_cnf,ths) = GCONJUNCTS tm th 194 val (cnfv,vc,eqs,tops,lfn) = 195 if is_cnf then 196 let val tops = List.map (fn (_,th) => (concl th,th)) ths 197 in (NONE,HOLset.numItems (FVL [tm] (HOLset.empty Term.var_compare)), 198 [],tops,RBM.mkDict Term.var_compare) end else 199 let 200 val cnfv = (!cnfv_ref) 201 val (n,tops,defs,lfn) = 202 itlist (fn (ic,th) => 203 fn (m,tops,defs,lfn) => 204 let val t = concl th 205 in if is_T t orelse is_F t then (m,tops,defs,lfn) else 206 let val (n,v,defs',lfn') = 207 if ic then transvar_clause cnfv (m,t,defs,lfn) 208 else localdefs cnfv t (m,defs,lfn) 209 in (n,(v,th)::tops,defs',lfn') end 210 end) ths 211 (~1,[],RBM.mkDict Term.compare,RBM.mkDict Term.var_compare) 212 val defg = RBM.foldl (fn (t,nv,a) => (t,nv)::a) [] defs 213 val mdefs = filter (fn (r,_) => not (is_var r)) defg 214 val eqs = map (fn (r,l) => mk_eq(l,r)) mdefs 215 val vc = (n + 1) 216 in (SOME cnfv,vc,eqs,tops,lfn) end 217 val all_clauses = itlist (clausify tm lfn) eqs tops 218 in (cnfv,vc,lfn,Array.fromList all_clauses) end 219 220(* verify that each t \in eqs in to_cnf above is of the required form: v = v' op v'' *) 221(* this is only used during development, for sanity checking *) 222fun verq eqs = 223List.app (fn eq => 224 if is_eq eq then 225 let val (l,r) = dest_eq eq 226 in if not (is_var l) then print "LHS is not a var\n" else 227 let val (opr,args) = strip_comb r 228 in if List.length args>2 then print "RHS op >2 args\n" else 229 if is_neg r then 230 if is_var (hd args) then () else print "neg RHS not a var\n" 231 else if is_conj r orelse is_disj r orelse 232 is_imp r orelse is_eq r 233 then if is_var (hd args) andalso is_var (last args) 234 then () else print "RHS binop args not vars\n" 235 else print "RHS not a recognized op\n" 236 end 237 end 238 else print "Not top-level eq!\n") eqs 239 240 241 242end 243end 244