1structure decompTools = struct 2 3local 4 5open HolKernel Parse boolLib bossLib 6 7(* app load ["bddTools","amba_apb_def","mod16Theory","amba_ahb_def","decompTheory","commonTools","muSyntax","muTheory","muCheck","envTheory"];*) 8open boolSyntax bossLib Ho_Rewrite Tactical Tactic PairRules pairSyntax pred_setTheory 9open bddTools commonTools ksTheory muSyntaxTheory muSyntax decompTheory ksTools muCheck envTheory 10 11in 12 13(* FIXME: this is gross right now because the REPEAT PGEN takes ages. fix it *) 14(* note that s2 is not the state of ks2. That's (s1,s2)*) 15fun prove_ap_ext_ap ks1_def ks2_def s1 s2 = 16 let val ksname1 = lhs(concl ks1_def) 17 val ksname2 = lhs(concl ks2_def) 18 in 19 prove(``!p. p IN (^ksname1).ap ==> ?p'. !s1 s2. p IN (^ksname1).L s1 = p' IN (^ksname2).L (s1,s2)``, 20 REPEAT STRIP_TAC 21 THEN CONV_TAC (QUANT_CONV (LAST_FORALL_CONV (GEN_PALPHA_CONV s2))) 22 THEN CONV_TAC (QUANT_CONV (GEN_PALPHA_CONV s1)) 23 THEN FULL_SIMP_TAC std_ss [KS_accfupds,combinTheory.K_THM,ks1_def,ks2_def] 24 THEN SIMP_TAC std_ss [IN_DEF] 25 THEN POP_ASSUM (MP_TAC o (CONV_RULE IN_FIN_CONV)) 26 THEN PURE_REWRITE_TAC [DISJ_IMP_THM] 27 THEN REPEAT CONJ_TAC 28 THEN DISCH_TAC 29 THEN POP_ASSUM (fn t => SIMP_TAC std_ss [t] THEN EXISTS_TAC (mk_pabs(mk_pair(s1,s2),pbody(rhs (concl t))))) 30 THEN PBETA_TAC 31 THEN REPEAT PGEN_TAC 32 THEN REFL_TAC) 33 end 34 35fun prove_ap_ext_ksL ks_def s = 36 let val ksname = lhs(concl ks_def) 37 in 38 prove(``!p. !s. p IN (^ksname).L s = p s``, 39 SIMP_TAC std_ss [KS_accfupds,combinTheory.K_THM,ks_def,IN_DEF] 40 THEN CONV_TAC (QUANT_CONV (GEN_PALPHA_CONV s)) 41 THEN PBETA_TAC 42 THEN REPEAT PGEN_TAC 43 THEN REFL_TAC) 44 end 45 46fun prove_ap_ext_ksT ks1_def ks2_def s1 s2 ks1_t_def ks2_t_def = 47 let val s1' = ksTools.mk_primed_state s1 48 val s2' = ksTools.mk_primed_state s2 49 val ksname1 = lhs(concl ks1_def) 50 val ksname2 = lhs(concl ks2_def) 51 in 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]) 54 THEN PURE_REWRITE_TAC [KS_TRANSITION_def,KS_accfupds,combinTheory.K_THM, 55 ks1_def,ks2_def,IN_DEF, ks1_t_def,ks2_t_def] 56 THEN SIMP_TAC std_ss [] 57 THEN REPEAT PGEN_TAC 58 THEN ACCEPT_TAC TRUTH) 59 end 60 61(*FIXME: I'm being lazy here by assuming empty environments. Generalise this. *) 62fun prove_ap_ext_e ks1_def ks2_def s1 s2 e1 e2 = 63 let val ksname1 = lhs(concl ks1_def) 64 val ksname2 = lhs(concl ks2_def) 65 in 66 prove(``!Q. !s1 s2. s1 IN ^e1 Q = (s1,s2) IN ^e2 Q``, 67 SIMP_TAC std_ss [NOT_IN_EMPTY,EMPTY_ENV_def]) 68 end 69 70fun prove_ap_ext_sub ks_def s f = 71 let val ksname = lhs(concl ks_def) 72 in 73 prove (``!p. AP p SUBF ^f ==> p IN (^ksname).ap``, 74 SIMP_TAC std_ss (IN_INSERT::ks_def::KS_accfupds::combinTheory.K_DEF:: 75 MU_SUB_def::NNF_def::RVNEG_def::(tsimps ``:'a mu``)) 76 THEN RW_TAC std_ss []) 77 end 78 79(* note that s2 is not the state of ks2. That's (s1,s2)*) 80(* other than that, all the args here are from the stuff returned by ksTools.mk_formal_KS *) 81fun gen_prove_ap_ext ks1_def ks2_def wfks1 wfks2 s1 s2 e1 e2 ks1_t_def ks2_t_def = 82 let val ksname1 = lhs(concl ks1_def) 83 val ksname2 = lhs(concl ks2_def) 84 val apth = prove_ap_ext_ap ks1_def ks2_def s1 s2 85 val ksl1 = prove_ap_ext_ksL ks1_def s1 86 val ksl2 = CONV_RULE (QUANT_CONV ELIM_TUPLED_QUANT_CONV) 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 91 in 92 List.foldl (fn (ass,th) => MATCH_MP th ass) (ISPECL [ksname1,ksname2,s1,s2,e1,e2] AP_EXT_THM) 93 [wfks1,wfks2,ksl1,ksl2,apth,ksTth,eth] 94 end 95 96fun spec_prove_ap_ext gapeth ks1_def s1 f = 97 let val subth = prove_ap_ext_sub ks1_def s1 f 98 val imfth = prove_imf f 99 in (MATCH_MP (MATCH_MP gapeth imfth) subth) end 100 101fun prove_psd_ap ks1_def ks2_def = 102 let val ksname1 = lhs(concl ks1_def) 103 val ksname2 = lhs(concl ks2_def) 104 in prove(``(^ksname1).ap = (^ksname2).ap``,PURE_REWRITE_TAC [KS_accfupds,combinTheory.K_THM,ks1_def,ks2_def] 105 THEN REFL_TAC) 106 end 107 108fun prove_psd_L ks1_def ks2_def = 109 let val ksname1 = lhs(concl ks1_def) 110 val ksname2 = lhs(concl ks2_def) 111 in prove(``(^ksname1).L = (^ksname2).L``,PURE_REWRITE_TAC [KS_accfupds,combinTheory.K_THM,ks1_def,ks2_def] 112 THEN REFL_TAC) 113 end 114 115(* here I am assuming that the rhs of ks1 is just the full rhs of the lifted ks (e.g. apb_h) 116 which is just the lhs of the unlifted ks (talking about the ks_t_def's produced by mk_formal_KS here) 117 and the rhs of ks2 is just the conjunction of the lhs's of the lifted ks and the ks it was composed with (e.g. ahb) 118 so we only rewrite out the defn of ks2_t *) 119(* we also need the defn of the transition system of ks1: ks1T_def, to get ks2_t in lifted rather than unlifted terms 120 note that this ks1T is not the same as the ks1T needed in the ap_ext proof: that was for the unlifted ks (e.g. apb), 121 this is for the lifted ks (e.g. apb_h)*) 122fun prove_psd_T ks1_def ks2_def ks1_t_def ks2_t_def s = 123 let val ksname1 = lhs(concl ks1_def) 124 val ksname2 = lhs(concl ks2_def) 125 val s' = ksTools.mk_primed_state s 126 (*val ks1d = PURE_ONCE_REWRITE_RULE [GSYM ks1T_def] ks1_t_def*) 127 in 128 prove(``!a s s'. (^ksname2).T a (s,s') ==> (^ksname1).T a (s,s')``, 129 CONV_TAC (QUANT_CONV (LAST_FORALL_CONV (GEN_PALPHA_CONV s'))) 130 THEN CONV_TAC (QUANT_CONV (GEN_PALPHA_CONV s)) 131 THEN PURE_REWRITE_TAC [KS_accfupds,combinTheory.K_THM,ks1_def,ks2_def, 132 (*ks1d,*)ks1_t_def,ks2_t_def] 133 THEN PURE_REWRITE_TAC [PURE_ONCE_REWRITE_RULE [combinTheory.I_THM] (hd (get_ss_rewrs boolSimps.LET_ss)), 134 AND1_THM] 135 THEN REPEAT PGEN_TAC 136 THEN ACCEPT_TAC TRUTH) 137 end 138 139(* imfth is an option type in case we already have that |- IMF f 140 the rest we can all get from mk_formal_KS 141 except ks1T_def, which is the TRANS def for ks1 and e1, which is the env *) 142fun gen_prove_par_sync_decomp wfks1 wfks2 ks1_def ks2_def ks1_t_def ks2_t_def s e1 = 143 let val ksname1 = lhs(concl ks1_def) 144 val ksname2 = lhs(concl ks2_def) 145 val apth = prove_psd_ap ks1_def ks2_def 146 val lth = prove_psd_L ks1_def ks2_def 147 val tth = prove_psd_T ks1_def ks2_def ks1_t_def ks2_t_def s 148 in List.foldl (fn (ass,th) => MATCH_MP th ass) (ISPECL [s,e1,ksname1,ksname2] PAR_SYNC_DECOMP) 149 [wfks1,wfks2,apth,lth,tth] 150 end 151 152fun prove_psd_imf imfth f ns_ty = 153 let val th1 = PURE_ONCE_REWRITE_RULE [ISPEC f APEXT_IMF] imfth 154 in INST_TYPE [beta|->ns_ty] th1 end 155 156(* copied from cearTools.mk_abs_cons_mf_thms *) 157fun prove_psd_subf f' = 158let val p_ty = muSyntax.get_prop_type f' 159 val g = inst [alpha|->p_ty] (mk_var("g",mu_ty)) 160 val avar = mk_var("a",stringLib.string_ty) 161 val gl = list_mk_forall([avar,g],mk_neg(list_mk_comb(get_mu_ty_sub_tm p_ty, 162 [mu_dmd avar g,mk_comb(get_mu_ty_nnf_tm p_ty,f')]))) 163 in prove (gl,Induct_on `g` THEN SIMP_TAC std_ss ([AP_EXT_def,(GSYM APEXT_NNF),MU_SUB_def,NNF_def,RVNEG_def] 164 @(tsimps ``:'a mu``))) end 165 166fun spec_prove_par_sync_decomp gpsdth f imfth = 167 let val ps_ty = List.hd(snd(dest_type(get_prop_type f))) (* unlifted state type*) 168 val ns_ty = List.last(snd(dest_type(List.hd(snd(dest_type 169 (get_prop_type (fst (dest_forall (concl gpsdth)))))))))(* lifted type's state's snd comp *) 170 val f' = mk_comb(inst [alpha|->ps_ty,beta|->ns_ty] ``AP_EXT``,f) (* lifted f *) 171 val imfth = prove_psd_imf (if isSome imfth then valOf imfth else prove_imf f) f ns_ty 172 val subth = prove_psd_subf f' 173 in (MATCH_MP (MATCH_MP (ISPEC f' gpsdth) imfth) subth) end 174 175(* decomp generation on full auto: this gives a theorem that says that f holds in M then it holds in M x M', 176 as long as f is universal and well formed *) 177(*FIXME: at the moment only the env=EMPTY_ENV will work here *) 178(*FIXME: at the moment there must be no overlap in the vars of s1 and s2 (I think this can be fixed)*) 179fun mk_gen_par_sync_comp_thm S01 TS1 nm1 S02 TS2 nm2 env = 180 let val s1 = mk_state S01 TS1 181 val s2 = mk_state S02 TS2 182 val sc = mk_pair(s1,s2) (* state of the composed model *) 183 val (ks1_ap,ks1_def,ks1_wf,(*SOME(ks1_s0,ks1_t)*)_,ks1_t_def,ks1_s',ks1_avar) = 184 ksTools.mk_formal_KS S01 TS1 s1 true NONE NONE (SOME nm1) 185 val s1' = ks1_s' 186 val (ks2_ap,ks2_def,ks2_wf,(*SOME(ks2_s0,ks2_t)*)_,ks2_t_def,ks2_s',ks2_avar) = 187 ksTools.mk_formal_KS S01 TS1 sc true NONE NONE (SOME (nm1^"_lift")) 188 val s2' = ks2_s' 189 val gapeth = gen_prove_ap_ext ks1_def ks2_def ks1_wf ks2_wf s1 s2 190 (inst [alpha|->type_of s1] ``\(s:string).{}``) 191 env ks1_t_def ks2_t_def 192 val S0c = mk_conj(S01,S02) 193 val TSc = [(".",mk_conj(snd(hd TS1),snd(hd TS2)))] (*ASSERT: sync, so assume TSi are of the form [(".",ts)] *) 194 val (ksc_ap,ksc_def,ksc_wf,(*SOME(ksc_s0,ksc_t)*)_,ksc_t_def,ksc_s',ksc_avar) = 195 ksTools.mk_formal_KS S0c TSc sc true NONE NONE (SOME (nm1^"_"^nm2)) 196 val sc' = ksc_s' 197 val gpsdth = gen_prove_par_sync_decomp ks2_wf ksc_wf ks2_def ksc_def ks2_t_def ksc_t_def sc env 198 val f = fst (dest_forall (concl gapeth)) 199 val f' = fst (dest_forall (concl gpsdth)) 200 val aef = mk_comb(inst [alpha|->type_of s1,beta|->type_of s2] ``AP_EXT``,f) 201 val sgpsdth = SPEC aef gpsdth 202 val sgapeth = PURE_ONCE_REWRITE_RULE [APEXT_IMF] gapeth 203 val psdl = strip_imp (concl sgpsdth) 204 val apel = strip_imp (snd(dest_forall (concl sgapeth))) 205 val th = prove(list_mk_imp([concl ks1_wf,concl ks2_wf,concl ksc_wf], (* these are needed because of lazy thms*) 206 mk_forall(f,list_mk_imp([hd (fst psdl),List.nth(fst psdl,1),List.nth(fst apel,1)], 207 mk_imp(lhs(snd apel),snd psdl)))),METIS_TAC [gpsdth,gapeth,APEXT_IMF]) 208 val th = PURE_ONCE_REWRITE_RULE [GSYM APEXT_IMF] (List.foldl (fn (ass,th) => MATCH_MP th ass) th 209 [ks1_wf,ks2_wf,ksc_wf]) 210 in (th,ks1_def,s1,s2) end 211 212(* takes the output f mk_gen_par_sync_comp_thm and an f and return thm that says f holds in M x M' *) 213(* FIXME: ideally this should take the thm produced by hc rather than just f, for full auto compositionality 214 but in that case we'll need to fix things so that it uses the ks already generated in the hc model 215 which means this will have to called from with modelTools so it has access to the internal cache *) 216fun mk_par_sync_comp_thm (gpscth,ks1_def,s1,s2) f imfth = 217 let val imfth = if isSome imfth then valOf imfth else prove_imf f 218 val ps_ty = type_of s1 (* unlifted state type*) 219 val ns_ty = type_of s2 (* lifted type's state's snd comp *) 220 val f' = mk_comb(inst [alpha|->ps_ty,beta|->ns_ty] ``AP_EXT``,f) (* lifted f *) 221 val psdsubth = prove_psd_subf f' 222 val apesubth = prove_ap_ext_sub ks1_def s1 f 223 in 224 (List.foldl (fn (ass,th) => MATCH_MP th ass) gpscth [imfth,psdsubth,apesubth]) 225 end 226 227end 228end 229