1153618Sruopen HolKernel Parse boolLib bossLib 2153618Sru 3153618Sruval _ = new_theory("decomp"); 4153618Sru 5153618Sru(* app load ["envTheory","muTheory","muSyntaxTheory","setLemmasTheory","pred_setTheory","ksTheory", 6153618Sru "pairSyntax","metisLib","commonTools"] *) 7153618Sru 8153618Sruopen pairSyntax metisLib 9153618Sruopen envTheory muTheory muSyntaxTheory setLemmasTheory pred_setTheory ksTheory commonTools 10 11infix &&; infix 8 by; 12 13(* NOTE: decompTheory imposes the restriction that prop types are always of the form state_ty --> bool *) 14(* otherwise AP_EXT_THM won't work*) 15 16(*take f:('state1->bool) mu and return f:('state2->bool) mu*) 17(*lesson: we _can_ muck around with types within the object logic, using choice and extensionality*) 18val AP_EXT_def = Define ` 19(AP_EXT (T:('state1->bool) mu) = (T:(('state1#'state2)->bool) mu)) /\ 20(AP_EXT F = F) /\ 21(AP_EXT (~f) = ~(AP_EXT f)) /\ 22(AP_EXT (f1 /\ f2) = (AP_EXT f1) /\ (AP_EXT f2)) /\ 23(AP_EXT (f1 \/ f2) = (AP_EXT f1) \/ (AP_EXT f2)) /\ 24(AP_EXT (RV Q) = (RV Q)) /\ 25(AP_EXT (AP p) = AP (@p'. !(s1:'state1) (s2:'state2). p s1 = p' (s1,s2))) /\ 26(AP_EXT (<<a>> f) = <<a>> (AP_EXT f)) /\ 27(AP_EXT ([[a]] f) = [[a]] (AP_EXT f)) /\ 28(AP_EXT (mu Q.. f) = (mu Q.. (AP_EXT f))) /\ 29(AP_EXT (nu Q.. f) = (nu Q.. (AP_EXT f)))`; 30 31 32val APEXT_RV = prove(``!f Q. (RV Q = AP_EXT f) = (f = RV Q)``, 33Induct_on `f` THEN FULL_SIMP_TAC std_ss ([AP_EXT_def,MU_SUB_def]@(tsimps ``:'a mu``)) THEN PROVE_TAC []) 34 35val APEXT_RV_SUBF = prove(``!f (Q:string). ~RV Q SUBF f = ~RV Q SUBF (AP_EXT f)``, 36Induct_on `f` THEN FULL_SIMP_TAC std_ss ([AP_EXT_def,MU_SUB_def]@(tsimps ``:'a mu``)) 37THEN METIS_TAC [APEXT_RV]) 38 39val APEXT_RVNEG = prove( 40 ``!f Q. AP_EXT (RVNEG Q f) = RVNEG Q (AP_EXT f)``, 41 Induct_on `f` THEN 42 FULL_SIMP_TAC std_ss ([AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)) THENL [ 43 MAP_EVERY Q.X_GEN_TAC [`s`, `Q`] THEN Cases_on `Q=s` THENL [ 44 FULL_SIMP_TAC std_ss ([AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)), 45 METIS_TAC [APEXT_RV] 46 ], 47 MAP_EVERY Q.X_GEN_TAC [`s`, `Q`] THEN Cases_on `Q=s` THEN 48 FULL_SIMP_TAC std_ss ([AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)), 49 MAP_EVERY Q.X_GEN_TAC [`s`, `Q`] THEN Cases_on `Q=s` THEN 50 FULL_SIMP_TAC std_ss ([AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)) 51 ]); 52 53val APEXT_NNF = save_thm("APEXT_NNF",prove(``!f. AP_EXT (NNF f) = NNF (AP_EXT f)``, 54recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC 55THEN RW_TAC std_ss ([MU_SUB_def,NNF_def,RVNEG_def,AP_EXT_def]@(tsimps ``:'a mu``)) 56THEN FULL_SIMP_TAC std_ss ([APEXT_RVNEG,AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)))) 57 58val APEXT_IMF = save_thm("APEXT_IMF",prove(``!f. IMF f = IMF (AP_EXT f)``, 59recInduct NNF_IND_def THEN REPEAT CONJ_TAC THEN BETA_TAC 60THEN RW_TAC std_ss ([IMF_def,MU_SUB_def,NNF_def,RVNEG_def,AP_EXT_def]@(tsimps ``:'a mu``)) THENL [ 61 METIS_TAC ([APEXT_NNF,APEXT_RV_SUBF,AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)), 62 METIS_TAC ([APEXT_NNF,APEXT_RV_SUBF,AP_EXT_def,RVNEG_def]@(tsimps ``:'a mu``)), 63 REWRITE_TAC [GSYM APEXT_NNF,GSYM APEXT_RV_SUBF] 64 THEN METIS_TAC [APEXT_RVNEG,IMF_INV_RVNEG], 65 REWRITE_TAC [GSYM APEXT_NNF,GSYM APEXT_RV_SUBF] 66 THEN METIS_TAC [APEXT_RVNEG,IMF_INV_RVNEG] 67])) 68 69val pair_rwts = BasicProvers.thy_ssfrag "pair" 70 71(* gen ap extension proof *) 72(* basic idea is that if f holds in some model then it should hold in the same model with extra ap's thrown in, 73 where the new ap's may possibly introduce new state vars*) 74(* note: the assumptions on L and T are very strong only because ks1 and ks2 are more or less the same 75 so these assumptions can be discharged for the cases for which AP_EXT is intended to be used 76 i.e. when ks1 and ks2 are different only in ap, and all the ap in f are in ap1 and ap1 SUBSET ap2 77 noting that all ap must have the same semantics *) 78(* since all the ap's type changes if new state vars are introduced, we have to resort to a little trickery (via AP_EXT) 79 to "lift" f to the new ap type that has extra state vars *) 80(* ASSERT: note also that this only works if the L are defined as \s p. p s; the 3rd and 4th assums *) 81val AP_EXT_THM = store_thm( 82 "AP_EXT_THM", 83 ``!ks1 ks2 s1 s2 e1 e2 f. 84 wfKS ks1 ==> wfKS ks2 ==> 85 (!p s1. p IN ks1.L s1 = p s1) ==> 86 (!p s1 s2. p IN ks2.L (s1,s2) = p (s1,s2)) ==> 87 (!p. p IN ks1.ap ==> 88 ?p'. !s1 s2. p IN ks1.L s1 = p' IN ks2.L (s1,s2)) ==> 89 (!a s1 s1' s2 s2'. s1>--ks1/a-->s1' = (s1,s2)>--ks2/a-->(s1',s2')) ==> 90 (!Q s1 s2. s1 IN e1 Q = (s1,s2) IN e2 Q) ==> 91 IMF f ==> 92 (!p. AP p SUBF f ==> p IN ks1.ap) 93 ==> 94 (s1 IN STATES f ks1 e1 = (s1,s2) IN STATES (AP_EXT f) ks2 e2)``, 95 Induct_on `f` THEN REPEAT CONJ_TAC THENL [ 96 SIMP_TAC std_ss [STATES_def,IN_UNIV,wfKS_def,AP_EXT_def], (* T *) 97 SIMP_TAC std_ss [STATES_def, NOT_IN_EMPTY,AP_EXT_def], (* F *) 98 RW_TAC std_ss [STATES_def,DIFF_DEF,SET_SPEC,IN_UNIV,AP_EXT_def] 99 THEN FULL_SIMP_TAC std_ss [IMF_def,SUB_AP_NEG] 100 THEN RES_TAC 101 THEN FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV], (* ~ *) 102 RW_TAC std_ss [STATES_def,INTER_DEF,SET_SPEC,AP_EXT_def] 103 THEN FULL_SIMP_TAC std_ss [SUB_AP_CONJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 104 THEN RES_TAC 105 THEN FULL_SIMP_TAC std_ss [] 106 THEN METIS_TAC [AP_EXT_def], (* /\ *) 107 RW_TAC std_ss [STATES_def,UNION_DEF,SET_SPEC,AP_EXT_def] 108 THEN FULL_SIMP_TAC std_ss [SUB_AP_DISJ,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 109 THEN RES_TAC 110 THEN FULL_SIMP_TAC std_ss [] 111 THEN METIS_TAC [AP_EXT_def], (* \/ *) 112 113 RW_TAC std_ss [STATES_def,SET_SPEC,IN_UNIV,wfKS_def,AP_EXT_def] 114 THEN FULL_SIMP_TAC std_ss [IN_DEF], (* RV *) 115 116 RW_TAC std_ss [STATES_def,SET_SPEC,IN_UNIV,wfKS_def,AP_EXT_def] 117 THEN FULL_SIMP_TAC std_ss (MU_SUB_def::(tsimps ``:'a mu``)) 118 THEN SELECT_ELIM_TAC 119 THEN PROVE_TAC [], (* AP *) 120 121 RW_TAC std_ss [STATES_def,SET_SPEC,IN_UNIV,AP_EXT_def] 122 THEN CONV_TAC (FORK_CONV(QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)), 123 QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)))) 124 THEN FULL_SIMP_TAC std_ss [SUB_AP_DMD,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 125 THEN EQ_TAC THENL [ 126 REPEAT STRIP_TAC 127 THEN RES_TAC 128 THEN Q.EXISTS_TAC `(q,s2)` 129 THEN FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV], 130 REPEAT STRIP_TAC 131 THEN RES_TAC 132 THEN Q.EXISTS_TAC `FST q` 133 THEN METIS_TAC ([wfKS_def,IN_UNIV]@(get_ss_rewrs pair_rwts)) 134 ], (* <> *) 135 136 RW_TAC std_ss [STATES_def,SET_SPEC,IN_UNIV,AP_EXT_def] 137 THEN CONV_TAC (FORK_CONV(QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)), 138 QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)))) 139 THEN FULL_SIMP_TAC std_ss [SUB_AP_BOX,IMF_def,FORALL_AND_THM,DISJ_IMP_THM] 140 THEN EQ_TAC THENL [ 141 REPEAT STRIP_TAC THENL [ 142 FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV], 143 RES_TAC THEN METIS_TAC (get_ss_rewrs pair_rwts) 144 ], 145 REPEAT STRIP_TAC THENL [ 146 FULL_SIMP_TAC std_ss [wfKS_def,IN_UNIV], 147 RES_TAC THEN METIS_TAC (get_ss_rewrs pair_rwts) 148 ] 149 ],(* [] *) 150 151 Q.X_GEN_TAC `s` THEN SIMP_TAC std_ss [STATES_def,SET_SPEC,AP_EXT_def] 152 THEN REPEAT STRIP_TAC 153 THEN FULL_SIMP_TAC std_ss [SUB_AP_MU,IMF_def,STATES_def,SET_SPEC] 154 THEN Q.SUBGOAL_THEN `!n s1 s2. s1 IN FP f s ks1 e1[[[s<--{}]]] n = (s1,s2) IN FP (AP_EXT f) s ks2 e2[[[s<--{}]]] n` ASSUME_TAC 155 THENL [ 156 Induct_on `n` THENL [ 157 RW_TAC std_ss [STATES_def,ENV_EVAL,NOT_IN_EMPTY], (* 0 *) 158 REPEAT GEN_TAC 159 THEN REWRITE_TAC [STATES_def,ENV_UPDATE] 160 THEN (Q.PAT_ASSUM `!q1 q2 q3 q4 q5 q6. t` (fn t => ASSUME_TAC (Q.SPECL [`ks1`,`ks2`,`s1`,`s2`,`e1[[[s <-- FP (f:('a -> bool) mu) s ks1 e1[[[s<--{}]]] n]]]`, `e2[[[s<--FP (AP_EXT (f:('a -> bool) mu)) s (ks2 :('a#'b -> bool,'a#'b) KS) e2[[[s<--{}]]] n]]]`] t))) 161 THEN RES_TAC 162 THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) 163 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN SUBGOAL_THEN (fst(dest_imp(concl t))) ASSUME_TAC) THENL [ 164 NTAC 2 (POP_ASSUM (K ALL_TAC)) 165 THEN REPEAT GEN_TAC 166 THEN POP_ASSUM_LIST (MAP_EVERY (fn t => ASSUME_TAC (SPEC_ALL t))) 167 THEN Cases_on `Q=s` THENL [ 168 FULL_SIMP_TAC std_ss [ENV_EVAL], 169 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] 170 ], 171 FULL_SIMP_TAC std_ss [IMF_def] 172 ] 173 ], 174 POP_ASSUM (fn t => METIS_TAC [t]) 175 ], (* mu *) 176 177 Q.X_GEN_TAC `s` THEN 178 SIMP_TAC std_ss [STATES_def,SET_SPEC,AP_EXT_def] 179 THEN REPEAT STRIP_TAC 180 THEN FULL_SIMP_TAC std_ss [SUB_AP_NU,IMF_def] 181 THEN Q.SUBGOAL_THEN `!n s1 s2. s1 IN FP f s ks1 e1[[[s<--ks1.S]]] n = (s1,s2) IN FP (AP_EXT f) s ks2 e2[[[s<--ks2.S]]] n` ASSUME_TAC THENL [ 182 Induct_on `n` THENL [ 183 FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,IN_UNIV,wfKS_def], (* 0 *) 184 REPEAT GEN_TAC 185 THEN REWRITE_TAC [STATES_def,ENV_UPDATE] 186 THEN (Q.PAT_ASSUM `!q1 q2 q3 q4 q5 q6. t` (fn t => ASSUME_TAC (Q.SPECL [`ks1`,`ks2`,`s1`,`s2`,`e1[[[s <-- FP (f:('a -> bool) mu) s ks1 e1[[[s<--ks1.S]]] n]]]`, `e2[[[s<--FP (AP_EXT (f:('a -> bool) mu)) s (ks2 :('a#'b -> bool,'a#'b) KS) e2[[[s<--ks2.S]]] n]]]`] t))) 187 THEN RES_TAC 188 THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) 189 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN SUBGOAL_THEN (fst(dest_imp(concl t))) ASSUME_TAC) THENL [ 190 NTAC 2 (POP_ASSUM (K ALL_TAC)) 191 THEN REPEAT GEN_TAC 192 THEN POP_ASSUM_LIST (MAP_EVERY (fn t => ASSUME_TAC (SPEC_ALL t))) 193 THEN Cases_on `Q=s` THENL [ 194 FULL_SIMP_TAC std_ss [ENV_EVAL], 195 FULL_SIMP_TAC std_ss [ENV_UPDATE_INV] 196 ], 197 FULL_SIMP_TAC std_ss [IMF_def] 198 ] 199 ], 200 POP_ASSUM (fn t => METIS_TAC [t]) 201 ] (* nu *) 202 ]) 203 204val lem3a = REWRITE_RULE [GSYM IMF_MU_NNF] (ISPECL [``ks:('prop,'state) KS``,``(NNF f):'prop mu``,``e:string->'state->bool``,``Y:'state->bool``,``X:'state->bool``,``Q:string``] (REWRITE_RULE [SUBSET_DEF] (GEN_ALL (SIMP_RULE std_ss [] (REWRITE_RULE [SUBSET_REFL] (ISPECL [``f:'prop mu``,``ks:('prop,'state) KS``,``e:string -> 'state -> bool``,``e:string -> 'state -> bool``,``Q:string``,``X:'state->bool``,``Y:'state->bool``] STATES_MONO)))))); 205 206(* gen decomp proof *) 207(* this is bascially that a universal property holding in M holds in M||M', where || is parallel synchronous composition, 208 assuming that whenever M||M' can do an action, M can as well *) 209val DECOMP = SIMP_RULE std_ss [STATES_NNF_ID] (prove( 210list_mk_pforall ([``(f:'prop mu)``,``s:'state``,``(e:string -> 'state -> bool)``,``Q:string``,``ks1:('prop,'state) KS``,``ks2:('prop,'state) KS``], 211list_mk_imp([ 212``IMF mu (Q:string) .. (f:'prop mu)``, 213``!a g. ~SUBFORMULA (<<a>> g) (NNF (f:'prop mu))``, 214``wfKS (ks1:('prop,'state) KS)``, 215``wfKS (ks2:('prop,'state) KS)``, 216``(ks1:('prop,'state) KS).ap=(ks2:('prop,'state) KS).ap``, 217``(ks1:('prop,'state) KS).L=(ks2:('prop,'state) KS).L``, 218``!a s s'. ((ks2:('prop,'state) KS).T a)(s,s') ==> ((ks1:('prop,'state) KS).T a)(s,s')``], 219``s IN STATES (NNF (f:'prop mu)) (ks1:('prop,'state) KS) e ==> s IN STATES (NNF f) (ks2:('prop,'state) KS) e``)), 220recInduct NNF_IND_def THEN REPEAT CONJ_TAC THENL [ 221 SIMP_TAC std_ss [NNF_def,STATES_def,wfKS_def,IN_UNIV], (* T *) 222 SIMP_TAC std_ss [NNF_def,STATES_def], (* F *) 223 RW_TAC std_ss [NNF_def,SUB_DMD_CONJ,IMF_MU_CONJ,STATES_def,INTER_DEF, 224 SET_SPEC] THEN PROVE_TAC [], (* /\ *) 225 226 RW_TAC std_ss [NNF_def,SUB_DMD_DISJ,IMF_MU_DISJ,STATES_def,UNION_DEF, 227 SET_SPEC] 228 THENL [ 229 DISJ1_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASSUM_LIST PROVE_TAC, 230 DISJ2_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASSUM_LIST PROVE_TAC 231 ], (* \/ *) 232 233 RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,IN_UNIV,wfKS_def], (* AP *) 234 RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,IN_UNIV,wfKS_def], (* RV *) 235 236 SIMP_TAC std_ss [NNF_def,SUB_DMD_DMD], (* <> *) 237 238 FULL_SIMP_TAC std_ss [NNF_def,SUB_DMD_BOX,IMF_MU_BOX,STATES_def,SET_SPEC, 239 IN_UNIV,wfKS_def] THEN 240 NTAC 15 STRIP_TAC THEN 241 CONV_TAC (FORK_CONV 242 (QUANT_CONV 243 (FORK_CONV 244 (REWRITE_CONV [KS_TRANSITION_def,KS_accfupds, 245 combinTheory.K_DEF], 246 ALL_CONV)), 247 QUANT_CONV 248 (FORK_CONV 249 (REWRITE_CONV [KS_TRANSITION_def,KS_accfupds, 250 combinTheory.K_DEF], 251 ALL_CONV)))) THEN 252 REPEAT STRIP_TAC THEN RES_TAC THEN PROVE_TAC [], (* [] *) 253 254 SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 255 THEN NTAC 15 STRIP_TAC 256 THEN IMP_RES_TAC IMF_MU_MU 257 THEN FULL_SIMP_TAC std_ss [SUB_DMD_MU] 258 THEN RES_TAC 259 THEN (SUBGOAL_THEN (mk_forall(``n:num``,list_mk_forall([``s:'state``],mk_imp(``s IN FP (NNF f) Q (ks1:('prop,'state) KS) e[[[Q<--{}]]] n``,``s IN FP (NNF f) Q (ks2:('prop,'state) KS) e[[[Q<--{}]]] n``)))) ASSUME_TAC) THENL [ 260 Induct_on `n` THENL [ 261 SIMP_TAC std_ss [STATES_def,ENV_EVAL], 262 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 263 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 264 THEN SPEC_TAC (``FP (NNF f) Q (ks1:('prop,'state) KS) e[[[Q<--{}]]] n``,``X:'state -> bool``) 265 THEN SPEC_TAC (``FP (NNF f) Q (ks2:('prop,'state) KS)e[[[Q<--{}]]] n``,``Y:'state->bool``) 266 THEN REPEAT GEN_TAC 267 THEN STRIP_TAC 268 THEN IMP_RES_TAC lem3a 269 THEN FULL_SIMP_TAC std_ss [] 270 ], 271 ASSUM_LIST PROVE_TAC 272 ], (* mu *) 273 274 SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 275 THEN NTAC 15 STRIP_TAC 276 THEN IMP_RES_TAC IMF_MU_NU 277 THEN FULL_SIMP_TAC std_ss [SUB_DMD_NU] 278 THEN RES_TAC 279 THEN (SUBGOAL_THEN (mk_forall(``n:num``,mk_forall(``s:'state``,mk_imp(``s IN FP (NNF f) Q (ks1:('prop,'state) KS) e[[[Q<--ks1.S]]] n``,``s IN FP (NNF f) Q (ks2:('prop,'state) KS) e[[[Q<--ks2.S]]] n``)))) ASSUME_TAC) THENL [ 280 Induct_on `n` THENL [ 281 SIMP_TAC std_ss [STATES_def,ENV_EVAL] 282 THEN FULL_SIMP_TAC std_ss [wfKS_def], 283 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 284 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 285 THEN SPEC_TAC (``FP (NNF f) Q (ks1:('prop,'state) KS) e[[[Q<--ks1.S]]] n``,``X:'state -> bool``) 286 THEN SPEC_TAC (``FP (NNF f) Q (ks2:('prop,'state) KS) e[[[Q<--ks2.S]]] n``,``Y:'state ->bool``) 287 THEN REPEAT GEN_TAC 288 THEN STRIP_TAC 289 THEN IMP_RES_TAC lem3a 290 THEN FULL_SIMP_TAC std_ss [] 291 ], 292 ASSUM_LIST PROVE_TAC 293 ], (* nu *) 294 295 SIMP_TAC std_ss [NNF_def,STATES_def], (* ~T *) 296 SIMP_TAC std_ss [NNF_def,STATES_def,wfKS_def,IN_UNIV], (* ~F *) 297 298 RW_TAC std_ss [NNF_def,SUB_DMD_DISJ,IMF_MU_NEG_CONJ,STATES_def,UNION_DEF, 299 SET_SPEC] 300 THENL [ 301 DISJ1_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASSUM_LIST PROVE_TAC, 302 DISJ2_TAC THEN FULL_SIMP_TAC std_ss [] THEN ASSUM_LIST PROVE_TAC 303 ], (* ~/\ *) 304 305 RW_TAC std_ss [NNF_def,SUB_DMD_CONJ,IMF_MU_NEG_DISJ,STATES_def,INTER_DEF, 306 SET_SPEC] THEN PROVE_TAC [], (* ~\/ *) 307 308 RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,IN_UNIV,wfKS_def], (* ~AP *) 309 RW_TAC std_ss [NNF_def,STATES_def,SET_SPEC,IN_UNIV,wfKS_def], (* ~RV *) 310 311FULL_SIMP_TAC std_ss [NNF_def,STATES_def,IMF_MU_NEG_DMD,SET_SPEC,IN_UNIV,wfKS_def] 312THEN NTAC 15 STRIP_TAC 313THEN CONV_TAC (FORK_CONV(QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)), 314 QUANT_CONV (FORK_CONV(REWRITE_CONV [KS_TRANSITION_def,KS_accfupds,combinTheory.K_DEF],ALL_CONV)))) 315THEN REPEAT STRIP_TAC 316THEN FULL_SIMP_TAC std_ss [SUB_DMD_BOX] 317THEN RES_TAC 318THEN ASSUM_LIST PROVE_TAC, (* ~<>*) 319SIMP_TAC std_ss [NNF_def,SUB_DMD_DMD], (* ~[] *) 320SIMP_TAC std_ss [NNF_def,SUB_DMD_NEG_NEG,IMF_MU_NEG_NEG], (* ~~ *) 321SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 322THEN NTAC 15 STRIP_TAC 323THEN IMP_RES_TAC IMF_MU_NEG_MU 324THEN FULL_SIMP_TAC std_ss [SUB_DMD_NU] 325THEN POP_ASSUM (fn t => ASSUME_TAC (ONCE_REWRITE_RULE [IMF_MU_INV_RVNEG] t)) 326THEN RES_TAC 327THEN (SUBGOAL_THEN (mk_forall(``n:num``,mk_forall(``s:'state``,mk_imp(``s IN FP (NNF (RVNEG Q ~f)) Q (ks1:('prop,'state) KS) e[[[Q<--ks1.S]]] n``,``s IN FP (NNF (RVNEG Q ~f)) Q (ks2:('prop,'state) KS) e[[[Q<--ks2.S]]] n``)))) ASSUME_TAC) THENL [ 328 Induct_on `n` THENL [ 329 FULL_SIMP_TAC std_ss [STATES_def,ENV_EVAL,wfKS_def], 330 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 331 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 332 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks1:('prop,'state) KS) e[[[Q<--ks1.S]]] n``,``X:'state -> bool``) 333 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks2:('prop,'state) KS) e[[[Q<--ks2.S]]] n``,``Y:'state->bool``) 334 THEN REPEAT GEN_TAC 335 THEN STRIP_TAC 336 THEN IMP_RES_TAC lem3a 337 THEN FULL_SIMP_TAC std_ss [] 338 ], 339 ASSUM_LIST PROVE_TAC 340 ], (* ~mu *) 341SIMP_TAC std_ss [STATES_def,NNF_def,SET_SPEC] 342THEN NTAC 15 STRIP_TAC 343THEN IMP_RES_TAC IMF_MU_NEG_NU 344THEN FULL_SIMP_TAC std_ss [SUB_DMD_MU] 345THEN POP_ASSUM (fn t => ASSUME_TAC (ONCE_REWRITE_RULE [IMF_MU_INV_RVNEG] t)) 346THEN RES_TAC 347THEN (SUBGOAL_THEN (mk_forall(``n:num``,mk_forall(``s:'state``,mk_imp(``s IN FP (NNF (RVNEG Q ~f)) Q (ks1:('prop,'state) KS) e[[[Q<--{}]]] n``,``s IN FP (NNF (RVNEG Q ~f)) Q (ks2:('prop,'state) KS) e[[[Q<--{}]]] n``)))) ASSUME_TAC) THENL [ 348 Induct_on `n` THENL [ 349 SIMP_TAC std_ss [STATES_def,ENV_EVAL], 350 SIMP_TAC std_ss [STATES_def,ENV_UPDATE] 351 THEN POP_ASSUM (fn t => ASSUME_TAC t THEN UNDISCH_TAC (concl t)) 352 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks1:('prop,'state) KS) e[[[Q<--{}]]] n``,``X:'state -> bool``) 353 THEN SPEC_TAC (``FP (NNF (RVNEG Q ~f)) Q (ks2:('prop,'state) KS) e[[[Q<--{}]]] n``,``Y:'state ->bool``) 354 THEN REPEAT GEN_TAC 355 THEN STRIP_TAC 356 THEN IMP_RES_TAC lem3a 357 THEN FULL_SIMP_TAC std_ss [] 358 ], 359 ASSUM_LIST PROVE_TAC 360 ] (* ~nu*) 361])); 362 363val DECOMP2 = 364 CONV_RULE (STRIP_QUANT_CONV (PUSHN_IMP_CONV 6)) 365(CONV_RULE (STRIP_QUANT_CONV (PUSHN_IMP_CONV 6)) 366(CONV_RULE (PUSH_QUANT_CONV SWAP_VARS_CONV 4) 367(CONV_RULE (LAST_FORALL_CONV FORALL_IMP_CONV) 368(CONV_RULE (QUANT_CONV (QUANT_CONV (QUANT_CONV (PUSH_QUANT_CONV SWAP_VARS_CONV 2)))) DECOMP)))) 369 370val DECOMP3 = save_thm("PAR_SYNC_DECOMP", prove(``!s e ks1 ks2 f. 371 wfKS ks1 ==> 372 wfKS ks2 ==> 373 (ks1.ap = ks2.ap) ==> 374 (ks1.L = ks2.L) ==> 375 (!a s s'. ks2.T a (s,s') ==> ks1.T a (s,s')) ==> 376 (IMF f) ==> 377 (!a g. ~(<<a>> g SUBF NNF f)) ==> 378 s IN STATES f ks1 e ==> 379 s IN STATES f ks2 e``, METIS_TAC [IMF_MU_EXT,DECOMP2])) 380 381val _ = export_theory(); 382