1 2(* various operations on terms of type mu, as well as on the ML datatype for mu formulas that is used by the checker *) 3 4structure muSyntax = 5struct 6 7local 8 9open Globals HolKernel Parse 10 11 12open Psyntax bossLib pairTheory pred_setTheory pred_setLib stringLib 13 listTheory simpLib pairSyntax pairLib PrimitiveBddRules 14 DerivedBddRules Binarymap PairRules pairTools boolSyntax Drule 15 Tactical Conv Rewrite Tactic boolTheory listSyntax stringTheory 16 boolSimps pureSimps listSimps numLib 17 18open setLemmasTheory muSyntaxTheory muTheory stringBinTree commonTools ksTools 19 20in 21 22(* shadow syntax for efficiently working with mu formulae. 23 mk_cache translates HOL formula to it and muCheck recurses over it*) 24datatype 'a mu = muTR of 'a (* the type var is for annotating nodes with whatever e.g. pointers into thm cache *) 25 | muFL of 'a 26 | muNot of 'a * ('a mu) 27 | muAnd of 'a * (('a mu) * ('a mu)) 28 | muOr of 'a * (('a mu) * ('a mu)) 29 | muRV of 'a (* relational var *) 30 | muAP of 'a (* atomic proposition *) 31 | muDIAMOND of 'a * (string * ('a mu)) (* diamond *) 32 | muBOX of 'a * (string * ('a mu)) (* box *) 33 | fpmu of 'a * 'a * ('a mu) (* lfp *) 34 | fpnu of 'a * 'a * ('a mu); (* mfp *) 35 36val mu_ty = ``:'a mu`` 37 38fun get_prop_type f = (hd o snd o dest_type o type_of) f 39 40val _ = set_trace "notify type variable guesses" 0; 41val mu_rv_tm = ``muSyntax$RV`` 42val mu_neg_tm = ``muSyntax$Not`` 43val mu_ap_tm = ``muSyntax$AP`` 44val mu_and_tm = ``muSyntax$And`` 45val mu_or_tm = ``muSyntax$Or`` 46val mu_dmd_tm = ``muSyntax$DIAMOND`` 47val mu_box_tm = ``muSyntax$BOX`` 48val mu_mu_tm = ``muSyntax$mu`` 49val mu_nu_tm = ``muSyntax$nu`` 50val mu_T_tm = ``muSyntax$TR`` 51val mu_F_tm = ``muSyntax$FL`` 52val mu_ap_tm = ``muSyntax$AP`` 53val mu_sub_tm = ``muSyntax$SUBFORMULA`` 54val mu_nnf_tm = ``muSyntax$NNF`` 55val mu_imf_tm = ``muSyntax$IMF`` 56val mu_rvneg_tm = ``muSyntax$RVNEG`` 57val _ = set_trace "notify type variable guesses" 1; 58 59fun is_RV f = (is_comb f andalso is_const (rator f) andalso String.compare("RV",(fst o dest_const o rator) f)=EQUAL) 60fun is_mu mf = is_comb mf andalso (Term.compare(fst(strip_comb mf),inst[alpha|->get_prop_type mf] mu_mu_tm)=EQUAL) 61fun is_nu mf = is_comb mf andalso (Term.compare(fst(strip_comb mf),inst[alpha|->get_prop_type mf] mu_nu_tm)=EQUAL) 62fun is_fp mf = is_nu mf orelse is_mu mf 63 64fun mu_RV p_ty rv = mk_comb(inst[alpha|->p_ty] mu_rv_tm,rv) 65fun mu_AP p = mk_comb(inst [alpha|->(type_of p)] mu_ap_tm,p) 66fun mu_neg f = mk_comb(inst [alpha|->get_prop_type f] mu_neg_tm, f) 67fun mu_conj l r = list_mk_comb(inst [alpha|->get_prop_type l] mu_and_tm,[l,r]) 68fun mu_disj l r = list_mk_comb(inst [alpha|->get_prop_type l] mu_or_tm,[l,r]) 69fun mu_dmd act rest = list_mk_comb(inst [alpha|->get_prop_type rest] mu_dmd_tm,[act,rest])(*``<<^act>> ^rest``*) 70fun mu_box act rest = list_mk_comb(inst [alpha|->get_prop_type rest] mu_box_tm,[act,rest])(*``[[^act]] ^rest``*) 71fun mu_lfp bv rest = list_mk_comb(inst [alpha|->get_prop_type rest] mu_mu_tm,[bv,rest])(*``mu ^bv .. ^rest``*) 72fun mu_gfp bv rest = list_mk_comb(inst [alpha|->get_prop_type rest] mu_nu_tm,[bv,rest])(*``nu ^bv .. ^rest``*) 73 74fun list_mu_conj l = 75 if (List.null l) then mu_T_tm 76 else if (List.null (List.tl l)) then (List.hd l) 77 else mu_conj (List.hd l) (list_mu_conj (List.tl l)) 78fun list_mu_disj l = 79 if (List.null l) then mu_F_tm 80 else if (List.null (List.tl l)) then (List.hd l) 81 else mu_disj (List.hd l) (list_mu_disj (List.tl l)) 82fun list_mu_dmd (acth::acttl) rest = mu_dmd acth (list_mu_dmd acttl rest) 83 | list_mu_dmd [] rest = rest 84fun list_mu_box (acth::acttl) rest = mu_box acth (list_mu_box acttl rest) 85 | list_mu_box [] rest = rest 86 87val concRV = ``"Q"`` 88 89fun get_mu_ty_T_tm p_ty = inst [alpha|-> p_ty] mu_T_tm 90fun get_mu_ty_F_tm p_ty = inst [alpha|-> p_ty] mu_F_tm 91fun get_mu_ty_ap_tm p_ty = inst [alpha|-> p_ty] mu_ap_tm 92fun get_mu_ty_rv_tm p_ty = inst [alpha|-> p_ty] mu_rv_tm 93fun get_mu_ty_conj_tm p_ty = inst [alpha|-> p_ty] mu_and_tm 94fun get_mu_ty_disj_tm p_ty = inst [alpha|-> p_ty] mu_or_tm 95fun get_mu_ty_neg_tm p_ty = inst [alpha|-> p_ty] mu_neg_tm 96fun get_mu_ty_dmd_tm p_ty = inst [alpha|-> p_ty] mu_dmd_tm 97fun get_mu_ty_box_tm p_ty = inst [alpha|-> p_ty] mu_box_tm 98fun get_mu_ty_rv_tm p_ty = inst [alpha|-> p_ty] mu_rv_tm 99fun get_mu_ty_mu_tm p_ty = inst [alpha|-> p_ty] mu_mu_tm 100fun get_mu_ty_nu_tm p_ty = inst [alpha|-> p_ty] mu_nu_tm 101fun get_mu_ty_sub_tm p_ty = inst [alpha|-> p_ty] mu_sub_tm 102fun get_mu_ty_nnf_tm p_ty = inst [alpha|-> p_ty] mu_nnf_tm 103fun get_mu_ty_rvneg_tm p_ty = inst [alpha|-> p_ty] mu_rvneg_tm 104 105fun get_ty_tms p_ty = 106 (get_mu_ty_T_tm p_ty, 107 get_mu_ty_F_tm p_ty, 108 get_mu_ty_ap_tm p_ty, 109 get_mu_ty_rv_tm p_ty, 110 get_mu_ty_neg_tm p_ty, 111 get_mu_ty_conj_tm p_ty, 112 get_mu_ty_disj_tm p_ty, 113 get_mu_ty_dmd_tm p_ty, 114 get_mu_ty_box_tm p_ty, 115 get_mu_ty_mu_tm p_ty, 116 get_mu_ty_nu_tm p_ty) 117 118fun get_ty_cons p_ty = 119 (get_mu_ty_T_tm p_ty, 120 get_mu_ty_F_tm p_ty, 121 fn n => mk_comb(get_mu_ty_ap_tm p_ty,n), 122 fn n => mk_comb(get_mu_ty_rv_tm p_ty,n), 123 fn n => mk_comb(get_mu_ty_neg_tm p_ty,n), 124 fn l => fn r => list_mk_comb(get_mu_ty_conj_tm p_ty,[l,r]), 125 fn l => fn r => list_mk_comb(get_mu_ty_disj_tm p_ty,[l,r]), 126 fn l => fn r => list_mk_comb(get_mu_ty_dmd_tm p_ty,[l,r]), 127 fn l => fn r => list_mk_comb(get_mu_ty_box_tm p_ty,[l,r]), 128 fn l => fn r => list_mk_comb(get_mu_ty_mu_tm p_ty,[l,r]), 129 fn l => fn r => list_mk_comb(get_mu_ty_nu_tm p_ty,[l,r])) 130 131(* free vars of a mu formula *) 132fun fv mf = 133 let val (opr,args) = HolKernel.strip_comb mf; 134 (*val (name,ty) = dest_const opr;*) 135 in case (fst (dest_const opr)) of 136 "AP" => [] 137 | "RV" => [List.hd args] 138 | "And" => (fv (List.hd args))@(fv (List.last args)) 139 | "Or" => (fv (List.hd args))@(fv (List.last args)) 140 | "Not" => fv (List.hd args) 141 | "TR" => [] 142 | "FL" => [] 143 | "DIAMOND" => fv (List.last args) 144 | "BOX" => fv (List.last args) 145 | "mu" => List.filter (fn v => not (Term.compare(v,List.hd args)=EQUAL)) (fv (List.last args)) 146 | "nu" => List.filter (fn v => not (Term.compare(v,List.hd args)=EQUAL)) (fv (List.last args)) 147 | _ => Raise Match 148 end 149 150(* return all top level sigma formulas in f (if nu then return nu formulas, else return mu formulas) *) 151fun top_sigma nu f = 152 let val (opr,args) = strip_comb f 153 in case (fst(dest_const opr)) of 154 "TR" => [] 155 | "FL" => [] 156 | "Not" => top_sigma nu (List.hd args) 157 | "And" => (top_sigma nu (List.hd args))@ (top_sigma nu (List.last args)) 158 | "Or" => (top_sigma nu (List.hd args))@(top_sigma nu (List.last args)) 159 | "RV" => [] 160 | "AP" => [] 161 | "DIAMOND" => top_sigma nu (List.last args) 162 | "BOX" => top_sigma nu (List.last args) 163 | "mu" => if (not nu) then [f] else [] 164 | "nu" => if nu then [f] else [] 165 | _ => failwith("muSyntax.top_sigma: failed on term "^(term_to_string f)^"\n") end 166 167(* return all top level sigma formulas in f (if nu then return nu formulas, else return mu formulas) *) 168(* return only those formulas in which the RV v is free *) 169fun top_sigma_free nu v f = 170 let val ts = top_sigma nu f 171 in List.filter (fn f => HOLset.member(HOLset.addList(HOLset.empty Term.compare,ts),v)) ts end 172 173(* is f purely propositional *) 174fun is_prop f = 175 let val (opr,args) = strip_comb f 176 in case (fst(dest_const opr)) of 177 "TR" => true 178 | "FL" => true 179 | "Not" => is_prop (List.hd args) 180 | "And" => (is_prop (List.hd args)) andalso (is_prop (List.last args)) 181 | "Or" => (is_prop (List.hd args)) andalso (is_prop (List.last args)) 182 | "RV" => false 183 | "AP" => true 184 | "DIAMOND" => false 185 | "BOX" => false 186 | "mu" => false 187 | "nu" => false 188 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 189 190(* return list of top-level propositional subterms of f with their sizes (this may include f itself) *) 191fun prop_subtms f = 192 let val (opr,args) = strip_comb f 193 in case (fst(dest_const opr)) of 194 "TR" => [(f,1)] 195 | "FL" => [(f,1)] 196 | "Not" => let val t = List.hd args 197 val S1 = prop_subtms t 198 in if ((not (List.null S1)) andalso (Portable.pointer_eq(fst(hd S1),t))) 199 then [(f,(snd(hd S1))+1)] else S1 end 200 | "And" => let val t1 = List.hd args 201 val t2 = List.last args 202 val S1 = prop_subtms t1 203 val S2 = prop_subtms t2 204 in if (((not (List.null S1)) andalso (Portable.pointer_eq(fst(hd S1),t1))) 205 andalso ((not (List.null S2)) andalso (Portable.pointer_eq(fst(hd S2),t2)))) 206 then [(f,(snd(hd S1))+(snd(hd S2))+1)] else S1@S2 end 207 | "Or" => let val t1 = List.hd args 208 val t2 = List.last args 209 val S1 = prop_subtms t1 210 val S2 = prop_subtms t2 211 in if (((not (List.null S1)) andalso (Portable.pointer_eq(fst(hd S1),t1))) 212 andalso ((not (List.null S2)) andalso (Portable.pointer_eq(fst(hd S2),t2)))) 213 then [(f,(snd(hd S1))+(snd(hd S2))+1)] else S1@S2 end 214 | "RV" => [] 215 | "AP" => [(f,1)] 216 | "DIAMOND" => prop_subtms (List.last args) 217 | "BOX" => prop_subtms (List.last args) 218 | "mu" => prop_subtms (List.last args) 219 | "nu" => prop_subtms (List.last args) 220 | _ => failwith ("prop_subtms ERROR:"^(term_to_string f)^"\n") end 221 222(* RVNEG(f,Q) == in f, all free ocurrances of Q are negated *) 223fun RVNEG ty rv f = 224 let val (opr,args) = strip_comb f 225 in case (fst(dest_const opr)) of 226 "TR" => f 227 | "FL" => f 228 | "Not" => mu_neg(RVNEG ty rv (List.hd args)) 229 | "And" => mu_conj (RVNEG ty rv (List.hd args)) (RVNEG ty rv (List.last args)) 230 | "Or" => mu_disj (RVNEG ty rv (List.hd args)) (RVNEG ty rv (List.last args)) 231 | "RV" => if (Term.compare(rv,List.hd args)=EQUAL) 232 then mu_neg(mu_RV ty (hd args)) 233 else mu_RV ty (hd args) 234 | "AP" => f 235 | "DIAMOND" => mu_dmd (hd args) (RVNEG ty rv (last args)) 236 | "BOX" => mu_box (hd args) (RVNEG ty rv (last args)) 237 | "mu" => if (Term.compare(rv,List.hd args)=EQUAL) 238 then mu_lfp (hd args) (last args) 239 else mu_lfp (hd args) (RVNEG ty rv (last args)) 240 | "nu" => if (Term.compare(rv,List.hd args)=EQUAL) 241 then mu_gfp (hd args) (last args) 242 else mu_gfp (hd args) (RVNEG ty rv (last args)) 243 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 244 245 246(* return list of propositional subterms of f with size >= n, with duplicates/T/F removed, in decreasing order of size *) 247fun prop_subtmset f n = let val p_ty = get_prop_type f 248 in List.rev(fst(ListPair.unzip(Listsort.sort (fn((_,l),(_,r))=>Int.compare(l,r)) 249 (Binaryset.listItems(Binaryset.addList(Binaryset.empty 250 (fn ((l,_),(r,_)) => Term.compare(l,r)), 251 (List.filter (fn (t,sz)=> (sz>=n) 252 andalso not (Term.compare(t,get_mu_ty_T_tm p_ty)=EQUAL) 253 andalso not (Term.compare(t,get_mu_ty_F_tm p_ty)=EQUAL)) 254 (prop_subtms f)))))))) 255 end 256 257(* take a propositional mu formula and convert it to a single ap (but not a mu AP, just \state. prop_tm) *) 258fun prop2ap f state = 259 let fun mk_ap f = 260 let val (opr,args) = strip_comb f 261 in case (fst(dest_const opr)) of 262 "TR" => T 263 | "FL" => F 264 | "And" => mk_conj (mk_ap (hd args),mk_ap (last args)) 265 | "Or" => mk_disj (mk_ap (hd args),mk_ap (last args)) 266 | "AP" => (pairSyntax.pbody o hd) args 267 | "Not" => mk_neg (mk_ap (hd args)) 268 | _ => failwith "Not a propositional formula" 269 end 270 val ap = mk_AP state (mk_ap f) 271 in ap end 272 273(* give negation normal form of f *) 274local fun NNF' (cons as (mu_t,mu_f,mu_ap,mu_rv,mu_neg,mu_conj,mu_disj,mu_dmd,mu_box,mu_mu,mu_nu)) f = 275 let val (opr,args) = strip_comb f 276 val ty = List.hd(snd(dest_type (type_of f))) 277 in case (fst(dest_const opr)) of 278 "TR" => f 279 | "FL" => f 280 | "And" => mu_conj(NNF' cons (List.hd args))(NNF' cons (List.last args)) 281 | "Or" => mu_disj(NNF' cons (List.hd args))(NNF' cons (List.last args)) 282 | "RV" => f 283 | "AP" => f 284 | "DIAMOND" => mu_dmd (List.hd args) (NNF' cons (List.last args)) 285 | "BOX" => mu_box (List.hd args) (NNF' cons (List.last args)) 286 | "mu" => mu_lfp (List.hd args) (NNF' cons (List.last args)) 287 | "nu" => mu_gfp (List.hd args) (NNF' cons (List.last args)) 288 | "Not" => 289 let val (opr,args) = strip_comb (List.hd args) 290 in case (fst(dest_const opr)) of 291 "TR" => mu_f 292 | "FL" => mu_t 293 | "And" => mu_disj(NNF' cons (mu_neg(List.hd args)))(NNF' cons (mu_neg(List.last args))) 294 | "Or" => mu_conj(NNF' cons (mu_neg(List.hd args)))(NNF' cons (mu_neg(List.last args))) 295 | "RV" => f 296 | "AP" => f 297 | "DIAMOND" => mu_box (List.hd args) (NNF' cons (mu_neg(List.last args))) 298 | "BOX" => mu_dmd (List.hd args) (NNF' cons (mu_neg(List.last args))) 299 | "Not" => NNF' cons (List.hd args) 300 | "mu" => mu_gfp (List.hd args) (NNF' cons (RVNEG ty (List.hd args) (mu_neg(List.last args)))) 301 | "nu" => mu_lfp (List.hd args) (NNF' cons (RVNEG ty (List.hd args) (mu_neg(List.last args)))) 302 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 303 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 304in fun NNF f = NNF' (get_ty_cons (get_prop_type f)) f 305end 306 307local 308fun isv s p f = 309 let val (opr,args) = strip_comb f 310 in case (fst(dest_const opr)) of 311 "TR" => true 312 | "FL" => true 313 | "Not" => isv s (not p) (List.hd args) 314 | "And" => (isv s p (List.hd args)) andalso (isv s p (List.last args)) 315 | "Or" => (isv s p (List.hd args)) andalso (isv s p (List.last args)) 316 | "RV" => ((Binarymap.find(s,List.hd args)=p) handle ex => true) 317 | "AP" => true 318 | "DIAMOND" => isv s p (List.last args) 319 | "BOX" => isv s p (List.last args) 320 | "mu" => isv (Binarymap.insert(s,List.hd args,p)) p (List.last args) 321 | "nu" => isv (Binarymap.insert(s,List.hd args,p)) p (List.last args) 322 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 323(* check if f has bound variables occuring positively only *) 324in fun is_valid f = isv (Binarymap.mkDict Term.compare) true f end 325 326local 327fun isx p f = 328 let val (opr,args) = strip_comb f 329 in case (fst(dest_const opr)) of 330 "TR" => false 331 | "FL" => false 332 | "Not" => isx (not p) (List.hd args) 333 | "And" => (isx p (List.hd args)) orelse (isx p (List.last args)) 334 | "Or" => (isx p (List.hd args)) orelse (isx p (List.last args)) 335 | "RV" => false 336 | "AP" => false 337 | "DIAMOND" => if p then true else isx p (List.last args) 338 | "BOX" => isx p (List.last args) 339 | "mu" => isx p (List.last args) 340 | "nu" => isx p (List.last args) 341 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 342(* is f an existential property i.e. ?g a. <a> g SUBF (NNF f) *) 343(* in other words, at least one <<>> must occur positively *) 344in fun is_existential f = isx true f end 345 346fun is_universal mf = not (is_existential mf) 347 348(* Can this mf have a counterexample/witness: is it a top level fp or negated fp *) 349(* FIXME : This is not completely accurate e.g. AG /\ AG fails the test. 350 However, we'll need to fix the trace generation code before formulas like that can be traced *) 351fun is_traceable mf = is_fp (NNF mf) 352 353(* take f:mu and create a HOL term that replaces all :mu constants by bool names of the same type structure. 354 This creates a nonsensical but purely boolean term out of f, and since we use exists and forall to replace the binders, 355 we can do alpha-equivalence analysis on the returned formula without having to implement alpha-equivalence for :mu *) 356fun mk_hol_proxy f = 357 let val (opr,args) = HolKernel.strip_comb f 358 val ttp = stringLib.string_ty --> bool 359 val ttq = bool --> bool 360 in case (fst (dest_const opr)) of 361 "AP" => mk_comb(``(PP:^(ty_antiq ttp))``,(List.hd args)) 362 | "RV" => mk_comb(``(QQ:^(ty_antiq ttq))``,mk_bool_var(fromHOLstring(List.hd args))) 363 | "And" => mk_conj(mk_hol_proxy (List.hd args),mk_hol_proxy (List.last args)) 364 | "Or" => mk_disj(mk_hol_proxy (List.hd args),mk_hol_proxy (List.last args)) 365 | "Not" => mk_neg (mk_hol_proxy (List.hd args)) 366 | "TR" => T 367 | "FL" => F 368 | "DIAMOND" => mk_comb (mk_comb(``DD:string -> bool -> bool``,List.hd args),mk_hol_proxy (List.last args)) 369 | "BOX" => mk_comb (mk_comb(``BB:string -> bool -> bool``,List.hd args),mk_hol_proxy (List.last args)) 370 | "mu" => mk_exists(mk_bool_var(fromHOLstring(List.hd args)), 371 mk_comb(``MM:bool -> bool``,mk_hol_proxy (List.last args))) 372 | "nu" => mk_forall(mk_bool_var(fromHOLstring(List.hd args)), 373 mk_comb(``NN:bool -> bool``,mk_hol_proxy (List.last args))) 374 | _ => Raise Match 375 end 376 377fun mu_unproxy f = 378 let val (opr,args) = HolKernel.strip_comb f 379 val nm = if is_const opr then fst (dest_const opr) else fst (dest_var opr) 380 in case nm of 381 "PP" => ``AP ^(List.hd args)`` 382 | "QQ" => ``RV ^(fromMLstring(term_to_string2(List.hd args)))`` 383 | "/\\" => mu_conj (mu_unproxy (List.hd args)) (mu_unproxy (List.last args)) 384 | "\\/" => mu_disj (mu_unproxy (List.hd args)) (mu_unproxy (List.last args)) 385 | "~" => mu_neg (mu_unproxy (List.hd args)) 386 | "T" => ``TR`` 387 | "F" => ``FL`` 388 | "DD" => mu_dmd (List.hd args) (mu_unproxy (List.last args)) 389 | "BB" => mu_box (List.hd args) (mu_unproxy (List.last args)) 390 | "?" => mu_lfp (fromMLstring(term_to_string2(fst(dest_abs(List.hd args))))) 391 (mu_unproxy (snd(dest_comb(snd(dest_abs(List.hd args)))))) 392 | "!" => mu_gfp (fromMLstring(term_to_string2(fst(dest_abs(List.hd args))))) 393 (mu_unproxy (snd(dest_comb(snd(dest_abs(List.hd args)))))) 394 | _ => Raise Match 395 end 396 397(* this will rename bound variables so that alpha-equivalent terms can be cached via a strict term-matcher that knows nothing about 398 alpha equivlance e.g. Term.compare *) 399fun rename f = 400 let val l1 = (find_terms (can (match_term ``mu Q .. t``)) f) @ (find_terms (can (match_term ``nu Q .. t``)) f) 401 val l2 = List.filter (fn t => List.null (fv t)) l1 402 val l2 = List.map mk_hol_proxy l2 403 val fp = mk_hol_proxy f 404 in List.foldl (fn (sf,f) => subst (List.map (fn t => (t |-> (mu_unproxy sf))) 405 (List.map mu_unproxy (find_terms (aconv sf) fp))) f) f l2 406 end 407 408(* given f, returns |- !Q. SUBFORMULA (~RV Q) (NNF f) = (RV Q = RV P1) ... where the P_i are free in f and occur -vely *) 409fun NNF_RVNEG_CONV f = 410 let val _ = print "NNF_RVNEG_CONV\n" 411 val _ = print_term f val _ = print " f\n"(*DBG*) 412 val fvl = fv f 413 val rvnl = List.map (fn t => snd(dest_comb(snd(dest_comb t)))) 414 ((find_terms (can (match_term (``~(RV a)``)))) (NNF f)) 415 val frvnl = Binaryset.foldl (fn (t,al) => t::al) [] 416 (Binaryset.intersection((Binaryset.addList(Binaryset.empty Term.compare,fvl)), 417 (Binaryset.addList(Binaryset.empty Term.compare,rvnl)))) 418 val _ = List.app print_term frvnl val _ = print " frvnl\n"(*DBG*) 419 val gl = ``!Q. SUBFORMULA (~(RV Q)) (NNF ^f) = ^(list_mk_disj2 (List.map (fn t => mk_eq(``Q:string``,t)) frvnl))`` 420 val _ = print_term gl val _ = print " goal\n"(*DBG*) 421 val res = prove(gl,SIMP_TAC std_ss (MU_SUB_def::RVNEG_def::NNF_def::(tsimps ``:'a mu``)) THEN PROVE_TAC []) 422 val _ = print "NNF_RVNEG_CONV done\n"(*DBG*) 423 in res end 424 425 426(* converts propositional mu formula to propositional formula *) 427(* assumes AP's are of type :state_type->bool where the body is purely boolean *) 428(* FIXME: this will need to be fixed once we have AP's that are not over bools *) 429fun boolify f = 430 let val (opr,args) = strip_comb f 431 in case (fst(dest_const opr)) of 432 "TR" => ``T`` 433 | "FL" => ``F`` 434 | "Not" => mk_neg(boolify(List.hd args)) 435 | "And" => mk_conj(boolify(List.hd args),boolify(List.last args)) 436 | "Or" => mk_disj(boolify (List.hd args),boolify (List.last args)) 437 | "AP" => pairSyntax.pbody (List.hd args) 438 | _ => (print "ERROR, non-boolean mu term in boolify:"; print_term f; print "\n"; Raise Match) end 439 440(* returns maximum quantifier depth *) 441fun qdepth f = 442 let val (opr,args) = strip_comb f 443 in case (fst(dest_const opr)) of 444 "TR" => 0 445 | "FL" => 0 446 | "Not" => qdepth (List.hd args) 447 | "And" => Int.max(qdepth (List.hd args),qdepth (List.last args)) 448 | "Or" => Int.max(qdepth (List.hd args),qdepth (List.last args)) 449 | "RV" => 0 450 | "AP" => 0 451 | "DIAMOND" => qdepth (List.last args) 452 | "BOX" => qdepth (List.last args) 453 | "mu" => 1+(qdepth (List.last args)) 454 | "nu" => 1+(qdepth (List.last args)) 455 | _ => (print "ERROR:"; print_term f; print "\n"; Raise Match) end 456 457 458(* return a list of all terms of the form AP p that occur in f *) 459fun find_APs f = let val p_ty = get_prop_type f 460 val pvar = mk_var("p",p_ty) 461 in find_terms (can (match_term (mk_comb(get_mu_ty_ap_tm p_ty,pvar)))) f end 462 463(* return a string term that is not the same as any in l, formed by priming mv enough times *) 464fun mk_subs mv l = 465 let fun mk_subs2 mv ll = 466 let val cla = List.find (fn x => (Term.compare(mv,x)=EQUAL)) ll 467 in if (Option.isSome cla) then fromMLstring((fromHOLstring mv)^"'") else mv end 468 in List.foldl (fn (_,av) => mk_subs2 av l) mv l end 469 470(* rename all bound vars so that no two are the same, or clash with a free var name *) 471fun uniq mf l subs = 472 let val (opr,args) = HolKernel.strip_comb mf; 473 val prop_type = List.hd(snd(dest_type(type_of mf))) 474 (*val (name,ty) = dest_const opr;*) 475 in case (fst (dest_const opr)) of 476 "AP" => (mf,l) 477 | "RV" => (inst [``:'a``|->prop_type] ``RV ^(List.foldr (fn (sb,av) => if (Term.compare(snd sb,av)=EQUAL) 478 then fst sb else av) (List.hd args) subs)``,l) 479 | "And" => let val (lf,ll) = uniq (List.hd args) l subs; 480 val (rf,rl) = uniq (List.last args) ll subs 481 in (``^lf /\ ^rf``,rl) end 482 | "Or" => let val (lf,ll) = uniq (List.hd args) l subs; 483 val (rf,rl) = uniq (List.last args) ll subs 484 in (``^lf \/ ^rf``,rl) end 485 | "Not" => let val (nf,nl) = uniq (List.hd args) l subs in (``~(^nf)``,nl) end 486 | "TR" => (mf,l) 487 | "FL" => (mf,l) 488 | "DIAMOND" => let val (nf,nl) = uniq (List.last args) l subs in (``<<^(List.hd args)>> (^nf)``,nl) end 489 | "BOX" => let val (nf,nl) = uniq (List.last args) l subs in (``[[^(List.hd args)]] (^nf)``,nl) end 490 | "mu" => if (Option.isSome (List.find (fn x => (Term.compare(List.hd args,x)=EQUAL)) l)) 491 then let val nn = mk_subs (List.hd args) l 492 val subs = subs@[(nn,List.hd args)] 493 val (nf,nl) = uniq (List.last args) (l@[nn]) subs 494 in (``mu ^(nn) .. ^nf``,l@nl) end 495 else let val (nf,nl) = uniq (List.last args) ((List.hd args)::l) subs in (``mu ^(List.hd args) .. ^nf``,l@nl) end 496 | "nu" => if (Option.isSome (List.find (fn x => (Term.compare(List.hd args,x)=EQUAL)) l)) 497 then let val nn = mk_subs (List.hd args) l 498 val subs = subs@[(nn,List.hd args)] 499 val (nf,nl) = uniq (List.last args) (l@[nn]) subs 500 in (``nu ^(nn) .. ^nf``,l@nl) end 501 else let val (nf,nl) = uniq (List.last args) ((List.hd args)::l) subs in (``nu ^(List.hd args) .. ^nf``,l@nl) end 502 | _ => Raise Match 503 end 504 505(* return the alternation depth of the given formula *) 506fun alt_depth mf = 507 let val (opr,args) = strip_comb mf 508 in case (fst(dest_const opr)) of 509 "TR" => 0 510 | "FL" => 0 511 | "Not" => alt_depth (List.hd args) 512 | "And" => Int.max(alt_depth (List.hd args),alt_depth (List.last args)) 513 | "Or" => Int.max(alt_depth (List.hd args),alt_depth (List.last args)) 514 | "RV" => 0 515 | "AP" => 0 516 | "DIAMOND" => alt_depth (List.last args) 517 | "BOX" => alt_depth (List.last args) 518 | "mu" => listmax [1,alt_depth (List.last args),1+listmax (List.map alt_depth (top_sigma_free true (hd args) (last args)))] 519 | "nu" => listmax [1,alt_depth (List.last args),1+listmax (List.map alt_depth (top_sigma_free false (hd args) (last args)))] 520 | _ => failwith ("alt_depth Match:"^(term_to_string mf)) end 521 522(* return the max same-quantifier nesting depth of the given formula *) 523fun sameq_depth mf = 524 let val (opr,args) = strip_comb mf 525 in case (fst(dest_const opr)) of 526 "TR" => 0 527 | "FL" => 0 528 | "Not" => sameq_depth (List.hd args) 529 | "And" => Int.max(sameq_depth (List.hd args),sameq_depth (List.last args)) 530 | "Or" => Int.max(sameq_depth (List.hd args),sameq_depth (List.last args)) 531 | "RV" => 0 532 | "AP" => 0 533 | "DIAMOND" => sameq_depth (List.last args) 534 | "BOX" => sameq_depth (List.last args) 535 | "mu" => listmax [1,sameq_depth (List.last args),1+listmax (List.map sameq_depth (top_sigma_free false (hd args) (last args)))] 536 | "nu" => listmax [1,sameq_depth (List.last args),1+listmax (List.map sameq_depth (top_sigma_free true (hd args) (last args)))] 537 | _ => failwith ("sameq_depth Match:"^(term_to_string mf)) end 538 539end 540end 541