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