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