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