examples/HolCheck/decompTools.sml

14 (* note that s2 is not the state of ks2. That's (s1,s2)*)
15 fun prove_ap_ext_ap ks1_def ks2_def s1 s2 =
19         prove(``!p. p IN (^ksname1).ap ==> ?p'. !s1 s2. p IN (^ksname1).L s1 = p' IN (^ksname2).L (s1,s2)``,
21               THEN CONV_TAC (QUANT_CONV (LAST_FORALL_CONV (GEN_PALPHA_CONV s2)))
29               THEN POP_ASSUM (fn t => SIMP_TAC std_ss [t] THEN EXISTS_TAC (mk_pabs(mk_pair(s1,s2),pbody(rhs (concl t)))))
46 fun prove_ap_ext_ksT ks1_def ks2_def s1 s2 ks1_t_def ks2_t_def =
48         val s2' = ksTools.mk_primed_state s2
52         prove(``!a s1 s1' s2 s2'. s1>--(^ksname1)/a-->s1' = (s1,s2)>--(^ksname2)/a-->(s1',s2')``,
53               EVERY (List.map (fn t => CONV_TAC (LAST_FORALL_CONV (GEN_PALPHA_CONV t))) [s2',s2,s1',s1])
62 fun prove_ap_ext_e ks1_def ks2_def s1 s2 e1 e2 =
66         prove(``!Q. !s1 s2. s1 IN ^e1 Q = (s1,s2) IN ^e2 Q``,
79 (* note that s2 is not the state of ks2. That's (s1,s2)*)
81 fun gen_prove_ap_ext ks1_def ks2_def wfks1 wfks2 s1 s2 e1 e2 ks1_t_def ks2_t_def =
84         val apth = prove_ap_ext_ap ks1_def ks2_def s1 s2
87             (CONV_RULE (QUANT_CONV (GEN_PALPHA_CONV (inst [alpha|->type_of s1,beta|->type_of s2] ``(s1,s2)``)))
88                              (prove_ap_ext_ksL ks2_def (mk_pair(s1,s2))))
89         val ksTth = prove_ap_ext_ksT ks1_def ks2_def s1 s2 ks1_t_def ks2_t_def
90         val eth = prove_ap_ext_e ks1_def ks2_def s1 s2 e1 e2
92       List.foldl (fn (ass,th) => MATCH_MP th ass) (ISPECL [ksname1,ksname2,s1,s2,e1,e2] AP_EXT_THM)
178 (*FIXME: at the moment there must be no overlap in the vars of s1 and s2 (I think this can be fixed)*)
181         val s2 = mk_state S02 TS2
182         val sc = mk_pair(s1,s2) (* state of the composed model *)
188         val s2' = ks2_s'
189         val gapeth = gen_prove_ap_ext ks1_def ks2_def ks1_wf ks2_wf s1 s2
200         val aef = mk_comb(inst [alpha|->type_of s1,beta|->type_of s2] ``AP_EXT``,f)
210     in (th,ks1_def,s1,s2) end
216 fun mk_par_sync_comp_thm (gpscth,ks1_def,s1,s2) f imfth =
219         val ns_ty =  type_of s2 (* lifted type's state's snd comp *)