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