1(* ========================================================================== *) 2(* FILE : TraceScript.sml *) 3(* DESCRIPTION : Reach, STEP, and TRACE relations *) 4(* *) 5(* THESIS : A Formalization of Unique Solutions of Equations in *) 6(* Process Algebra *) 7(* AUTHOR : (c) Chun Tian, University of Bologna *) 8(* DATE : 2017 *) 9(* ========================================================================== *) 10 11open HolKernel Parse boolLib bossLib; 12 13open pred_setTheory relationTheory arithmeticTheory listTheory; 14open CCSLib CCSTheory StrongEQTheory WeakEQTheory; 15 16val _ = new_theory "Trace"; 17val _ = temp_loose_equality (); 18 19(******************************************************************************) 20(* *) 21(* The reachability relation (and finite-state CCS) *) 22(* *) 23(******************************************************************************) 24 25val Reach_defn = ``\E E'. ?u. TRANS E u E'``; 26val Reach_def = Define `Reach = RTC ^Reach_defn`; 27 28val Reach_one = store_thm ((* NEW *) 29 "Reach_one", ``!E E'. (?u. TRANS E u E') ==> Reach E E'``, 30 REWRITE_TAC [Reach_def] 31 >> REPEAT STRIP_TAC 32 >> MATCH_MP_TAC RTC_SINGLE 33 >> BETA_TAC 34 >> Q.EXISTS_TAC `u` >> art []); 35 36val Reach_self = store_thm ((* NEW *) 37 "Reach_self", ``!E. Reach E E``, 38 REWRITE_TAC [Reach_def, RTC_REFL]); 39 40local 41 val trans = (REWRITE_RULE [GSYM Reach_def]) o BETA_RULE o (ISPEC Reach_defn); 42in 43val Reach_trans = save_thm ((* NEW *) 44 "Reach_trans", trans (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)); 45 46val Reach_ind = save_thm ((* NEW *) 47 "Reach_ind", trans RTC_INDUCT); 48 49val Reach_strongind = save_thm ((* NEW *) 50 "Reach_strongind", trans RTC_STRONG_INDUCT); 51 52val Reach_ind_right = save_thm ((* NEW *) 53 "Reach_ind_right", trans RTC_INDUCT_RIGHT1); 54 55val Reach_strongind_right = save_thm ((* NEW *) 56 "Reach_strongind_right", trans RTC_STRONG_INDUCT_RIGHT1); 57 58val Reach_cases1 = save_thm ((* NEW *) 59 "Reach_cases1", trans RTC_CASES1); 60 61val Reach_cases2 = save_thm ((* NEW *) 62 "Reach_cases2", trans RTC_CASES2); 63end; 64 65(* Define the set of states reachable from any CCS process *) 66val NODES_def = Define ` 67 NODES (p :('a, 'b) CCS) = { q | Reach p q }`; 68 69(* Finite-state CCS *) 70val finite_state_def = Define ` 71 finite_state (p :('a, 'b) CCS) = FINITE (NODES p)`; 72 73val Reach_NODES = store_thm ( 74 "Reach_NODES", ``!p q. Reach p q ==> q IN (NODES p)``, 75 REPEAT STRIP_TAC 76 >> SRW_TAC [] [NODES_def]); 77 78val SELF_NODES = store_thm ( 79 "SELF_NODES", ``!p. p IN (NODES p)``, 80 REPEAT STRIP_TAC 81 >> SRW_TAC [] [NODES_def] 82 >> REWRITE_TAC [Reach_self]); 83 84val MORE_NODES = store_thm ( 85 "MORE_NODES", ``!p q q'. q IN (NODES p) /\ Reach q q' ==> q' IN (NODES p)``, 86 REPEAT GEN_TAC 87 >> SRW_TAC [] [NODES_def] 88 >> IMP_RES_TAC Reach_trans); 89 90val TRANS_IN_NODES = store_thm ( 91 "TRANS_IN_NODES", ``!p q u. TRANS p u q ==> q IN (NODES p)``, 92 REPEAT STRIP_TAC 93 >> REWRITE_TAC [NODES_def] 94 >> SRW_TAC [] [] 95 >> MATCH_MP_TAC Reach_one 96 >> Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC []); 97 98val EPS_Reach = store_thm ((* NEW *) 99 "EPS_Reach", ``!p q. EPS p q ==> Reach p q``, 100 HO_MATCH_MP_TAC EPS_ind_right 101 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 102 >- REWRITE_TAC [Reach_self] 103 >> IMP_RES_TAC Reach_one 104 >> IMP_RES_TAC Reach_trans); 105 106val EPS_IN_NODES = store_thm ((* NEW *) 107 "EPS_IN_NODES", ``!p q. EPS p q ==> q IN (NODES p)``, 108 REPEAT STRIP_TAC 109 >> MATCH_MP_TAC Reach_NODES 110 >> IMP_RES_TAC EPS_Reach); 111 112val WEAK_TRANS_Reach = store_thm ((* NEW *) 113 "WEAK_TRANS_Reach", ``!p q u. WEAK_TRANS p u q ==> Reach p q``, 114 REWRITE_TAC [WEAK_TRANS] 115 >> REPEAT STRIP_TAC 116 >> IMP_RES_TAC EPS_Reach 117 >> IMP_RES_TAC Reach_one 118 >> IMP_RES_TAC Reach_trans); 119 120val WEAK_TRANS_IN_NODES = store_thm ((* NEW *) 121 "WEAK_TRANS_IN_NODES", ``!p q u. WEAK_TRANS p u q ==> q IN (NODES p)``, 122 REPEAT STRIP_TAC 123 >> MATCH_MP_TAC Reach_NODES 124 >> IMP_RES_TAC WEAK_TRANS_Reach); 125 126(******************************************************************************) 127(* *) 128(* N-steps transition of CCS, based on arithmetic.NRC *) 129(* *) 130(******************************************************************************) 131 132val STEP_defn = ``\E E'. ?u. TRANS E u E'``; 133val STEP_def = Define `STEP P n Q = NRC ^STEP_defn n P Q`; 134 135local 136 val trans = (REWRITE_RULE [GSYM STEP_def]) o BETA_RULE o (ISPEC STEP_defn); 137in 138(* |- ���x y. x --0--> y ��� (x = y) *) 139val STEP0 = save_thm ("STEP0", trans NRC_0); 140 141(* |- x --1--> y ��� ���u. x --u--> y *) 142val STEP1 = save_thm ("STEP1", trans (Q.GEN `R` NRC_1)); 143 144(* |- ���n x y. x --SUC n--> y ��� ���z. (���u. x --u--> z) ��� z --n--> y *) 145val STEP_SUC = save_thm ( 146 "STEP_SUC", trans (CONJUNCT2 NRC)); 147 148(* |- ���n x y. x --SUC n--> y ��� ���z. x --n--> z ��� ���u. z --u--> y *) 149val STEP_SUC_LEFT = save_thm ( 150 "STEP_SUC_LEFT", trans (Q_GENL [`R`, `n`, `x`, `y`] NRC_SUC_RECURSE_LEFT)); 151 152(* |- ���m n x z. x --m + n--> z ��� ���y. x --m--> y ��� y --n--> z *) 153val STEP_ADD_E = save_thm ( 154 "STEP_ADD_E", trans (Q.GEN `R` NRC_ADD_E)); 155 156(* |- ���m n x z. x --m + n--> z ��� ���y. x --m--> y ��� y --n--> z *) 157val STEP_ADD_EQN = save_thm ( 158 "STEP_ADD_EQN", trans (Q_GENL [`R`, `m`, `n`, `x`, `z`] NRC_ADD_EQN)); 159 160(* |- ���m n x y z. x --m--> y ��� y --n--> z ��� x --m + n--> z *) 161val STEP_ADD_I = save_thm ( 162 "STEP_ADD_I", trans (Q.GEN `R` NRC_ADD_I)); 163end; 164 165val EPS_AND_STEP = store_thm ( 166 "EPS_AND_STEP", ``!E E'. EPS E E' ==> ?n. STEP E n E'``, 167 HO_MATCH_MP_TAC EPS_ind 168 >> rpt STRIP_TAC 169 >| [ (* goal 1 (of 2) *) 170 Q.EXISTS_TAC `0` >> PROVE_TAC [STEP0], 171 (* goal 2 (of 2) *) 172 Q.EXISTS_TAC `SUC n` \\ 173 ONCE_REWRITE_TAC [STEP_SUC] \\ 174 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] \\ 175 Q.EXISTS_TAC `tau` >> ASM_REWRITE_TAC [] ]); 176 177val WEAK_TRANS_AND_STEP = store_thm ( 178 "WEAK_TRANS_AND_STEP", ``!E u E'. WEAK_TRANS E u E' ==> ?n. STEP E n E'``, 179 REWRITE_TAC [WEAK_TRANS] 180 >> rpt STRIP_TAC 181 >> IMP_RES_TAC EPS_AND_STEP 182 >> Q.EXISTS_TAC `n' + 1 + n` 183 >> REWRITE_TAC [STEP_ADD_EQN] 184 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] 185 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] 186 >> ONCE_REWRITE_TAC [STEP1] 187 >> Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC []); 188 189(******************************************************************************) 190(* *) 191(* Reflexive Transitive Closure with a List (LRTC) *) 192(* *) 193(******************************************************************************) 194 195val LRTC_DEF = new_definition ("LRTC_DEF", 196 ``LRTC (R :'a -> 'b -> 'a -> bool) a l b = 197 !P. (!x. P x [] x) /\ 198 (!x h y t z. R x h y /\ P y t z ==> P x (h :: t) z) ==> P a l b``); 199 200val LRTC_INDUCT = store_thm ( 201 "LRTC_INDUCT", 202 ``!R P. (!x. P x [] x) /\ (!x h y t z. R x h y /\ P y t z ==> P x (h :: t) z) ==> 203 (!x l (y :'a). LRTC R x l y ==> P x l y)``, 204 REWRITE_TAC [LRTC_DEF] >> PROVE_TAC []); 205 206val LRTC_RULES = store_thm ( 207 "LRTC_RULES", 208 ``!R. (!x. LRTC R (x :'a) [] x) /\ 209 (!x h y t z. R x h y /\ LRTC R y t z ==> LRTC R x (h :: t) z)``, 210 REWRITE_TAC [LRTC_DEF] >> PROVE_TAC []); 211 212val LRTC_REFL = store_thm ( 213 "LRTC_REFL", ``!R. LRTC R x [] x``, 214 REWRITE_TAC [LRTC_RULES]); 215 216val LRTC_SINGLE = store_thm ( 217 "LRTC_SINGLE", 218 ``!R x t y. R x t y ==> LRTC R x [t] y``, 219 rpt STRIP_TAC 220 >> `~NULL [t]` by PROVE_TAC [NULL_DEF] 221 >> POP_ASSUM (ASSUME_TAC o SYM o (MATCH_MP (Q.SPEC `[t]` CONS))) 222 >> ONCE_ASM_REWRITE_TAC [] 223 >> MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) 224 >> PURE_ONCE_REWRITE_TAC [HD, TL] 225 >> Q.EXISTS_TAC `y` 226 >> ASM_REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)]); 227 228val LRTC_STRONG_INDUCT = store_thm ( 229 "LRTC_STRONG_INDUCT", 230 ``!R P. (!x. P x [] x) /\ 231 (!x h y t z. R x h y /\ LRTC R y t z /\ P y t z ==> P x (h :: t) z) ==> 232 (!x l (y :'a). LRTC R x l y ==> P x l y)``, 233 REPEAT GEN_TAC 234 >> STRIP_TAC 235 >> MATCH_MP_TAC ((CONV_RULE (SIMP_CONV list_ss [LRTC_RULES]) o 236 Q.SPECL [`R`, `\u l v. LRTC R u l v /\ P u l v`]) LRTC_INDUCT) 237 >> rpt STRIP_TAC 238 >> PROVE_TAC [LRTC_RULES]); 239 240val LRTC_LRTC = store_thm ( 241 "LRTC_LRTC", 242 ``!R (x :'a) m y. LRTC R x m y ==> !n z. LRTC R y n z ==> LRTC R x (m ++ n) z``, 243 GEN_TAC 244 >> HO_MATCH_MP_TAC LRTC_STRONG_INDUCT 245 >> FULL_SIMP_TAC list_ss [] 246 >> rpt STRIP_TAC 247 >> RES_TAC 248 >> MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) 249 >> Q.EXISTS_TAC `x'` 250 >> ASM_REWRITE_TAC []); 251 252val LRTC_TRANS = store_thm ( 253 "LRTC_TRANS", 254 ``!R (x :'a) m y n z. LRTC R x m y /\ LRTC R y n z ==> LRTC R x (m ++ n) z``, 255 rpt STRIP_TAC 256 >> irule LRTC_LRTC 257 >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC []); 258 259val LRTC_CASES1 = store_thm ( 260 "LRTC_CASES1", 261 ``!R (x :'a) l y. LRTC R x l y = if NULL l then (x = y) 262 else ?u. R x (HD l) u /\ LRTC R u (TL l) y``, 263 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] 264 >> CONJ_TAC (* 2 sub-goals here *) 265 >| [ (* goal 1 (of 2) *) 266 GEN_TAC >> HO_MATCH_MP_TAC LRTC_INDUCT \\ 267 SIMP_TAC list_ss [] \\ 268 rpt STRIP_TAC \\ 269 Q.EXISTS_TAC `x'` >> ASM_REWRITE_TAC [] \\ 270 Cases_on `NULL l` >> FULL_SIMP_TAC std_ss [] >| (* 2 sub-goals here *) 271 [ (* goal 1.1 (of 2) *) 272 POP_ASSUM (REWRITE_TAC o wrap o (REWRITE_RULE [NULL_EQ])) \\ 273 REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)], 274 (* goal 1.2 (of 2) *) 275 POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM o (MATCH_MP CONS)) \\ 276 MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) \\ 277 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] ], 278 (* goal 2 (of 2) *) 279 rpt STRIP_TAC \\ 280 Cases_on `NULL l` >> FULL_SIMP_TAC std_ss [] >| (* 2 sub-goals here *) 281 [ (* goal 2.1 (of 2) *) 282 POP_ASSUM (REWRITE_TAC o wrap o (REWRITE_RULE [NULL_EQ])) \\ 283 REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)], 284 (* goal 2.2 (of 2) *) 285 POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM o (MATCH_MP CONS)) \\ 286 MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) \\ 287 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] ] ]); 288 289val LRTC_NIL = store_thm ( 290 "LRTC_NIL", ``!R (x :'a) y. LRTC R x [] y = (x = y)``, 291 rpt GEN_TAC 292 >> ONCE_REWRITE_TAC [LRTC_CASES1] 293 >> SIMP_TAC list_ss []); 294 295val LRTC_ONE = store_thm ( 296 "LRTC_ONE", 297 ``!R x t y. LRTC R x [t] y = R x t y``, 298 rpt GEN_TAC 299 >> Rev EQ_TAC 300 >- ( DISCH_TAC >> MATCH_MP_TAC LRTC_SINGLE >> ASM_REWRITE_TAC [] ) 301 >> ONCE_REWRITE_TAC [LRTC_CASES1] 302 >> SIMP_TAC list_ss [] 303 >> rpt STRIP_TAC 304 >> IMP_RES_TAC LRTC_NIL 305 >> FULL_SIMP_TAC std_ss []); 306 307val LRTC_CASES2 = store_thm ( 308 "LRTC_CASES2", 309 ``!R (x :'a) l y. LRTC R x l y = if NULL l then (x = y) 310 else ?u. LRTC R x (FRONT l) u /\ R u (LAST l) y``, 311 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] 312 >> CONJ_TAC (* 2 sub-goals here *) 313 >| [ (* goal 1 (of 2) *) 314 GEN_TAC >> HO_MATCH_MP_TAC LRTC_INDUCT \\ 315 SIMP_TAC list_ss [] \\ 316 rpt STRIP_TAC \\ 317 Cases_on `l` >> FULL_SIMP_TAC list_ss [] >| (* 2 sub-goals here *) 318 [ (* goal 1.1 (of 2) *) 319 Q.EXISTS_TAC `x` >> ASM_REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)], 320 (* goal 1.2 (of 2) *) 321 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] \\ 322 MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) \\ 323 Q.EXISTS_TAC `x'` >> ASM_REWRITE_TAC [] ], 324 (* goal 2 (of 2) *) 325 rpt STRIP_TAC \\ 326 Cases_on `l` >> FULL_SIMP_TAC list_ss [] 327 >- REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)] \\ 328 Cases_on `t = []` \\ 329 FULL_SIMP_TAC list_ss [FRONT_DEF, LAST_DEF] >| (* 2 sub-goals here *) 330 [ (* goal 2.1 (of 2) *) 331 MATCH_MP_TAC LRTC_SINGLE \\ 332 IMP_RES_TAC (EQ_IMP_LR LRTC_NIL) >> ASM_REWRITE_TAC [], 333 (* goal 2.2 (of 2) *) 334 Know `h :: t = (h :: FRONT t) ++ [LAST t]` 335 >- ( SIMP_TAC list_ss [] >> PROVE_TAC [APPEND_FRONT_LAST] ) \\ 336 Rewr \\ 337 MATCH_MP_TAC LRTC_TRANS \\ 338 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] \\ 339 MATCH_MP_TAC LRTC_SINGLE >> ASM_REWRITE_TAC [] ] ]); 340 341val LRTC_CASES_LRTC_TWICE = store_thm ( 342 "LRTC_CASES_LRTC_TWICE", 343 ``!R (x :'a) l y. LRTC R x l y = ?u l1 l2. LRTC R x l1 u /\ LRTC R u l2 y /\ (l = l1 ++ l2)``, 344 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] 345 >> CONJ_TAC (* 2 sub-goals here *) 346 >| [ (* goal 1 (of 2) *) 347 GEN_TAC >> HO_MATCH_MP_TAC LRTC_INDUCT \\ 348 rpt STRIP_TAC >| (* 2 sub-goals here *) 349 [ (* goal 1.1 (of 2) *) 350 take [`x`, `[]`, `[]`] >> SIMP_TAC list_ss [] \\ 351 PROVE_TAC [LRTC_RULES], 352 (* goal 1.2 (of 2) *) 353 take [`u`, `h :: l1`, `l2`] >> ASM_SIMP_TAC list_ss [] \\ 354 MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) \\ 355 Q.EXISTS_TAC `x'` >> ASM_REWRITE_TAC [] ], 356 (* goal 2 (of 2) *) 357 rpt STRIP_TAC >> ASM_REWRITE_TAC [] \\ 358 MATCH_MP_TAC LRTC_TRANS \\ 359 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] ]); 360 361val LRTC_APPEND_CASES = store_thm ( 362 "LRTC_APPEND_CASES", 363 ``!R l1 l2 (x :'a) y. LRTC R x (l1 ++ l2) y = ?u. LRTC R x l1 u /\ LRTC R u l2 y``, 364 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] 365 >> Rev CONJ_TAC 366 >- ( rpt STRIP_TAC >> Q.ABBREV_TAC `l = l1 ++ l2` \\ 367 ONCE_REWRITE_TAC [LRTC_CASES_LRTC_TWICE] \\ 368 take [`u`, `l1`, `l2`] >> Q.UNABBREV_TAC `l` >> ASM_REWRITE_TAC [] ) 369 >> GEN_TAC 370 >> Induct_on `l1` 371 >| [ (* goal 1 (of 2) *) 372 rpt STRIP_TAC >> FULL_SIMP_TAC list_ss [] \\ 373 Q.EXISTS_TAC `x` >> ASM_REWRITE_TAC [CONJUNCT1 (Q.SPEC `R` LRTC_RULES)], 374 (* goal 2 (of 2) *) 375 rpt STRIP_TAC \\ 376 IMP_RES_TAC LRTC_CASES1 \\ 377 FULL_SIMP_TAC list_ss [] \\ 378 RES_TAC \\ 379 Q.EXISTS_TAC `u'` >> ASM_REWRITE_TAC [] \\ 380 MATCH_MP_TAC (CONJUNCT2 (Q.SPEC `R` LRTC_RULES)) \\ 381 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] ]); 382 383(******************************************************************************) 384(* *) 385(* The trace relation *) 386(* *) 387(******************************************************************************) 388 389val _ = overload_on ("epsilon", ``[] :'b Action list``); 390 391val _ = Unicode.unicode_version { u = UTF8.chr 0x03B5, tmnm = "epsilon"}; 392val _ = TeX_notation { hol = "epsilon", 393 TeX = ("\\ensuremath{\\epsilon}", 1) }; 394 395val TRACE_def = Define `TRACE = LRTC TRANS`; 396 397val _ = type_abbrev ("trace", 398 ``:('a, 'b) CCS -> 'b Action list -> ('a, 'b) CCS -> bool``); 399 400local 401 val trans = (REWRITE_RULE [SYM TRACE_def]) o (ISPEC ``TRANS``); 402in 403 404(* (���x. x --��--> x) ��� 405 ���x h y t z. x --h--> y ��� y --t--> z ��� x --h::t--> z *) 406val TRACE_rules = save_thm ( 407 "TRACE_rules", trans LRTC_RULES); 408 409(* |- ���x m y. x --m--> y ��� ���n z. y --n--> z ��� x --m ++ n--> z *) 410val TRACE_trans = save_thm ( 411 "TRACE_trans", trans LRTC_LRTC); 412 413(* |- ���P. 414 (���x. P x �� x) ��� (���x h y t z. x --h--> y ��� P y t z ��� P x (h::t) z) ��� 415 ���x l y. x --l--> y ��� P x l y *) 416val TRACE_ind = save_thm ( 417 "TRACE_ind", trans LRTC_INDUCT); 418 419(* |- ���P. 420 (���x. P x �� x) ��� 421 (���x h y t z. x --h--> y ��� y --t--> z ��� P y t z ��� P x (h::t) z) ��� 422 ���x l y. x --l--> y ��� P x l y *) 423val TRACE_strongind = save_thm ( 424 "TRACE_strongind", trans LRTC_STRONG_INDUCT); 425 426(* |- ���x l y. 427 x --l--> y ��� 428 if NULL l then x = y else ���u. x --HD l--> u ��� u --TL l--> y *) 429val TRACE_cases1 = save_thm ( 430 "TRACE_cases1", trans LRTC_CASES1); 431 432(* |- ���x l y. 433 x --l--> y ��� 434 if NULL l then x = y else ���u. x --FRONT l--> u ��� u --LAST l--> y *) 435val TRACE_cases2 = save_thm ( 436 "TRACE_cases2", trans LRTC_CASES2); 437 438(* |- ���x l y. 439 x --l--> y ��� ���u l1 l2. x --l1--> u ��� u --l2--> y ��� (l = l1 ++ l2) *) 440val TRACE_cases_twice = save_thm ( 441 "TRACE_cases_twice", trans LRTC_CASES_LRTC_TWICE); 442 443(* |- ���l1 l2 x y. x --l1 ++ l2--> y ��� ���u. x --l1--> u ��� u --l2--> y *) 444val TRACE_APPEND_cases = save_thm ( 445 "TRACE_APPEND_cases", trans LRTC_APPEND_CASES); 446 447(* |- ���x y. x --��--> y ��� (x = y) *) 448val TRACE_NIL = save_thm ( 449 "TRACE_NIL", trans LRTC_NIL); 450 451(* |- ���x t y. x --t--> y ��� x --[t]--> y *) 452val TRACE1 = save_thm ( 453 "TRACE1", trans LRTC_SINGLE); 454 455(* |- ���x t y. x --[t]--> y ��� x --t--> y *) 456val TRACE_ONE = save_thm ( 457 "TRACE_ONE", trans LRTC_ONE); 458end; 459 460val [TRACE_rule0, TRACE_rule1] = 461 map save_thm (combine (["TRACE_rule0", "TRACE_rule1"], CONJUNCTS TRACE_rules)); 462 463(* The `transitivity` of TRACE relation *) 464val TRACE_trans_applied = store_thm ( 465 "TRACE_trans_applied", 466 ``!xs ys E E1 E'. TRACE E xs E1 /\ TRACE E1 ys E' ==> TRACE E (xs ++ ys) E'``, 467 PROVE_TAC [TRACE_trans]); 468 469val TRACE_REFL = store_thm ("TRACE_REFL", ``!E. TRACE E [] E``, 470 PROVE_TAC [TRACE_def, LRTC_REFL]); 471 472val TRACE2 = store_thm ("TRACE2", 473 ``!E x E1 xs E'. TRANS E x E1 /\ TRACE E1 xs E' ==> TRACE E (x :: xs) E'``, 474 rpt STRIP_TAC 475 >> MATCH_MP_TAC TRACE_rule1 476 >> Q.EXISTS_TAC `E1` 477 >> ASM_REWRITE_TAC []); 478 479val EPS_TRACE = store_thm ( 480 "EPS_TRACE", ``!E E'. EPS E E' ==> ?xs. TRACE E xs E'``, 481 HO_MATCH_MP_TAC EPS_ind 482 >> rpt STRIP_TAC 483 >| [ (* goal 1 (of 2) *) 484 Q.EXISTS_TAC `[]` >> REWRITE_TAC [TRACE_REFL], 485 (* goal 2 (of 2) *) 486 Q.EXISTS_TAC `tau :: xs` \\ 487 MATCH_MP_TAC TRACE2 \\ 488 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] ]); 489 490val WEAK_TRANS_TRACE = store_thm ( 491 "WEAK_TRANS_TRACE", ``!E u E'. WEAK_TRANS E u E' ==> ?xs. TRACE E xs E'``, 492 REWRITE_TAC [WEAK_TRANS] 493 >> rpt STRIP_TAC 494 >> IMP_RES_TAC EPS_TRACE 495 >> IMP_RES_TAC TRACE1 496 >> Q.EXISTS_TAC `xs' ++ [u] ++ xs` 497 >> MATCH_MP_TAC TRACE_trans_applied 498 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] 499 >> MATCH_MP_TAC TRACE_trans_applied 500 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC []); 501 502val NO_LABEL_def = Define ` 503 NO_LABEL (L :'b Action list) = ~?l. MEM (label l) L`; 504 505val NO_LABEL_cases = store_thm ( 506 "NO_LABEL_cases", 507 ``!(x :'b Action) xs. NO_LABEL (x :: xs) = (x = tau) /\ NO_LABEL xs``, 508 REWRITE_TAC [NO_LABEL_def] 509 >> rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 510 >| [ (* goal 1 (of 2) *) 511 REWRITE_TAC [MEM] \\ 512 Cases_on `x` >> SIMP_TAC list_ss [Action_distinct_label, IS_LABEL_def] \\ 513 Q.EXISTS_TAC `x'` >> DISJ1_TAC \\ 514 ACCEPT_TAC (REFL ``x' :'b Label``), 515 (* goal 2 (of 2) *) 516 REWRITE_TAC [MEM] \\ 517 rpt STRIP_TAC >- rfs [Action_distinct_label] \\ 518 METIS_TAC [] ]); 519 520val EPS_TRACE2 = Q.prove ( 521 `!E E'. EPS E E' ==> ?xs. TRACE E xs E' /\ NO_LABEL xs`, 522 REWRITE_TAC [NO_LABEL_def] 523 >> HO_MATCH_MP_TAC EPS_ind 524 >> rpt STRIP_TAC 525 >| [ (* goal 1 (of 2) *) 526 Q.EXISTS_TAC `[]` >> REWRITE_TAC [TRACE_REFL] \\ 527 REWRITE_TAC [MEM], 528 (* goal 2 (of 2) *) 529 Q.EXISTS_TAC `tau :: xs` \\ 530 CONJ_TAC >| (* 2 sub-goal here *) 531 [ (* goal 2.1 (of 2) *) 532 MATCH_MP_TAC TRACE2 \\ 533 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [], 534 (* goal 2.2 (of 2) *) 535 REWRITE_TAC [MEM] \\ 536 ASM_REWRITE_TAC [Action_distinct_label] ] ]); 537 538val EPS_AND_TRACE = store_thm ( 539 "EPS_AND_TRACE", ``!E E'. EPS E E' <=> ?xs. TRACE E xs E' /\ NO_LABEL xs``, 540 rpt GEN_TAC >> EQ_TAC 541 >- ( DISCH_TAC \\ 542 MATCH_MP_TAC EPS_TRACE2 >> ASM_REWRITE_TAC [] ) 543 >> REWRITE_TAC [NO_LABEL_def] 544 >> rpt STRIP_TAC 545 >> NTAC 2 (POP_ASSUM MP_TAC) 546 >> Q.SPEC_TAC (`E`, `E`) 547 >> Q.SPEC_TAC (`xs`, `xs`) 548 >> Induct_on `xs` (* 2 sub-goals here *) 549 >| [ (* goal 1 (of 2) *) 550 GEN_TAC >> REWRITE_TAC [TRACE_NIL] \\ 551 RW_TAC std_ss [EPS_REFL], 552 (* goal 2 (of 2) *) 553 rpt STRIP_TAC \\ 554 qpat_x_assum `TRACE E (h::xs) E'` 555 (ASSUME_TAC o (ONCE_REWRITE_RULE [TRACE_cases1])) \\ 556 FULL_SIMP_TAC list_ss [] \\ 557 RES_TAC \\ 558 Cases_on `h` >- ( IMP_RES_TAC ONE_TAU >> IMP_RES_TAC EPS_TRANS ) \\ 559 FULL_SIMP_TAC std_ss [Action_11] \\ 560 PROVE_TAC [] ]); 561 562(* u is the unique Label in L, learnt from Robert Beers *) 563val UNIQUE_LABEL_def = Define ` 564 UNIQUE_LABEL u (L :'b Action list) = 565 ?L1 L2. (L1 ++ [u] ++ L2 = L) /\ NO_LABEL L1 /\ NO_LABEL L2`; 566 567(* old equivalent definition without using NO_LABEL *) 568val UNIQUE_LABEL_DEF = store_thm ( 569 "UNIQUE_LABEL_DEF", 570 ``!u (L :'b Action list). 571 UNIQUE_LABEL u (L :'b Action list) = 572 ?L1 L2. (L1 ++ [u] ++ L2 = L) /\ ~?l. MEM (label l) L1 \/ MEM (label l) L2``, 573 Know `!L1 L2. (?l. MEM (label l) L1 \/ MEM (label l) L2) = 574 (?l. MEM (label l) L1) \/ (?l. MEM (label l) L2)` 575 >- ( NTAC 2 GEN_TAC \\ 576 Q.ABBREV_TAC `P = \x. MEM (label x) L1` \\ 577 Q.ABBREV_TAC `Q = \x. MEM (label x) L2` >> fs [] \\ 578 REWRITE_TAC [EXISTS_OR_THM] \\ 579 Q.UNABBREV_TAC `P` \\ 580 Q.UNABBREV_TAC `Q` \\ 581 BETA_TAC >> PROVE_TAC [] ) 582 >> STRIP_TAC 583 >> REWRITE_TAC [UNIQUE_LABEL_def, NO_LABEL_def] 584 >> NTAC 2 GEN_TAC 585 >> EQ_TAC (* 2 goals here, same tactic *) 586 >> STRIP_TAC 587 >> Q.EXISTS_TAC `L1` 588 >> Q.EXISTS_TAC `L2` 589 >> fs []); 590 591val UNIQUE_LABEL_IMP_MEM = store_thm ( 592 "UNIQUE_LABEL_IMP_MEM", 593 ``!u (L :'b Action list). UNIQUE_LABEL u L ==> MEM u L``, 594 rpt GEN_TAC 595 >> REWRITE_TAC [UNIQUE_LABEL_DEF] 596 >> rpt STRIP_TAC 597 >> POP_ASSUM K_TAC 598 >> POP_ASSUM (REWRITE_TAC o wrap o SYM) 599 >> SIMP_TAC list_ss []); 600 601val UNIQUE_LABEL_NOT_NULL = store_thm ( 602 "UNIQUE_LABEL_NOT_NULL", 603 ``!u (L :'b Action list). UNIQUE_LABEL u L ==> ~NULL L``, 604 rpt GEN_TAC >> STRIP_TAC 605 >> IMP_RES_TAC UNIQUE_LABEL_IMP_MEM 606 >> POP_ASSUM MP_TAC 607 >> KILL_TAC 608 >> PROVE_TAC [NOT_NULL_MEM]); 609 610val UNIQUE_LABEL_cases1 = store_thm ( 611 "UNIQUE_LABEL_cases1", 612 ``!(l :'b Label) xs. UNIQUE_LABEL (label l) (tau :: xs) = UNIQUE_LABEL (label l) xs``, 613 rpt GEN_TAC 614 >> REWRITE_TAC [UNIQUE_LABEL_DEF] 615 >> EQ_TAC >> rpt STRIP_TAC (* 2 sub-goals here *) 616 >| [ (* goal 1 (of 2) *) 617 Cases_on `L1` >- FULL_SIMP_TAC list_ss [Action_distinct_label] \\ 618 REV_FULL_SIMP_TAC list_ss [Action_distinct_label] \\ 619 take [`t`, `L2`] >> ASM_REWRITE_TAC [], 620 (* goal 2 (of 2) *) 621 take [`tau :: L1`, `L2`] \\ 622 FULL_SIMP_TAC list_ss [Action_distinct_label] ]); 623 624val UNIQUE_LABEL_cases2 = store_thm ( 625 "UNIQUE_LABEL_cases2", 626 ``!(l :'b Label) l' xs. UNIQUE_LABEL (label l) (label l' :: xs) = (l = l') /\ NO_LABEL xs``, 627 rpt GEN_TAC 628 >> REWRITE_TAC [UNIQUE_LABEL_DEF] 629 >> EQ_TAC >> rpt STRIP_TAC (* 3 sub-goals here *) 630 >| [ (* goal 1 (of 3) *) 631 Cases_on `L1` >- FULL_SIMP_TAC list_ss [Action_11] \\ 632 FULL_SIMP_TAC list_ss [], 633 (* goal 2 (of 3) *) 634 REWRITE_TAC [NO_LABEL_def] \\ 635 Cases_on `L1` >- REV_FULL_SIMP_TAC list_ss [Action_11] \\ 636 FULL_SIMP_TAC list_ss [], 637 (* goal 3 (of 3) *) 638 take [`[]`, `xs`] \\ 639 FULL_SIMP_TAC list_ss [Action_11, NO_LABEL_def] ]); 640 641val WEAK_TRANS_TRACE2 = Q.prove ( 642 `!E u E'. WEAK_TRANS E u E' ==> ?us. TRACE E us E' /\ ~NULL us /\ 643 if (u = tau) then NO_LABEL us else UNIQUE_LABEL u us`, 644 REWRITE_TAC [WEAK_TRANS] 645 >> rpt STRIP_TAC 646 >> IMP_RES_TAC EPS_TRACE2 647 >> IMP_RES_TAC TRACE1 648 >> Q.EXISTS_TAC `xs' ++ [u] ++ xs` 649 >> CONJ_TAC (* 2 sub-goals here *) 650 >| [ (* goal 1 (of 2) *) 651 MATCH_MP_TAC TRACE_trans_applied \\ 652 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 653 MATCH_MP_TAC TRACE_trans_applied \\ 654 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 655 (* goal 2 (of 2) *) 656 FULL_SIMP_TAC list_ss [NO_LABEL_def, NULL_EQ, Action_distinct_label] \\ 657 Cases_on `u` >> RW_TAC std_ss [] \\ 658 REWRITE_TAC [UNIQUE_LABEL_DEF] \\ 659 take [`xs'`, `xs`] >> FULL_SIMP_TAC list_ss [] ]); 660 661val WEAK_TRANS_AND_TRACE = store_thm ( 662 "WEAK_TRANS_AND_TRACE", 663 ``!E u E'. WEAK_TRANS E u E' <=> ?us. TRACE E us E' /\ ~NULL us /\ 664 if (u = tau) then NO_LABEL us else UNIQUE_LABEL u us``, 665 rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 666 >- ( DISCH_TAC \\ 667 MATCH_MP_TAC WEAK_TRANS_TRACE2 >> ASM_REWRITE_TAC [] ) 668 >> rpt STRIP_TAC 669 >> Cases_on `u` 670 >> FULL_SIMP_TAC std_ss [Action_distinct_label, NO_LABEL_def] (* 2 sub-goals here *) 671 >| [ (* goal 1 (of 2) *) 672 REWRITE_TAC [WEAK_TRANS] \\ 673 Q.EXISTS_TAC `E` >> REWRITE_TAC [EPS_REFL] \\ 674 qpat_x_assum `TRACE E us E'` (ASSUME_TAC o (ONCE_REWRITE_RULE [TRACE_cases1])) \\ 675 REV_FULL_SIMP_TAC list_ss [] \\ 676 Know `HD us = tau` 677 >- ( Cases_on `HD us` >- REWRITE_TAC [] \\ 678 qpat_x_assum `!l. ~MEM (label l) us` (ASSUME_TAC o (Q.SPEC `x`)) \\ 679 qpat_x_assum `HD us = label x` ((FULL_SIMP_TAC list_ss) o wrap o SYM) \\ 680 PROVE_TAC [CONS, MEM] ) \\ 681 DISCH_TAC >> FULL_SIMP_TAC list_ss [] \\ 682 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] \\ 683 REWRITE_TAC [EPS_AND_TRACE, NO_LABEL_def] \\ 684 Q.EXISTS_TAC `TL us` >> ASM_REWRITE_TAC [] \\ 685 CCONTR_TAC >> FULL_SIMP_TAC bool_ss [] \\ 686 qpat_x_assum `!l. ~MEM (label l) us` (MP_TAC o (Q.SPEC `l`)) \\ 687 Cases_on `us` >- FULL_SIMP_TAC list_ss [] \\ 688 REWRITE_TAC [MEM] \\ 689 FULL_SIMP_TAC list_ss [], 690 (* goal 2 (of 2) *) 691 REWRITE_TAC [WEAK_TRANS] \\ 692 IMP_RES_TAC UNIQUE_LABEL_DEF \\ 693 qpat_x_assum `L1 ++ [label L] ++ L2 = us` ((FULL_SIMP_TAC std_ss) o wrap o SYM) \\ 694 qpat_x_assum `TRACE E (L1 ++ [label L] ++ L2) E'` 695 (STRIP_ASSUME_TAC o (REWRITE_RULE [TRACE_APPEND_cases])) \\ 696 take [`u'`, `u`] \\ 697 IMP_RES_TAC TRACE_ONE >> ASM_REWRITE_TAC [] \\ 698 REWRITE_TAC [EPS_AND_TRACE, NO_LABEL_def] \\ 699 CONJ_TAC >| (* 2 sub-goals here *) 700 [ (* goal 2.1 (of 2) *) 701 Q.EXISTS_TAC `L1` >> ASM_REWRITE_TAC [], 702 (* goal 2.2 (of 2) *) 703 Q.EXISTS_TAC `L2` >> ASM_REWRITE_TAC [] ] ]); 704 705(* changed variables to P and P' *) 706val WEAK_TRANS_AND_TRACE' = store_thm ( 707 "WEAK_TRANS_AND_TRACE'", 708 ``!P u P'. WEAK_TRANS P u P' <=> ?acts. TRACE P acts P' /\ ~NULL acts /\ 709 if (u = tau) then NO_LABEL acts else UNIQUE_LABEL u acts``, 710 rpt GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 711 >- ( DISCH_TAC \\ 712 MATCH_MP_TAC WEAK_TRANS_TRACE2 >> ASM_REWRITE_TAC [] ) 713 >> rpt STRIP_TAC 714 >> Cases_on `u` 715 >> FULL_SIMP_TAC std_ss [Action_distinct_label, NO_LABEL_def] (* 2 sub-goals here *) 716 >| [ (* goal 1 (of 2) *) 717 REWRITE_TAC [WEAK_TRANS] \\ 718 Q.EXISTS_TAC `P` >> REWRITE_TAC [EPS_REFL] \\ 719 qpat_x_assum `TRACE P acts P'` (ASSUME_TAC o (ONCE_REWRITE_RULE [TRACE_cases1])) \\ 720 REV_FULL_SIMP_TAC list_ss [] \\ 721 Know `HD acts = tau` 722 >- ( Cases_on `HD acts` >- REWRITE_TAC [] \\ 723 qpat_x_assum `!l. ~MEM (label l) acts` (ASSUME_TAC o (Q.SPEC `x`)) \\ 724 qpat_x_assum `HD acts = label x` ((FULL_SIMP_TAC list_ss) o wrap o SYM) \\ 725 PROVE_TAC [CONS, MEM] ) \\ 726 DISCH_TAC >> FULL_SIMP_TAC list_ss [] \\ 727 Q.EXISTS_TAC `u` >> ASM_REWRITE_TAC [] \\ 728 REWRITE_TAC [EPS_AND_TRACE, NO_LABEL_def] \\ 729 Q.EXISTS_TAC `TL acts` >> ASM_REWRITE_TAC [] \\ 730 CCONTR_TAC >> FULL_SIMP_TAC bool_ss [] \\ 731 qpat_x_assum `!l. ~MEM (label l) acts` (MP_TAC o (Q.SPEC `l`)) \\ 732 Cases_on `acts` >- FULL_SIMP_TAC list_ss [] \\ 733 REWRITE_TAC [MEM] \\ 734 FULL_SIMP_TAC list_ss [], 735 (* goal 2 (of 2) *) 736 REWRITE_TAC [WEAK_TRANS] \\ 737 IMP_RES_TAC UNIQUE_LABEL_DEF \\ 738 qpat_x_assum `L1 ++ [label L] ++ L2 = acts` ((FULL_SIMP_TAC std_ss) o wrap o SYM) \\ 739 qpat_x_assum `TRACE P (L1 ++ [label L] ++ L2) P'` 740 (STRIP_ASSUME_TAC o (REWRITE_RULE [TRACE_APPEND_cases])) \\ 741 take [`u'`, `u`] \\ 742 IMP_RES_TAC TRACE_ONE >> ASM_REWRITE_TAC [] \\ 743 REWRITE_TAC [EPS_AND_TRACE, NO_LABEL_def] \\ 744 CONJ_TAC >| (* 2 sub-goals here *) 745 [ (* goal 2.1 (of 2) *) 746 Q.EXISTS_TAC `L1` >> ASM_REWRITE_TAC [], 747 (* goal 2.2 (of 2) *) 748 Q.EXISTS_TAC `L2` >> ASM_REWRITE_TAC [] ] ]); 749 750val _ = export_theory (); 751val _ = html_theory "Trace"; 752 753(* last updated: Oct 7, 2017 *) 754