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