1 2structure cacheTools = 3struct 4 5local 6 7open Globals HolKernel Parse 8 9open bossLib pairTheory pred_setTheory pred_setLib stringLib 10 listTheory simpLib pairSyntax pairLib PrimitiveBddRules 11 DerivedBddRules Binarymap PairRules pairTools boolSyntax Drule 12 Tactical Conv Rewrite Tactic boolTheory listSyntax stringTheory 13 boolSimps pureSimps listSimps numLib 14 15open setLemmasTheory muSyntax muSyntaxTheory muTheory reachTheory 16 stringBinTree bddTools envTheory envTools muTools cacheTheory 17 commonTools lazyTools 18 19val dpfx = "ct_" 20 21structure Polyhash = 22struct 23 fun peek (ref dict,cmp) k = Binarymap.peek(dict,k) 24 fun peekInsert (r as ref dict, cmp) (k,v) = 25 case Binarymap.peek(dict,k) of 26 NONE => (r := Binarymap.insert(dict,k,v); NONE) 27 | x => x 28 fun insert (r as ref dict, cmp) (k,v) = 29 r := Binarymap.insert(dict,k,v) 30 fun listItems (ref dict, cmp) = Binarymap.listItems dict 31 fun map f (ref dict, cmp) = let 32 fun foldthis (k,v,acc) = Binarymap.insert (acc, k, f (k,v)) 33 in 34 (ref (Binarymap.foldl foldthis (Binarymap.mkDict cmp) dict), cmp) 35 end 36 fun find (ref dict, cmp) k = Binarymap.find(dict, k) 37 38 fun mkDict cmp = (ref (Binarymap.mkDict cmp), cmp) 39end 40 41in 42 43(* given f e and e', proves |- !Q. if ~(SUBFORMULA (~RV Q) (NNF f) then e Q = e' Q else e Q SUBSET e' Q where 44 e is the env for the previous iteration and e' is the env for the current iteration 45 seth are the string equality theorems required for evaluating the envs *) 46fun ITER_ENV_LEGAL_CONV t2 t1 e e' seth state ksname ttm imf_thms imf_t2 frv_thms wfKS_ks abthm cabthm eeq = 47 let 48 val _ = dbgTools.DEN dpfx "ielc" (*DBG*) 49 (* FIXME: need to have unwound version of t2 for passing to NNF_RVNEG_CONV but this could have efficiency issues *) 50 val gl = ``!Q'. if (SUBFORMULA (~(RV Q')) (NNF ^t2)) then (^e) Q' = (^e') Q' else (^e) Q' SUBSET (^e') Q'``; 51 (*val _ = dbgTools.DTM (dpfx^ t2) val _ = dbgTools.DST (dpfx^ " ielc t2\n") (*DBG*)*) 52 val th1 = PURE_ONCE_REWRITE_RULE [cabthm] (NNF_RVNEG_CONV t2) 53 (*val _ = dbgTools.DTH (dpfx^ th1) val _ = dbgTools.DST (dpfx^ " ielc th1\n") (*DBG*) 54 val _ = dbgTools.DTM (dpfx^ gl) val _ = dbgTools.DST (dpfx^ " ielc goal\n") (*DBG*) 55 val _ = dbgTools.DTM (dpfx^ e ) val _ = dbgTools.DST (dpfx^ " ielc env\n") (*DBG*) 56 val _ = dbgTools.DTM (dpfx^ e') val _ = dbgTools.DST (dpfx^ " ielc env'\n") (*DBG*)*) 57 val gl1 = (REWRITE_CONV [ENV_CASES,th1] THENC REPEATC (SIMP_CONV (bool_ss ++ boolSimps.COND_elim_ss) [SUBSET_REFL])) gl; 58 (*val _ = dbgTools.DTM (dpfx^ (rhs(concl gl1))) val _ = dbgTools.DST (dpfx^ " ielc second goal \n") (*DBG*)*) 59 val res = if (Term.compare(rhs(concl gl1),T)=EQUAL) then ONCE_REWRITE_RULE [EQ_CLAUSES] gl1 60 else let val env_seq_thms = List.map fst eeq 61 in SIMP_RULE bool_ss env_seq_thms gl1 end 62 (*val _ = dbgTools.DTH (dpfx^ res) val _ = dbgTools.DST (dpfx^ " ielc res\n") (*DBG*)*) 63 val _ = dbgTools.DEX dpfx "ielc" (*DBG*) 64 in res end 65 66(* show that term of conjuncts of the form e[q<--x] p = e'[q<--x] p can be mapped to conjuncts e p = e'p 67either because q != p or if q=p then that particular conjunct becomes true and disappears *) 68fun mk_ante_eq_thm goal seth = 69 let val _ = dbgTools.DEN dpfx "maet"(*DBG*) 70 val _ = dbgTools.DTM (dpfx^"maet_gl") goal(*DBG*) 71 val goals = strip_conj goal 72 val thms = List.map (fn g => let (*val _ = dbgTools.DTM (dpfx^ g) val _ = dbgTools.DST (dpfx^ " goal\n") (*DBG*)*) 73 val (glhs,grhs) = dest_eq g 74 (*val _ = dbgTools.DTM (dpfx^ glhs) val _ = dbgTools.DST (dpfx^" glhs\n") (*DBG*) 75 val _ = dbgTools.DTM (dpfx^grhs) val _ = dbgTools.DST (dpfx^ " grhs\n") (*DBG*)*) 76 val (lenv,p) = dest_comb glhs 77 val (renv,_) = dest_comb grhs 78 val ll1 = snd(strip_comb lenv) 79 val le = List.nth(ll1,0) 80 val q = List.nth(ll1,1) 81 val x = List.nth(ll1,2) 82 val ll2 = snd(strip_comb renv) 83 val re = List.nth(ll2,0) 84 val ps = fromHOLstring p val qs = fromHOLstring q 85 val seqthm = Binarymap.find(Binarymap.find(seth,qs),ps) 86 (*val _ = dbgTools.DTH (dpfx^seqthm) (*DBG*) *) 87 val eqth = GEN_ALL(List.hd(List.tl(CONJUNCTS(SPEC_ALL EQ_CLAUSES)))) 88 val eqth1 = if (is_neg (concl seqthm)) then eqth else ISPEC (fst(dest_eq(concl seqthm))) eqth 89 (*val _ = dbgTools.DTH (dpfx^ eqth) (*DBG*)*) 90 val seqthm = if (is_neg (concl seqthm)) then seqthm else PURE_ONCE_REWRITE_RULE [eqth1] seqthm 91 (*val _ = dbgTools.DTH (dpfx^ seqthm) (*DBG*)*) 92 val envth = if (String.compare(qs,ps)=EQUAL) then ENV_EVAL_EQ_INV else ENV_EVAL_NEQ_INV 93 (*val _ = dbgTools.DTH (dpfx^ (ISPECL [le,re,q,p,x] envth)) 94 val _ = dbgTools.DST (dpfx^ " envth\n") (*DBG*)*) 95 val th = MP (ISPECL [le,re,q,p,x] envth) seqthm 96 in if (is_neg(concl seqthm)) then th 97 else PURE_ONCE_REWRITE_RULE [ISPEC (concl th) (GSYM eqth)] th end) goals 98 (*val _ = List.app (fn tt => dbgTools.DTH (dpfx^"maet_sethm") tt)) thms(*DBG*)*) 99 val thl = List.map (fn (g,th) => PURE_ONCE_REWRITE_CONV [th] g) (ListPair.zip(goals,thms)) 100 (*val _ = List.app (fn tt => let val _ = dbgTools.DTH (dpfx^"maet_sethm2" tt) in () end) thl(*DBG*)*) 101 val _ = dbgTools.DEX dpfx "maet"(*DBG*) 102 in thl end 103 104fun mk_inv_zero_ante speclist spec_thm mp_thm = 105 let 106 val _ = dbgTools.DEN dpfx "i0" (*DBG*) 107 val _ = profTools.bgt (dpfx^"i0")(*PRF*) 108 (*val _ = dbgTools.DTH (dpfx^ spec_thm) val _ = dbgTools.DST (dpfx^ " spec_thm\n") (*DBG*) 109 val _ = dbgTools.DTH (dpfx^ mp_thm) val _ = dbgTools.DST (dpfx^ " mp_thm\n") (*DBG*) 110 val _ = List.app (fn tt=> let val _= dbgTools.DTM (dpfx^ tt) in () end) speclist(*DBG*) *) 111 val (l,bod) = strip_forall (concl spec_thm) 112 val jf = (fn _ => MATCH_MP (CONV_RULE FORALL_IMP_CONV ((CONV_RULE (LAST_FORALL_CONV FORALL_IMP_CONV)) 113 (ISPECL speclist spec_thm))) mp_thm) 114 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length speclist), 115 subst (List.map (fn (f,r) => (f|->r)) (ListPair.zip(l,speclist))) (rand bod)),jf)) jf 116 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " th\n") (*DBG*)*) 117 val _ = profTools.ent (dpfx^"i0")(*PRF*) 118 val _ = dbgTools.DEX dpfx "i0" (*DBG*) 119 in th end 120 121fun mk_inv_one_ante args cthm tthm ithm left = 122 let val _ = dbgTools.DEN dpfx "i1" (*DBG*) 123 val _ = profTools.bgt (dpfx^"i1")(*PRF*) 124 (*val _ = dbgTools.DTM (dpfx^ (List.hd args)) val _ = dbgTools.DST (dpfx^ " hd args\n") (*DBG*) 125 val _ = dbgTools.DTM (dpfx^ (List.last args)) val _ = dbgTools.DST (dpfx^ " last args\n") (*DBG*) 126 val _ = dbgTools.DTH (dpfx^ cthm) val _ = dbgTools.DST (dpfx^ " cthm\n") (*DBG*) 127 val _ = dbgTools.DTH (dpfx^ tthm) val _ = dbgTools.DST (dpfx^ " tthm\n") (*DBG*) 128 val _ = dbgTools.DTH (dpfx^ ithm) val _ = dbgTools.DST (dpfx^ " ithm\n") (*DBG*)*) 129 val (ante,tc) = dest_imp(snd(strip_forall(concl cthm))) 130 val (l,bod) = strip_forall (concl ithm) 131 val jf = (fn _ => let val (ql,t) = strip_forall(concl tthm) 132 val tthm2 = prove(list_mk_forall(ql,mk_imp(ante,t)),SIMP_TAC std_ss [tthm]) 133 (*val _ = dbgTools.DTH (dpfx^ tthm2) val _ = dbgTools.DST (dpfx^ " tthm2\n") (*DBG*)*) 134 val th2 = CONV_RULE (QUANT_CONV AND_FORALL_CONV) 135 (CONV_RULE AND_FORALL_CONV (LIST_CONJ (if left then [cthm,tthm2] else [tthm2,cthm]))) 136 (*val _ = dbgTools.DTH (dpfx^ th2) val _ = dbgTools.DST (dpfx^ " th2\n") (*DBG*)*) 137 val th3 = MATCH_MP (ISPECL ([ante,ante]@(if left then [tc,t] else [t,tc])) fol1) (SPEC_ALL th2) 138 (*val _ = dbgTools.DTH (dpfx^ th3) val _ = dbgTools.DST (dpfx^ " th3\n") (*DBG*)*) 139 val th4 = SIMP_RULE bool_ss [] (GENL [List.hd ql,List.last ql] th3) 140 (*val _ = dbgTools.DTH (dpfx^ th4) val _ = dbgTools.DST (dpfx^ " th4\n") (*DBG*)*) 141 val geninv = (ISPECL [List.hd args,List.last args, List.hd ql,List.last ql] ithm) 142 (*val _ = dbgTools.DTH (dpfx^ geninv) val _ = dbgTools.DST (dpfx^ " geninv\n") (*DBG*)*) 143 val sfol = ISPECL (ante::((if left then [tc,t] else [t,tc])@[snd(dest_imp(concl geninv))])) fol3 144 (*val _ = dbgTools.DTH (dpfx^ sfol) val _ = dbgTools.DST (dpfx^ " sfol\n") (*DBG*)*) 145 val th5 = MATCH_MP sfol geninv 146 (*val _ = dbgTools.DTH (dpfx^ th5) val _ = dbgTools.DST (dpfx^ " th5\n") (*DBG*)*) 147 val th6 = MATCH_MP th5 (SPEC_ALL th4) 148 (*val _ = dbgTools.DTH (dpfx^ th6) val _ = dbgTools.DST (dpfx^ " th6\n") (*DBG*)*) 149 val res = GENL [List.hd ql,List.last ql] th6 150 (*val _ = dbgTools.DTH (dpfx^ res) val _ = dbgTools.DST (dpfx^ " res\n") (*DBG*)*) 151 in res end) 152 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 153 mk_imp(ante,subst (List.map (fn (f,r) => (f|->r)) (ListPair.zip(l,args))) (rand bod))), 154 jf)) jf 155 val _ = profTools.ent (dpfx^"i1")(*PRF*) 156 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " th\n") (*DBG*)*) 157 val _ = dbgTools.DEX dpfx "i1" (*DBG*) 158 in th end 159 160fun mk_inv_two_ante args ithml ithm = 161 let 162 val _ = dbgTools.DEN dpfx "i2" (*DBG*) 163 val _ = profTools.bgt (dpfx^"i2")(*PRF*) 164 (*val _ = dbgTools.DTM (dpfx^ (List.hd args)) val _ = dbgTools.DST (dpfx^ " hd args\n") (*DBG*) 165 val _ = dbgTools.DTM (dpfx^ (List.last args)) val _ = dbgTools.DST (dpfx^ " last args\n") (*DBG*)*) 166 val cthm1 = List.hd ithml 167 val (ante1,t1) = dest_imp(snd(strip_forall(concl cthm1))) 168 val cthm2 = List.last ithml 169 (*val _ = dbgTools.DTH (dpfx^ ithm) val _ = dbgTools.DST (dpfx^ " ithm\n") (*DBG*) 170 val _ = dbgTools.DTH (dpfx^ cthm1) val _ = dbgTools.DST (dpfx^ " cthm1\n") (*DBG*) 171 val _ = dbgTools.DTH (dpfx^ cthm2) val _ = dbgTools.DST (dpfx^ " cthm2\n") (*DBG*)*) 172 val (ante2,t2) = dest_imp(snd(strip_forall(concl cthm2))) 173 val (l,bod) = strip_forall (concl ithm) 174 val jf = (fn _ => 175 let val (ql,_) = strip_forall(concl cthm1) 176 val th2 = CONV_RULE (QUANT_CONV AND_FORALL_CONV) (CONV_RULE AND_FORALL_CONV (LIST_CONJ [cthm1,cthm2])) 177 val th3 = MATCH_MP (ISPECL [ante1,ante2,t1,t2] fol1) (SPEC_ALL th2) 178 val th4 = (*CONV_RULE (STRIP_QUANT_CONV(LAND_CONV(SIMP_CONV bool_ss [])))*) (GENL ql th3) 179 val geninv = (ISPECL [List.hd args, List.last args,List.hd ql,List.last ql] ithm) 180 val sfol = ISPECL [(*snd(dest_eq(concl(SIMP_CONV bool_ss [] (mk_conj(ante1,ante2))))) handle ex =>*) 181 (mk_conj(ante1,ante2)), t1,t2,snd(dest_imp(concl geninv))] fol3 182 val th5 = MATCH_MP sfol geninv 183 val th6 = MATCH_MP th5 (SPEC_ALL th4) 184 val res = GENL ql th6 185 (*val _ = dbgTools.DTH (dpfx^ res) val _ = dbgTools.DST (dpfx^ " res\n") (*DBG*)*) 186 in res end) 187 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 188 mk_imp(mk_conj(ante1,ante2), 189 subst (List.map (fn (f,r) => (f|->r)) (ListPair.zip(l,args))) (rand bod))),jf)) jf 190 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " th\n") (*DBG*)*) 191 val _ = profTools.ent (dpfx^"i2")(*PRF*) 192 val _ = dbgTools.DEX dpfx "i2" (*DBG*) 193 in th end 194 195fun mk_inv_modal_ante args ithml ithm1 ithm2 chc state env = 196 let val _ = dbgTools.DEN dpfx "imod" (*DBG*) 197 val _ = profTools.bgt (dpfx^"imod") (*PRF*) 198 val res = 199 if (chc=0) 200 then (* child does not have antecedents *) 201 let 202 val _ = dbgTools.DST (dpfx^"imod_ modal no ante") (*DBG*) 203 val th = mk_inv_zero_ante [List.hd args,List.last args] ithm1 (List.hd ithml) 204 val _ = dbgTools.DST (dpfx^"imod_ modal no ante done") (*DBG*) 205 in th end 206 else 207 let val _ = dbgTools.DST (dpfx^"imod_ modal with ante") (*DBG*) 208 val cthm = List.hd ithml 209 (*val _ = dbgTools.DTH (dpfx^ cthm) val _ = dbgTools.DST (dpfx^ " cthm\n") (*DBG*)*) 210 val (ante,_) = dest_imp(snd(strip_forall(concl cthm))) 211 val (l,bod) = strip_forall (concl ithm2) 212 val jf = (fn _ => 213 let val (ql,_) = strip_forall(concl cthm) 214 val geninv = ISPECL [List.hd args,List.last args,List.hd ql,List.last ql] ithm2 215 (*val _ = dbgTools.DTH (dpfx^"imod_ ithm2") ithm2 (*DBG*) 216 val _ = dbgTools.DTH (dpfx^"imod_ geninv") geninv) (*DBG*)*) 217 val tc3 = fst(dest_imp(concl geninv)) 218 val sfol = ISPECL [ante,tc3,snd(dest_imp(concl geninv))] fol5 219 (*val _ = dbgTools.DTH (dpfx^ sfol) val _ = dbgTools.DST (dpfx^ " sfol\n") (*DBG*)*) 220 val th1 = MATCH_MP sfol geninv 221 (*val _ = dbgTools.DTH (dpfx^ th1) val _ = dbgTools.DST (dpfx^ " th1\n") (*DBG*)*) 222 val cth2 = SPEC_ALL cthm 223 (*val _ = dbgTools.DTH (dpfx^ cth2) val _ = dbgTools.DST (dpfx^ " cth2\n") (*DBG*)*) 224 val th2 = MATCH_MP th1 cth2 225 (*val _ = dbgTools.DTH (dpfx^ th2) val _ = dbgTools.DST (dpfx^ " th2\n") (*DBG*)*) 226 val res =GENL [``e:^(ty_antiq(type_of env))``,``e':^(ty_antiq(type_of env))``] th2 227 (*val _ = dbgTools.DTH (dpfx^ res) val _ = dbgTools.DST (dpfx^ " res\n") (*DBG*)*) 228 in res end) 229 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 230 mk_imp(ante,subst (List.map (fn (f,r) => (f|->r)) 231 (ListPair.zip(l,args))) (rand bod))),jf)) jf 232 val _ = dbgTools.DST (dpfx^"imod_ modal with ante done") (*DBG*) 233 in th end 234 val _ = profTools.ent (dpfx^"imod")(*PRF*) 235 val _ = dbgTools.DEX dpfx "imod" (*DBG*) 236 in res end 237 238fun remove_bv ante bv = (* ante is e Q = e' Q /\ e P = e' P ... term, bv is current bound var *) 239 let val eqs = strip_conj ante 240 val ante' = List.filter (fn el => not (Term.compare(snd(dest_comb(fst(dest_eq el))),bv)=EQUAL)) eqs 241 in if (List.null ante') then T else list_mk_conj ante' end 242 243fun mk_inv_fp_ante args ithml ithm chc state seth = 244 let 245 val _ = dbgTools.DEN dpfx "ifp" (*DBG*) 246 val _ = profTools.bgt (dpfx^"ifp")(*PRF*) 247 val th = if (chc=0) (* child does not have antecedents *) 248 then 249 let val _ = dbgTools.DST (dpfx^"ifp_ mk_inv_fp_ante no ante") (*DBG*) 250 val cthm = List.hd ithml 251 (*val _ = dbgTools.DTH (dpfx^ ithm) val _ = dbgTools.DST (dpfx^ " ithm\n") (*DBG*) 252 val _ = DMSG(TM(List.hd args)) val _ = dbgTools.DST (dpfx^ " hd args\n") (*DBG*) 253 val _= DMSG(TM(List.last args)) val _=dbgTools.DST (dpfx^" last args\n") (*DBG*)*) 254 val (l,bod) = strip_forall (concl ithm) 255 val jf = (fn _ => let val (ql,_) = strip_forall(concl cthm) 256 (*val _ = with_flag (show_types,true) DMSG(TM(List.hd ql)) *) 257 (*val _ = dbgTools.DST (dpfx^ " hd ql\n") (*DBG*)*) 258 (*val _ = with_flag(show_types,true) DMSG(TM(List.last ql)) *) 259 (*val _ =dbgTools.DST (dpfx^ " last ql\n") (*DBG*)*) 260 val geninv = ISPECL [List.hd args, List.last args,List.hd ql,List.last ql] ithm 261 (*val _ = dbgTools.DTH (dpfx^ geninv) val _ = dbgTools.DST (dpfx^ " geninv\n") (*DBG*)*) 262 val X = ``X: ^(ty_antiq(type_of state --> bool))`` 263 val cthm2 = ISPECL [``^(List.hd ql)[[[^(List.hd args)<--^X]]]``, 264 ``^(List.last ql)[[[^(List.hd args)<--^X]]]``] cthm 265 (*val _ = dbgTools.DTH (dpfx^ cthm2) val _ = dbgTools.DST (dpfx^ " cthm2\n") (*DBG*)*) 266 val cthm3 = (GEN X cthm2) 267 val th1 = GENL [List.hd ql, List.last ql] (MATCH_MP geninv cthm3) 268 val _ = dbgTools.DST (dpfx^"ifp_ mk_inv_fp_ante no ante done") (*DBG*) 269 in th1 end) 270 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 271 subst (List.map (fn (f,r) => (f|->r)) 272 (ListPair.zip(l,args))) (rand bod)),jf)) jf 273 in th end 274 else 275 let val _ = dbgTools.DST (dpfx^"ifp_ mk_inv_fp_ante yes ante") (*DBG*) 276 val cthm = List.hd ithml 277 (*val _ = dbgTools.DTH (dpfx^ cthm) val _ = dbgTools.DST (dpfx^ " cthm\n") (*DBG*)*) 278 val (ql,_) = strip_forall(concl cthm) 279 val (ante,_) = dest_imp(snd(strip_forall(concl cthm))) 280 val ante1 = remove_bv ante (List.hd args) 281 val X = ``X: ^(ty_antiq(mk_type("fun",[type_of state,``:bool``])))`` 282 val cthm2 = ISPECL [``^(List.hd ql)[[[^(List.hd args)<--^X]]]``, 283 ``^(List.last ql)[[[^(List.hd args)<--^X]]]``] cthm 284 (*val _ = dbgTools.DTH (dpfx^ cthm2) val _ = dbgTools.DST (dpfx^ " cthm2\n") (*DBG*)*) 285 val (sante,_) = dest_imp(snd(strip_forall(concl cthm2))) (* no need to remove_bv; mk_ante_eq takes care of it*) 286 val geninv = ISPECL [List.hd args, List.last args,List.hd ql,List.last ql] ithm 287 (*val _ = dbgTools.DTH (dpfx^ geninv) val _ = dbgTools.DST (dpfx^ " geninv\n") (*DBG*)*) 288 val tc3 = fst(dest_imp(concl geninv)) 289 val _ = dbgTools.DST (dpfx^"ifp_ mk_inv_fp_ante yes ante done") (*DBG*) 290 in if (Term.compare(ante1,T)=EQUAL) 291 then (* no antecedents left, remove completely; this happens if bv was the only sub-RV *) 292 let 293 val (l,bod) = strip_forall (concl ithm) 294 val jf = (fn _ => let val noantethm = mk_ante_eq_thm sante seth 295 val cthm3 = SIMP_RULE std_ss noantethm cthm2 296 val cthm4 = (GEN X cthm3) 297 (*val _ = dbgTools.DTH (dpfx^ cthm4) (*DBG*)*) 298 val th1 = GENL [List.hd ql, List.last ql] (MATCH_MP geninv cthm4) 299 in th1 end) 300 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 301 subst (List.map (fn (f,r) => (f|->r)) 302 (ListPair.zip(l,args))) (rand bod)),jf)) jf 303 in th end 304 else (* antecedents still left; ripple to current inv thm *) 305 let val (l,bod) = strip_forall (concl ithm) 306 val jf = (fn _ => let val sfol = ISPECL [ante1,tc3,snd(dest_imp(concl geninv))] fol5 307 val th1 = MATCH_MP sfol geninv 308 val ae = mk_ante_eq_thm sante seth 309 val cthm3 = REWRITE_RULE ae cthm2 310 val cthm4 = (CONV_RULE FORALL_IMP_CONV (GEN X cthm3)) 311 val th2 = MATCH_MP th1 cthm4 312 val res = GENL ql th2 313 in res end) 314 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 315 mk_imp(ante1,subst (List.map (fn (f,r) => (f|->r)) 316 (ListPair.zip(l,args))) (rand bod))),jf)) jf 317 in th end 318 end 319 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " final th\n") (*DBG*)*) 320 val _ = profTools.ent (dpfx^"ifp")(*PRF*) 321 val _ = dbgTools.DEX dpfx "ifp" (*DBG*) 322 in th end 323 324(* return NONE if entire list is NONE, else a list of just the thms*) 325fun merge_abthms abthml = List.map Option.valOf (List.filter Option.isSome abthml) 326 327fun mk_inv_thm opr args env ithml (githms as [AP_I,RV_I,T_I,F_I,NEG_I,NEG_I2,CONJ_I,CONJ_I2,DISJ_I,DISJ_I2,DMD_I,DMD_I2,BOX_I,BOX_I2,LFP_I,LFP_I2,GFP_I,GFP_I2]) state chc (msp as [MU_SAT_T,MU_SAT_F,MU_SAT_NEG,MU_SAT_CONJ,MU_SAT_DISJ]) seth = 328 let val _ = dbgTools.DEN dpfx "mit" (*DBG*) 329 val _ = profTools.bgt (dpfx^"mit")(*PRF*) 330 val res = case (fst (dest_const opr)) of 331 "AP" => let (*val _ = with_flag(show_types,true) dbgTools.DTH (dpfx^ AP_I) (*DBG*) 332 val _ = dbgTools.DST (dpfx^ " (AP_I)\n") (*DBG*) 333 val _ = with_flag(show_types,true)dbgTools.DTM (dpfx^ (List.hd args)) (*DBG*) 334 val _ = dbgTools.DST (dpfx^ " (hd args)\n") (*DBG*) *) 335 in ISPEC (List.hd args) AP_I end 336 | "RV" => ISPEC (List.hd args) RV_I (* note this is not used if this RV is current bound *) 337 | "And" => (case chc of (* 0=neither child has antecedents, 1=left child, 2= right, 3 = both *) 338 0 => mk_inv_zero_ante [List.hd args, List.last args] CONJ_I (LIST_CONJ ithml) 339 | 1 => mk_inv_one_ante args (List.hd ithml) (List.last ithml) CONJ_I2 true 340 | 2 => mk_inv_one_ante args (List.last ithml) (List.hd ithml) CONJ_I2 false 341 | 3 => mk_inv_two_ante args ithml CONJ_I2 342 | _ => Raise Match ) 343 | "Or" => (case chc of (* 0=neither child has antecedents, 1=left child, 2= right, 3 = both *) 344 0 => mk_inv_zero_ante [List.hd args, List.last args] DISJ_I (LIST_CONJ ithml) 345 | 1 => mk_inv_one_ante args (List.hd ithml) (List.last ithml) DISJ_I2 true 346 | 2 => mk_inv_one_ante args (List.last ithml) (List.hd ithml) DISJ_I2 false 347 | 3 => mk_inv_two_ante args ithml DISJ_I2 348 | _ => Raise Match) 349 | "Not" => if (chc=0) 350 then (* child does not have antecedents *) 351 let val _ = profTools.bgt (dpfx^"ineg")(*PRF*) 352 val res = mk_inv_zero_ante [List.hd args] NEG_I (List.hd ithml) 353 val _ = profTools.ent (dpfx^"ineg")(*PRF*) 354 in res end 355 else 356 let val _ = profTools.bgt (dpfx^"ineg")(*PRF*) 357 val cthm = List.hd ithml 358 val (ante,tc) = dest_imp(snd(strip_forall(concl cthm))) 359 val (l,bod) = strip_forall (concl NEG_I2) 360 val jf = (fn _ => let val (ql,_) = strip_forall(concl cthm) 361 val geninv = ISPECL [List.hd args,List.hd ql,List.last ql] NEG_I2 362 val sfol = ISPECL [ante,tc,snd(dest_imp(concl geninv))] fol5 363 val th1 = MATCH_MP sfol geninv 364 val th2 = MATCH_MP th1 (SPEC_ALL cthm) 365 val th3 =GENL[``e:^(ty_antiq(type_of env))``,``e':^(ty_antiq(type_of env))``] th2 366 in th3 end) 367 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args), 368 mk_imp(ante,subst (List.map (fn (f,r) => (f|->r)) 369 (ListPair.zip(l,args))) (rand bod))),jf)) jf 370 val _ = profTools.ent (dpfx^"ineg")(*PRF*) 371 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " Not th\n") (*DBG*)*) 372 in th end 373 | "TR" => T_I 374 | "FL" => F_I 375 | "DIAMOND" => mk_inv_modal_ante args ithml DMD_I DMD_I2 chc state env 376 | "BOX" => mk_inv_modal_ante args ithml BOX_I BOX_I2 chc state env 377 | "mu" => mk_inv_fp_ante args ithml LFP_I2 chc state seth 378 | "nu" => mk_inv_fp_ante args ithml GFP_I2 chc state seth 379 | _ => Raise Match 380 val _ = profTools.ent (dpfx^"mit")(*PRF*) 381 val _ = dbgTools.DEX dpfx "mit" (*DBG*) 382 in res end 383| mk_inv_thm _ _ _ _ _ _ _ _ _ = Raise Match 384 385fun print_rsc rsc label = let 386in 387 print (label^" rsc "); 388 Vector.appi (fn (i,iv) => print (Int.toString i^":"^ 389 Int.toString(Vector.sub(rsc,i))^" ")) 390 rsc; 391 print "\n" 392end 393 394fun is_eq_rsc rsc rsc' = 395 let val _ = profTools.bgt (dpfx^"ier")(*PRF*) 396 val res = List.foldl (fn (i,t) => t andalso Vector.sub(rsc,i)=Vector.sub(rsc',i)) true (List.tabulate(Vector.length rsc,I)) 397 val _ = profTools.ent (dpfx^"ier")(*PRF*) 398 in res end 399 400(* cache entry is (term_bdd,gth,sth,env for which sth and tb are valid, index of RV tb if any else -1, 401reverse scope of bound RV, environment invariance thm for this node, abbrev thm for this node, ado sub thm, ado eq thm *) 402fun cache_add depth rvnm2ix env (nf,mf) mfo ce rsc rvty ithml (githms as [_,_,T_I,F_I,_,_,_,_,_,_,_,_,_,_,_,_,_,_]) 403 state seth msp guid abthml (cons as (ctm,dtm,ntm,dmdtm,boxtm,rvtm,mutm,nutm,imftm)) = 404 let val _ = dbgTools.DEN dpfx "ca" (*DBG*) 405 val _ = profTools.bgt (dpfx^"ca")(*PRF*) 406 val _ = profTools.bgt (dpfx^"ca_init")(*PRF*) 407 val _ = profTools.bgt (dpfx^"ca_init_irv")(*PRF*) 408 val irv = is_RV mf 409 val _ = profTools.ent (dpfx^"ca_init_irv")(*PRF*) 410 val _ = profTools.bgt (dpfx^"ca_init_mrv")(*PRF*) 411 val cekey = if irv then mk_comb(rvtm, (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth)))) else mf 412 (*mu_RV (type_of state) (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth))) else mf*) 413 val _ = profTools.ent (dpfx^"ca_init_mrv")(*PRF*) 414 (*val _ = dbgTools.DTM (dpfx^ cekey) val _ = dbgTools.DST (dpfx^ " cekey\n") (*DBG*)*) 415 val _ = profTools.bgt (dpfx^"ca_init_bmp")(*PRF*) 416 val en = Polyhash.peek ce cekey(*Redblackmap.peek(ce,cekey)*) 417 val _ = profTools.ent (dpfx^"ca_init_bmp")(*PRF*) 418 (*val _ = dbgTools.DTM (dpfx^ mf) val _ = dbgTools.DST (dpfx^ " mf\n") (*DBG*)*) 419 fun same_rsc rsc en = let val (_,_,_,_,_,rsc',_,_,_,_) = !(Option.valOf en) in is_eq_rsc rsc rsc' end 420 val _ = profTools.ent (dpfx^"ca_init")(*PRF*) 421 (* if not RV then must agree on reverse scope otherwise (say) <.> Q and <.> Q in different scopes would be identified *) 422 (* reverse scoping for RV's is more complicated, so it is quicker to just cache on name+depth (a la de Bruijn) to tell them apart *) 423 val res = 424 if (Option.isSome en) andalso (is_RV mf orelse same_rsc rsc en) then 425 let 426 val (_,_,_,_,_,rsc,ithm,abthm,_,_) = !(Option.valOf en) 427 val _ = dbgTools.DST (dpfx^"ca_ already cached") (*DBG*) 428 in 429 (Option.valOf en,(ce,rsc,ithm,abthm)) 430 end 431 else let 432 fun mk_abbr rhs = let 433 val _ = profTools.bgt (dpfx^"ca_ma")(*PRF*) 434 val df = mk_adf (nf^(int_to_string (!guid))) rhs (* fast abbrev definition *) 435 val _ = (guid := (!guid)+1) 436 val _ = profTools.ent (dpfx^"ca_ma")(*PRF*) 437 in 438 df 439 end 440 val (opr,args) = strip_comb mf 441 val (_,argso) = strip_comb mfo 442 val (en,rsc,ithm,abthm) = 443 case (fst (dest_const opr)) of 444 "AP" => let 445 val _ = profTools.bgt (dpfx^"ca_ap")(*PRF*) 446 val abthm = REFL mf 447 val _ = profTools.ent (dpfx^"ca_ap")(*PRF*) 448 val ithm = mk_inv_thm opr args env ithml githms 449 state 0 msp seth 450 in 451 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 452 NONE,NONE),rsc,ithm,SOME abthm) 453 end 454 | "RV" => let 455 val _ = profTools.bgt (dpfx^"ca_rv")(*PRF*) 456 val rv = snd(dest_comb mf) 457 (*val _ = dbgTools.DST (dpfx^ ("RV")) ; val _ = dbgTools.DST (dpfx^ (fromHOLstring rv)) ;(*DBG*) 458 val _ = List.app (fn (b,i) => 459 let val _ = dbgTools.DST (dpfx^ (b^"::"^(int_to_string i)^"\n")) in () end) 460 (rvnm2ix)(*DBG*)*) 461 val ix = commonTools.listkeyfind 462 rvnm2ix 463 (fromHOLstring rv) 464 String.compare 465 val rsc = 466 Vector.mapi 467 (fn (i,v)=> if (i=ix) then let 468 val ty = commonTools.listkeyfind 469 rvty rv Term.compare 470 in 471 if ty then 2 else 1 472 end handle NotFound => 0 473 else v) 474 rsc 475 (*val _ = print_rsc rsc "RV cache_add depth"*) 476 val abthm = REFL mf 477 val _ = profTools.ent (dpfx^"ca_rv")(*PRF*) 478 val ithm = mk_inv_thm opr args env ithml githms 479 state 0 msp seth 480 in 481 (ref (NONE,SOME TRUTH,NONE,env,ix,rsc,ithm,SOME abthm, 482 NONE,NONE),rsc,ithm,SOME abthm) 483 end 484 | "And" => let 485 val _ = dbgTools.DST (dpfx^ "ca_ And") (*DBG*) 486 (*val _ = dbgTools.DTH (dpfx^ CONJ_I) (*DBG*)*) 487 (*val _ = dbgTools.DST (dpfx^ " gen\n") (*DBG*)*) 488 val _ = profTools.bgt (dpfx^"ca_c1")(*PRF*) 489 val chc = (if (is_imp(snd(strip_forall(concl(List.hd ithml))))) then 1 else 0) 490 +(if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 2 else 0) 491 val lcabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 492 val rcabthmnm = lhs(concl(Option.valOf(List.last abthml))) 493 val _ = profTools.ent (dpfx^"ca_c1")(*PRF*) 494 val abthm = mk_abbr (list_mk_comb(ctm,[lcabthmnm,rcabthmnm])) 495 val ithm = mk_inv_thm opr [lcabthmnm,rcabthmnm] env ithml githms state chc msp seth 496 val _ = profTools.bgt (dpfx^"ca_c2")(*PRF*) 497 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 498 val _ = profTools.ent (dpfx^"ca_c2")(*PRF*) 499 in 500 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 501 NONE,NONE),rsc,ithm,SOME abthm) 502 end 503 | "Or" => let 504 val _ = dbgTools.DST (dpfx^"ca_ Or") (*DBG*) 505 (*val _ = dbgTools.DTH (dpfx^ DISJ_I) (*DBG*)*) 506 (* val _ = dbgTools.DST (dpfx^ " gen\n") (*DBG*)*) 507 val _ = profTools.bgt (dpfx^"ca_d1")(*PRF*) 508 val chc = (if (is_imp(snd(strip_forall(concl(List.hd ithml))))) then 1 else 0) 509 +(if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 2 else 0) 510 val lcabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 511 val rcabthmnm = lhs(concl(Option.valOf(List.last abthml))) 512 val _ = profTools.ent (dpfx^"ca_d1")(*PRF*) 513 val abthm = mk_abbr (list_mk_comb(dtm,[lcabthmnm,rcabthmnm]))(*``Or(^lcabthmnm)(^rcabthmnm)``*) 514 val ithm = mk_inv_thm opr [lcabthmnm,rcabthmnm] env ithml githms state chc msp seth 515 val _ = profTools.bgt (dpfx^"ca_d2")(*PRF*) 516 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 517 val _ = profTools.ent (dpfx^"ca_d2")(*PRF*) 518 in 519 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 520 NONE,NONE),rsc,ithm,SOME abthm) 521 end 522 | "Not" => let 523 val _ = profTools.bgt (dpfx^"ca_n1")(*PRF*) 524 val chc = (if (is_imp(snd(strip_forall(concl(List.hd ithml))))) then 1 else 0) 525 val cabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 526 val _ = profTools.ent (dpfx^"ca_n1")(*PRF*) 527 val abthm = mk_abbr (mk_comb(ntm,cabthmnm))(*``Not (^cabthmnm)`` *) 528 val ithm = mk_inv_thm opr [cabthmnm] env ithml githms state chc msp seth 529 val _ = profTools.bgt (dpfx^"ca_n2")(*PRF*) 530 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 531 val _ = profTools.ent (dpfx^"ca_n2")(*PRF*) 532 in 533 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 534 NONE,NONE),rsc,ithm,SOME abthm) 535 end 536 | "TR" => (ref (NONE,NONE,NONE,env,~1,rsc,T_I, 537 SOME (REFL mf),NONE,NONE),rsc,T_I, 538 SOME (REFL mf)) 539 | "FL" => (ref (NONE,NONE,NONE,env,~1,rsc,F_I, 540 SOME (REFL mf),NONE,NONE),rsc,F_I, 541 SOME (REFL mf)) 542 | "DIAMOND" => let 543 val _ = dbgTools.DST (dpfx^"ca_ DMD\n") (*DBG*) 544 (*val _ = dbgTools.DTH (dpfx^ DMD_I) val _ = dbgTools.DST (dpfx^ " gen\n") (*DBG*)*) 545 val _ = profTools.bgt (dpfx^"ca_dmd")(*PRF*) 546 val chc = (if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 1 else 0) 547 val cabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 548 val actnm = List.hd args 549 val _ = profTools.ent (dpfx^"ca_dmd")(*PRF*) 550 val abthm = mk_abbr (list_mk_comb(dmdtm,[actnm,cabthmnm]))(*``DIAMOND (^actnm) (^cabthmnm)``*) 551 val ithm = mk_inv_thm opr [List.hd args,cabthmnm] env ithml githms state chc msp seth 552 val _ = profTools.bgt (dpfx^"ca_dmd")(*PRF*) 553 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 554 val _ = profTools.ent (dpfx^"ca_dmd")(*PRF*) 555 in 556 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 557 NONE,NONE),rsc,ithm,SOME abthm) 558 end 559 | "BOX" => let 560 val _ = dbgTools.DST (dpfx^ "ca_ BOX") (*DBG*) 561 (*val _ = dbgTools.DTH (dpfx^ BOX_I) val _ = dbgTools.DST (dpfx^ " gen\n") (*DBG*)*) 562 val _ = profTools.bgt (dpfx^"ca_box")(*PRF*) 563 val chc = (if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 1 else 0) 564 val cabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 565 val actnm = List.hd args 566 val _ = profTools.ent (dpfx^"ca_box")(*PRF*) 567 val abthm = mk_abbr (list_mk_comb(boxtm,[actnm,cabthmnm]))(*``BOX (^actnm) (^cabthmnm)``*) 568 val ithm = mk_inv_thm opr [List.hd args,cabthmnm] env ithml githms state chc msp seth 569 val _ = profTools.bgt (dpfx^"ca_box")(*PRF*) 570 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 571 val _ = profTools.ent (dpfx^"ca_box")(*PRF*) 572 in 573 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 574 NONE,NONE),rsc,ithm,SOME abthm) 575 end 576 | "mu" => let 577 val _ = dbgTools.DST (dpfx^ "ca_ mu") (*DBG*) 578 val _ = profTools.bgt (dpfx^"ca_mu")(*PRF*) 579 val chc = (if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 1 else 0) 580 val cabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 581 val rvnm = List.hd args 582 val _ = profTools.ent (dpfx^"ca_mu")(*PRF*) 583 val abthm = mk_abbr (list_mk_comb(mutm,[rvnm,cabthmnm]))(*``mu (^rvnm) .. (^cabthmnm)``*) 584 val ithm = mk_inv_thm opr [List.hd args,cabthmnm] env 585 ithml githms state chc msp seth 586 val _ = profTools.bgt (dpfx^"ca_mu")(*PRF*) 587 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 588 val _ = profTools.ent (dpfx^"ca_mu")(*PRF*) 589 in 590 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 591 NONE,NONE),rsc,ithm,SOME abthm) 592 end 593 | "nu" => let 594 val _ = dbgTools.DST (dpfx^ "ca_ nu") (*DBG*) 595 val _ = profTools.bgt (dpfx^"ca_nu")(*PRF*) 596 val chc = (if (is_imp(snd(strip_forall(concl(List.last ithml))))) then 1 else 0) 597 val cabthmnm = lhs(concl(Option.valOf(List.hd abthml))) 598 val rvnm = List.hd args 599 val _ = profTools.ent (dpfx^"ca_nu")(*PRF*) 600 val abthm = mk_abbr (list_mk_comb(nutm,[rvnm,cabthmnm]))(*``nu (^rvnm) .. (^cabthmnm)`` *) 601 val ithm = mk_inv_thm opr [List.hd args,cabthmnm] env ithml githms state chc msp seth 602 val _ = profTools.bgt (dpfx^"ca_nu")(*PRF*) 603 val ithm = PURE_ONCE_REWRITE_RULE [SYM abthm] ithm 604 val _ = profTools.ent (dpfx^"ca_nu")(*PRF*) 605 in 606 (ref (NONE,NONE,NONE,env,~1,rsc,ithm,SOME abthm, 607 NONE,NONE),rsc,ithm,SOME abthm) 608 end 609 | _ => Raise Match 610 in 611 let 612 val _ = profTools.bgt(dpfx^"ca_bmi")(*PRF*) 613 val _ = Polyhash.insert ce (cekey,en)(*Redblackmap.insert(ce,cekey,en) *) 614 val _ = profTools.ent(dpfx^"ca_bmi")(*PRF*) 615 in 616 (en,(ce,rsc,ithm,abthm)) 617 end 618 end 619 val _ = profTools.ent (dpfx^"ca")(*PRF*) 620 val _ = dbgTools.DEX dpfx "ca" (*DBG*) 621 in res end 622| cache_add _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = Raise Match 623 624(* take two reverse scopes and merge into one *) 625fun rcs_merge r1 r2 = 626 Vector.mapi (fn (i,_) => if (Vector.sub(r1,i)>Vector.sub(r2,i)) then 627 Vector.sub(r1,i) 628 else Vector.sub(r2,i)) 629 (Vector.tabulate(Vector.length r1,fn i => 0)) 630 631fun BST_merge b1 b2 = (* merge two binary maps, b2 overwriting b1 in case of key collision *) 632 let val _ = profTools.bgt (dpfx^"bstm")(*PRF*) 633 val res = Binarymap.foldl (fn (k,v,ab) => Binarymap.insert(ab,k,v)) b1 b2 634 val _ = profTools.ent (dpfx^"bstm")(*PRF*) 635 in res end 636 637fun PH_merge p1 p2 = (* merge two hashtables, p2 overwriting p1 in case of key collision *) 638 let val _ = profTools.bgt (dpfx^"phm")(*PRF*) 639 val _ = Polyhash.map (fn (k,v) => Polyhash.peekInsert p2 (k,v)) p1 640 val _ = profTools.ent (dpfx^"phm")(*PRF*) 641 in p2 end 642 643(* these are place holders for whatever data structure I use to handle the frv abbrev thms*) 644val frv_merge = PH_merge(*BST_merge*) 645fun frv_insert (s,k,v) = (Polyhash.insert s (k,v); s)(*Binarymap.insert(s,k,v)*) 646fun frv_empty ce = Polyhash.mkDict Term.compare 647fun frv_find s k = Polyhash.find s k 648 649(* ASSERT: mf = uniq mf (fv mf) [] *) 650fun mk_cache_aux ee rvnm2ix env (nf,mf) mfo ce rscope depth rvty githms state seth msp guid tysimps p_ty 651 (cons as (ctm,dtm,ntm,dmdtm,boxtm,rvtm,mutm,nutm,imftm)) = 652 let 653 val _ = dbgTools.DEN dpfx "mca" (*DBG*) 654 val (opr,args) = strip_comb mf 655 val (opro,argso) = strip_comb mfo 656 (*val _ = dbgTools.DTM (dpfx^ mf) val _ = dbgTools.DST (dpfx^ " mf\n") (*DBG*)*) 657 val lab = ""(*DBG*) 658 val res = case (fst(dest_const opr)) of 659 "TR" =>let val _ = profTools.bgt (dpfx^"mca_t")(*PRF*) 660 val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 661 githms state seth msp guid [] cons 662 val frv = lhs(concl (Option.valOf abthm)) 663 val res = ((muTR pt, 664 (Binarymap.mkDict Term.compare),frv_insert(frv_empty ce,frv,Option.valOf abthm)), 665 (ce1,rsc,ithm,abthm,Option.valOf abthm)) 666 val _ = profTools.ent (dpfx^"mca_t")(*PRF*) 667 in res end 668 | "FL" =>let val _ = profTools.bgt (dpfx^"mca_f")(*PRF*) 669 val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 670 githms state seth msp guid [] cons 671 val frv = lhs(concl (Option.valOf abthm)) 672 val res = ((muFL pt, 673 (Binarymap.mkDict Term.compare),frv_insert(frv_empty ce,frv,Option.valOf abthm)), 674 (ce1,rsc,ithm,abthm,Option.valOf abthm)) 675 val _ = profTools.ent (dpfx^"mca_f")(*PRF*) 676 in res end 677 | "RV" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 678 githms state seth msp guid [] cons 679 val _ = profTools.bgt (dpfx^"mca_rv")(*PRF*) 680 val frv = lhs(concl (Option.valOf abthm)) 681 val res = ((muRV pt, 682 (Binarymap.mkDict Term.compare),frv_insert(frv_empty ce,frv,Option.valOf abthm)), 683 (ce1,rsc,ithm,abthm,Option.valOf abthm)) 684 val _ = profTools.ent (dpfx^"mca_rv")(*PRF*) 685 in res end 686 | "AP" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 687 githms state seth msp guid [] cons 688 val _ = profTools.bgt (dpfx^"mca_ap")(*PRF*) 689 val frv = lhs(concl (Option.valOf abthm)) 690 val res = ((muAP pt, 691 (Binarymap.mkDict Term.compare),frv_insert(frv_empty ce,frv,Option.valOf abthm)), 692 (ce1,rsc,ithm,abthm,Option.valOf abthm)) 693 val _ = profTools.ent (dpfx^"mca_ap")(*PRF*) 694 in res end 695 | "Not" =>let val ((pt1,imfs,abs),(ce1,rsc,ithm,abthm,xabthm)) = 696 mk_cache_aux ee rvnm2ix env (nf,(List.hd args)) (List.hd argso) 697 ce rscope depth rvty githms state seth msp guid tysimps p_ty cons 698 val (pt,(ce2,rsc2,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty 699 [ithm] githms state seth msp guid [abthm] cons 700 val _ = profTools.bgt (dpfx^"mca_n")(*PRF*) (* this is here so we don't include the recursive call as part of Not *) 701 val xabthm = PURE_ONCE_REWRITE_RULE [xabthm] (Option.valOf abthm) 702 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) 703 val _ = profTools.ent (dpfx^"mca_n")(*PRF*) 704 in ((muNot(pt,pt1),imfs,abs),(ce2,rsc2,ithm,abthm,xabthm)) end 705 | "And" =>let val ((ptl,imfsl,absl),(ce1,rsc,it1,ab1,xab1)) = 706 mk_cache_aux ee rvnm2ix env (nf,(List.hd args)) (List.hd argso) ce 707 rscope depth rvty githms state seth msp guid tysimps p_ty cons 708 val ((ptr,imfsr,absr),(ce2,rsc2,it2,ab2,xab2)) = 709 mk_cache_aux ee rvnm2ix env (nf,(List.last args)) (List.last argso) ce1 710 rsc depth rvty githms state seth msp guid tysimps p_ty cons 711 val (pt,(ce3,rsc3,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce2 (rcs_merge rsc rsc2) 712 rvty [it1,it2] githms state seth msp guid [ab1,ab2] cons 713 val _ = profTools.bgt (dpfx^"mca_c")(*PRF*) 714 val _ = profTools.bgt (dpfx^"mca_c1")(*PRF*) 715 val xabthm = PURE_ONCE_REWRITE_RULE [xab1] (PURE_ONCE_REWRITE_RULE [xab2] (Option.valOf abthm)) 716 val _ = profTools.ent (dpfx^"mca_c1")(*PRF*) 717 val _ = profTools.bgt (dpfx^"mca_c2")(*PRF*) 718 val abs = frv_insert(frv_merge absl absr,lhs(concl (xabthm)),xabthm) 719 val _ = profTools.ent (dpfx^"mca_c2")(*PRF*) 720 val _ = profTools.bgt (dpfx^"mca_c3")(*PRF*) 721 val res = ((muAnd(pt,(ptl,ptr)),BST_merge imfsl imfsr,abs),(ce3,rsc3,ithm,abthm,xabthm)) 722 val _ = profTools.ent (dpfx^"mca_c3")(*PRF*) 723 val _ = profTools.ent (dpfx^"mca_c")(*PRF*) 724 in res end 725 | "Or" =>let val ((ptl,imfsl,absl),(ce1,rsc,it1,ab1,xab1)) = 726 mk_cache_aux ee rvnm2ix env (nf,(List.hd args)) (List.hd argso) ce 727 rscope depth rvty githms state seth msp guid tysimps p_ty cons 728 val ((ptr,imfsr,absr),(ce2,rsc2,it2,ab2,xab2)) = 729 mk_cache_aux ee rvnm2ix env (nf,(List.last args)) (List.last argso) ce1 730 rsc depth rvty githms state seth msp guid tysimps p_ty cons 731 val (pt,(ce3,rsc3,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce2 (rcs_merge rsc rsc2) 732 rvty [it1,it2] githms state seth msp guid [ab1,ab2] cons 733 val _ = profTools.bgt (dpfx^"mca_d")(*PRF*) 734 val xabthm = PURE_ONCE_REWRITE_RULE [xab1] (PURE_ONCE_REWRITE_RULE [xab2] (Option.valOf abthm)) 735 val abs = frv_insert(frv_merge absl absr,lhs(concl (xabthm)),xabthm) 736 val res = ((muOr(pt,(ptl,ptr)),BST_merge imfsl imfsr,abs),(ce3,rsc3,ithm,abthm,xabthm)) 737 val _ = profTools.ent (dpfx^"mca_d")(*PRF*) 738 in res end 739 | "DIAMOND" =>let val ((pt1,imfs,abs),(ce1,rsc,ithm,ab,xab)) = 740 mk_cache_aux ee rvnm2ix env (nf,(List.last args)) (List.last argso) ce 741 rscope depth rvty githms state seth msp guid tysimps p_ty cons 742 val (pt,(ce2,rsc2,ithm,ab))=cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty 743 [ithm] githms state seth msp guid [ab] cons 744 val _ = profTools.bgt (dpfx^"mca_dmd")(*PRF*) 745 val xabthm = PURE_ONCE_REWRITE_RULE [xab] (Option.valOf ab) 746 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) 747 val res = ((muDIAMOND(pt,(fromHOLstring(List.hd args),pt1)),imfs,abs),(ce2,rsc2,ithm,ab,xabthm)) 748 val _ = profTools.ent (dpfx^"mca_dmd")(*PRF*) 749 in res end 750 | "BOX" =>let val ((pt1,imfs,abs),(ce1,rsc,ithm,ab,xab)) = 751 mk_cache_aux ee rvnm2ix env (nf,(List.last args)) (List.last argso) ce 752 rscope depth rvty githms state seth msp guid tysimps p_ty cons 753 val (pt,(ce2,rsc2,ithm,ab))=cache_add depth rvnm2ix env (nf,mf) mfo ce1 rsc rvty 754 [ithm] githms state seth msp guid [ab] cons 755 val _ = profTools.bgt (dpfx^"mca_box")(*PRF*) 756 val xabthm = PURE_ONCE_REWRITE_RULE [xab] (Option.valOf ab) 757 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) 758 val res = ((muBOX(pt,(fromHOLstring(List.hd args),pt1)),imfs,abs),(ce2,rsc2,ithm,ab,xabthm)) 759 val _ = profTools.ent (dpfx^"mca_box")(*PRF*) 760 in res end 761 | "mu" => let val (ptr,(ce0,rsc,ithm,abthm)) = cache_add (depth+1) 762 ((fromHOLstring(List.hd args),depth)::rvnm2ix) 763 env (nf,(mk_comb(rvtm,List.hd args))) (mk_comb(rvtm,List.hd argso)) ce rscope 764 ((List.hd args,false)::rvty) [] githms state seth msp guid [] cons 765 val ((pt1,imfs,abs),(ce1,rsc,ithm,abthm,xabthm)) = 766 mk_cache_aux ee ((fromHOLstring(List.hd args),depth)::rvnm2ix) 767 env (nf,(List.last args)) (List.last argso) ce0 rscope (depth+1) 768 ((List.hd args,false)::rvty) githms state seth msp guid tysimps p_ty cons 769 val _ = profTools.bgt (dpfx^"mca_mu")(*PRF*) 770 val abs = frv_insert(abs,List.last args,xabthm) 771 val _ = profTools.ent (dpfx^"mca_mu")(*PRF*) 772 val (pt,(ce2,rsc2,ithm,abthm)) = 773 cache_add depth rvnm2ix env (nf,mf) mfo ce1 774 (Vector.mapi (fn (i,v) => if (i=depth) then 775 0 776 else v) 777 rsc) 778 rvty [ithm] githms state seth msp guid 779 [abthm] cons 780 val _ = profTools.bgt (dpfx^"mca_mu")(*PRF*) 781 val xabthm = PURE_ONCE_REWRITE_RULE [xabthm] (Option.valOf abthm) 782 val imfth = PURE_ONCE_REWRITE_RULE [SYM xabthm] (mk_imf_thm imftm mf tysimps p_ty) 783 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) 784 val res = ((fpmu(ptr,pt,pt1),Binarymap.insert(imfs,mf,imfth),abs),(ce2,rsc2,ithm,abthm,xabthm)) 785 val _ = profTools.ent (dpfx^"mca_mu")(*PRF*) 786 val _ = dbgTools.DST (dpfx^ "mu done\n") 787 in res end 788 | "nu" => let val (ptr,(ce0,rsc,ithm,abthm)) = cache_add (depth+1) 789 ((fromHOLstring(List.hd args),depth)::rvnm2ix) 790 env (nf,(mk_comb(rvtm,List.hd args))) (mk_comb(rvtm,List.hd argso)) ce rscope 791 ((List.hd args,true)::rvty) [] githms state seth msp guid [] cons 792 val ((pt1,imfs,abs),(ce1,rsc,ithm,abthm,xabthm)) = 793 mk_cache_aux ee ((fromHOLstring(List.hd args),depth)::rvnm2ix) 794 env (nf,(List.last args)) (List.last argso) ce0 rscope (depth+1) 795 ((List.hd args,true)::rvty) githms state seth msp guid tysimps p_ty cons 796 val _ = profTools.bgt (dpfx^"mca_nu1")(*PRF*) 797 val abs = frv_insert(abs,List.last args,xabthm) 798 val _ = profTools.ent (dpfx^"mca_nu1")(*PRF*) 799 val (pt,(ce2,rsc2,ithm,abthm)) = 800 cache_add depth rvnm2ix env (nf,mf) mfo ce1 801 (Vector.mapi (fn (i,v) => if (i=depth) then 802 0 803 else v) 804 rsc) 805 rvty [ithm] githms state seth msp 806 guid [abthm] cons 807 val _ = profTools.bgt (dpfx^"mca_nu2a")(*PRF*) 808 val xabthm = PURE_ONCE_REWRITE_RULE [xabthm] (Option.valOf abthm) 809 val _ = profTools.ent (dpfx^"mca_nu2a")(*PRF*) 810 val _ = profTools.bgt (dpfx^"mca_nu2b")(*PRF*) 811 val imfth = PURE_ONCE_REWRITE_RULE [SYM xabthm] (mk_imf_thm imftm mf tysimps p_ty) 812 val _ = profTools.ent (dpfx^"mca_nu2b")(*PRF*) 813 val _ = profTools.bgt (dpfx^"mca_nu3")(*PRF*) 814 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) 815 val res = ((fpnu(ptr,pt,pt1),Binarymap.insert(imfs,mf,imfth),abs),(ce2,rsc2,ithm,abthm,xabthm)) 816 val _ = profTools.ent (dpfx^"mca_nu3")(*PRF*) 817 val _ = dbgTools.DST (dpfx^ "nu done\n") 818 in res end 819 | _ => failwith ("mk_cache_aux Match:"^(term_to_string mf)) 820 val _ = dbgTools.DEX dpfx "mca" (*DBG*) 821 in res end 822 823 824(*FIXME: this still takes a significant portion of the time *) 825fun mk_cache ee env (nf,mf) mfo qd githms state (seth,sel) msp = 826 let val _ = dbgTools.DEN dpfx "mc" (*DBG*) 827 (*val _ = dbgTools.DTM (dpfx^ mf) *)(*DBG*) 828 val _ = profTools.bgt (dpfx^"mc")(*PRF*) 829 (* make a mapping from rv's to their index in ee *) 830 val rvnm2ix = fst(Array.foldl(fn ((k,tb),(l,n)) => ((k,n)::l,n+1)) ([],0) ee) 831 val p_ty = get_prop_type mf 832 val res = fst (mk_cache_aux ee rvnm2ix env (nf^"frv",mf) mfo 833 (Polyhash.mkDict Term.compare) 834 (Vector.tabulate(qd+(List.length rvnm2ix),fn ix => 0)) 835 (List.length rvnm2ix) 836 [] githms state seth msp (ref 0) 837 (mk_tysimps sel p_ty) 838 p_ty 839 (get_mu_ty_conj_tm p_ty,get_mu_ty_disj_tm p_ty,get_mu_ty_neg_tm p_ty, 840 get_mu_ty_dmd_tm p_ty,get_mu_ty_box_tm p_ty,get_mu_ty_rv_tm p_ty, 841 get_mu_ty_mu_tm p_ty,get_mu_ty_nu_tm p_ty,inst [alpha |-> p_ty] mu_imf_tm) 842 ) 843 val _ = profTools.ent (dpfx^"mc")(*PRF*) 844 val _ = dbgTools.DEX dpfx "mc" (*DBG*) 845 in res end 846 847 848fun upd_cch_tb cch tb = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(SOME tb,b,c,d,e,f,g,h,i,j)) end 849fun upd_cch_gth cch gth = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(a,SOME gth,c,d,e,f,g,h,i,j)) end 850fun upd_cch_sth cch sth = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(a,b,SOME sth,d,e,f,g,h,i,j)) end 851fun upd_cch_env cch env = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(a,b,c,env,e,f,g,h,i,j)) end 852fun upd_cch_subth cch subth = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(a,b,c,d,e,f,g,h,SOME subth,j)) end 853fun upd_cch_eqth cch eqth = let val (a,b,c,d,e,f,g,h,i,j) = !cch in (cch:=(a,b,c,d,e,f,g,h,i,SOME eqth)) end 854 855fun mk_ado_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm wfKS_ks ie t1 initset finset seth imf_t2 ess eus chainth n = 856 let 857 (* make ado sub_thm i.e.initset SUBSET STATES f ks e[[[Q<--initset]]],used to discharge GEN_MU_FP_STATES *) 858 val _ = dbgTools.DEN dpfx "as" (*DBG*) 859 (*val _ = dbgTools.DTM (dpfx^ initset) val _ = dbgTools.DST (dpfx^ " ADO initset\n") (*DBG*) 860 val _ = dbgTools.DTM (dpfx^ finset) val _ = dbgTools.DST (dpfx^ " ADO finset\n") (*DBG*)*) 861 val res = if (Term.compare(initset,finset)=EQUAL) then ado_subthm 862 else 863 let 864 val n = rand finset 865 (*val _ = dbgTools.DTH (dpfx^" spec glc") (ISPECL [t2,ksname,ie,n,t1,initset] chainth)) (*DBG*) 866 val _ = dbgTools.DTH (dpfx^ ado_subthm) val _ = dbgTools.DST (dpfx^ " prev ado_subthm\n") (*DBG*)*) 867 val ado_subthm = (MP (ISPECL [t2,ksname,ie,n,t1,initset] chainth) 868 (LIST_CONJ [wfKS_ks,PURE_ONCE_REWRITE_RULE [abthm] imf_t2,ado_subthm])) 869 val ado_subthm'' = CONV_RULE (RAND_CONV(ONCE_REWRITE_CONV [STATES_def] 870 THENC REWRITE_CONV [ENV_EVAL,ENV_UPDATE])) ado_subthm 871 (*val _ = dbgTools.DTH (dpfx^ ado_subthm'') val _ = dbgTools.DST (dpfx^ " init ado_subthm\n") (*DBG*)*) 872 in ado_subthm'' end 873 val _ = dbgTools.DEX dpfx "as" (*DBG*) 874 in res end 875 876fun lift_ado_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm wfKS_ks ie t1 initset seth imf_t2 ess 877 Ss eus adogeneqthm initsubth n = 878 let 879 (* make ado sub_thm i.e.initset SUBSET STATES f ks e[[[Q<--initset]]],used to discharge GEN_MU_FP_STATES *) 880 val _ = dbgTools.DEN dpfx "al" (*DBG*) 881 (*val _ = dbgTools.DTM (dpfx^ initset) val _ = dbgTools.DST (dpfx^ " ADOlift initset\n") (*DBG*)*) 882 val n = if ((Term.compare(initset,ess)=EQUAL) orelse (Term.compare(initset,Ss)=EQUAL)) then numSyntax.zero_tm else rand initset 883 val prev_adosubthm = if ado then (Option.valOf ado_subthm) 884 else (ISPEC ``STATES ^t2 ^ksname ^ie1`` initsubth) 885 (*val _ = dbgTools.DTH (dpfx^ prev_adosubthm) val _ = dbgTools.DST (dpfx^ " ADOlift prev ado_subthm\n") (*DBG*) 886 val _ = if (not (null eeq)) then dbgTools.DTH (dpfx^ (fst (hd eeq))) else dbgTools.DST (dpfx^ "empty") (*DBG*) 887 val _ = dbgTools.DST (dpfx^ " ADOlift hd eeq\n") (*DBG*) *) 888 val ado_subthm = 889 if ado then 890 let 891 (*val _ = dbgTools.DTM (dpfx^ t2) val _ = dbgTools.DST (dpfx^ " ADOlift t1\n") (*DBG*) 892 val _ = dbgTools.DTH (dpfx^ (Binarymap.find(imf_thms,t2))) (*DBG*) 893 val _ = dbgTools.DTH (dpfx^ (snd(hd eeq))) val _ = dbgTools.DST (dpfx^ " ADOlift prev ab th\n") (*DBG*) 894 val _ = dbgTools.DTH (dpfx^ abthm) val _ = dbgTools.DST (dpfx^ " ADOlift curr ab th\n") (*DBG*)*) 895 val prevth = MATCH_MP STATES_MONO_EQ 896 (LIST_CONJ [wfKS_ks,PURE_ONCE_REWRITE_RULE [snd(hd eeq)] (Binarymap.find(imf_thms,t2)), 897 PURE_ONCE_REWRITE_RULE [adogeneqthm] (fst(hd eeq))]) 898 (*val _ = dbgTools.DTH (dpfx^ prevth) val _ = dbgTools.DST (dpfx^ " ADOlift prev th\n") (*DBG*)*) 899 val (ie0,(t1o,_)) = dest_env ie 900 val ie0' = list_mk_comb(eus,[ie0,t1,initset]) 901 val prevth2 = REWRITE_RULE [MATCH_MP ENV_SWAP (Binarymap.find(Binarymap.find(seth,fromHOLstring t1), 902 fromHOLstring t1o))] (SPEC ie0' prevth) 903 (*val _ = dbgTools.DTH (dpfx^ prevth2) val _ = dbgTools.DST (dpfx^ " ADOlift prev th 2\n") (*DBG*)*) 904 in MATCH_MP SUBSET_TRANS (LIST_CONJ [prev_adosubthm,prevth2]) end 905 else prev_adosubthm 906 (*val _ = dbgTools.DTH (dpfx^ ado_subthm) val _ = dbgTools.DST (dpfx^ " lifted ado_subthm\n") (*DBG*)*) 907 val _ = dbgTools.DEX dpfx "al" (*DBG*) 908 in ado_subthm end 909 910fun mk_ado_pre_sub_thm ado ado_subthm t2 ksname ie1 eeq imf_thms abthm wfKS_ks ie t1 initset seth imf_t2 ess 911 eus chainth adogeneqthm initsubth n = 912 let 913 (* make ado sub_thm i.e.initset SUBSET STATES f ks e[[[Q<--initset]]],used to discharge GEN_MU_FP_STATES *) 914 val _ = dbgTools.DEN dpfx "ap" (*DBG*) 915 (*val _ = dbgTools.DTM (dpfx^ initset) val _ = dbgTools.DST (dpfx^ " ADOpre initset\n") (*DBG*) 916 val _ = dbgTools.DTH (dpfx^" ADOpre spec glc\n" (ISPECL [t2,ksname,ie,n,t1,initset] chainth)) (*DBG*)*) 917 val prev_adosubthm = if ado then (Option.valOf ado_subthm) 918 else (ISPEC ``STATES ^t2 ^ksname ^ie1`` initsubth) 919 (*val _ = dbgTools.DTH (dpfx^ prev_adosubthm) val _ = dbgTools.DST (dpfx^ " ADOpre prev ado_subthm\n") (*DBG*)*) 920 val _ = if (not (null eeq)) then dbgTools.DTH (dpfx^"ap_ hd eeq") (fst (hd eeq)) else dbgTools.DST (dpfx^"ap_ empty") 921 (*val _ = dbgTools.DST (dpfx^ " hd eeq\n") (*DBG*) *) 922 val ado_subthm' = 923 if ado then 924 let 925 (*val _ = dbgTools.DTM (dpfx^ t2) val _ = dbgTools.DST (dpfx^ " ADOpre t1\n") (*DBG*) 926 val _ = dbgTools.DTH (dpfx^" ADO prev imf th\n" (Binarymap.find(imf_thms,t2))) (*DBG*) 927 val _ = dbgTools.DTH (dpfx^ (snd(hd eeq))) val _ = dbgTools.DST (dpfx^ " ADO prev ab th\n") (*DBG*) 928 val _ = dbgTools.DTH (dpfx^ abthm) val _ = dbgTools.DST (dpfx^ " ADOpre curr ab th\n") (*DBG*)*) 929 val prevth = MATCH_MP STATES_MONO_EQ 930 (LIST_CONJ [wfKS_ks,PURE_ONCE_REWRITE_RULE [snd(hd eeq)] (Binarymap.find(imf_thms,t2)), 931 PURE_ONCE_REWRITE_RULE [adogeneqthm] (fst(hd eeq))]) 932 (*val _ = dbgTools.DTH (dpfx^ prevth) val _ = dbgTools.DST (dpfx^ " ADOpre prev th\n") (*DBG*)*) 933 val (ie0,(t1o,_)) = dest_env ie 934 val ie0' = list_mk_comb(eus,[ie0,t1,initset]) 935 val prevth2 = REWRITE_RULE [MATCH_MP ENV_SWAP (Binarymap.find(Binarymap.find(seth,fromHOLstring t1), 936 fromHOLstring t1o))] (SPEC ie0' prevth) 937 (*val _ = dbgTools.DTH (dpfx^ prevth2) val _ = dbgTools.DST (dpfx^ " ADOpre prev th 2\n") (*DBG*)*) 938 in MATCH_MP SUBSET_TRANS (LIST_CONJ [prev_adosubthm,prevth2]) end 939 else (MP (ISPECL [t2,ksname,ie,n,t1,initset] chainth) 940 (LIST_CONJ [wfKS_ks,PURE_ONCE_REWRITE_RULE [abthm] imf_t2,prev_adosubthm])) 941 (*val _ = dbgTools.DTH (dpfx^ ado_subthm') val _ = dbgTools.DST (dpfx^ " ado_presubthm'\n") (*DBG*)*) 942 val _ = dbgTools.DEX dpfx "ap" (*DBG*) 943 in ado_subthm' end 944 945(* called by muCheck.mk_gen_thms *) 946fun mk_gen_inv_thms ksname state wfKS_ks = 947 let 948 val _ = dbgTools.DEN dpfx "mgit" (*DBG*) 949 val res = 950 [ISPEC ksname SAT_AP_ENV_INV, 951 ISPEC ksname SAT_RV_ENV_INV, 952 ISPEC ksname SAT_T_ENV_INV, 953 ISPEC ksname SAT_F_ENV_INV, 954 MP (ISPEC ksname SAT_NEG_ENV_INV) wfKS_ks, MP (ISPEC ksname SAT_NEG_ENV_INV2) wfKS_ks, 955 ISPEC ksname SAT_CONJ_ENV_INV,ISPEC ksname SAT_CONJ_ENV_INV2, 956 ISPEC ksname SAT_DISJ_ENV_INV,ISPEC ksname SAT_DISJ_ENV_INV2, 957 ISPEC ksname SAT_DMD_ENV_INV, ISPEC ksname SAT_DMD_ENV_INV2, 958 ISPEC ksname SAT_BOX_ENV_INV, ISPEC ksname SAT_BOX_ENV_INV2, 959 ISPECL [ksname,state] SAT_LFP_ENV_INV, ISPEC ksname SAT_LFP_ENV_INV2, 960 ISPECL [ksname,state] SAT_GFP_ENV_INV, ISPEC ksname SAT_GFP_ENV_INV2] 961 val _ = dbgTools.DEX dpfx "mgit" (*DBG*) 962 in res end 963 964 965fun mk_ado_imf_goals [] = [] 966| mk_ado_imf_goals sigfl = 967 let 968 val _ = dbgTools.DEN dpfx "aig" (*DBG*) 969 val sfl2 = List.filter (fn (_,l) => not (null l)) (List.map (fn f => (f,top_sigma (is_nu f) (rand f))) sigfl) 970 val prop_type = hd(snd(dest_type(type_of (hd sigfl)))) 971 val ip = inst [alpha|->prop_type] 972 val gls = List.map (fn (f,sfl) => List.map (fn sf => mk_comb((ip mu_imf_tm), 973 list_mk_comb(ip(if is_nu f then mu_nu_tm else mu_mu_tm), 974 [rand (rator f),rand sf]))) sfl) sfl2 975 val res = (List.concat gls)@(mk_ado_imf_goals (List.concat (List.map snd sfl2))) 976 val _ = dbgTools.DEX dpfx "aig" (*DBG*) 977 in res end 978 979(* for each sigma formula sig Q.f, if there exists in f a top-level sig formula of the same type (mu/nu) sig P.g, then prove that 980 IMF Q. g *) 981fun mk_ado_imf_thms mf seth tysimps frv_thms imf_thms= 982 let 983 val _ = dbgTools.DEN dpfx "ai"(*DBG*) 984 val sigfl = (top_sigma true mf)@(top_sigma false mf) 985 val prop_type = hd(snd(dest_type(type_of mf))) 986 (*val _ = DMSG (TY prop_type) val _ = dbgTools.DST (dpfx^ "ptype\n") *) 987 val ip = inst [alpha|->prop_type] 988 val res = if null sigfl then imf_thms 989 else let 990 val gls = mk_ado_imf_goals sigfl 991 val sel = (List.map (fn (rv,eqs) => eqs) (flatten(List.map (fn (rv,bm)=>Binarymap.listItems bm) 992 (Binarymap.listItems seth)))) 993 val res = List.foldl (fn (gl,bm) => 994 let val jf = (fn _ => prove(gl,SIMP_TAC std_ss ([IMF_def,MU_SUB_def,NNF_def,RVNEG_def] @ 995 tysimps @ sel))) 996 val th = mk_lthm (fn _ => (gl,jf)) jf 997 (*val _ = dbgTools.DTH (dpfx^" ADO imf th\n" th) (*DBG*)*) 998 val frv_thm = frv_find frv_thms (rand (rand gl)) 999 (*val _ = dbgTools.DTH (dpfx^ frv_thm) (*DBG*) 1000 val _ = dbgTools.DST (dpfx^ " ADO ab th\n") (*DBG*)*) 1001 val th1 = ONCE_REWRITE_RULE [SYM frv_thm] th 1002 (*val _ = dbgTools.DTH (dpfx^" ab ADO imf th" th1) (*DBG*)*) 1003 in Binarymap.insert(bm,lhs(concl frv_thm),th1) end) 1004 imf_thms gls 1005 in res end 1006 val _ = dbgTools.DEX dpfx "ai"(*DBG*) 1007 in res end 1008 1009end 1010end 1011