1structure reachTools = 2struct 3 4local 5 6open Globals HolKernel Parse 7 8open bossLib pairTheory pred_setTheory pred_setLib stringLib 9 listTheory simpLib pairSyntax pairLib PrimitiveBddRules 10 DerivedBddRules Binarymap PairRules pairTools setLemmasTheory 11 muSyntax muSyntaxTheory muTheory boolSyntax Drule Tactical Conv 12 Rewrite Tactic boolTheory listSyntax stringTheory stringBinTree 13 boolSimps pureSimps listSimps numLib reachTheory bddTools ksTools 14 15fun t2tb vm t = DerivedBddRules.GenTermToTermBdd (!DerivedBddRules.termToTermBddFun) vm t 16 17in 18 19 20fun RiterRep n b = List.app print ["Depth: ", term_to_string n, ", ", Int.toString(bdd.nodecount b), " nodes, ", Real.toString(statecount b), " states\n"]; 21 22fun RiterComputeReachable tbR tbS s sp2s n state state' Rname Iname etqcth = 23 let val tbS2 = BddOp(bdd.Or,tbS, (BddReplace sp2s (BddAppex s (bdd.And,tbR,tbS)))) 24 val rcth = ISPECL [Rname,Iname,n,state] reachTheory.ReachableRecSimp 25 val rcth' = PURE_ONCE_REWRITE_RULE [GEN_PALPHA_CONV state' (snd(dest_disj(rhs(concl rcth))))] rcth 26 val rcth'' = PURE_ONCE_REWRITE_RULE [SPEC n etqcth] rcth' 27 val tbS2' = BddEqMp (SYM rcth'') tbS2 28 val _ = RiterRep n (getBdd tbS) 29 in if (bdd.equal (getBdd tbS) (getBdd tbS2')) 30 then let val eqth = PairRules.PGEN state (BddThmOracle (BddOp(bdd.Biimp,tbS,tbS2'))) 31 val feqth = ISPECL [fst(dest_comb(getTerm tbS)),fst(dest_comb(getTerm tbS2'))] (GSYM FUN_EQ_THM) 32 val eqth2 = REWRITE_RULE [REWRITE_RULE [GEN_PALPHA_CONV state (lhs (concl feqth))] feqth] eqth 33 in BddEqMp (AP_THM (SYM (MATCH_MP (ISPECL [Rname,Iname,n] reachTheory.ReachableFP) eqth2)) state) tbS end 34 else RiterComputeReachable tbR tbS2' s sp2s ``SUC ^n`` state state' Rname Iname etqcth end; 35 36fun computeReachable_aux R1 I1 tbR tbI vm = 37 let val state = rand(lhs(concl(SPEC_ALL I1))) 38 val state' = mk_primed_state state 39 val (s,s') = (strip_pair ## strip_pair) (state,state') 40 val Iname = rator(lhs(concl(SPEC_ALL I1))) 41 val Rname = rator(lhs(concl(SPEC_ALL R1))) 42 val tbI' = BddEqMp (SYM (REWRITE_RULE [I1] (AP_THM (REWRITE_CONV [reachTheory.ReachableRec_def] 43 ``ReachableRec (^Rname) (^Iname) (0:num)``) state))) tbI 44 (*val _ = List.app (print o term_to_string) s*) 45 val lFvLhsR = free_vars(lhs(concl(SPEC_ALL(R1)))) 46 val sp = List.drop(rev(lFvLhsR),length(lFvLhsR) div 2) 47 (*val _ = List.app (print o term_to_string) sp*) 48 val sp2s = ListPair.map (fn (vp,v) => (BddVar true vm vp,BddVar true vm v)) (sp,s) 49 val etqcgl = mk_forall(``n:num``,mk_eq(mk_pexists(state',mk_conj(mk_comb(Rname,mk_pair(state',state)), 50 list_mk_comb(inst [alpha |-> type_of state] ``ReachableRec``,[Rname,Iname,``n:num``,state']))), 51 list_mk_exists(s',mk_conj(mk_comb(Rname,mk_pair(state',state)), 52 list_mk_comb(inst [alpha |-> type_of state] ``ReachableRec``,[Rname,Iname,``n:num``,state']))))) 53 (*val _ = print_term etqcgl 54 val _ = print " h3\n"*) 55 val etqcth = prove(etqcgl,REWRITE_TAC [ELIM_TUPLED_QUANT_CONV (lhs(snd(dest_forall etqcgl)))]) 56 (*val _ = print "h4\n"*) 57 in RiterComputeReachable tbR tbI' s sp2s ``0:num`` state state' Rname Iname etqcth end; 58 59(* ASSERT: R1 and I1 are equational predicate definitions of HOL type thm *) 60fun RcomputeReachable I1 R1 Ric vm = 61 let val tbR = BddEqMp (SYM (SPEC_ALL R1)) (t2tb vm (rhs(concl(SPEC_ALL(R1))))) 62 val tbI = t2tb vm (rhs(concl(SPEC_ALL(I1)))) 63 in computeReachable_aux R1 I1 tbR tbI vm end 64 65(* same as RcomputeReachable but in this case the tb's have already been computed *) 66fun computeReachable R1 I1 tbRl tbI vm Ric = 67let val tbR = if Ric then BddListConj vm (List.map snd tbRl) else BddListDisj vm (List.map snd tbRl) 68in computeReachable_aux R1 I1 (BddEqMp (SYM (SPEC_ALL R1)) tbR) tbI vm end 69 end 70end 71