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