1structure ksTools = 2struct 3 4local 5 6open Globals HolKernel Parse 7 8open bossLib 9open pairTheory 10open pred_setTheory 11open pred_setLib 12open stringLib 13open listTheory 14open simpLib 15open pairSyntax 16open pairLib 17open PrimitiveBddRules 18open DerivedBddRules 19open Binarymap 20open PairRules 21open pairTools 22open setLemmasTheory 23open boolSyntax 24open Drule 25open Tactical 26open Conv 27open Rewrite 28open Tactic 29open bddTools 30open stringBinTree 31open ksTheory 32open commonTools 33open boolTheory 34open lazyTools 35open lzPairRules 36 37val dpfx = "kt_"; 38 39in 40 41fun mk_bool_var s = mk_var(s,bool) 42 43fun mk_AP state ap = mk_pabs(state,ap) 44 45(* take a state and return it with all vars primed, preserving nested tuple structure if any *) 46fun mk_primed_state s = 47if is_pair s then list_mk_pair(List.map mk_primed_state (spine_pair s)) 48else mk_var((term_to_string2 s)^"'",type_of s) 49 50fun has_primed_vars t = List.exists (fn v => Char.compare(#"'", 51 List.last(String.explode ((with_flag(show_types,false) 52 term_to_string) v)))=EQUAL) (free_vars t) 53 54val ks_p_ty = ``:'prop`` 55val ks_s_ty = ``:'state`` 56val ks_as_ty = ``:'astate`` 57 58fun get_types ksname = let val (_,l) = dest_type (type_of ksname) in (hd l,last l) end 59 60val dotacn = ``"."`` 61 62val _ = set_trace "notify type variable guesses" 0; 63val ksS_tm = ``ks$KS_S`` 64val ksS0_tm = ``ks$KS_S0`` 65val ksT_tm = ``ks$KS_T`` 66val ksap_tm = ``ks$KS_ap`` 67val ksL_tm = ``ks$KS_L`` 68 69val ksSu_tm = ``ks$KS_S_fupd`` 70val ksS0u_tm = ``ks$KS_S0_fupd`` 71val ksTu_tm = ``ks$KS_T_fupd`` 72val ksapu_tm = ``ks$KS_ap_fupd`` 73val ksLu_tm = ``ks$KS_L_fupd`` 74val _ = set_trace "notify type variable guesses" 1; 75 76val getS = (rand o rand o rator) 77val getS0 = rand o rand o rator o rand 78val getT = rand o rand o rator o rand o rand 79val getap = (rand o rand o rator o rand o rand o rand) 80fun getL tm = (rand o rand o rator o rand o rand o rand o rand) tm 81 handle ex => (rand o rand o rator o rand o rand o rand) tm (* in case there is no ap *) 82 83(* FIXME: this assumes alpha stands for st_ty etc. This could change if HOL records change *) 84fun mk_ks s_ty p_ty ks_ty S S0 T ap L = 85let val _ = dbgTools.DEN dpfx "mk" (*DBG*) 86 val ksSu = inst [alpha |-> s_ty,beta |-> p_ty] ksSu_tm 87 val ksS0u = inst [alpha |-> s_ty,beta |-> p_ty] ksS0u_tm 88 val ksTu = inst [alpha |-> s_ty,beta |-> p_ty] ksTu_tm 89 val ksapu = inst [alpha |-> p_ty,beta |-> s_ty] ksapu_tm (* FIXME: why are alpha and beta inverted here?*) 90 val ksLu = inst [alpha |-> s_ty,beta |-> p_ty] ksLu_tm 91 val arb_ks = inst [alpha |-> ks_ty] boolSyntax.arb 92 val _ = dbgTools.DTY (dpfx^"mk_arb_ks") (type_of arb_ks) (*DBG*) 93 val upds = if isSome ap then [(ksSu,S),(ksS0u,S0),(ksTu,T),(ksapu,valOf ap),(ksLu,L)] 94 else [(ksSu,S),(ksS0u,S0),(ksTu,T),(ksLu,L)] 95 val res = List.foldr (fn ((u,v),ks) => 96 let val _ = dbgTools.DTY (dpfx^"mk_u_ty") (type_of u) (*DBG*) 97 val _ = dbgTools.DTY (dpfx^"mk_v_ty") (type_of v) (*DBG*) 98 val _ = dbgTools.DTY (dpfx^"mk_ks_ty") (type_of ks) (*DBG*) 99 in mk_comb(mk_comb (u,mk_comb(inst [alpha |-> type_of v, beta |->type_of v] 100 combinSyntax.K_tm,v)),ks) end) 101 arb_ks upds 102 val _ = dbgTools.DEX dpfx "mk" (*DBG*) 103in res end 104 105fun get_APs_aux tm = 106if (is_neg tm orelse is_conj tm orelse is_imp tm orelse is_disj tm orelse is_cond tm orelse is_eq tm) 107then let val (_,args) = strip_comb tm 108 val res = List.concat (List.map get_APs_aux args) 109 in if is_eq tm (* an eq which has no AP's on either side is itself an AP *) 110 andalso List.null res (* either lhs nor rhs contained an AP *) 111 andalso List.null (List.filter has_primed_vars args) (* neither lhs nor rhs contain a primed var *) 112 then [tm] else res end 113else if Term.compare(tm,T)=EQUAL orelse Term.compare(tm,F)=EQUAL then [] 114else if (Type.compare(type_of tm,bool)=EQUAL) andalso not (has_primed_vars tm) then [tm] 115else []; 116 117(* given a term tm of type bool, return the list of all atomic propositions in tm, removing duplicates *) 118(* FIXME: should we fail if tm is not of type :bool? *) 119(* we do not count any atomic propositions over next state variables since by defn AP's are :state->bool *) 120fun get_APs tm = Binaryset.listItems(Binaryset.addList(Binaryset.empty Term.compare,get_APs_aux tm)) 121 122(* R is a term_bdd representing a transition relation. return totalised version *) 123fun totalise tbR S0 vm = 124 let val sv = strip_pair(rand (lhs (concl(SPEC_ALL(S0))))) 125 val s = List.map (with_flag(show_types,false) term_to_string) sv 126 val sp = List.map (fn v => mk_bool_var (v^"'")) s 127 val s2sp = List.map (fn(v,v') => (BddVar true vm v,BddVar true vm v')) (ListPair.zip(sv,sp)) 128 val self = list_mk_conj(List.map (fn v => mk_eq(mk_bool_var (v^"'"),mk_bool_var v)) (List.map term_to_string sv)) 129 val tbt = BddNot(BddAppex sp (bdd.And,tbR,(BddReplace s2sp (BddCon true vm)))) (*reachable terminal states*) 130 val tbl = t2tb vm self (* property saying all states have self loops *) 131 val tbtl = BddOp(bdd.And,tbt,tbl) (* terminal states with self loops *) 132 in BddOp(bdd.Or,tbR,tbtl) end 133 134(* Convert map from names to terms to names to term_bdds. 135 NOTE: the use of termToTermBddFun requires that the term argument not contain any uninterpreted constants. 136 T is a (string * term) list where each pair is (action name, corresponding transition relation) 137 vm is term_bdd varmap 138 OUT: a map : name of action -> termbdd of corresponding transition relation also add the dot action 139 TODO: fix NOTE issue above *) 140fun RmakeTmap KS_trans_def TS vm Ric state state' avar = 141 let val _ = dbgTools.DEN dpfx "rt" (*DBG*) 142 val _ = profTools.bgt (dpfx^"rt")(*PRF*) 143 fun makeR (h::t) mp = makeR t (insert(mp,(fst h), t2tb vm (snd h))) 144 | makeR [] mp = mp 145 val mp = mkDict String.compare 146 (*val U_T = if Ric then list_mk_conj(snd(unzip T)) else list_mk_disj(snd(unzip T))*) 147 val Tmap = makeR TS mp (*,".",DerivedBddRules.GenTermToTermBdd (!DerivedBddRules.termToTermBddFun) vm (U_T))*) 148 val _ = profTools.bgt (dpfx^"rt_fc")(*PRF*) 149 val kstdnm = fst(strip_comb(lhs(concl (SPEC_ALL KS_trans_def)))) 150 val Tmap' = Binarymap.map (fn (nm,tb) => 151 let val holnm = fromMLstring nm 152 val jf = (fn _ => SYM (CONV_RULE (RHS_CONV find_CONV) (SPEC_ALL (SPEC holnm KS_trans_def)))) 153 val th = mk_lthm 154 (fn _ => (mk_eq(getTerm tb,list_mk_comb(kstdnm,[holnm,mk_pair(state,state')])), 155 jf)) jf 156 val _ = dbgTools.DTH (dpfx^"rt_"^nm) th (*DBG*) 157 in BddEqMp th tb end) Tmap 158 val _ = profTools.ent (dpfx^"rt_fc")(*PRF*) 159 val _ = Binarymap.app (fn (nm,tb) => dbgTools.DTB (dpfx^"rt_"^nm) tb) Tmap'(*DBG*) 160 val _ = profTools.ent (dpfx^"rt")(*PRF*) 161 val _ = dbgTools.DEX dpfx "rt" (*DBG*) 162 in Tmap' end 163 164fun prove_wfKS ks_def = 165 let val jf = (fn _ => prove(``wfKS ^(lhs (concl ks_def))``, 166 PURE_ONCE_REWRITE_TAC [wfKS_def] THEN CONJ_TAC THENL 167 [PURE_REWRITE_TAC [ks_def,KS_accfupds,combinTheory.K_DEF] 168 THEN (CONV_TAC (DEPTH_CONV BETA_CONV)) THEN PURE_REWRITE_TAC [SUBSET_UNIV], 169 PURE_REWRITE_TAC [ks_def,KS_accfupds,combinTheory.K_DEF] 170 THEN (CONV_TAC (DEPTH_CONV BETA_CONV)) THEN REFL_TAC])) 171 in mk_lthm (fn _ => (``wfKS ^(lhs (concl ks_def))``,jf)) jf end 172 173 174fun mk_model_names ksname state_type prop_type = 175 let val _ = dbgTools.DEN dpfx "mmn" (*DBG*) 176 val kn = if (Option.isSome ksname) then "muKS_"^(Option.valOf ksname) else "muKS" 177 val Tn = "T_"^kn 178 val _ = new_constant(Tn,stringLib.string_ty --> (mk_prod(state_type,state_type)) --> bool) 179 val Tnm = mk_const(Tn,stringLib.string_ty --> (mk_prod(state_type,state_type)) --> bool) 180 val S0n = "S0_"^kn 181 val _ = new_constant(S0n,state_type --> bool) 182 val S0nm = mk_const(S0n, state_type --> bool) 183 val _ = dbgTools.DEX dpfx "mmn" (*DBG*) 184in (kn,Tnm,Tn,S0nm,S0n) end 185 186 187(* TS is the (nm,term) list derived from the output of RmakeTmap, S0 is the initial state set *) 188fun mk_formal_KS S0 TS state Ric apl abs_fun ksname = 189 let val _ = dbgTools.DEN dpfx "mw" (*DBG*) 190 val _ = profTools.bgt (dpfx^"mw")(*PRF*) 191 val _ = profTools.bgt (dpfx^"mw_init")(*PRF*) 192 val state' = mk_primed_state state 193 val _ = dbgTools.DTM (dpfx^"mw_state'") state'(*DBG*) 194 val (cstate,cstate',cstate_type,cpvar,ht,htc,cT) = (*compute concrete stuff in case this is building abstract ks*) 195 if isSome abs_fun 196 then let val (aftb,cT,cstate,cstate') = valOf abs_fun 197 val _ = dbgTools.DTM (dpfx^"mw_cstate") cstate(*DBG*) 198 val ht = getTerm aftb 199 val _ = dbgTools.DTM (dpfx^"mw_ht") ht(*DBG*) 200 val cstate_type = type_of cstate 201 val cpvar = mk_var("p",cstate_type --> bool) 202 val htc = rator ht (* name of abs fun *) 203 in (SOME cstate,SOME cstate',SOME cstate_type,SOME cpvar,SOME ht,SOME htc,SOME cT) end 204 else (NONE,NONE,NONE,NONE,NONE,NONE,NONE) 205 val apl = if (Option.isSome apl) then Option.valOf apl 206 else if (Option.isSome abs_fun) 207 then List.map (fn ap => mk_pabs(valOf cstate,ap)) (strip_pair (valOf cstate)) 208 else List.map (fn ap => mk_pabs(state,ap)) (strip_pair state) 209 (*(get_APs(mk_conj(list_mk_conj(List.map snd TS),S0)))*) 210 val _ = List.app (dbgTools.DTM (dpfx^"mw_apl")) apl(*DBG*) 211 val state_type = type_of state 212 val prop_type = if isSome abs_fun then (valOf cstate_type) --> bool else state_type --> bool 213 val (kn,Tnm,Tn,S0nm,S0n) = mk_model_names ksname state_type prop_type 214 val ks_ty = mk_thy_type {Tyop="KS", Thy="ks", Args=[prop_type,state_type]} 215 val avar= mk_var("t",stringLib.string_ty) 216 val _ = dbgTools.DTM (dpfx^"mw_pvar") avar(*DBG*) 217 val _ = profTools.ent (dpfx^"mw_init")(*PRF*) 218 val _ = profTools.bgt (dpfx^"mw_ap")(*PRF*) 219 val KS_ap = List.foldl (fn (e,ac) => list_mk_comb (inst [alpha|->prop_type] pred_setSyntax.insert_tm,[e,ac])) 220 (inst [alpha|->prop_type] pred_setSyntax.empty_tm) apl 221 val _ = profTools.ent (dpfx^"mw_ap")(*PRF*) 222 val KS_states = inst [alpha|->state_type] pred_setSyntax.univ_tm 223 val KS_initstates = S0 224 val _ = profTools.bgt (dpfx^"mw_L")(*PRF*) 225 val pvar = mk_var("p",prop_type) 226 val _ = dbgTools.DTM (dpfx^"mw_pvar") pvar(*DBG*) 227 val KS_valids = if (isSome abs_fun) 228 then let val (cv,cs,ht) = (valOf cpvar,valOf cstate,valOf ht) 229 in list_mk_pabs([state,cv],list_mk_exists(strip_pair cs,mk_conj(ht,mk_comb(cv,cs)))) end 230 else list_mk_pabs([state,pvar],mk_comb(pvar,state)) 231 val _ = profTools.ent (dpfx^"mw_L")(*PRF*) 232 val _ = dbgTools.DTM (dpfx^"mw_KS_valids") KS_valids(*DBG*) 233 val _ = profTools.bgt (dpfx^"mw_df_i")(*PRF*) 234 val KS_init_def = hd(Defn.eqns_of(Hol_defn (S0n) `^(mk_eq(mk_comb(S0nm,state),KS_initstates))`)) 235 val _ = profTools.ent (dpfx^"mw_df_i")(*PRF*) 236 val _ = dbgTools.DTH (dpfx^"mw_KS_init_def") KS_init_def (*DBG*) 237 val _ = profTools.bgt (dpfx^"mw_T")(*PRF*) 238 val Rvar = mk_var("R",(mk_prod(state_type,state_type)) --> bool) 239 val TS = (".",if Ric then list_mk_conj (snd(unzip TS)) 240 else list_mk_disj (snd(unzip TS)))::TS (*add wildcard action *) 241 val KS_trans = if isSome abs_fun 242 then let val (cs,cs') = (valOf cstate,valOf cstate') 243 in list_mk_pabs([avar,mk_pair(state,state')], 244 list_mk_pexists([cs,cs'], 245 list_mk_conj [list_mk_comb(valOf cT,[avar,mk_pair(cs,cs')]), 246 mk_comb(valOf htc,mk_pair(cs,state)), 247 mk_comb(valOf htc,mk_pair(cs',state'))])) end 248 else mk_tree (SOME (mk_pair(state,state'))) TS 249 val _ = profTools.ent (dpfx^"mw_T")(*PRF*) 250 val _ = dbgTools.DTM (dpfx^"mw_KS_trans") KS_trans(*DBG*) 251 val _ = profTools.bgt (dpfx^"mw_df_t")(*PRF*) 252 val KS_trans_def =hd(Defn.eqns_of(Hol_defn(Tn) 253 `^(mk_eq(list_mk_comb(Tnm,[avar,mk_pair(state,state')]),pbody(body KS_trans)))`)) 254 val _ = profTools.ent (dpfx^"mw_df_t")(*PRF*) 255 val _ = dbgTools.DTH (dpfx^"mw_KS_trans_def") KS_trans_def (*DBG*) 256 (* skip M.ap for abstracted M since cearTheory.ABS_KS_def does not define M.ap *) 257 (* FIXME: since aks.ap is simply the set of abstract state variables, we could pass it in to ABS_KS_def *) 258 val _ = profTools.bgt (dpfx^"mw_df_k")(*PRF*) 259 val ks_def = if (isSome abs_fun) 260 then mk_adf kn (mk_ks state_type prop_type ks_ty KS_states (mk_pabs(state,KS_initstates)) 261 KS_trans NONE KS_valids) 262 else mk_adf kn (mk_ks state_type prop_type ks_ty KS_states 263 (rator (lhs (snd(strip_forall(concl KS_init_def))))) 264 (rator (rator (lhs (snd (strip_forall(concl KS_trans_def)))))) 265 (SOME KS_ap) KS_valids) 266 val _ = profTools.ent (dpfx^"mw_df_k")(*PRF*) 267 val ksnm = lhs(concl ks_def) 268 val _ = profTools.bgt (dpfx^"mw_pw")(*PRF*) 269 val wfKS_ks = prove_wfKS ks_def 270 val _ = profTools.ent (dpfx^"mw_pw")(*PRF*) 271 val ITdf = if isSome abs_fun then NONE else SOME (SPEC_ALL KS_init_def,SPEC_ALL KS_trans_def) 272 val _ = profTools.ent (dpfx^"mw")(*PRF*) 273 val _ = dbgTools.DEX dpfx "mw" (*DBG*) 274 in (apl,ks_def,wfKS_ks,ITdf,KS_trans_def,state',avar) end 275 276fun mk_wfKS S0 TS RTm state vm Ric apl abs_fun ksname = 277 let 278 val (apl,ks_def,wfKS_ks,ITdf,KS_trans_def,state',avar) = mk_formal_KS S0 TS state Ric apl abs_fun ksname 279 val RTm = if Option.isSome RTm then Option.valOf RTm else RmakeTmap KS_trans_def TS vm Ric state state' avar 280 in (apl,ks_def,wfKS_ks,RTm,ITdf) end 281 282(* construct state var tuple from I and T*) 283fun mk_state S0 (TS:(string * term) list) = 284 let val R1 = list_mk_conj (List.map snd TS) (* whether conj or disj doesn't matter for our purposes here *) 285 val vars = (free_vars S0) @ (free_vars R1) 286 val (st1',st1) = List.partition (fn v => is_prime v) 287 (Binaryset.listItems(Binaryset.addList(Binaryset.empty Term.compare,vars))) 288 val sts = Binaryset.addList(Binaryset.empty Term.compare,st1) 289 val st2 = List.foldl (fn (v,l) => if (Binaryset.member(sts,unprime v)) then l else (unprime v)::l) [] st1' 290 val st = st1@st2 291 val state = list_mk_pair st 292 in state end 293 294(* this does not require or create BDD's. Mainly for experimenting with ideas on combining mc and tp *) 295fun auto_mk_formal_ks S0 TS Ric apl ksname = 296 let val state = mk_state S0 TS 297 in mk_formal_KS S0 TS state Ric apl NONE ksname end 298 299val getT = rand o rand o rator o rand o rand 300 301val getS0 = rand o rand o rator o rand 302 303fun getL tm = (rand o rand o rator o rand o rand o rand o rand) tm 304 handle ex => (rand o rand o rator o rand o rand o rand) tm (* in case there is no ap *) 305 306(* S0_CONV conv will apply conv to the S0 part of the ks *) 307val S0_CONV = (RAND_CONV o RATOR_CONV o RAND_CONV o RAND_CONV) 308 309(* T_CONV conv will apply conv to the T part of the ks *) 310val T_CONV = (RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV o RAND_CONV) 311 312(* prove that the set of all boolean tuples of size k is finite *) 313fun BOOLVEC_UNIV_FINITE_CONV k = 314if k = 0 then FINITE_EMPTY 315else if k = 1 then BOOL_UNIV_FINITE 316else let val th2 = BOOLVEC_UNIV_FINITE_CONV (k-1) 317 val u1 = inst [alpha |-> bool ] pred_setSyntax.univ_tm 318 val ty = (hd(snd(dest_type(type_of(snd(dest_comb(concl th2))))))) 319 val u2 = inst [alpha |-> ty ] pred_setSyntax.univ_tm 320 val ucuth = INST_TYPE [alpha |-> ty] UNIV_CROSS_UNIV 321 val fcth = ISPECL [u1,u2] FINITE_CROSS 322in ONCE_REWRITE_RULE [ucuth] (MP fcth (LIST_CONJ [BOOL_UNIV_FINITE,th2])) end 323 324fun empty_ks p_ty s_ty = 325 let val ks_ty = mk_thy_type {Tyop="KS", Thy="ks", Args=[p_ty,s_ty]} 326 in inst [alpha |-> ks_ty] boolSyntax.arb end 327 328fun set_L ks Lv = 329 let val (p_ty,s_ty) = get_types ks 330 val ksLu = inst [alpha |-> s_ty,beta |-> p_ty] ksLu_tm 331 in mk_comb(mk_comb (ksLu,mk_comb(inst [alpha |-> type_of Lv, beta |->type_of Lv] 332 combinSyntax.K_tm,Lv)),ks) end 333 334fun set_ap ks apv = 335 let val (p_ty,s_ty) = get_types ks 336 val ksapu = inst [alpha |-> p_ty,beta |-> s_ty] ksapu_tm 337 in mk_comb(mk_comb (ksapu,mk_comb(inst [alpha |-> type_of apv, beta |->type_of apv] 338 combinSyntax.K_tm,apv)),ks) end 339 340fun mk_ks_dot_ap ks = 341 let val (p_ty,s_ty) = get_types ks 342 val ksap = inst [alpha|->p_ty,beta|->s_ty] ksap_tm 343 in mk_comb(ksap,ks) end 344 345fun mk_ks_dot_L ks = 346 let val (p_ty,s_ty) = get_types ks 347 val ksL = inst [alpha|->p_ty,beta|->s_ty] ksL_tm 348 in mk_comb(ksL,ks) end 349 350fun mk_ks_dot_S0 ks = 351 let val (p_ty,s_ty) = get_types ks 352 val ksS0 = inst [alpha|->p_ty,beta|->s_ty] ksS0_tm 353 in mk_comb(ksS0,ks) end 354 355fun mk_ks_dot_S ks = 356 let val (p_ty,s_ty) = get_types ks 357 val ksS = inst [alpha|->p_ty,beta|->s_ty] ksS_tm 358 in mk_comb(ksS,ks) end 359 360fun mk_ks_dot_T ks = 361 let val (p_ty,s_ty) = get_types ks 362 val ksT = inst [alpha|->p_ty,beta|->s_ty] ksT_tm 363 in mk_comb(ksT,ks) end 364 365(* called by muCheck.mk_gen_thms *) 366fun mk_Lth ks_def = 367 let val _ = dbgTools.DEN dpfx "ml" (*DBG*) 368 (*val L = ``KS_L:^(ty_antiq(list_mk_fun([type_of ksname,state_type,prop_type],bool)))`` 369 val ksL = mk_comb(L,ksname)*) 370 val ksname = lhs(concl ks_def) 371 val (p_ty,s_ty) = get_types ksname 372 val L = inst [alpha|->p_ty,beta|->s_ty] ksL_tm 373 val ksL = mk_comb(L,ksname) 374 (*val _ = DMSG (TM ksL) dbgkt (*DBG*) 375 val _ = DMSG (TH (REWRITE_CONV [ks_def,KS_accfupds,combinTheory.K_DEF] ksL)) dbgkt (*DBG*)*) 376 val kt = type_of ksL 377 (* FIXME: get rid of the quotations *) 378 val tm = mk_eq(ksL,list_mk_comb(``(\(x:(^(ty_antiq kt))) (y:(^(ty_antiq kt))). x)``, 379 [getL (rhs(concl ks_def)),mk_comb(L,``ARB:(^(ty_antiq(type_of ksname)))``)])) 380 (*val _ = with_flag (show_types,true) (DMSG (TM tm)) dbgkt val _ = DMSG (ST "own term") dbgkt*) 381 (*val res = (REWRITE_CONV [ks_def,KS_accfupds,combinTheory.K_DEF] ksL) 382 val _ = with_flag (show_types,true) (DMSG (TM (concl res))) dbgkt val _ = DMSG (ST "rw term") dbgkt 383 val _ = if (Term.compare(concl res,tm)=EQUAL) then () else Raise Match*) 384 val jf = (fn _ => REWRITE_CONV [ks_def,KS_accfupds,combinTheory.K_DEF] ksL) 385 val res = BETA_RULE (mk_lthm (fn _ => (tm,jf)) jf) 386 val _ = dbgTools.DEX dpfx "ml" (*DBG*) 387 in res end 388 389val ksTupx_tm = ``KS_T_fupd x`` 390 391(* return Tth and dmdth of mk_gen_dmd_thms *) 392fun mk_Tth ks_def ksname msd2 msb2 state' state_type prop_type = 393 let 394 val _ = dbgTools.DEN dpfx "mt" (*DBG*) 395 val ksT = mk_ks_dot_T ksname 396 val jf = (fn _ => PURE_ONCE_REWRITE_RULE 397 [GEN_ALL (hd(tl(CONJUNCTS(SPEC_ALL EQ_CLAUSES))))] 398 (((REWRITE_CONV [ks_def,DB.fetch "ks" "KS_accfupds",combinTheory.K_DEF]) 399 THENC (DEPTH_CONV BETA_CONV) 400 THENC (REWRITE_CONV [])) 401 (mk_eq(ksT,rand((rand((hd(find_terms (can (match_term (inst [alpha|->state_type,beta |-> prop_type] 402 ksTupx_tm))) (rhs(concl(ks_def)))))))))))) 403 val Tth = mk_lthm (fn _ => (mk_eq(ksT,getT (rhs(concl ks_def))),jf)) jf 404 val (dmdth,boxth) = (CONV_RULE (STRIP_QUANT_CONV (RHS_CONV commonTools.lzELIM_TUPLED_QUANT_CONV)) 405 ((CONV_RULE ((STRIP_QUANT_CONV (RHS_CONV (lzGEN_PALPHA_CONV state'))) 406 THENC lzSWAP_PFORALL_CONV)) msd2), 407 CONV_RULE (STRIP_QUANT_CONV (RHS_CONV commonTools.lzELIM_TUPLED_QUANT_CONV)) 408 ((CONV_RULE ((STRIP_QUANT_CONV (RHS_CONV (lzGEN_PALPHA_CONV state'))) 409 THENC lzSWAP_PFORALL_CONV)) msb2)) 410 val _ = dbgTools.DTH (dpfx^"mt_Tth") Tth(*DBG*) 411 val _ = dbgTools.DTH (dpfx^"mt_msd2") msd2(*DBG*) 412 val _ = dbgTools.DTH (dpfx^"mt_dmdth") dmdth(*DBG*) 413 val _ = dbgTools.DTH (dpfx^"mt_msb2") msb2(*DBG*) 414 val _ = dbgTools.DTH (dpfx^"mt_boxth") boxth(*DBG*) 415 val _ = dbgTools.DEX dpfx "mt" (*DBG*) 416 in (Tth,(dmdth,boxth)) end 417 418(*given t of the form \s. P s = \s. Q s, prove t=T or die, where P s and Q s must be completely propositional *) 419fun AP_EQ vm t = 420 let val _ = dbgTools.DEN dpfx "ae" (*DBG*) 421 val (l,r) = dest_eq t 422 val ((ls,lb),(rs,rb)) = (dest_pabs ## dest_pabs)(l,r) 423 val eq = mk_eq(lb,rb) 424 val tb = t2tb vm eq 425 val th1 = PABS ls (BddThmOracle tb) 426 handle ex => (dbgTools.DBD (dpfx^"ae_toe_bdd") (getBdd tb);(*DBG*) 427 dbgTools.DTM (dpfx^"ae_toe_tm") t;(*DBG*) 428 dbgTools.DBD (dpfx^"ae_toe_neg_bdd") (getBdd (BddNot tb));(*DBG*) 429 dbgTools.DEX dpfx "ae" (*DBG*); 430 failwith "AP_EQ failure") 431 val eqth = GEN_ALL (SYM (List.nth(CONJUNCTS (SPEC_ALL EQ_CLAUSES),1))) 432 val th2 = PURE_ONCE_REWRITE_RULE [ISPEC (concl th1) eqth] th1 433 val _ = dbgTools.DEX dpfx "ae" (*DBG*) 434 in th2 end 435 436end 437end 438