1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6open HolKernel Parse boolLib bossLib; 7 8open pred_setTheory prim_recTheory arithmeticTheory relationTheory; 9open CCSLib CCSTheory StrongEQTheory StrongLawsTheory; 10open WeakEQTheory WeakEQLib; 11 12val _ = new_theory "WeakLaws"; 13 14(******************************************************************************) 15(* *) 16(* Basic laws of observation equivalence for the binary summation operator *) 17(* derived through strong equivalence *) 18(* *) 19(******************************************************************************) 20 21(* Prove WEAK_SUM_IDENT_R: |- !E. WEAK_EQUIV (sum E nil) E *) 22val WEAK_SUM_IDENT_R = save_thm ( 23 "WEAK_SUM_IDENT_R", 24 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_IDENT_R); 25 26(* Prove WEAK_SUM_IDENT_L: |- !E. WEAK_EQUIV (sum nil E) E *) 27val WEAK_SUM_IDENT_L = save_thm ( 28 "WEAK_SUM_IDENT_L", 29 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_IDENT_L); 30 31(* Prove WEAK_SUM_IDEMP: |- !E. WEAK_EQUIV (sum E E) E *) 32val WEAK_SUM_IDEMP = save_thm ( 33 "WEAK_SUM_IDEMP", 34 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_IDEMP); 35 36(* Prove WEAK_SUM_COMM: |- !E E'. WEAK_EQUIV (sum E E') (sum E' E) *) 37val WEAK_SUM_COMM = save_thm ( 38 "WEAK_SUM_COMM", 39 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_COMM); 40 41(* Observation equivalence of stable agents is substitutive under the binary 42 summation operator on the left: 43 |- !E E'. WEAK_EQUIV E E' /\ STABLE E /\ STABLE E' ==> 44 (!E''. WEAK_EQUIV (sum E'' E) (sum E'' E')) 45 *) 46val WEAK_EQUIV_SUBST_SUM_L = save_thm ( 47 "WEAK_EQUIV_SUBST_SUM_L", 48 Q.GENL [`E`, `E'`] 49 (DISCH_ALL 50 (Q.GEN `E''` 51 (OE_TRANS 52 (Q.SPECL [`E''`, `E`] WEAK_SUM_COMM) 53 (OE_TRANS 54 (SPEC_ALL (UNDISCH (SPEC_ALL WEAK_EQUIV_SUBST_SUM_R))) 55 (Q.SPECL [`E'`, `E''`] WEAK_SUM_COMM)))))); 56 57(* Prove WEAK_SUM_ASSOC_R: 58 |- !E E' E''. WEAK_EQUIV (sum (sum E E') E'') (sum E (sum E' E'')) 59 *) 60val WEAK_SUM_ASSOC_R = save_thm ( 61 "WEAK_SUM_ASSOC_R", 62 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_ASSOC_R); 63 64(* Prove WEAK_SUM_ASSOC_L: 65 |- !E E' E''. WEAK_EQUIV (sum E (sum E' E'')) (sum (sum E E') E'') 66 *) 67val WEAK_SUM_ASSOC_L = save_thm ( 68 "WEAK_SUM_ASSOC_L", 69 STRONG_IMP_WEAK_EQUIV_RULE STRONG_SUM_ASSOC_L); 70 71(******************************************************************************) 72(* *) 73(* Basic laws of observation equivalence for the parallel *) 74(* operator derived through strong equivalence *) 75(* *) 76(******************************************************************************) 77 78(* Prove WEAK_PAR_IDENT_R: |- !E. WEAK_EQUIV (par E nil) E 79 *) 80val WEAK_PAR_IDENT_R = save_thm ( 81 "WEAK_PAR_IDENT_R", 82 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_IDENT_R); 83 84(* Prove WEAK_PAR_IDENT_L: |- !E. WEAK_EQUIV (par nil E) E 85 *) 86val WEAK_PAR_IDENT_L = save_thm ( 87 "WEAK_PAR_IDENT_L", 88 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_IDENT_L); 89 90(* Prove WEAK_PAR_COMM: |- !E E'. WEAK_EQUIV (par E E') (par E' E) 91 *) 92val WEAK_PAR_COMM = save_thm ( 93 "WEAK_PAR_COMM", 94 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_COMM); 95 96(* Prove WEAK_PAR_ASSOC: 97 |- !E E' E''. WEAK_EQUIV (par (par E E') E'') (par E (par E' E'')) 98 *) 99val WEAK_PAR_ASSOC = save_thm ( 100 "WEAK_PAR_ASSOC", 101 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_ASSOC); 102 103(* Prove WEAK_PAR_PREF_TAU: 104 |- !u E E'. 105 WEAK_EQUIV (par (prefix u E) (prefix tau E')) 106 (sum (prefix u (par E (prefix tau E'))) 107 (prefix tau (par (prefix u E) E'))) 108 *) 109val WEAK_PAR_PREF_TAU = save_thm ( 110 "WEAK_PAR_PREF_TAU", 111 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_PREF_TAU); 112 113(* Prove WEAK_PAR_TAU_PREF: 114 |- !E u E'. 115 WEAK_EQUIV (par (prefix tau E) (prefix u E')) 116 (sum (prefix tau (par E (prefix u E'))) 117 (prefix u (par (prefix tau E) E'))) 118 *) 119val WEAK_PAR_TAU_PREF = save_thm ( 120 "WEAK_PAR_TAU_PREF", 121 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PAR_TAU_PREF); 122 123(* Prove WEAK_PAR_TAU_TAU: 124 |- !E E'. 125 WEAK_EQUIV (par (prefix tau E) (prefix tau E')) 126 (sum (prefix tau (par E (prefix tau E'))) 127 (prefix tau (par (prefix tau E) E'))) 128 *) 129val WEAK_PAR_TAU_TAU = save_thm ( 130 "WEAK_PAR_TAU_TAU", Q.SPEC `tau` WEAK_PAR_PREF_TAU); 131 132(* Prove WEAK_PAR_PREF_NO_SYNCR: 133 |- !l l'. 134 ~(l = COMPL l') ==> 135 (!E E'. 136 WEAK_EQUIV (par (prefix (label l) E) (prefix (label l') E')) 137 (sum (prefix (label l) (par E (prefix (label l') E'))) 138 (prefix (label l') (par (prefix (label l) E) E')))) 139 *) 140val WEAK_PAR_PREF_NO_SYNCR = save_thm ( 141 "WEAK_PAR_PREF_NO_SYNCR", 142 STRIP_FORALL_RULE ((DISCH ``~((l :'b Label) = COMPL l')``) o 143 (STRONG_IMP_WEAK_EQUIV_RULE) o 144 UNDISCH) 145 STRONG_PAR_PREF_NO_SYNCR); 146 147(* Prove WEAK_PAR_PREF_SYNCR: 148 |- !l l'. 149 (l = COMPL l') ==> 150 (!E E'. 151 WEAK_EQUIV (par (prefix (label l) E) (prefix (label l') E')) 152 (sum 153 (sum (prefix (label l) (par E (prefix (label l') E'))) 154 (prefix (label l') (par (prefix (label l) E) E'))) 155 (prefix tau (par E E')))) 156 *) 157val WEAK_PAR_PREF_SYNCR = save_thm ( 158 "WEAK_PAR_PREF_SYNCR", 159 STRIP_FORALL_RULE ((DISCH ``((l :'b Label) = COMPL l')``) o 160 (STRONG_IMP_WEAK_EQUIV_RULE) o 161 UNDISCH) 162 STRONG_PAR_PREF_SYNCR); 163 164(* The expansion law for observation equivalence: 165 |- !f n f' m. 166 (!i. i <= n ==> Is_Prefix (f i)) /\ (!j. j <= m ==> Is_Prefix (f' j)) 167 ==> 168 WEAK_EQUIV 169 (par (SIGMA f n) (SIGMA f' m)) 170 (sum 171 (sum 172 (SIGMA (\i. prefix (PREF_ACT (f i)) (par (PREF_PROC (f i)) (SIGMA f' m))) n) 173 (SIGMA (\j. prefix (PREF_ACT (f' j)) (par (SIGMA f n) (PREF_PROC (f' j)))) m)) 174 (ALL_SYNC f n f' m)) 175 *) 176val WEAK_EXPANSION_LAW = save_thm ( 177 "WEAK_EXPANSION_LAW", 178 STRIP_FORALL_RULE (DISCH_ALL o (MATCH_MP STRONG_IMP_WEAK_EQUIV) o UNDISCH) 179 STRONG_EXPANSION_LAW); 180 181(******************************************************************************) 182(* *) 183(* Basic laws of observation equivalence for the restriction *) 184(* operator derived through strong equivalence *) 185(* *) 186(******************************************************************************) 187 188(* Prove WEAK_RESTR_NIL: |- !L. WEAK_EQUIV (restr nil L) nil *) 189val WEAK_RESTR_NIL = save_thm ( 190 "WEAK_RESTR_NIL", 191 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RESTR_NIL); 192 193(* Prove WEAK_RESTR_SUM: 194 |- !E E' L. WEAK_EQUIV (restr (sum E E') L) (sum (restr E L) (restr E' L)) 195 *) 196val WEAK_RESTR_SUM = save_thm ( 197 "WEAK_RESTR_SUM", 198 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RESTR_SUM); 199 200(* Prove WEAK_RESTR_PREFIX_TAU: 201 |- !E L. WEAK_EQUIV (restr (prefix tau E) L) (prefix tau (restr E L)) 202 *) 203val WEAK_RESTR_PREFIX_TAU = save_thm ( 204 "WEAK_RESTR_PREFIX_TAU", 205 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RESTR_PREFIX_TAU); 206 207(* Prove WEAK_RESTR_PR_LAB_NIL: 208 |- !l L. l IN L \/ (COMPL l) IN L ==> 209 (!E. WEAK_EQUIV (restr (prefix (label l) E) L) nil) 210 *) 211val WEAK_RESTR_PR_LAB_NIL = save_thm ( 212 "WEAK_RESTR_PR_LAB_NIL", 213 GEN_ALL 214 (DISCH ``(l :'b Label) IN L \/ (COMPL l) IN L`` 215 (Q.GEN `E` 216 (UNDISCH 217 (IMP_TRANS 218 (DISCH ``(l :'b Label) IN L \/ (COMPL l) IN L`` 219 (Q.SPEC `E` 220 (UNDISCH 221 (Q.SPECL [`l`, `L`] STRONG_RESTR_PR_LAB_NIL)))) 222 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, ``nil``] 223 STRONG_IMP_WEAK_EQUIV)))))); 224 225(* Prove WEAK_RESTR_PREFIX_LABEL: 226 |- !l L. 227 ~l IN L /\ ~(COMPL l) IN L ==> 228 (!E. WEAK_EQUIV (restr (prefix (label l) E) L) (prefix (label l) (restr E L))) 229 *) 230val WEAK_RESTR_PREFIX_LABEL = save_thm ( 231 "WEAK_RESTR_PREFIX_LABEL", 232 GEN_ALL 233 (DISCH ``~((l :'b Label) IN L) /\ ~((COMPL l) IN L)`` 234 (Q.GEN `E` 235 (UNDISCH 236 (IMP_TRANS 237 (DISCH ``~((l :'b Label) IN L) /\ ~((COMPL l) IN L)`` 238 (Q.SPEC `E` 239 (UNDISCH 240 (Q.SPECL [`l`, `L`] STRONG_RESTR_PREFIX_LABEL)))) 241 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, 242 ``prefix (label (l :'b Label)) (restr L E)``] 243 STRONG_IMP_WEAK_EQUIV)))))); 244 245(******************************************************************************) 246(* *) 247(* Basic laws of observation equivalence for the relabelling *) 248(* operator derived through strong equivalence *) 249(* *) 250(******************************************************************************) 251 252(* Prove WEAK_RELAB_NIL: |- !rf. WEAK_EQUIV (relab nil rf) nil *) 253val WEAK_RELAB_NIL = save_thm ( 254 "WEAK_RELAB_NIL", 255 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RELAB_NIL); 256 257(* Prove WEAK_RELAB_SUM: 258 |- !E E' rf. WEAK_EQUIV (relab (sum E E') rf) (sum (relab E rf) (relab E' rf)) 259 *) 260val WEAK_RELAB_SUM = save_thm ( 261 "WEAK_RELAB_SUM", 262 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RELAB_SUM); 263 264(* Prove WEAK_RELAB_PREFIX: 265 |- !u E labl. 266 WEAK_EQUIV (relab (prefix u E) (RELAB labl)) 267 (prefix (relabel (Apply_Relab labl) u) (relab E (RELAB labl))) 268 *) 269val WEAK_RELAB_PREFIX = save_thm ( 270 "WEAK_RELAB_PREFIX", 271 STRONG_IMP_WEAK_EQUIV_RULE STRONG_RELAB_PREFIX); 272 273(******************************************************************************) 274(* *) 275(* Basic laws of observation equivalence for the recursion *) 276(* operator through strong equivalence *) 277(* *) 278(******************************************************************************) 279 280(* The unfolding law: 281 WEAK_UNFOLDING: |- !X E. WEAK_EQUIV (rec X E) (CCS_Subst E (rec X E) X) 282 *) 283val WEAK_UNFOLDING = save_thm ( 284 "WEAK_UNFOLDING", 285 STRONG_IMP_WEAK_EQUIV_RULE STRONG_UNFOLDING); 286 287(* Prove the theorem WEAK_PREF_REC_EQUIV: 288 |- !u s v. 289 WEAK_EQUIV 290 (prefix u (rec s (prefix v (prefix u (var s))))) 291 (rec s (prefix u (prefix v (var s)))) 292 *) 293val WEAK_PREF_REC_EQUIV = save_thm ( 294 "WEAK_PREF_REC_EQUIV", 295 STRONG_IMP_WEAK_EQUIV_RULE STRONG_PREF_REC_EQUIV); 296 297(******************************************************************************) 298(* *) 299(* the tau-law "tau.E = E" for observation equivalence *) 300(* *) 301(******************************************************************************) 302 303(* Prove TAU_WEAK: |- !E. WEAK_EQUIV (prefix tau E) E *) 304val TAU_WEAK = store_thm ("TAU_WEAK", 305 ``!E. WEAK_EQUIV (prefix tau E) E``, 306 GEN_TAC 307 >> PURE_ONCE_REWRITE_TAC [WEAK_PROPERTY_STAR] 308 >> REPEAT STRIP_TAC (* 4 sub-goals here *) 309 >| [ (* goal 1 (of 4) *) 310 IMP_RES_TAC TRANS_PREFIX \\ 311 IMP_RES_TAC Action_distinct_label, 312 (* goal 2 (of 4) *) 313 Q.EXISTS_TAC `E2` \\ 314 REWRITE_TAC [WEAK_TRANS, WEAK_EQUIV_REFL] \\ 315 take [`E`, `E2`] \\ 316 ASM_REWRITE_TAC [EPS_REFL] \\ 317 MATCH_MP_TAC ONE_TAU \\ 318 REWRITE_TAC [PREFIX], 319 (* goal 3 (of 4) *) 320 IMP_RES_TAC TRANS_PREFIX \\ 321 Q.EXISTS_TAC `E1` \\ 322 ASM_REWRITE_TAC [EPS_REFL, WEAK_EQUIV_REFL], 323 (* goal 4 (of 4) *) 324 Q.EXISTS_TAC `E2` \\ 325 REWRITE_TAC [WEAK_EQUIV_REFL] \\ 326 MATCH_MP_TAC EPS_TRANS \\ 327 Q.EXISTS_TAC `E` \\ 328 IMP_RES_TAC ONE_TAU >> ASM_REWRITE_TAC [] \\ 329 MATCH_MP_TAC ONE_TAU \\ 330 REWRITE_TAC [PREFIX] ]); 331 332val _ = export_theory (); 333val _ = html_theory "WeakLaws"; 334 335(* last updated: Jun 20, 2017 *) 336