1(* ===================================================================== *)
2(* File         : algebraScript.sml                                      *)
3(* DESCRIPTION  : Maximal trace semantics and transition semantics of a  *)
4(*                small process algebra.                                 *)
5(*                                                                       *)
6(* AUTHORS      : Juanito Camilleri and Tom Melham                       *)
7(* DATE         : 91.05.13                                               *)
8(* ===================================================================== *)
9
10(*
11  app load ["stringLib"];
12*)
13
14(* --------------------------------------------------------------------- *)
15(* Open a new theory and load the inductive definitions library and      *)
16(* other libraries.                                                      *)
17(* --------------------------------------------------------------------- *)
18
19open HolKernel Parse boolLib bossLib
20     listTheory IndDefRules IndDefLib stringLib;
21
22val _ = new_theory "algebra";
23
24
25(* ===================================================================== *)
26(* Syntax of a small process algebra                                     *)
27(* ===================================================================== *)
28
29(* --------------------------------------------------------------------- *)
30(* We use the recursive types package to define the syntax of a small    *)
31(* process algebra, with processes                                       *)
32(*                                                                       *)
33(*    agent  ::=   Nil                    [does nothing]                 *)
34(*               | Pre  label agent       [prefix agent with label]      *)
35(*               | Sum  agent agent       [nondeterministic choice]      *)
36(*               | Prod agent agent       [composition]                  *)
37(*                                                                       *)
38(* The different syntactic classes of processes are thus represented by  *)
39(* the constructors (constant functions):                                *)
40(*                                                                       *)
41(*  Nil:agent, Pre:label->agent->agent, Sum and Prod:agent->agent->agent *)
42(*                                                                       *)
43(* for the concrete data type :agent.  The type :label here is just an   *)
44(* abbreviation for :string.                                             *)
45(* --------------------------------------------------------------------- *)
46
47Type label = ���:string���
48
49Datatype: agent = Nil
50                | Pre label agent
51                | Sum agent agent
52                | Prod agent agent
53End
54
55
56(* ===================================================================== *)
57(* Definition of a maximal trace semantics for the process algebra.      *)
58(* ===================================================================== *)
59
60(* --------------------------------------------------------------------- *)
61(* Type abbreviation for traces.   These are just finite sequences of    *)
62(* labels, represented here by lists.                                    *)
63(* --------------------------------------------------------------------- *)
64
65val _ = type_abbrev("trace", ``:label list``);
66
67(* --------------------------------------------------------------------- *)
68(* Inductive definition of a trace relation MTRACE.  This is defined so  *)
69(* that MTRACE P A means A is the maximal trace of the process P. The    *)
70(* definition is done inductively by the rules given below.              *)
71(* --------------------------------------------------------------------- *)
72
73val (trules, tind, tcases) = Hol_reln
74     `MTRACE Nil []
75 /\   (!P A a. MTRACE P A ==> MTRACE (Pre a P) (a::A))
76 /\   (!P Q A. MTRACE P A ==> MTRACE (Sum P Q) A)
77 /\   (!P Q A. MTRACE Q A ==> MTRACE (Sum P Q) A)
78 /\   (!P Q A. MTRACE P A /\ MTRACE Q A ==> MTRACE (Prod P Q) A)`;
79
80
81val trulel = CONJUNCTS trules;
82
83(* --------------------------------------------------------------------- *)
84(* Stronger form of rule induction.                                      *)
85(* --------------------------------------------------------------------- *)
86
87val tsind = derive_strong_induction (trules,tind);
88
89(* --------------------------------------------------------------------- *)
90(* Definition of a terminal process: one with [] as a maximal trace.     *)
91(* --------------------------------------------------------------------- *)
92
93val TERMINAL_def =
94 Define
95   `TERMINAL P = MTRACE P []`;
96
97(* ===================================================================== *)
98(* Inductive definition of a labelled transition system.                 *)
99(* ===================================================================== *)
100
101(* --------------------------------------------------------------------- *)
102(* We now define a labelled transition relation TRANS P l Q to mean      *)
103(* there that process P can participate in action l and thereby evolve   *)
104(* into process Q.  The definition is done inductively, as usual.        *)
105(* --------------------------------------------------------------------- *)
106
107val (lrules, lind, lcases) = Hol_reln
108    `(!Q a. TRANS (Pre a Q) a Q)
109 /\  (!P P' Q a. TRANS P a P' ==> TRANS (Sum P Q) a P')
110 /\  (!P Q Q' a. TRANS Q a Q' ==> TRANS (Sum P Q) a Q')
111 /\  (!P P' Q Q' a. TRANS P a P' /\ TRANS Q a Q'
112                ==> TRANS (Prod P Q) a (Prod P' Q'))`;
113
114val lrulel = CONJUNCTS lrules;
115
116(* --------------------------------------------------------------------- *)
117(* Strong form of rule induction for TRANS.                              *)
118(* --------------------------------------------------------------------- *)
119
120val lsind = derive_strong_induction (lrules,lind);
121
122
123(* ===================================================================== *)
124(* Inductive definition of a trace transition system                     *)
125(* ===================================================================== *)
126
127(* --------------------------------------------------------------------- *)
128(* We now define a transition system that accumulates the trace of a     *)
129(* process.  This is essentially the reflexive-transitive closure of     *)
130(* TRANS, but with the label being a list of the labels from TRANS.      *)
131(* --------------------------------------------------------------------- *)
132
133val (Lrules, Lind, Lcases) = Hol_reln
134   `(!P. TRANSIT P [] P)
135/\  (!P P' B a Q. TRANS P a Q /\ TRANSIT Q B P' ==> TRANSIT P (a::B) P')`;
136
137val Lrulel = CONJUNCTS Lrules;
138
139(* --------------------------------------------------------------------- *)
140(* Strong form of rule induction for labelled (trace) transitions.       *)
141(* --------------------------------------------------------------------- *)
142
143val Lsind = derive_strong_induction (Lrules,Lind);
144
145(* ===================================================================== *)
146(* Theorem 1: Maximal trace semantics "agrees' with transition semantics *)
147(* ===================================================================== *)
148
149(* --------------------------------------------------------------------- *)
150(* Lemma 1 is to prove the following theorem:                            *)
151(*                                                                       *)
152(*    |- !P a Q. TRANS P a Q ==> !A. MTRACE Q A ==> MTRACE P (a::A)      *)
153(*                                                                       *)
154(* The proof is a straightforward rule induction on TRANS, followed by   *)
155(* a case analysis on MTRACE Q A when Q is a product (Prod), and then    *)
156(* completed by a simple search for the proof of the conclusion using    *)
157(* the tactic MTRACE_TAC.                                                *)
158(* --------------------------------------------------------------------- *)
159
160Theorem Lemma1[local]:
161  !P a Q. TRANS P a Q ==> !A. MTRACE Q A ==> MTRACE P (a::A)
162Proof
163  Induct_on ���TRANS��� >> RW_TAC std_ss [] >| [
164    METIS_TAC trulel,
165    METIS_TAC trulel,
166    METIS_TAC trulel,
167    qpat_x_assum ���MTRACE (PROD _ _) _���
168                 (strip_assume_tac o REWRITE_RULE [Once tcases]) >>
169    FULL_SIMP_TAC list_ss [] THEN RW_TAC list_ss [] THEN
170    METIS_TAC [trules]
171  ]
172QED
173
174(* --------------------------------------------------------------------- *)
175(* Theorem 1:  |- !P A Q. TRANSIT P A Q ==> TERMINAL Q ==> MTRACE P A    *)
176(*                                                                       *)
177(* This theorem shows that the trace semantics agrees with the           *)
178(* trace-transition semantics, in the sense that if we follow the        *)
179(* transitions of a process P until we reach a terminal process Q, that  *)
180(* is a process with an empty maximal trace, then we will have gone      *)
181(* through a maximal trace of P.                                         *)
182(* --------------------------------------------------------------------- *)
183
184Theorem Theorem1:
185   !P A Q. TRANSIT P A Q ==> TERMINAL Q ==> MTRACE P A
186Proof
187 REWRITE_TAC [TERMINAL_def] THEN
188 Induct_on ���TRANSIT��� THEN METIS_TAC [Lemma1]
189QED
190
191
192(* --------------------------------------------------------------------- *)
193(* Corollary 1: !P A Q. TRANSIT P A Nil ==> MTRACE P A                   *)
194(*                                                                       *)
195(* Note that the converse does not hold.                                 *)
196(* --------------------------------------------------------------------- *)
197
198Theorem Corollary1:   !P A. TRANSIT P A Nil ==> MTRACE P A
199Proof METIS_TAC (TERMINAL_def::Theorem1::trulel)
200QED
201
202
203(* ===================================================================== *)
204(* Theorem 2: Transition semantics "agrees" with maximal trace semantics *)
205(* ===================================================================== *)
206
207(* --------------------------------------------------------------------- *)
208(* Lemma 2 shows that the trace of a product is just the trace of its    *)
209(* two components in the relation TRANSIT. The proof is a sraightfoward  *)
210(* structural induction on the list A, with simplification using the     *)
211(* case analysis theorem for TRANSIT.                                    *)
212(* --------------------------------------------------------------------- *)
213
214val Lemma2 = Q.prove
215(`!A P Q P' Q'.
216    TRANSIT P A Q /\ TRANSIT P' A Q' ==> TRANSIT (Prod P P') A (Prod Q Q')`,
217 Induct THEN PURE_ONCE_REWRITE_TAC [Lcases] THEN
218  RW_TAC std_ss [] THEN METIS_TAC lrulel);
219
220(* --------------------------------------------------------------------- *)
221(* Theorem 2:  |- !P A. MTRACE P A ==> ?Q. TRANSIT P A Q /\ TERMINAL Q   *)
222(*                                                                       *)
223(* This theorem shows that the transition semantics "agrees" with the    *)
224(* trace semantics, in the sense that every maximal trace A leads in the *)
225(* transition semantics to a terminal process.  The proof proceeds by    *)
226(* rule induction on MTRACE P A, followed by semi-automatic search for   *)
227(* proofs of TRANSIT P A Q and TERMINAL Q.  The user supplies a witness  *)
228(* for any existential goals that arise.  There is also a case analysis  *)
229(* on the TRANSIT assumption in the Sum cases, there being different     *)
230(* witnesses required for the two TRANSIT rules.                         *)
231(* --------------------------------------------------------------------- *)
232
233Theorem Theorem2:
234  !P A. MTRACE P A ==> ?Q. TRANSIT P A Q /\ TERMINAL Q
235Proof
236  Induct_on ���MTRACE��� >> RW_TAC std_ss [] >| [
237    METIS_TAC (TERMINAL_def::Lrulel@trulel@lrulel),
238    METIS_TAC (Lrulel@trulel@lrulel),
239    RULE_ASSUM_TAC (REWRITE_RULE [Once Lcases])
240    THEN RW_TAC list_ss []
241    THEN METIS_TAC (TERMINAL_def::Lrulel@trulel@lrulel),
242    RULE_ASSUM_TAC (REWRITE_RULE [Once Lcases])
243    THEN RW_TAC list_ss []
244    THEN METIS_TAC (TERMINAL_def::Lrulel@trulel@lrulel),
245    METIS_TAC (Lemma2::TERMINAL_def::Lrulel@trulel@lrulel)
246  ]
247QED
248
249
250
251(* ===================================================================== *)
252(* Theorem3: The transition and maximal trace semantics "agree".         *)
253(* ===================================================================== *)
254
255val Theorem3 = Q.store_thm
256("Theorem3",
257 `!P A. MTRACE P A = ?Q. TRANSIT P A Q /\ TERMINAL Q`,
258 METIS_TAC [Theorem1,Theorem2]);
259
260
261(* ===================================================================== *)
262(* Definitions of notions of equivalence                                 *)
263(* ===================================================================== *)
264
265(* --------------------------------------------------------------------- *)
266(* Maximal trace equivalence. Two processes are maximal trace equivalent *)
267(* if they have the same maximal traces.                                 *)
268(* --------------------------------------------------------------------- *)
269
270val _ = set_fixity "MEQUIV" (Infixl 701);
271val _ = set_fixity "BEQUIV" (Infixl 701);
272
273val MEQUIV_def =
274 Define
275  `(P MEQUIV Q) = !A. MTRACE P A = MTRACE Q A`;
276
277(* --------------------------------------------------------------------- *)
278(* Bisimulation equivalence.  A binary relation s:agent->agent->bool is  *)
279(* a simulation if s P Q implies that any transitions that P can do can  *)
280(* also be done by Q such that the corresponding successive pairs of     *)
281(* agents remain in the relation s.  Equivalence is then defined to be   *)
282(* the bisimulation (simulation whose inverse is also a simulation).     *)
283(* --------------------------------------------------------------------- *)
284
285val SIM_def =
286 Define
287   `SIM s = !P Q. s P Q ==>
288                   !a P'. TRANS P a P' ==>
289                           ?Q'. TRANS Q a Q' /\ s P' Q'`;
290
291val BEQUIV_def =
292 Define
293   `(P BEQUIV Q) = ?s. SIM s /\ s P Q /\ SIM(\x y. s y x)`;
294
295
296(* --------------------------------------------------------------------- *)
297(* End of example.                                                       *)
298(* --------------------------------------------------------------------- *)
299
300val _ = export_theory();
301