# HG changeset patch # User wenzelm # Date 1435311862 -7200 # Node ID 0318b43ee95c5e3333b85a5322f3f6d52b1b8f14 # Parent 1d31e3a503739e051005632562f7b96a08c0ad50 more symbols; diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Action.thy Fri Jun 26 11:44:22 2015 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/TLA/Action.thy +(* Title: HOL/TLA/Action.thy Author: Stephan Merz Copyright: 1998 University of Munich *) @@ -66,9 +66,9 @@ defs square_def: "ACT [A]_v == ACT (A | unchanged v)" - angle_def: "ACT _v == ACT (A & ~ unchanged v)" + angle_def: "ACT _v == ACT (A & \ unchanged v)" - enabled_def: "s |= Enabled A == EX u. (s,u) |= A" + enabled_def: "s |= Enabled A == \u. (s,u) |= A" (* The following assertion specializes "intI" for any world type @@ -76,7 +76,7 @@ *) lemma actionI [intro!]: - assumes "!!s t. (s,t) |= A" + assumes "\s t. (s,t) |= A" shows "|- A" apply (rule assms intI prod.induct)+ done @@ -87,11 +87,11 @@ lemma pr_rews [int_rewrite]: "|- (#c)` = #c" - "!!f. |- f` = f" - "!!f. |- f` = f" - "!!f. |- f` = f" - "|- (! x. P x)` = (! x. (P x)`)" - "|- (? x. P x)` = (? x. (P x)`)" + "\f. |- f` = f" + "\f. |- f` = f" + "\f. |- f` = f" + "|- (\x. P x)` = (\x. (P x)`)" + "|- (\x. P x)` = (\x. (P x)`)" by (rule actionI, unfold unl_after intensional_rews, rule refl)+ @@ -137,7 +137,7 @@ lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v" by (simp add: square_def) - + lemma squareE [elim]: "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)" apply (unfold square_def action_rews) @@ -145,34 +145,34 @@ apply simp_all done -lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v" +lemma squareCI [intro]: "[| v t \ v s ==> A (s,t) |] ==> (s,t) |= [A]_v" apply (unfold square_def action_rews) apply (rule disjCI) apply (erule (1) meta_mp) done -lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= _v" +lemma angleI [intro]: "\s t. [| A (s,t); v t \ v s |] ==> (s,t) |= _v" by (simp add: angle_def) -lemma angleE [elim]: "[| (s,t) |= _v; [| A (s,t); v t ~= v s |] ==> R |] ==> R" +lemma angleE [elim]: "[| (s,t) |= _v; [| A (s,t); v t \ v s |] ==> R |] ==> R" apply (unfold angle_def action_rews) apply (erule conjE) apply simp done lemma square_simulation: - "!!f. [| |- unchanged f & ~B --> unchanged g; - |- A & ~unchanged g --> B + "\f. [| |- unchanged f & \B --> unchanged g; + |- A & \unchanged g --> B |] ==> |- [A]_f --> [B]_g" apply clarsimp apply (erule squareE) apply (auto simp add: square_def) done -lemma not_square: "|- (~ [A]_v) = <~A>_v" +lemma not_square: "|- (\ [A]_v) = <\A>_v" by (auto simp: square_def angle_def) -lemma not_angle: "|- (~ _v) = [~A]_v" +lemma not_angle: "|- (\ _v) = [\A]_v" by (auto simp: square_def angle_def) @@ -181,13 +181,13 @@ lemma enabledI: "|- A --> $Enabled A" by (auto simp add: enabled_def) -lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q" +lemma enabledE: "[| s |= Enabled A; \u. A (s,u) ==> Q |] ==> Q" apply (unfold enabled_def) apply (erule exE) apply simp done -lemma notEnabledD: "|- ~$Enabled G --> ~ G" +lemma notEnabledD: "|- \$Enabled G --> \ G" by (auto simp add: enabled_def) (* Monotonicity *) @@ -203,7 +203,7 @@ (* stronger variant *) lemma enabled_mono2: assumes min: "s |= Enabled F" - and maj: "!!t. F (s,t) ==> G (s,t)" + and maj: "\t. F (s,t) ==> G (s,t)" shows "s |= Enabled G" apply (rule min [THEN enabledE]) apply (rule enabledI [action_use]) @@ -239,13 +239,13 @@ apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+ done -lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))" +lemma enabled_ex: "|- Enabled (\x. F x) = (\x. Enabled (F x))" by (force simp add: enabled_def) (* A rule that combines enabledI and baseE, but generates fewer instantiations *) lemma base_enabled: - "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A" + "[| basevars vs; \c. \u. vs u = c --> A(s,u) |] ==> s |= Enabled A" apply (erule exE) apply (erule baseE) apply (rule enabledI [action_use]) diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Buffer/Buffer.thy --- a/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Buffer/Buffer.thy Fri Jun 26 11:44:22 2015 +0200 @@ -21,24 +21,24 @@ defs BInit_def: "BInit ic q oc == PRED q = #[]" - Enq_def: "Enq ic q oc == ACT (ic$ ~= $ic) + Enq_def: "Enq ic q oc == ACT (ic$ \ $ic) & (q$ = $q @ [ ic$ ]) & (oc$ = $oc)" - Deq_def: "Deq ic q oc == ACT ($q ~= #[]) + Deq_def: "Deq ic q oc == ACT ($q \ #[]) & (oc$ = hd< $q >) & (q$ = tl< $q >) & (ic$ = $ic)" Next_def: "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)" IBuffer_def: "IBuffer ic q oc == TEMP Init (BInit ic q oc) - & [][Next ic q oc]_(ic,q,oc) + & \[Next ic q oc]_(ic,q,oc) & WF(Deq ic q oc)_(ic,q,oc)" - Buffer_def: "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)" + Buffer_def: "Buffer ic oc == TEMP (\\q. IBuffer ic q oc)" (* ---------------------------- Data lemmas ---------------------------- *) (*FIXME: move to theory List? Maybe as (tl xs = xs) = (xs = [])"?*) -lemma tl_not_self [simp]: "xs ~= [] ==> tl xs ~= xs" +lemma tl_not_self [simp]: "xs \ [] ==> tl xs \ xs" by (auto simp: neq_Nil_conv) @@ -52,14 +52,14 @@ (* Enabling condition for dequeue -- NOT NEEDED *) lemma Deq_enabled: - "!!q. basevars (ic,q,oc) ==> |- Enabled (_(ic,q,oc)) = (q ~= #[])" + "\q. basevars (ic,q,oc) ==> |- Enabled (_(ic,q,oc)) = (q \ #[])" apply (unfold Deq_visible [temp_rewrite]) apply (force elim!: base_enabled [temp_use] enabledE [temp_use] simp: Deq_def) done (* For the left-to-right implication, we don't need the base variable stuff *) lemma Deq_enabledE: - "|- Enabled (_(ic,q,oc)) --> (q ~= #[])" + "|- Enabled (_(ic,q,oc)) --> (q \ #[])" apply (unfold Deq_visible [temp_rewrite]) apply (auto elim!: enabledE simp add: Deq_def) done diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Buffer/DBuffer.thy --- a/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Buffer/DBuffer.thy Fri Jun 26 11:44:22 2015 +0200 @@ -37,7 +37,7 @@ & (out$ = $out)" and DBNext_def: "DBNext == ACT (DBEnq | DBDeq | DBPass)" and DBuffer_def: "DBuffer == TEMP Init DBInit - & [][DBNext]_(inp,mid,out,q1,q2) + & \[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)" @@ -72,7 +72,7 @@ done lemma DBDeq_enabled: - "|- Enabled (_(inp,mid,out,q1,q2)) = (q2 ~= #[])" + "|- Enabled (_(inp,mid,out,q1,q2)) = (q2 \ #[])" apply (unfold DBDeq_visible [action_rewrite]) apply (force intro!: DB_base [THEN base_enabled, temp_use] elim!: enabledE simp: angle_def DBDeq_def Deq_def) @@ -82,7 +82,7 @@ by (auto simp: angle_def DBPass_def Deq_def) lemma DBPass_enabled: - "|- Enabled (_(inp,mid,out,q1,q2)) = (q1 ~= #[])" + "|- Enabled (_(inp,mid,out,q1,q2)) = (q1 \ #[])" apply (unfold DBPass_visible [action_rewrite]) apply (force intro!: DB_base [THEN base_enabled, temp_use] elim!: enabledE simp: angle_def DBPass_def Deq_def) @@ -90,15 +90,15 @@ (* The plan for proving weak fairness at the higher level is to prove - (0) DBuffer => (Enabled (Deq inp qc out) ~> (Deq inp qc out)) + (0) DBuffer => (Enabled (Deq inp qc out) \ (Deq inp qc out)) which is in turn reduced to the two leadsto conditions - (1) DBuffer => (Enabled (Deq inp qc out) ~> q2 ~= []) - (2) DBuffer => (q2 ~= [] ~> DBDeq) + (1) DBuffer => (Enabled (Deq inp qc out) \ q2 \ []) + (2) DBuffer => (q2 \ [] \ DBDeq) and the fact that DBDeq implies _(inp,qc,out) - (and therefore DBDeq ~> _(inp,qc,out) trivially holds). + (and therefore DBDeq \ _(inp,qc,out) trivially holds). Condition (1) is reduced to - (1a) DBuffer => (qc ~= [] /\ q2 = [] ~> q2 ~= []) + (1a) DBuffer => (qc \ [] /\ q2 = [] \ q2 \ []) by standard leadsto rules (leadsto_classical) and rule Deq_enabledE. Both (1a) and (2) are proved from DBuffer's WF conditions by standard @@ -109,8 +109,8 @@ *) (* Condition (1a) *) -lemma DBFair_1a: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) - --> (qc ~= #[] & q2 = #[] ~> q2 ~= #[])" +lemma DBFair_1a: "|- \[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) + --> (qc \ #[] & q2 = #[] \ q2 \ #[])" apply (rule WF1) apply (force simp: db_defs) apply (force simp: angle_def DBPass_def) @@ -118,8 +118,8 @@ done (* Condition (1) *) -lemma DBFair_1: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) - --> (Enabled (_(inp,qc,out)) ~> q2 ~= #[])" +lemma DBFair_1: "|- \[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) + --> (Enabled (_(inp,qc,out)) \ q2 \ #[])" apply clarsimp apply (rule leadsto_classical [temp_use]) apply (rule DBFair_1a [temp_use, THEN LatticeTransitivity [temp_use]]) @@ -130,8 +130,8 @@ done (* Condition (2) *) -lemma DBFair_2: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2) - --> (q2 ~= #[] ~> DBDeq)" +lemma DBFair_2: "|- \[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2) + --> (q2 \ #[] \ DBDeq)" apply (rule WF_leadsto) apply (force simp: DBDeq_enabled [temp_use]) apply (force simp: angle_def) @@ -139,7 +139,7 @@ done (* High-level fairness *) -lemma DBFair: "|- [][DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) +lemma DBFair: "|- \[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2) --> WF(Deq inp qc out)_(inp,qc,out)" apply (auto simp del: qc_def intro!: leadsto_WF [temp_use] diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Inc/Inc.thy --- a/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Inc/Inc.thy Fri Jun 26 11:44:22 2015 +0200 @@ -48,7 +48,7 @@ InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0" and M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y" and M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x" and - Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y) + Phi_def: "Phi == TEMP Init InitPhi & \[M1 | M2]_(x,y) & WF(M1)_(x,y) & WF(M2)_(x,y)" and (* definitions for low-level program *) @@ -69,7 +69,7 @@ N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)" and N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)" and Psi_def: "Psi == TEMP Init InitPsi - & [][N1 | N2]_(x,y,sem,pc1,pc2) + & \[N1 | N2]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)" and @@ -110,7 +110,7 @@ lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$" by (auto simp: PsiInv_defs) -lemma PsiInv: "|- Psi --> []PsiInv" +lemma PsiInv: "|- Psi --> \PsiInv" apply (invariant simp: Psi_def) apply (force simp: PsiInv_Init [try_rewrite] Init_def) apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite] @@ -123,7 +123,7 @@ More realistic examples require user guidance anyway. *) -lemma "|- Psi --> []PsiInv" +lemma "|- Psi --> \PsiInv" by (auto_invariant simp: PsiInv_defs Psi_defs) @@ -132,7 +132,7 @@ lemma Init_sim: "|- Psi --> Init InitPhi" by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def) -lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)" +lemma Step_sim: "|- Psi --> \[M1 | M2]_(x,y)" by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use]) @@ -154,7 +154,7 @@ the auxiliary lemmas are very similar. *) -lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)" +lemma Stuck_at_b: "|- \[(N1 | N2) & \ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)" by (auto elim!: Stable squareE simp: Psi_defs) lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (_(x,y,sem,pc1,pc2))" @@ -166,14 +166,14 @@ done lemma g1_leadsto_a1: - "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True - --> (pc1 = #g ~> pc1 = #a)" + "|- \[(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \#True + --> (pc1 = #g \ pc1 = #a)" apply (rule SF1) apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *}) apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *}) - (* reduce |- []A --> <>Enabled B to |- A --> Enabled B *) + (* reduce |- \A --> \Enabled B to |- A --> Enabled B *) apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use] dest!: STL2_gen [temp_use] simp: Init_def) done @@ -188,8 +188,8 @@ done lemma g2_leadsto_a2: - "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True - --> (pc2 = #g ~> pc2 = #a)" + "|- \[(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \#True + --> (pc2 = #g \ pc2 = #a)" apply (rule SF1) apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *}) apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) @@ -207,8 +207,8 @@ done lemma b2_leadsto_g2: - "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True - --> (pc2 = #b ~> pc2 = #g)" + "|- \[(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \#True + --> (pc2 = #b \ pc2 = #g)" apply (rule SF1) apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *}) @@ -220,18 +220,18 @@ (* Combine above lemmas: the second component will eventually reach pc2 = a *) lemma N2_leadsto_a: - "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True - --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)" + "|- \[(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \#True + --> (pc2 = #a | pc2 = #b | pc2 = #g \ pc2 = #a)" apply (auto intro!: LatticeDisjunctionIntro [temp_use]) apply (rule LatticeReflexivity [temp_use]) apply (rule LatticeTransitivity [temp_use]) apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use]) done -(* Get rid of disjunction on the left-hand side of ~> above. *) +(* Get rid of disjunction on the left-hand side of \ above. *) lemma N2_live: - "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) - --> <>(pc2 = #a)" + "|- \[(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) + --> \(pc2 = #a)" apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]]) apply (case_tac "pc2 (st1 sigma)") apply auto @@ -249,9 +249,9 @@ done lemma a1_leadsto_b1: - "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2)) - & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2) - --> (pc1 = #a ~> pc1 = #b)" + "|- \($PsiInv & [(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2)) + & SF(N1)_(x,y,sem,pc1,pc2) & \ SF(N2)_(x,y,sem,pc1,pc2) + --> (pc1 = #a \ pc1 = #b)" apply (rule SF1) apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *}) apply (tactic @@ -263,9 +263,9 @@ (* Combine the leadsto properties for N1: it will arrive at pc1 = b *) -lemma N1_leadsto_b: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2)) - & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2) - --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)" +lemma N1_leadsto_b: "|- \($PsiInv & [(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2)) + & SF(N1)_(x,y,sem,pc1,pc2) & \ SF(N2)_(x,y,sem,pc1,pc2) + --> (pc1 = #b | pc1 = #g | pc1 = #a \ pc1 = #b)" apply (auto intro!: LatticeDisjunctionIntro [temp_use]) apply (rule LatticeReflexivity [temp_use]) apply (rule LatticeTransitivity [temp_use]) @@ -273,9 +273,9 @@ simp: split_box_conj) done -lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2)) - & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2) - --> <>(pc1 = #b)" +lemma N1_live: "|- \($PsiInv & [(N1 | N2) & \beta1]_(x,y,sem,pc1,pc2)) + & SF(N1)_(x,y,sem,pc1,pc2) & \ SF(N2)_(x,y,sem,pc1,pc2) + --> \(pc1 = #b)" apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]]) apply (case_tac "pc1 (st1 sigma)") apply auto @@ -291,8 +291,8 @@ (* Now assemble the bits and pieces to prove that Psi is fair. *) -lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2)) - & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2) +lemma Fair_M1_lemma: "|- \($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2)) + & SF(N1)_(x,y,sem,pc1,pc2) & \SF(N2)_(x,y,sem,pc1,pc2) --> SF(M1)_(x,y)" apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2) (* action premises *) diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Init.thy --- a/src/HOL/TLA/Init.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Init.thy Fri Jun 26 11:44:22 2015 +0200 @@ -36,9 +36,9 @@ Init_def: "sigma |= Init F == (first_world sigma) |= F" defs (overloaded) - fw_temp_def: "first_world == %sigma. sigma" + fw_temp_def: "first_world == \sigma. sigma" fw_stp_def: "first_world == st1" - fw_act_def: "first_world == %sigma. (st1 sigma, st2 sigma)" + fw_act_def: "first_world == \sigma. (st1 sigma, st2 sigma)" lemma const_simps [int_rewrite, simp]: "|- (Init #True) = #True" @@ -46,14 +46,14 @@ by (auto simp: Init_def) lemma Init_simps1 [int_rewrite]: - "!!F. |- (Init ~F) = (~ Init F)" + "\F. |- (Init \F) = (\ Init F)" "|- (Init (P --> Q)) = (Init P --> Init Q)" "|- (Init (P & Q)) = (Init P & Init Q)" "|- (Init (P | Q)) = (Init P | Init Q)" "|- (Init (P = Q)) = ((Init P) = (Init Q))" - "|- (Init (!x. F x)) = (!x. (Init F x))" - "|- (Init (? x. F x)) = (? x. (Init F x))" - "|- (Init (?! x. F x)) = (?! x. (Init F x))" + "|- (Init (\x. F x)) = (\x. (Init F x))" + "|- (Init (\x. F x)) = (\x. (Init F x))" + "|- (Init (\!x. F x)) = (\!x. (Init F x))" by (auto simp: Init_def) lemma Init_stp_act: "|- (Init $P) = (Init P)" diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Intensional.thy Fri Jun 26 11:44:22 2015 +0200 @@ -39,7 +39,7 @@ "" :: "var => lift" ("_") "_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999) "" :: "lift => lift" ("'(_')") - "_lambda" :: "[idts, 'a] => lift" ("(3%_./ _)" [0, 3] 3) + "_lambda" :: "[idts, 'a] => lift" ("(3\_./ _)" [0, 3] 3) "_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3) "" :: "lift => liftargs" ("_") "_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _") @@ -155,29 +155,17 @@ "_liftMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) -syntax (HTML output) - "_liftNeq" :: "[lift, lift] => lift" (infixl "\" 50) - "_liftNot" :: "lift => lift" ("\ _" [40] 40) - "_liftAnd" :: "[lift, lift] => lift" (infixr "\" 35) - "_liftOr" :: "[lift, lift] => lift" (infixr "\" 30) - "_RAll" :: "[idts, lift] => lift" ("(3\_./ _)" [0, 10] 10) - "_REx" :: "[idts, lift] => lift" ("(3\_./ _)" [0, 10] 10) - "_REx1" :: "[idts, lift] => lift" ("(3\!_./ _)" [0, 10] 10) - "_liftLeq" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) - "_liftMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) - "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) - defs - Valid_def: "|- A == ALL w. w |= A" + Valid_def: "|- A == \w. w |= A" unl_con: "LIFT #c w == c" unl_lift: "lift f x w == f (x w)" unl_lift2: "LIFT f w == f (x w) (y w)" unl_lift3: "LIFT f w == f (x w) (y w) (z w)" - unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)" - unl_Rex: "w |= EX x. A x == EX x. (w |= A x)" - unl_Rex1: "w |= EX! x. A x == EX! x. (w |= A x)" + unl_Rall: "w |= \x. A x == \x. (w |= A x)" + unl_Rex: "w |= \x. A x == \ x. (w |= A x)" + unl_Rex1: "w |= \!x. A x == \!x. (w |= A x)" subsection {* Lemmas and tactics for "intensional" logics. *} @@ -192,7 +180,7 @@ apply (erule spec) done -lemma intI [intro!]: "(!!w. w |= A) ==> |- A" +lemma intI [intro!]: "(\w. w |= A) ==> |- A" apply (unfold Valid_def) apply (rule allI) apply (erule meta_spec) @@ -207,21 +195,21 @@ lemma int_simps: "|- (x=x) = #True" - "|- (~#True) = #False" "|- (~#False) = #True" "|- (~~ P) = P" - "|- ((~P) = P) = #False" "|- (P = (~P)) = #False" - "|- (P ~= Q) = (P = (~Q))" + "|- (\#True) = #False" "|- (\#False) = #True" "|- (\\ P) = P" + "|- ((\P) = P) = #False" "|- (P = (\P)) = #False" + "|- (P \ Q) = (P = (\Q))" "|- (#True=P) = P" "|- (P=#True) = P" "|- (#True --> P) = P" "|- (#False --> P) = #True" "|- (P --> #True) = #True" "|- (P --> P) = #True" - "|- (P --> #False) = (~P)" "|- (P --> ~P) = (~P)" + "|- (P --> #False) = (\P)" "|- (P --> \P) = (\P)" "|- (P & #True) = P" "|- (#True & P) = P" "|- (P & #False) = #False" "|- (#False & P) = #False" - "|- (P & P) = P" "|- (P & ~P) = #False" "|- (~P & P) = #False" + "|- (P & P) = P" "|- (P & \P) = #False" "|- (\P & P) = #False" "|- (P | #True) = #True" "|- (#True | P) = #True" "|- (P | #False) = P" "|- (#False | P) = P" - "|- (P | P) = P" "|- (P | ~P) = #True" "|- (~P | P) = #True" - "|- (! x. P) = P" "|- (? x. P) = P" - "|- (~Q --> ~P) = (P --> Q)" + "|- (P | P) = P" "|- (P | \P) = #True" "|- (\P | P) = #True" + "|- (\x. P) = P" "|- (\x. P) = P" + "|- (\Q --> \P) = (P --> Q)" "|- (P|Q --> R) = ((P-->R)&(Q-->R))" apply (unfold Valid_def intensional_rews) apply blast+ @@ -296,10 +284,10 @@ attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *} -lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)" +lemma Not_Rall: "|- (\(\x. F x)) = (\x. \F x)" by (simp add: Valid_def) -lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)" +lemma Not_Rex: "|- (\ (\x. F x)) = (\x. \ F x)" by (simp add: Valid_def) end diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/MemClerk.thy --- a/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/MemClerk.thy Fri Jun 26 11:44:22 2015 +0200 @@ -16,7 +16,7 @@ definition (* state predicates *) MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" - where "MClkInit rcv cst p = PRED (cst!p = #clkA & ~Calling rcv p)" + where "MClkInit rcv cst p = PRED (cst!p = #clkA & \Calling rcv p)" definition (* actions *) @@ -39,7 +39,7 @@ definition MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" where "MClkReply send rcv cst p = ACT - ~$Calling rcv p + \$Calling rcv p & $(cst!p) = #clkB & Return send p MClkReplyVal> & (cst!p)$ = #clkA @@ -57,13 +57,13 @@ MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" where "MClkIPSpec send rcv cst p = TEMP Init MClkInit rcv cst p - & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) + & \[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p) & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)" definition MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" - where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)" + where "MClkISpec send rcv cst = TEMP (\p. MClkIPSpec send rcv cst p)" lemmas MC_action_defs = MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def @@ -73,17 +73,17 @@ (* The Clerk engages in an action for process p only if there is an outstanding, unanswered call for that process. *) -lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p" +lemma MClkidle: "|- \$Calling send p & $(cst!p) = #clkA --> \MClkNext send rcv cst p" by (auto simp: Return_def MC_action_defs) -lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p" +lemma MClkbusy: "|- $Calling rcv p --> \MClkNext send rcv cst p" by (auto simp: Call_def MC_action_defs) (* Enabledness of actions *) -lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> - |- Calling send p & ~Calling rcv p & cst!p = #clkA +lemma MClkFwd_enabled: "\p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> + |- Calling send p & \Calling rcv p & cst!p = #clkA --> Enabled (MClkFwd send rcv cst p)" by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] @@ -97,8 +97,8 @@ _(cst!p, rtrner send!p, caller rcv!p)" by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use]) -lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> - |- Calling send p & ~Calling rcv p & cst!p = #clkB +lemma MClkReply_enabled: "\p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> + |- Calling send p & \Calling rcv p & cst!p = #clkB --> Enabled (_(cst!p, rtrner send!p, caller rcv!p))" apply (tactic {* action_simp_tac @{context} [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *}) @@ -107,7 +107,7 @@ [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) done -lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p" +lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> \MClkRetry send rcv cst p" by (auto simp: MClkReply_def MClkRetry_def) end diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/Memory.thy --- a/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/Memory.thy Fri Jun 26 11:44:22 2015 +0200 @@ -63,31 +63,31 @@ #l : #MemLoc & ((rs!p)$ = $(mm!l))" (* a read that raises BadArg *) BadRead_def: "BadRead mm rs p l == ACT - #l ~: #MemLoc & ((rs!p)$ = #BadArg)" + #l \ #MemLoc & ((rs!p)$ = #BadArg)" (* the read action with l visible *) ReadInner_def: "ReadInner ch mm rs p l == ACT $(RdRequest ch p l) & (GoodRead mm rs p l | BadRead mm rs p l) & unchanged (rtrner ch ! p)" (* the read action with l quantified *) - Read_def: "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)" + Read_def: "Read ch mm rs p == ACT (\l. ReadInner ch mm rs p l)" (* similar definitions for the write action *) GoodWrite_def: "GoodWrite mm rs p l v == ACT #l : #MemLoc & #v : #MemVal & ((mm!l)$ = #v) & ((rs!p)$ = #OK)" BadWrite_def: "BadWrite mm rs p l v == ACT - ~ (#l : #MemLoc & #v : #MemVal) + \ (#l : #MemLoc & #v : #MemVal) & ((rs!p)$ = #BadArg) & unchanged (mm!l)" WriteInner_def: "WriteInner ch mm rs p l v == ACT $(WrRequest ch p l v) & (GoodWrite mm rs p l v | BadWrite mm rs p l v) & unchanged (rtrner ch ! p)" - Write_def: "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)" + Write_def: "Write ch mm rs p l == ACT (\v. WriteInner ch mm rs p l v)" (* the return action *) MemReturn_def: "MemReturn ch rs p == ACT - ( ($(rs!p) ~= #NotAResult) + ( ($(rs!p) \ #NotAResult) & ((rs!p)$ = #NotAResult) & Return ch p (rs!p))" @@ -99,33 +99,33 @@ (* next-state relations for reliable / unreliable memory *) RNext_def: "RNext ch mm rs p == ACT ( Read ch mm rs p - | (EX l. Write ch mm rs p l) + | (\l. Write ch mm rs p l) | MemReturn ch rs p)" UNext_def: "UNext ch mm rs p == ACT (RNext ch mm rs p | MemFail ch rs p)" RPSpec_def: "RPSpec ch mm rs p == TEMP Init(PInit rs p) - & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) + & \[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" UPSpec_def: "UPSpec ch mm rs p == TEMP Init(PInit rs p) - & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) + & \[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" MSpec_def: "MSpec ch mm rs l == TEMP Init(MInit mm l) - & [][ EX p. Write ch mm rs p l ]_(mm!l)" + & \[ \p. Write ch mm rs p l ]_(mm!l)" IRSpec_def: "IRSpec ch mm rs == TEMP - (ALL p. RPSpec ch mm rs p) - & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)" + (\p. RPSpec ch mm rs p) + & (\l. #l : #MemLoc --> MSpec ch mm rs l)" IUSpec_def: "IUSpec ch mm rs == TEMP - (ALL p. UPSpec ch mm rs p) - & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)" + (\p. UPSpec ch mm rs p) + & (\l. #l : #MemLoc --> MSpec ch mm rs l)" - RSpec_def: "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)" - USpec_def: "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)" + RSpec_def: "RSpec ch rs == TEMP (\\mm. IRSpec ch mm rs)" + USpec_def: "USpec ch == TEMP (\\mm rs. IUSpec ch mm rs)" MemInv_def: "MemInv mm l == PRED #l : #MemLoc --> mm!l : #MemVal" @@ -146,15 +146,15 @@ by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE) (* The memory spec implies the memory invariant *) -lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)" +lemma MemoryInvariant: "|- MSpec ch mm rs l --> \(MemInv mm l)" by (auto_invariant simp: RM_temp_defs RM_action_defs) (* The invariant is trivial for non-locations *) -lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)" +lemma NonMemLocInvariant: "|- #l \ #MemLoc --> \(MemInv mm l)" by (auto simp: MemInv_def intro!: necT [temp_use]) lemma MemoryInvariantAll: - "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))" + "|- (\l. #l : #MemLoc --> MSpec ch mm rs l) --> (\l. \(MemInv mm l))" apply clarify apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use]) done @@ -164,7 +164,7 @@ We need this only for the reliable memory. *) -lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p" +lemma Memoryidle: "|- \$(Calling ch p) --> \ RNext ch mm rs p" by (auto simp: Return_def RM_action_defs) (* Enabledness conditions *) @@ -172,8 +172,8 @@ lemma MemReturn_change: "|- MemReturn ch rs p --> _(rtrner ch ! p, rs!p)" by (force simp: MemReturn_def angle_def) -lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==> - |- Calling ch p & (rs!p ~= #NotAResult) +lemma MemReturn_enabled: "\p. basevars (rtrner ch ! p, rs!p) ==> + |- Calling ch p & (rs!p \ #NotAResult) --> Enabled (_(rtrner ch ! p, rs!p))" apply (tactic {* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *}) @@ -182,14 +182,14 @@ @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) done -lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==> +lemma ReadInner_enabled: "\p. basevars (rtrner ch ! p, rs!p) ==> |- Calling ch p & (arg = #(read l)) --> Enabled (ReadInner ch mm rs p l)" apply (case_tac "l : MemLoc") apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def intro!: exI elim!: base_enabled [temp_use])+ done -lemma WriteInner_enabled: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==> +lemma WriteInner_enabled: "\p. basevars (mm!l, rtrner ch ! p, rs!p) ==> |- Calling ch p & (arg = #(write l v)) --> Enabled (WriteInner ch mm rs p l v)" apply (case_tac "l:MemLoc & v:MemVal") @@ -197,18 +197,18 @@ intro!: exI elim!: base_enabled [temp_use])+ done -lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult" +lemma ReadResult: "|- Read ch mm rs p & (\l. $(MemInv mm l)) --> (rs!p)` \ #NotAResult" by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def) -lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult" +lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` \ #NotAResult" by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def) -lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p - --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)" +lemma ReturnNotReadWrite: "|- (\l. $MemInv mm l) & MemReturn ch rs p + --> \ Read ch mm rs p & (\l. \ Write ch mm rs p l)" by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use]) lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l) - & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l)) + & Enabled (Read ch mm rs p | (\l. Write ch mm rs p l)) --> Enabled (_(rtrner ch ! p, rs!p))" by (force simp: RNext_def angle_def elim!: enabled_mono2 dest: ReadResult [temp_use] WriteResult [temp_use]) @@ -217,8 +217,8 @@ (* Combine previous lemmas: the memory can make a visible step if there is an outstanding call for which no result has been produced. *) -lemma RNext_enabled: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==> - |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l) +lemma RNext_enabled: "\p. \l. basevars (mm!l, rtrner ch!p, rs!p) ==> + |- (rs!p = #NotAResult) & Calling ch p & (\l. MemInv mm l) --> Enabled (_(rtrner ch ! p, rs!p))" apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use]) apply (case_tac "arg (ch w p)") diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Jun 26 11:44:22 2015 +0200 @@ -63,7 +63,7 @@ definition (* the environment action *) ENext :: "PrIds => action" - where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))" + where "ENext p = ACT (\l. #l : #MemLoc & Call memCh p #(read l))" definition @@ -83,24 +83,24 @@ definition HistP :: "histType => PrIds => temporal" where "HistP rmhist p = (TEMP Init HInit rmhist p - & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))" + & \[HNext rmhist p]_(c p,r p,m p, rmhist!p))" definition Hist :: "histType => temporal" - where "Hist rmhist = TEMP (ALL p. HistP rmhist p)" + where "Hist rmhist = TEMP (\p. HistP rmhist p)" definition (* the implementation *) IPImp :: "PrIds => temporal" - where "IPImp p = (TEMP ( Init ~Calling memCh p & [][ENext p]_(e p) + where "IPImp p = (TEMP ( Init \Calling memCh p & \[ENext p]_(e p) & MClkIPSpec memCh crCh cst p & RPCIPSpec crCh rmCh rst p & RPSpec rmCh mm ires p - & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))" + & (\l. #l : #MemLoc --> MSpec rmCh mm ires l)))" definition ImpInit :: "PrIds => stpred" - where "ImpInit p = PRED ( ~Calling memCh p + where "ImpInit p = PRED ( \Calling memCh p & MClkInit crCh cst p & RPCInit rmCh rst p & PInit ires p)" @@ -122,7 +122,7 @@ definition Implementation :: "temporal" - where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p)) + where "Implementation = (TEMP ( (\p. Init (\Calling memCh p) & \[ENext p]_(e p)) & MClkISpec memCh crCh cst & RPCISpec crCh rmCh rst & IRSpec rmCh mm ires))" @@ -139,11 +139,11 @@ Calling memCh p = #ecalling & Calling crCh p = #ccalling & (#ccalling --> arg = MClkRelayArg>) - & (~ #ccalling & cst!p = #clkB --> MVOKBARF>) + & (\ #ccalling & cst!p = #clkB --> MVOKBARF>) & Calling rmCh p = #rcalling & (#rcalling --> arg = RPCRelayArg>) - & (~ #rcalling --> ires!p = #NotAResult) - & (~ #rcalling & rst!p = #rpcB --> MVOKBA>) + & (\ #rcalling --> ires!p = #NotAResult) + & (\ #rcalling & rst!p = #rpcB --> MVOKBA>) & cst!p = #cs & rst!p = #rs & (rmhist!p = #hs1 | rmhist!p = #hs2) @@ -241,9 +241,9 @@ section "History variable" -lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p) - --> (EEX rmhist. Init(ALL p. HInit rmhist p) - & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))" +lemma HistoryLemma: "|- Init(\p. ImpInit p) & \(\p. ImpNext p) + --> (\\rmhist. Init(\p. HInit rmhist p) + & \(\p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))" apply clarsimp apply (rule historyI) apply assumption+ @@ -255,7 +255,7 @@ apply (erule fun_cong) done -lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)" +lemma History: "|- Implementation --> (\\rmhist. Hist rmhist)" apply clarsimp apply (rule HistoryLemma [temp_use, THEN eex_mono]) prefer 3 @@ -274,14 +274,14 @@ (* RPCFailure notin MemVals U {OK,BadArg} *) -lemma MVOKBAnotRF: "MVOKBA x ==> x ~= RPCFailure" +lemma MVOKBAnotRF: "MVOKBA x ==> x \ RPCFailure" apply (unfold MVOKBA_def) apply auto done (* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *) -lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult" +lemma MVOKBARFnotNR: "MVOKBARF x ==> x \ NotAResult" apply (unfold MVOKBARF_def) apply auto done @@ -294,32 +294,32 @@ *) (* --- not used --- -lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p & - ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p" +lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & \S2 rmhist p & \S3 rmhist p & + \S4 rmhist p & \S5 rmhist p & \S6 rmhist p" by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def) *) -lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p" +lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & \S1 rmhist p" by (auto simp: S_def S1_def S2_def) -lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p" +lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & \S1 rmhist p & \S2 rmhist p" by (auto simp: S_def S1_def S2_def S3_def) -lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p" +lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & \S1 rmhist p & \S2 rmhist p & \S3 rmhist p" by (auto simp: S_def S1_def S2_def S3_def S4_def) -lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p - & ~S3 rmhist p & ~S4 rmhist p" +lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & \S1 rmhist p & \S2 rmhist p + & \S3 rmhist p & \S4 rmhist p" by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def) -lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p - & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p" +lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & \S1 rmhist p & \S2 rmhist p + & \S3 rmhist p & \S4 rmhist p & \S5 rmhist p" by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def) (* ==================== Lemmas about the environment ============================== *) -lemma Envbusy: "|- $(Calling memCh p) --> ~ENext p" +lemma Envbusy: "|- $(Calling memCh p) --> \ENext p" by (auto simp: ENext_def Call_def) (* ==================== Lemmas about the implementation's states ==================== *) @@ -447,7 +447,7 @@ @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *}) lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p) - & HNext rmhist p & (!l. $MemInv mm l) + & HNext rmhist p & (\l. $MemInv mm l) --> (S4 rmhist p)$ & unchanged (rmhist!p)" by (auto simp: Read_def dest!: S4ReadInner [temp_use]) @@ -563,7 +563,7 @@ (* Figure 16 is a predicate-action diagram for the implementation. *) lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p + & \unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] (map (temp_elim @{context}) @@ -573,7 +573,7 @@ done lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p + & \unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p)" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] @@ -584,7 +584,7 @@ done lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p + & \unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] @@ -596,10 +596,10 @@ done lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) - & $S4 rmhist p & (!l. $(MemInv mm l)) + & \unchanged (e p, c p, r p, m p, rmhist!p) + & $S4 rmhist p & (\l. $(MemInv mm l)) --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p)) - | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) + | ((S4 rmhist p)$ & (\l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *}) @@ -610,7 +610,7 @@ done lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p + & \unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p)) | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] @@ -621,7 +621,7 @@ done lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p - & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p + & \unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p)) | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) [] @@ -694,7 +694,7 @@ done lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ - & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l)) + & unchanged (e p, c p, r p, rmhist!p) & (\l. $(MemInv mm l)) --> Read memCh mm (resbar rmhist) p" by (force simp: Read_def elim!: Step1_4_4a1 [temp_use]) @@ -816,7 +816,7 @@ (* Steps that leave all variables unchanged are safe, so I may assume that some variable changes in the proof that a step is safe. *) -lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p) +lemma unchanged_safe: "|- (\unchanged (e p, c p, r p, m p, rmhist!p) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" apply (split_idle simp: square_def) @@ -850,7 +850,7 @@ done lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) - & (!l. $(MemInv mm l)) + & (\l. $(MemInv mm l)) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" apply clarsimp apply (rule unchanged_safeI) @@ -900,23 +900,23 @@ *) lemma S1_RNextdisabled: "|- S1 rmhist p --> - ~Enabled (_(rtrner memCh!p, resbar rmhist!p))" + \Enabled (_(rtrner memCh!p, resbar rmhist!p))" apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *}) apply force done lemma S1_Returndisabled: "|- S1 rmhist p --> - ~Enabled (_(rtrner memCh!p, resbar rmhist!p))" + \Enabled (_(rtrner memCh!p, resbar rmhist!p))" by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def}, @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *}) -lemma RNext_fair: "|- []<>S1 rmhist p +lemma RNext_fair: "|- \\S1 rmhist p --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use]) -lemma Return_fair: "|- []<>S1 rmhist p +lemma Return_fair: "|- \\S1 rmhist p --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" by (auto simp: WF_alt [try_rewrite] intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use]) @@ -942,9 +942,9 @@ apply (simp_all add: S_def S2_def) done -lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) +lemma S2_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(MClkFwd memCh crCh cst p)_(c p) - --> (S2 rmhist p ~> S3 rmhist p)" + --> (S2 rmhist p \ S3 rmhist p)" by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+ (* ------------------------------ State S3 ------------------------------ *) @@ -969,15 +969,15 @@ apply (simp_all add: S_def S3_def) done -lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) +lemma S3_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(RPCNext crCh rmCh rst p)_(r p) - --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)" + --> (S3 rmhist p \ S4 rmhist p | S6 rmhist p)" by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+ (* ------------- State S4 -------------------------------------------------- *) lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) - & (ALL l. $MemInv mm l) + & (\l. $MemInv mm l) --> (S4 rmhist p)$ | (S5 rmhist p)$" apply split_idle apply (auto dest!: Step1_2_4 [temp_use]) @@ -986,22 +986,22 @@ (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *) lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult) - & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l) + & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\l. $MemInv mm l) --> (S4 rmhist p & ires!p = #NotAResult)$ - | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" + | ((S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p)$" apply split_idle apply (auto dest!: Step1_2_4 [temp_use]) done lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult) - & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)) + & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\l. $MemInv mm l)) & _(m p) - --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" + --> ((S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p)$" by (auto simp: angle_def dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use]) lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult) - & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) + & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\l. $MemInv mm l) --> $Enabled (_(m p))" apply (auto simp: m_def intro!: RNext_enabled [temp_use]) apply (cut_tac MI_base) @@ -1009,30 +1009,30 @@ apply (simp add: S_def S4_def) done -lemma S4a_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) - & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p) +lemma S4a_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) + & (\l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p) --> (S4 rmhist p & ires!p = #NotAResult - ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)" + \ (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p)" by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+ (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *) -lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult) - & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) - --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$" +lemma S4b_successors: "|- $(S4 rmhist p & ires!p \ #NotAResult) + & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\l. $MemInv mm l) + --> (S4 rmhist p & ires!p \ #NotAResult)$ | (S5 rmhist p)$" apply (split_idle simp: m_def) apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) done -lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p ~= #NotAResult) +lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p \ #NotAResult) & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) - & (ALL l. $MemInv mm l)) & _(m p) + & (\l. $MemInv mm l)) & _(m p) --> (S5 rmhist p)$" by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use]) -lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult) +lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p \ #NotAResult) & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) - & (ALL l. $MemInv mm l) + & (\l. $MemInv mm l) --> $Enabled (_(m p))" apply (auto simp: m_def intro!: MemReturn_enabled [temp_use]) apply (cut_tac MI_base) @@ -1040,9 +1040,9 @@ apply (simp add: S_def S4_def) done -lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l)) +lemma S4b_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\l. $MemInv mm l)) & WF(MemReturn rmCh ires p)_(m p) - --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)" + --> (S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p)" by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+ (* ------------------------------ State S5 ------------------------------ *) @@ -1066,9 +1066,9 @@ apply (simp_all add: S_def S5_def) done -lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) +lemma S5_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)) & WF(RPCNext crCh rmCh rst p)_(r p) - --> (S5 rmhist p ~> S6 rmhist p)" + --> (S5 rmhist p \ S6 rmhist p)" by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+ (* ------------------------------ State S6 ------------------------------ *) @@ -1099,11 +1099,11 @@ addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *}) done -lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p)) - & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p) - --> []<>(S1 rmhist p)" +lemma S6_live: "|- \(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p)) + & SF(MClkReply memCh crCh cst p)_(c p) & \\(S6 rmhist p) + --> \\(S1 rmhist p)" apply clarsimp - apply (subgoal_tac "sigma |= []<> (_ (c p))") + apply (subgoal_tac "sigma |= \\ (_ (c p))") apply (erule InfiniteEnsures) apply assumption apply (tactic {* action_simp_tac @{context} [] @@ -1115,26 +1115,26 @@ (* --------------- aggregate leadsto properties----------------------------- *) -lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p - ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p" +lemma S5S6LeadstoS6: "sigma |= S5 rmhist p \ S6 rmhist p + ==> sigma |= (S5 rmhist p | S6 rmhist p) \ S6 rmhist p" by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) -lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; - sigma |= S5 rmhist p ~> S6 rmhist p |] - ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p - ~> S6 rmhist p" +lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p; + sigma |= S5 rmhist p \ S6 rmhist p |] + ==> sigma |= (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p | S6 rmhist p + \ S6 rmhist p" by (auto intro!: LatticeDisjunctionIntro [temp_use] S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use]) lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult - ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; - sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; - sigma |= S5 rmhist p ~> S6 rmhist p |] - ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" + \ (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p; + sigma |= S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p; + sigma |= S5 rmhist p \ S6 rmhist p |] + ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p \ S6 rmhist p" apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) | - (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p") + (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p | S6 rmhist p \ S6 rmhist p") apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) | - (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in + (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p | S6 rmhist p)" in LatticeTransitivity [temp_use]) apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) apply (rule LatticeDisjunctionIntro [temp_use]) @@ -1144,12 +1144,12 @@ apply (auto intro!: S4bS5S6LeadstoS6 [temp_use]) done -lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; +lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p \ S4 rmhist p | S6 rmhist p; sigma |= S4 rmhist p & ires!p = #NotAResult - ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p; - sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; - sigma |= S5 rmhist p ~> S6 rmhist p |] - ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p" + \ (S4 rmhist p & ires!p \ #NotAResult) | S5 rmhist p; + sigma |= S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p; + sigma |= S5 rmhist p \ S6 rmhist p |] + ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \ S6 rmhist p" apply (rule LatticeDisjunctionIntro [temp_use]) apply (erule LatticeTriangle2 [temp_use]) apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]]) @@ -1157,14 +1157,14 @@ intro: ImplLeadsto_gen [temp_use] simp: Init_defs) done -lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p; - sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; +lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p \ S3 rmhist p; + sigma |= S3 rmhist p \ S4 rmhist p | S6 rmhist p; sigma |= S4 rmhist p & ires!p = #NotAResult - ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; - sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; - sigma |= S5 rmhist p ~> S6 rmhist p |] + \ S4 rmhist p & ires!p \ #NotAResult | S5 rmhist p; + sigma |= S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p; + sigma |= S5 rmhist p \ S6 rmhist p |] ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p - ~> S6 rmhist p" + \ S6 rmhist p" apply (rule LatticeDisjunctionIntro [temp_use]) apply (rule LatticeTransitivity [temp_use]) prefer 2 apply assumption @@ -1173,14 +1173,14 @@ intro: ImplLeadsto_gen [temp_use] simp: Init_defs) done -lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p; - sigma |= S2 rmhist p ~> S3 rmhist p; - sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p; +lemma NotS1LeadstoS6: "[| sigma |= \ImpInv rmhist p; + sigma |= S2 rmhist p \ S3 rmhist p; + sigma |= S3 rmhist p \ S4 rmhist p | S6 rmhist p; sigma |= S4 rmhist p & ires!p = #NotAResult - ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p; - sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p; - sigma |= S5 rmhist p ~> S6 rmhist p |] - ==> sigma |= ~S1 rmhist p ~> S6 rmhist p" + \ S4 rmhist p & ires!p \ #NotAResult | S5 rmhist p; + sigma |= S4 rmhist p & ires!p \ #NotAResult \ S5 rmhist p; + sigma |= S5 rmhist p \ S6 rmhist p |] + ==> sigma |= \S1 rmhist p \ S6 rmhist p" apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]]) apply assumption+ apply (erule INV_leadsto [temp_use]) @@ -1189,9 +1189,9 @@ apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use]) done -lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p; - sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |] - ==> sigma |= []<>S1 rmhist p" +lemma S1Infinite: "[| sigma |= \S1 rmhist p \ S6 rmhist p; + sigma |= \\S6 rmhist p --> \\S1 rmhist p |] + ==> sigma |= \\S1 rmhist p" apply (rule classical) apply (tactic {* asm_lr_simp_tac (@{context} addsimps [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *}) @@ -1204,12 +1204,12 @@ a. memory invariant b. "implementation invariant": always in states S1,...,S6 *) -lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)" +lemma Step1_5_1a: "|- IPImp p --> (\l. \$MemInv mm l)" by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use]) -lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p) - & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l) - --> []ImpInv rmhist p" +lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & \(ImpNext p) + & \[HNext rmhist p]_(c p, r p, m p, rmhist!p) & \(\l. $MemInv mm l) + --> \ImpInv rmhist p" apply invariant apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use] dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use] @@ -1222,9 +1222,9 @@ by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3 [temp_use]) (*** step simulation ***) -lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p) - & $ImpInv rmhist p & (!l. $MemInv mm l)) - --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" +lemma Step1_5_2b: "|- \(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p) + & $ImpInv rmhist p & (\l. $MemInv mm l)) + --> \[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" by (auto simp: ImpInv_def elim!: STL4E [temp_use] dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use] S5safe [temp_use] S6safe [temp_use]) @@ -1232,12 +1232,12 @@ (*** Liveness ***) lemma GoodImpl: "|- IPImp p & HistP rmhist p --> Init(ImpInit p & HInit rmhist p) - & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) + & \(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & \(\l. $MemInv mm l) & \($ImpInv rmhist p) & ImpLive p" apply clarsimp - apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) & - [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)") + apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & \ (ImpNext p) & + \[HNext rmhist p]_ (c p, r p, m p, rmhist!p) & \ (\l. $MemInv mm l)") apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite] dest!: Step1_5_1b [temp_use]) apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def @@ -1251,10 +1251,10 @@ done (* The implementation is infinitely often in state S1... *) -lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & [](ALL l. $MemInv mm l) - & []($ImpInv rmhist p) & ImpLive p - --> []<>S1 rmhist p" +lemma Step1_5_3a: "|- \(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & \(\l. $MemInv mm l) + & \($ImpInv rmhist p) & ImpLive p + --> \\S1 rmhist p" apply (clarsimp simp: ImpLive_def) apply (rule S1Infinite) apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite] @@ -1264,13 +1264,13 @@ done (* ... and therefore satisfies the fairness requirements of the specification *) -lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p +lemma Step1_5_3b: "|- \(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & \(\l. $MemInv mm l) & \($ImpInv rmhist p) & ImpLive p --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use]) -lemma Step1_5_3c: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p +lemma Step1_5_3c: "|- \(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & \(\l. $MemInv mm l) & \($ImpInv rmhist p) & ImpLive p --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use]) @@ -1296,25 +1296,25 @@ apply (auto simp: square_def dest: S4Write [temp_use]) done -lemma Step2_2: "|- (ALL p. ImpNext p) - & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & (ALL p. $ImpInv rmhist p) - & [EX q. Write rmCh mm ires q l]_(mm!l) - --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)" +lemma Step2_2: "|- (\p. ImpNext p) + & (\p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & (\p. $ImpInv rmhist p) + & [\q. Write rmCh mm ires q l]_(mm!l) + --> [\q. Write memCh mm (resbar rmhist) q l]_(mm!l)" apply (auto intro!: squareCI elim!: squareE) apply (assumption | rule exI Step1_4_4b [action_use])+ apply (force intro!: WriteS4 [temp_use]) apply (auto dest!: Step2_2a [temp_use]) done -lemma Step2_lemma: "|- []( (ALL p. ImpNext p) - & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) - & (ALL p. $ImpInv rmhist p) - & [EX q. Write rmCh mm ires q l]_(mm!l)) - --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)" +lemma Step2_lemma: "|- \( (\p. ImpNext p) + & (\p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)) + & (\p. $ImpInv rmhist p) + & [\q. Write rmCh mm ires q l]_(mm!l)) + --> \[\q. Write memCh mm (resbar rmhist) q l]_(mm!l)" by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use]) -lemma Step2: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p) +lemma Step2: "|- #l : #MemLoc & (\p. IPImp p & HistP rmhist p) --> MSpec memCh mm (resbar rmhist) l" apply (auto simp: MSpec_def) apply (force simp: IPImp_def MSpec_def) diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/MemoryParameters.thy --- a/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Fri Jun 26 11:44:22 2015 +0200 @@ -27,20 +27,20 @@ axiomatization where (* basic assumptions about the above constants and predicates *) - BadArgNoMemVal: "BadArg ~: MemVal" and - MemFailNoMemVal: "MemFailure ~: MemVal" and + BadArgNoMemVal: "BadArg \ MemVal" and + MemFailNoMemVal: "MemFailure \ MemVal" and InitValMemVal: "InitVal : MemVal" and - NotAResultNotVal: "NotAResult ~: MemVal" and - NotAResultNotOK: "NotAResult ~= OK" and - NotAResultNotBA: "NotAResult ~= BadArg" and - NotAResultNotMF: "NotAResult ~= MemFailure" + NotAResultNotVal: "NotAResult \ MemVal" and + NotAResultNotOK: "NotAResult \ OK" and + NotAResultNotBA: "NotAResult \ BadArg" and + NotAResultNotMF: "NotAResult \ MemFailure" lemmas [simp] = BadArgNoMemVal MemFailNoMemVal InitValMemVal NotAResultNotVal NotAResultNotOK NotAResultNotBA NotAResultNotMF NotAResultNotOK [symmetric] NotAResultNotBA [symmetric] NotAResultNotMF [symmetric] -lemma MemValNotAResultE: "[| x : MemVal; (x ~= NotAResult ==> P) |] ==> P" +lemma MemValNotAResultE: "[| x : MemVal; (x \ NotAResult ==> P) |] ==> P" using NotAResultNotVal by blast end diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/ProcedureInterface.thy --- a/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Fri Jun 26 11:44:22 2015 +0200 @@ -58,23 +58,23 @@ defs slice_def: "(PRED (x!i)) s == x s i" - caller_def: "caller ch == %s p. (cbit (ch s p), arg (ch s p))" - rtrner_def: "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" + caller_def: "caller ch == \s p. (cbit (ch s p), arg (ch s p))" + rtrner_def: "rtrner ch == \s p. (rbit (ch s p), res (ch s p))" - Calling_def: "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" - Call_def: "(ACT Call ch p v) == ACT ~ $Calling ch p - & (cbit$ ~= $rbit) + Calling_def: "Calling ch p == PRED cbit< ch!p > \ rbit< ch!p >" + Call_def: "(ACT Call ch p v) == ACT \ $Calling ch p + & (cbit$ \ $rbit) & (arg$ = $v)" Return_def: "(ACT Return ch p v) == ACT $Calling ch p & (rbit$ = $cbit) & (res$ = $v)" PLegalCaller_def: "PLegalCaller ch p == TEMP - Init(~ Calling ch p) - & [][ ? a. Call ch p a ]_((caller ch)!p)" - LegalCaller_def: "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" + Init(\ Calling ch p) + & \[\a. Call ch p a ]_((caller ch)!p)" + LegalCaller_def: "LegalCaller ch == TEMP (\p. PLegalCaller ch p)" PLegalReturner_def: "PLegalReturner ch p == TEMP - [][ ? v. Return ch p v ]_((rtrner ch)!p)" - LegalReturner_def: "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" + \[\v. Return ch p v ]_((rtrner ch)!p)" + LegalReturner_def: "LegalReturner ch == TEMP (\p. PLegalReturner ch p)" declare slice_def [simp] diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/RPC.thy --- a/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/RPC.thy Fri Jun 26 11:44:22 2015 +0200 @@ -28,7 +28,7 @@ RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal" defs - RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)" + RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \Calling rcv p)" RPCFwd_def: "RPCFwd send rcv rst p == ACT $(Calling send p) @@ -40,18 +40,18 @@ RPCReject_def: "RPCReject send rcv rst p == ACT $(rst!p) = # rpcA - & ~IsLegalRcvArg> + & \IsLegalRcvArg> & Return send p #BadCall & unchanged ((rst!p), (caller rcv!p))" RPCFail_def: "RPCFail send rcv rst p == ACT - ~$(Calling rcv p) + \$(Calling rcv p) & Return send p #RPCFailure & (rst!p)$ = #rpcA & unchanged (caller rcv!p)" RPCReply_def: "RPCReply send rcv rst p == ACT - ~$(Calling rcv p) + \$(Calling rcv p) & $(rst!p) = #rpcB & Return send p res & (rst!p)$ = #rpcA @@ -65,10 +65,10 @@ RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP Init RPCInit rcv rst p - & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p) + & \[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p) & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)" - RPCISpec_def: "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)" + RPCISpec_def: "RPCISpec send rcv rst == TEMP (\p. RPCIPSpec send rcv rst p)" lemmas RPC_action_defs = @@ -81,10 +81,10 @@ unanswered call for that process. *) -lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p" +lemma RPCidle: "|- \$(Calling send p) --> \RPCNext send rcv rst p" by (auto simp: Return_def RPC_action_defs) -lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p" +lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \RPCNext send rcv rst p" by (auto simp: RPC_action_defs) (* RPC failure actions are visible. *) @@ -97,14 +97,14 @@ by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use]) (* Enabledness of some actions *) -lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> - |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)" +lemma RPCFail_enabled: "\p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> + |- \Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)" by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) -lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> - |- ~Calling rcv p & Calling send p & rst!p = #rpcB +lemma RPCReply_enabled: "\p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> + |- \Calling rcv p & Calling send p & rst!p = #rpcB --> Enabled (RPCReply send rcv rst p)" by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/RPCParameters.thy --- a/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Memory/RPCParameters.thy Fri Jun 26 11:44:22 2015 +0200 @@ -30,10 +30,10 @@ axiomatization where (* RPCFailure is different from MemVals and exceptions *) - RFNoMemVal: "RPCFailure ~: MemVal" and - NotAResultNotRF: "NotAResult ~= RPCFailure" and - OKNotRF: "OK ~= RPCFailure" and - BANotRF: "BadArg ~= RPCFailure" + RFNoMemVal: "RPCFailure \ MemVal" and + NotAResultNotRF: "NotAResult \ RPCFailure" and + OKNotRF: "OK \ RPCFailure" and + BANotRF: "BadArg \ RPCFailure" defs IsLegalRcvArg_def: "IsLegalRcvArg ra == diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Stfun.thy --- a/src/HOL/TLA/Stfun.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/Stfun.thy Fri Jun 26 11:44:22 2015 +0200 @@ -50,13 +50,13 @@ basevars_def: "stvars vs == range vs = UNIV" -lemma basevars: "!!vs. basevars vs ==> EX u. vs u = c" +lemma basevars: "\vs. basevars vs ==> \u. vs u = c" apply (unfold basevars_def) apply (rule_tac b = c and f = vs in rangeE) apply auto done -lemma base_pair1: "!!x y. basevars (x,y) ==> basevars x" +lemma base_pair1: "\x y. basevars (x,y) ==> basevars x" apply (simp (no_asm) add: basevars_def) apply (rule equalityI) apply (rule subset_UNIV) @@ -65,7 +65,7 @@ apply auto done -lemma base_pair2: "!!x y. basevars (x,y) ==> basevars y" +lemma base_pair2: "\x y. basevars (x,y) ==> basevars y" apply (simp (no_asm) add: basevars_def) apply (rule equalityI) apply (rule subset_UNIV) @@ -74,7 +74,7 @@ apply auto done -lemma base_pair: "!!x y. basevars (x,y) ==> basevars x & basevars y" +lemma base_pair: "\x y. basevars (x,y) ==> basevars x & basevars y" apply (rule conjI) apply (erule base_pair1) apply (erule base_pair2) @@ -89,7 +89,7 @@ apply auto done -lemma baseE: "[| basevars v; !!x. v x = c ==> Q |] ==> Q" +lemma baseE: "[| basevars v; \x. v x = c ==> Q |] ==> Q" apply (erule basevars [THEN exE]) apply blast done @@ -99,7 +99,7 @@ The following shows that there should not be duplicates in a "stvars" tuple: *) -lemma "!!v. basevars (v::bool stfun, v) ==> False" +lemma "\v. basevars (v::bool stfun, v) ==> False" apply (erule baseE) apply (subgoal_tac "(LIFT (v,v)) x = (True, False)") prefer 2 diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Fri Jun 26 11:07:04 2015 +0200 +++ b/src/HOL/TLA/TLA.thy Fri Jun 26 11:44:22 2015 +0200 @@ -60,49 +60,45 @@ "_EEx" :: "[idts, lift] => lift" ("(3\\ _./ _)" [0,10] 10) "_AAll" :: "[idts, lift] => lift" ("(3\\ _./ _)" [0,10] 10) -syntax (HTML output) - "_EEx" :: "[idts, lift] => lift" ("(3\\ _./ _)" [0,10] 10) - "_AAll" :: "[idts, lift] => lift" ("(3\\ _./ _)" [0,10] 10) - axiomatization where (* Definitions of derived operators *) - dmd_def: "\F. TEMP <>F == TEMP ~[]~F" + dmd_def: "\F. TEMP \F == TEMP \\\F" axiomatization where - boxInit: "\F. TEMP []F == TEMP []Init F" and - leadsto_def: "\F G. TEMP F ~> G == TEMP [](Init F --> <>G)" and - stable_def: "\P. TEMP stable P == TEMP []($P --> P$)" and - WF_def: "TEMP WF(A)_v == TEMP <>[] Enabled(_v) --> []<>_v" and - SF_def: "TEMP SF(A)_v == TEMP []<> Enabled(_v) --> []<>_v" and - aall_def: "TEMP (AALL x. F x) == TEMP ~ (EEX x. ~ F x)" + boxInit: "\F. TEMP \F == TEMP \Init F" and + leadsto_def: "\F G. TEMP F \ G == TEMP \(Init F --> \G)" and + stable_def: "\P. TEMP stable P == TEMP \($P --> P$)" and + WF_def: "TEMP WF(A)_v == TEMP \\ Enabled(_v) --> \\_v" and + SF_def: "TEMP SF(A)_v == TEMP \\ Enabled(_v) --> \\_v" and + aall_def: "TEMP (\\x. F x) == TEMP \ (\\x. \ F x)" axiomatization where (* Base axioms for raw TLA. *) - normalT: "\F G. |- [](F --> G) --> ([]F --> []G)" and (* polymorphic *) - reflT: "\F. |- []F --> F" and (* F::temporal *) - transT: "\F. |- []F --> [][]F" and (* polymorphic *) - linT: "\F G. |- <>F & <>G --> (<>(F & <>G)) | (<>(G & <>F))" and - discT: "\F. |- [](F --> <>(~F & <>F)) --> (F --> []<>F)" and - primeI: "\P. |- []P --> Init P`" and - primeE: "\P F. |- [](Init P --> []F) --> Init P` --> (F --> []F)" and - indT: "\P F. |- [](Init P & ~[]F --> Init P` & F) --> Init P --> []F" and - allT: "\F. |- (ALL x. [](F x)) = ([](ALL x. F x))" + normalT: "\F G. |- \(F --> G) --> (\F --> \G)" and (* polymorphic *) + reflT: "\F. |- \F --> F" and (* F::temporal *) + transT: "\F. |- \F --> \\F" and (* polymorphic *) + linT: "\F G. |- \F & \G --> (\(F & \G)) | (\(G & \F))" and + discT: "\F. |- \(F --> \(\F & \F)) --> (F --> \\F)" and + primeI: "\P. |- \P --> Init P`" and + primeE: "\P F. |- \(Init P --> \F) --> Init P` --> (F --> \F)" and + indT: "\P F. |- \(Init P & \\F --> Init P` & F) --> Init P --> \F" and + allT: "\F. |- (\x. \(F x)) = (\(\ x. F x))" axiomatization where - necT: "\F. |- F ==> |- []F" (* polymorphic *) + necT: "\F. |- F ==> |- \F" (* polymorphic *) axiomatization where (* Flexible quantification: refinement mappings, history variables *) - eexI: "|- F x --> (EEX x. F x)" and - eexE: "[| sigma |= (EEX x. F x); basevars vs; - (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) + eexI: "|- F x --> (\\x. F x)" and + eexE: "[| sigma |= (\\x. F x); basevars vs; + (\x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) |] ==> G sigma" and - history: "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)" + history: "|- \\h. Init(h = ha) & \(\x. $h = #x --> h` = hb x)" (* Specialize intensional introduction/elimination rules for temporal formulas *) -lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F" +lemma tempI [intro!]: "(\sigma. sigma |= (F::temporal)) ==> |- F" apply (rule intI) apply (erule meta_spec) done @@ -145,20 +141,20 @@ (* ------------------------------------------------------------------------- *) -(*** "Simple temporal logic": only [] and <> ***) +(*** "Simple temporal logic": only \ and \ ***) (* ------------------------------------------------------------------------- *) section "Simple temporal logic" -(* []~F == []~Init F *) -lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F +(* \\F == \\Init F *) +lemmas boxNotInit = boxInit [of "LIFT \F", unfolded Init_simps] for F -lemma dmdInit: "TEMP <>F == TEMP <> Init F" +lemma dmdInit: "TEMP \F == TEMP \ Init F" apply (unfold dmd_def) - apply (unfold boxInit [of "LIFT ~F"]) + apply (unfold boxInit [of "LIFT \F"]) apply (simp (no_asm) add: Init_simps) done -lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F +lemmas dmdNotInit = dmdInit [of "LIFT \F", unfolded Init_simps] for F (* boxInit and dmdInit cannot be used as rewrites, because they loop. Non-looping instances for state predicates and actions are occasionally useful. @@ -180,21 +176,21 @@ lemmas STL2 = reflT (* The "polymorphic" (generic) variant *) -lemma STL2_gen: "|- []F --> Init F" +lemma STL2_gen: "|- \F --> Init F" apply (unfold boxInit [of F]) apply (rule STL2) done -(* see also STL2_pr below: "|- []P --> Init P & Init (P`)" *) +(* see also STL2_pr below: "|- \P --> Init P & Init (P`)" *) -(* Dual versions for <> *) -lemma InitDmd: "|- F --> <> F" +(* Dual versions for \ *) +lemma InitDmd: "|- F --> \ F" apply (unfold dmd_def) apply (auto dest!: STL2 [temp_use]) done -lemma InitDmd_gen: "|- Init F --> <>F" +lemma InitDmd_gen: "|- Init F --> \F" apply clarsimp apply (drule InitDmd [temp_use]) apply (simp add: dmdInitD) @@ -202,17 +198,17 @@ (* ------------------------ STL3 ------------------------------------------- *) -lemma STL3: "|- ([][]F) = ([]F)" +lemma STL3: "|- (\\F) = (\F)" by (auto elim: transT [temp_use] STL2 [temp_use]) (* corresponding elimination rule introduces double boxes: - [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W + [| (sigma |= \F); (sigma |= \\F) ==> PROP W |] ==> PROP W *) lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format] lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1] -(* dual versions for <> *) -lemma DmdDmd: "|- (<><>F) = (<>F)" +(* dual versions for \ *) +lemma DmdDmd: "|- (\\F) = (\F)" by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite]) lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format] @@ -222,7 +218,7 @@ (* ------------------------ STL4 ------------------------------------------- *) lemma STL4: assumes "|- F --> G" - shows "|- []F --> []G" + shows "|- \F --> \G" apply clarsimp apply (rule normalT [temp_use]) apply (rule assms [THEN necT, temp_use]) @@ -230,38 +226,38 @@ done (* Unlifted version as an elimination rule *) -lemma STL4E: "[| sigma |= []F; |- F --> G |] ==> sigma |= []G" +lemma STL4E: "[| sigma |= \F; |- F --> G |] ==> sigma |= \G" by (erule (1) STL4 [temp_use]) -lemma STL4_gen: "|- Init F --> Init G ==> |- []F --> []G" +lemma STL4_gen: "|- Init F --> Init G ==> |- \F --> \G" apply (drule STL4) apply (simp add: boxInitD) done -lemma STL4E_gen: "[| sigma |= []F; |- Init F --> Init G |] ==> sigma |= []G" +lemma STL4E_gen: "[| sigma |= \F; |- Init F --> Init G |] ==> sigma |= \G" by (erule (1) STL4_gen [temp_use]) (* see also STL4Edup below, which allows an auxiliary boxed formula: - []A /\ F => G + \A /\ F => G ----------------- - []A /\ []F => []G + \A /\ \F => \G *) -(* The dual versions for <> *) +(* The dual versions for \ *) lemma DmdImpl: assumes prem: "|- F --> G" - shows "|- <>F --> <>G" + shows "|- \F --> \G" apply (unfold dmd_def) apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use]) done -lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G" +lemma DmdImplE: "[| sigma |= \F; |- F --> G |] ==> sigma |= \G" by (erule (1) DmdImpl [temp_use]) (* ------------------------ STL5 ------------------------------------------- *) -lemma STL5: "|- ([]F & []G) = ([](F & G))" +lemma STL5: "|- (\F & \G) = (\(F & G))" apply auto - apply (subgoal_tac "sigma |= [] (G --> (F & G))") + apply (subgoal_tac "sigma |= \ (G --> (F & G))") apply (erule normalT [temp_use]) apply (fastforce elim!: STL4E [temp_use])+ done @@ -275,9 +271,9 @@ Use "addSE2" etc. if you want to add this to a claset, otherwise it will loop! *) lemma box_conjE: - assumes "sigma |= []F" - and "sigma |= []G" - and "sigma |= [](F&G) ==> PROP R" + assumes "sigma |= \F" + and "sigma |= \G" + and "sigma |= \(F&G) ==> PROP R" shows "PROP R" by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+ @@ -292,7 +288,7 @@ a bit kludgy in order to simulate "double elim-resolution". *) -lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" . +lemma box_thin: "[| sigma |= \F; PROP W |] ==> PROP W" . ML {* fun merge_box_tac i = @@ -317,29 +313,29 @@ method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} (* rewrite rule to push universal quantification through box: - (sigma |= [](! x. F x)) = (! x. (sigma |= []F x)) + (sigma |= \(\x. F x)) = (\x. (sigma |= \F x)) *) lemmas all_box = allT [temp_unlift, symmetric] -lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)" +lemma DmdOr: "|- (\(F | G)) = (\F | \G)" apply (auto simp add: dmd_def split_box_conj [try_rewrite]) apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+ done -lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))" +lemma exT: "|- (\x. \(F x)) = (\(\x. F x))" by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite]) lemmas ex_dmd = exT [temp_unlift, symmetric] -lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G" +lemma STL4Edup: "\sigma. [| sigma |= \A; sigma |= \F; |- F & \A --> G |] ==> sigma |= \G" apply (erule dup_boxE) apply merge_box apply (erule STL4E) apply assumption done -lemma DmdImpl2: - "!!sigma. [| sigma |= <>F; sigma |= [](F --> G) |] ==> sigma |= <>G" +lemma DmdImpl2: + "\sigma. [| sigma |= \F; sigma |= \(F --> G) |] ==> sigma |= \G" apply (unfold dmd_def) apply auto apply (erule notE) @@ -348,10 +344,10 @@ done lemma InfImpl: - assumes 1: "sigma |= []<>F" - and 2: "sigma |= []G" + assumes 1: "sigma |= \\F" + and 2: "sigma |= \G" and 3: "|- F & G --> H" - shows "sigma |= []<>H" + shows "sigma |= \\H" apply (insert 1 2) apply (erule_tac F = G in dup_boxE) apply merge_box @@ -360,7 +356,7 @@ (* ------------------------ STL6 ------------------------------------------- *) (* Used in the proof of STL6, but useful in itself. *) -lemma BoxDmd: "|- []F & <>G --> <>([]F & G)" +lemma BoxDmd: "|- \F & \G --> \(\F & G)" apply (unfold dmd_def) apply clarsimp apply (erule dup_boxE) @@ -370,14 +366,14 @@ done (* weaker than BoxDmd, but more polymorphic (and often just right) *) -lemma BoxDmd_simple: "|- []F & <>G --> <>(F & G)" +lemma BoxDmd_simple: "|- \F & \G --> \(F & G)" apply (unfold dmd_def) apply clarsimp apply merge_box apply (fastforce elim!: notE STL4E [temp_use]) done -lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)" +lemma BoxDmd2_simple: "|- \F & \G --> \(G & F)" apply (unfold dmd_def) apply clarsimp apply merge_box @@ -385,15 +381,15 @@ done lemma DmdImpldup: - assumes 1: "sigma |= []A" - and 2: "sigma |= <>F" - and 3: "|- []A & F --> G" - shows "sigma |= <>G" + assumes 1: "sigma |= \A" + and 2: "sigma |= \F" + and 3: "|- \A & F --> G" + shows "sigma |= \G" apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE]) apply (rule 3) done -lemma STL6: "|- <>[]F & <>[]G --> <>[](F & G)" +lemma STL6: "|- \\F & \\G --> \\(F & G)" apply (auto simp: STL5 [temp_rewrite, symmetric]) apply (drule linT [temp_use]) apply assumption @@ -414,13 +410,13 @@ (* ------------------------ True / False ----------------------------------------- *) section "Simplification of constants" -lemma BoxConst: "|- ([]#P) = #P" +lemma BoxConst: "|- (\#P) = #P" apply (rule tempI) apply (cases P) apply (auto intro!: necT [temp_use] dest: STL2_gen [temp_use] simp: Init_simps) done -lemma DmdConst: "|- (<>#P) = #P" +lemma DmdConst: "|- (\#P) = #P" apply (unfold dmd_def) apply (cases P) apply (simp_all add: BoxConst [try_rewrite]) @@ -432,23 +428,23 @@ (* ------------------------ Further rewrites ----------------------------------------- *) section "Further rewrites" -lemma NotBox: "|- (~[]F) = (<>~F)" +lemma NotBox: "|- (\\F) = (\\F)" by (simp add: dmd_def) -lemma NotDmd: "|- (~<>F) = ([]~F)" +lemma NotDmd: "|- (\\F) = (\\F)" by (simp add: dmd_def) (* These are not declared by default, because they could be harmful, - e.g. []F & ~[]F becomes []F & <>~F !! *) + e.g. \F & \\F becomes \F & \\F !! *) lemmas more_temp_simps1 = STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite] NotBox [temp_unlift, THEN eq_reflection] NotDmd [temp_unlift, THEN eq_reflection] -lemma BoxDmdBox: "|- ([]<>[]F) = (<>[]F)" +lemma BoxDmdBox: "|- (\\\F) = (\\F)" apply (auto dest!: STL2 [temp_use]) apply (rule ccontr) - apply (subgoal_tac "sigma |= <>[][]F & <>[]~[]F") + apply (subgoal_tac "sigma |= \\\F & \\\\F") apply (erule thin_rl) apply auto apply (drule STL6 [temp_use]) @@ -457,7 +453,7 @@ apply (simp_all add: more_temp_simps1) done -lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)" +lemma DmdBoxDmd: "|- (\\\F) = (\\F)" apply (unfold dmd_def) apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite]) done @@ -467,11 +463,11 @@ (* ------------------------ Miscellaneous ----------------------------------- *) -lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)" +lemma BoxOr: "\sigma. [| sigma |= \F | \G |] ==> sigma |= \(F | G)" by (fastforce elim!: STL4E [temp_use]) (* "persistently implies infinitely often" *) -lemma DBImplBD: "|- <>[]F --> []<>F" +lemma DBImplBD: "|- \\F --> \\F" apply clarsimp apply (rule ccontr) apply (simp add: more_temp_simps2) @@ -480,13 +476,13 @@ apply simp done -lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)" +lemma BoxDmdDmdBox: "|- \\F & \\G --> \\(F & G)" apply clarsimp apply (rule ccontr) apply (unfold more_temp_simps2) apply (drule STL6 [temp_use]) apply assumption - apply (subgoal_tac "sigma |= <>[]~F") + apply (subgoal_tac "sigma |= \\\F") apply (force simp: dmd_def) apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use]) done @@ -498,11 +494,11 @@ section "priming" (* ------------------------ TLA2 ------------------------------------------- *) -lemma STL2_pr: "|- []P --> Init P & Init P`" +lemma STL2_pr: "|- \P --> Init P & Init P`" by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use]) (* Auxiliary lemma allows priming of boxed actions *) -lemma BoxPrime: "|- []P --> []($P & P$)" +lemma BoxPrime: "|- \P --> \($P & P$)" apply clarsimp apply (erule dup_boxE) apply (unfold boxInit_act) @@ -512,17 +508,17 @@ lemma TLA2: assumes "|- $P & P$ --> A" - shows "|- []P --> []A" + shows "|- \P --> \A" apply clarsimp apply (drule BoxPrime [temp_use]) apply (auto simp: Init_stp_act_rev [try_rewrite] intro!: assms [temp_use] elim!: STL4E [temp_use]) done -lemma TLA2E: "[| sigma |= []P; |- $P & P$ --> A |] ==> sigma |= []A" +lemma TLA2E: "[| sigma |= \P; |- $P & P$ --> A |] ==> sigma |= \A" by (erule (1) TLA2 [temp_use]) -lemma DmdPrime: "|- (<>P`) --> (<>P)" +lemma DmdPrime: "|- (\P`) --> (\P)" apply (unfold dmd_def) apply (fastforce elim!: TLA2E [temp_use]) done @@ -533,13 +529,13 @@ section "stable, invariant" lemma ind_rule: - "[| sigma |= []H; sigma |= Init P; |- H --> (Init P & ~[]F --> Init(P`) & F) |] - ==> sigma |= []F" + "[| sigma |= \H; sigma |= Init P; |- H --> (Init P & \\F --> Init(P`) & F) |] + ==> sigma |= \F" apply (rule indT [temp_use]) apply (erule (2) STL4E) done -lemma box_stp_act: "|- ([]$P) = ([]P)" +lemma box_stp_act: "|- (\$P) = (\P)" by (simp add: boxInit_act Init_simps) lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2] @@ -547,32 +543,32 @@ lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2 -lemma INV1: - "|- (Init P) --> (stable P) --> []P" +lemma INV1: + "|- (Init P) --> (stable P) --> \P" apply (unfold stable_def boxInit_stp boxInit_act) apply clarsimp apply (erule ind_rule) apply (auto simp: Init_simps elim: ind_rule) done -lemma StableT: - "!!P. |- $P & A --> P` ==> |- []A --> stable P" +lemma StableT: + "\P. |- $P & A --> P` ==> |- \A --> stable P" apply (unfold stable_def) apply (fastforce elim!: STL4E [temp_use]) done -lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P" +lemma Stable: "[| sigma |= \A; |- $P & A --> P` |] ==> sigma |= stable P" by (erule (1) StableT [temp_use]) (* Generalization of INV1 *) -lemma StableBox: "|- (stable P) --> [](Init P --> []P)" +lemma StableBox: "|- (stable P) --> \(Init P --> \P)" apply (unfold stable_def) apply clarsimp apply (erule dup_boxE) apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use]) done -lemma DmdStable: "|- (stable P) & <>P --> <>[]P" +lemma DmdStable: "|- (stable P) & \P --> \\P" apply clarsimp apply (rule DmdImpl2) prefer 2 @@ -583,7 +579,7 @@ (* ---------------- (Semi-)automatic invariant tactics ---------------------- *) ML {* -(* inv_tac reduces goals of the form ... ==> sigma |= []P *) +(* inv_tac reduces goals of the form ... ==> sigma |= \P *) fun inv_tac ctxt = SELECT_GOAL (EVERY @@ -593,7 +589,7 @@ TRYALL (etac @{thm Stable})]); (* auto_inv_tac applies inv_tac and then tries to attack the subgoals - in simple cases it may be able to handle goals like |- MyProg --> []Inv. + in simple cases it may be able to handle goals like |- MyProg --> \Inv. In these simple cases the simplifier seems to be more useful than the auto-tactic, which applies too much propositional logic and simplifies too late. @@ -613,7 +609,7 @@ Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac)) *} -lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q" +lemma unless: "|- \($P --> P` | Q`) --> (stable P) | \Q" apply (unfold dmd_def) apply (clarsimp dest!: BoxPrime [temp_use]) apply merge_box @@ -625,29 +621,29 @@ (* --------------------- Recursive expansions --------------------------------------- *) section "recursive expansions" -(* Recursive expansions of [] and <> for state predicates *) -lemma BoxRec: "|- ([]P) = (Init P & []P`)" +(* Recursive expansions of \ and \ for state predicates *) +lemma BoxRec: "|- (\P) = (Init P & \P`)" apply (auto intro!: STL2_gen [temp_use]) apply (fastforce elim!: TLA2E [temp_use]) apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use]) done -lemma DmdRec: "|- (<>P) = (Init P | <>P`)" +lemma DmdRec: "|- (\P) = (Init P | \P`)" apply (unfold dmd_def BoxRec [temp_rewrite]) apply (auto simp: Init_simps) done -lemma DmdRec2: "!!sigma. [| sigma |= <>P; sigma |= []~P` |] ==> sigma |= Init P" +lemma DmdRec2: "\sigma. [| sigma |= \P; sigma |= \\P` |] ==> sigma |= Init P" apply (force simp: DmdRec [temp_rewrite] dmd_def) done -lemma InfinitePrime: "|- ([]<>P) = ([]<>P`)" +lemma InfinitePrime: "|- (\\P) = (\\P`)" apply auto apply (rule classical) apply (rule DBImplBD [temp_use]) - apply (subgoal_tac "sigma |= <>[]P") + apply (subgoal_tac "sigma |= \\P") apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use]) - apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)") + apply (subgoal_tac "sigma |= \\ (\P & \\P`)") apply (force simp: boxInit_stp [temp_use] elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use]) apply (force intro!: STL6 [temp_use] simp: more_temp_simps3) @@ -655,7 +651,7 @@ done lemma InfiniteEnsures: - "[| sigma |= []N; sigma |= []<>A; |- A & N --> P` |] ==> sigma |= []<>P" + "[| sigma |= \N; sigma |= \\A; |- A & N --> P` |] ==> sigma |= \\P" apply (unfold InfinitePrime [temp_rewrite]) apply (rule InfImpl) apply assumption+ @@ -665,27 +661,27 @@ section "fairness" (* alternative definitions of fairness *) -lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(_v) | []<>_v)" +lemma WF_alt: "|- WF(A)_v = (\\\Enabled(_v) | \\_v)" apply (unfold WF_def dmd_def) apply fastforce done -lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(_v) | []<>_v)" +lemma SF_alt: "|- SF(A)_v = (\\\Enabled(_v) | \\_v)" apply (unfold SF_def dmd_def) apply fastforce done (* theorems to "box" fairness conditions *) -lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v" +lemma BoxWFI: "|- WF(A)_v --> \WF(A)_v" by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) -lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v" +lemma WF_Box: "|- (\WF(A)_v) = WF(A)_v" by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use]) -lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v" +lemma BoxSFI: "|- SF(A)_v --> \SF(A)_v" by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use]) -lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v" +lemma SF_Box: "|- (\SF(A)_v) = SF(A)_v" by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use]) lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite] @@ -704,30 +700,30 @@ (* ------------------------------ leads-to ------------------------------ *) -section "~>" +section "\" -lemma leadsto_init: "|- (Init F) & (F ~> G) --> <>G" +lemma leadsto_init: "|- (Init F) & (F \ G) --> \G" apply (unfold leadsto_def) apply (auto dest!: STL2 [temp_use]) done -(* |- F & (F ~> G) --> <>G *) +(* |- F & (F \ G) --> \G *) lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps] -lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))" +lemma streett_leadsto: "|- (\\Init F --> \\G) = (\(F \ G))" apply (unfold leadsto_def) apply auto apply (simp add: more_temp_simps) apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use]) - apply (subgoal_tac "sigma |= []<><>G") + apply (subgoal_tac "sigma |= \\\G") apply (simp add: more_temp_simps) apply (drule BoxDmdDmdBox [temp_use]) apply assumption apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use]) done -lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G" +lemma leadsto_infinite: "|- \\F & (F \ G) --> \\G" apply clarsimp apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]]) apply (simp add: dmdInitD) @@ -736,18 +732,18 @@ (* In particular, strong fairness is a Streett condition. The following rules are sometimes easier to use than WF2 or SF2 below. *) -lemma leadsto_SF: "|- (Enabled(_v) ~> _v) --> SF(A)_v" +lemma leadsto_SF: "|- (Enabled(_v) \ _v) --> SF(A)_v" apply (unfold SF_def) apply (clarsimp elim!: leadsto_infinite [temp_use]) done -lemma leadsto_WF: "|- (Enabled(_v) ~> _v) --> WF(A)_v" +lemma leadsto_WF: "|- (Enabled(_v) \ _v) --> WF(A)_v" by (clarsimp intro!: SFImplWF [temp_use] leadsto_SF [temp_use]) (* introduce an invariant into the proof of a leadsto assertion. - []I --> ((P ~> Q) = (P /\ I ~> Q)) + \I --> ((P \ Q) = (P /\ I \ Q)) *) -lemma INV_leadsto: "|- []I & (P & I ~> Q) --> (P ~> Q)" +lemma INV_leadsto: "|- \I & (P & I \ Q) --> (P \ Q)" apply (unfold leadsto_def) apply clarsimp apply (erule STL4Edup) @@ -755,24 +751,24 @@ apply (auto simp: Init_simps dest!: STL2_gen [temp_use]) done -lemma leadsto_classical: "|- (Init F & []~G ~> G) --> (F ~> G)" +lemma leadsto_classical: "|- (Init F & \\G \ G) --> (F \ G)" apply (unfold leadsto_def dmd_def) apply (force simp: Init_simps elim!: STL4E [temp_use]) done -lemma leadsto_false: "|- (F ~> #False) = ([]~F)" +lemma leadsto_false: "|- (F \ #False) = (\~F)" apply (unfold leadsto_def) apply (simp add: boxNotInitD) done -lemma leadsto_exists: "|- ((EX x. F x) ~> G) = (ALL x. (F x ~> G))" +lemma leadsto_exists: "|- ((\x. F x) \ G) = (\x. (F x \ G))" apply (unfold leadsto_def) apply (auto simp: allT [try_rewrite] Init_simps elim!: STL4E [temp_use]) done (* basic leadsto properties, cf. Unity *) -lemma ImplLeadsto_gen: "|- [](Init F --> Init G) --> (F ~> G)" +lemma ImplLeadsto_gen: "|- \(Init F --> Init G) --> (F \ G)" apply (unfold leadsto_def) apply (auto intro!: InitDmd_gen [temp_use] elim!: STL4E_gen [temp_use] simp: Init_simps) @@ -781,19 +777,19 @@ lemmas ImplLeadsto = ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps] -lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G" +lemma ImplLeadsto_simple: "\F G. |- F --> G ==> |- F \ G" by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use]) lemma EnsuresLeadsto: assumes "|- A & $P --> Q`" - shows "|- []A --> (P ~> Q)" + shows "|- \A --> (P \ Q)" apply (unfold leadsto_def) apply (clarsimp elim!: INV_leadsto [temp_use]) apply (erule STL4E_gen) apply (auto simp: Init_defs intro!: PrimeDmd [temp_use] assms [temp_use]) done -lemma EnsuresLeadsto2: "|- []($P --> Q`) --> (P ~> Q)" +lemma EnsuresLeadsto2: "|- \($P --> Q`) --> (P \ Q)" apply (unfold leadsto_def) apply clarsimp apply (erule STL4E_gen) @@ -803,13 +799,13 @@ lemma ensures: assumes 1: "|- $P & N --> P` | Q`" and 2: "|- ($P & N) & A --> Q`" - shows "|- []N & []([]P --> <>A) --> (P ~> Q)" + shows "|- \N & \(\P --> \A) --> (P \ Q)" apply (unfold leadsto_def) apply clarsimp apply (erule STL4Edup) apply assumption apply clarsimp - apply (subgoal_tac "sigmaa |= [] ($P --> P` | Q`) ") + apply (subgoal_tac "sigmaa |= \($P --> P` | Q`) ") apply (drule unless [temp_use]) apply (clarsimp dest!: INV1 [temp_use]) apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]]) @@ -819,16 +815,16 @@ done lemma ensures_simple: - "[| |- $P & N --> P` | Q`; - |- ($P & N) & A --> Q` - |] ==> |- []N & []<>A --> (P ~> Q)" + "[| |- $P & N --> P` | Q`; + |- ($P & N) & A --> Q` + |] ==> |- \N & \\A --> (P \ Q)" apply clarsimp apply (erule (2) ensures [temp_use]) apply (force elim!: STL4E [temp_use]) done lemma EnsuresInfinite: - "[| sigma |= []<>P; sigma |= []A; |- A & $P --> Q` |] ==> sigma |= []<>Q" + "[| sigma |= \\P; sigma |= \A; |- A & $P --> Q` |] ==> sigma |= \\Q" apply (erule leadsto_infinite [temp_use]) apply (erule EnsuresLeadsto [temp_use]) apply assumption @@ -838,64 +834,64 @@ (*** Gronning's lattice rules (taken from TLP) ***) section "Lattice rules" -lemma LatticeReflexivity: "|- F ~> F" +lemma LatticeReflexivity: "|- F \ F" apply (unfold leadsto_def) apply (rule necT InitDmd_gen)+ done -lemma LatticeTransitivity: "|- (G ~> H) & (F ~> G) --> (F ~> H)" +lemma LatticeTransitivity: "|- (G \ H) & (F \ G) --> (F \ H)" apply (unfold leadsto_def) apply clarsimp - apply (erule dup_boxE) (* [][] (Init G --> H) *) + apply (erule dup_boxE) (* \\(Init G --> H) *) apply merge_box apply (clarsimp elim!: STL4E [temp_use]) apply (rule dup_dmdD) - apply (subgoal_tac "sigmaa |= <>Init G") + apply (subgoal_tac "sigmaa |= \Init G") apply (erule DmdImpl2) apply assumption apply (simp add: dmdInitD) done -lemma LatticeDisjunctionElim1: "|- (F | G ~> H) --> (F ~> H)" +lemma LatticeDisjunctionElim1: "|- (F | G \ H) --> (F \ H)" apply (unfold leadsto_def) apply (auto simp: Init_simps elim!: STL4E [temp_use]) done -lemma LatticeDisjunctionElim2: "|- (F | G ~> H) --> (G ~> H)" +lemma LatticeDisjunctionElim2: "|- (F | G \ H) --> (G \ H)" apply (unfold leadsto_def) apply (auto simp: Init_simps elim!: STL4E [temp_use]) done -lemma LatticeDisjunctionIntro: "|- (F ~> H) & (G ~> H) --> (F | G ~> H)" +lemma LatticeDisjunctionIntro: "|- (F \ H) & (G \ H) --> (F | G \ H)" apply (unfold leadsto_def) apply clarsimp apply merge_box apply (auto simp: Init_simps elim!: STL4E [temp_use]) done -lemma LatticeDisjunction: "|- (F | G ~> H) = ((F ~> H) & (G ~> H))" +lemma LatticeDisjunction: "|- (F | G \ H) = ((F \ H) & (G \ H))" by (auto intro: LatticeDisjunctionIntro [temp_use] LatticeDisjunctionElim1 [temp_use] LatticeDisjunctionElim2 [temp_use]) -lemma LatticeDiamond: "|- (A ~> B | C) & (B ~> D) & (C ~> D) --> (A ~> D)" +lemma LatticeDiamond: "|- (A \ B | C) & (B \ D) & (C \ D) --> (A \ D)" apply clarsimp - apply (subgoal_tac "sigma |= (B | C) ~> D") + apply (subgoal_tac "sigma |= (B | C) \ D") apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use]) apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+ done -lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)" +lemma LatticeTriangle: "|- (A \ D | B) & (B \ D) --> (A \ D)" apply clarsimp - apply (subgoal_tac "sigma |= (D | B) ~> D") + apply (subgoal_tac "sigma |= (D | B) \ D") apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use]) apply assumption apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) done -lemma LatticeTriangle2: "|- (A ~> B | D) & (B ~> D) --> (A ~> D)" +lemma LatticeTriangle2: "|- (A \ B | D) & (B \ D) --> (A \ D)" apply clarsimp - apply (subgoal_tac "sigma |= B | D ~> D") + apply (subgoal_tac "sigma |= B | D \ D") apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use]) apply assumption apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use]) @@ -905,10 +901,10 @@ section "Fairness rules" lemma WF1: - "[| |- $P & N --> P` | Q`; - |- ($P & N) & _v --> Q`; - |- $P & N --> $(Enabled(_v)) |] - ==> |- []N & WF(A)_v --> (P ~> Q)" + "[| |- $P & N --> P` | Q`; + |- ($P & N) & _v --> Q`; + |- $P & N --> $(Enabled(_v)) |] + ==> |- \N & WF(A)_v --> (P \ Q)" apply (clarsimp dest!: BoxWFI [temp_use]) apply (erule (2) ensures [temp_use]) apply (erule (1) STL4Edup) @@ -923,8 +919,8 @@ lemma WF_leadsto: assumes 1: "|- N & $P --> $Enabled (_v)" and 2: "|- N & _v --> B" - and 3: "|- [](N & [~A]_v) --> stable P" - shows "|- []N & WF(A)_v --> (P ~> B)" + and 3: "|- \(N & [~A]_v) --> stable P" + shows "|- \N & WF(A)_v --> (P \ B)" apply (unfold leadsto_def) apply (clarsimp dest!: BoxWFI [temp_use]) apply (erule (1) STL4Edup) @@ -943,10 +939,10 @@ done lemma SF1: - "[| |- $P & N --> P` | Q`; - |- ($P & N) & _v --> Q`; - |- []P & []N & []F --> <>Enabled(_v) |] - ==> |- []N & SF(A)_v & []F --> (P ~> Q)" + "[| |- $P & N --> P` | Q`; + |- ($P & N) & _v --> Q`; + |- \P & \N & \F --> \Enabled(_v) |] + ==> |- \N & SF(A)_v & \F --> (P \ Q)" apply (clarsimp dest!: BoxSFI [temp_use]) apply (erule (2) ensures [temp_use]) apply (erule_tac F = F in dup_boxE) @@ -964,8 +960,8 @@ assumes 1: "|- N & _f --> _g" and 2: "|- $P & P` & _f --> B" and 3: "|- P & Enabled(_g) --> Enabled(_f)" - and 4: "|- [](N & [~B]_f) & WF(A)_f & []F & <>[]Enabled(_g) --> <>[]P" - shows "|- []N & WF(A)_f & []F --> WF(M)_g" + and 4: "|- \(N & [~B]_f) & WF(A)_f & \F & \\Enabled(_g) --> \\P" + shows "|- \N & WF(A)_f & \F --> WF(M)_g" apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2] simp: WF_def [where A = M]) apply (erule_tac F = F in dup_boxE) @@ -974,7 +970,7 @@ apply assumption apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) apply (rule classical) - apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & _f)") + apply (subgoal_tac "sigmaa |= \ (($P & P` & N) & _f)") apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) @@ -983,8 +979,8 @@ apply assumption+ apply (drule STL6 [temp_use]) apply assumption - apply (erule_tac V = "sigmaa |= <>[]P" in thin_rl) - apply (erule_tac V = "sigmaa |= []F" in thin_rl) + apply (erule_tac V = "sigmaa |= \\P" in thin_rl) + apply (erule_tac V = "sigmaa |= \F" in thin_rl) apply (drule BoxWFI [temp_use]) apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) apply merge_temp_box @@ -1002,26 +998,26 @@ assumes 1: "|- N & _f --> _g" and 2: "|- $P & P` & _f --> B" and 3: "|- P & Enabled(_g) --> Enabled(_f)" - and 4: "|- [](N & [~B]_f) & SF(A)_f & []F & []<>Enabled(_g) --> <>[]P" - shows "|- []N & SF(A)_f & []F --> SF(M)_g" + and 4: "|- \(N & [~B]_f) & SF(A)_f & \F & \\Enabled(_g) --> \\P" + shows "|- \N & SF(A)_f & \F --> SF(M)_g" apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M]) apply (erule_tac F = F in dup_boxE) - apply (erule_tac F = "TEMP <>Enabled (_g) " in dup_boxE) + apply (erule_tac F = "TEMP \Enabled (_g) " in dup_boxE) apply merge_temp_box apply (erule STL4Edup) apply assumption apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]]) apply (rule classical) - apply (subgoal_tac "sigmaa |= <> (($P & P` & N) & _f)") + apply (subgoal_tac "sigmaa |= \ (($P & P` & N) & _f)") apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use]) apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use]) apply (simp add: NotDmd [temp_use] not_angle [try_rewrite]) apply merge_act_box apply (frule 4 [temp_use]) apply assumption+ - apply (erule_tac V = "sigmaa |= []F" in thin_rl) + apply (erule_tac V = "sigmaa |= \F" in thin_rl) apply (drule BoxSFI [temp_use]) - apply (erule_tac F = "TEMP <>Enabled (_g)" in dup_boxE) + apply (erule_tac F = "TEMP \Enabled (_g)" in dup_boxE) apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE) apply merge_temp_box apply (erule DmdImpldup) @@ -1041,8 +1037,8 @@ lemma wf_leadsto: assumes 1: "wf r" - and 2: "!!x. sigma |= F x ~> (G | (EX y. #((y,x):r) & F y)) " - shows "sigma |= F x ~> G" + and 2: "\x. sigma |= F x \ (G | (\y. #((y,x):r) & F y)) " + shows "sigma |= F x \ G" apply (rule 1 [THEN wf_induct]) apply (rule LatticeTriangle [temp_use]) apply (rule 2) @@ -1053,10 +1049,10 @@ done (* If r is well-founded, state function v cannot decrease forever *) -lemma wf_not_box_decrease: "!!r. wf r ==> |- [][ (v`, $v) : #r ]_v --> <>[][#False]_v" +lemma wf_not_box_decrease: "\r. wf r ==> |- \[ (v`, $v) : #r ]_v --> \\[#False]_v" apply clarsimp apply (rule ccontr) - apply (subgoal_tac "sigma |= (EX x. v=#x) ~> #False") + apply (subgoal_tac "sigma |= (\x. v=#x) \ #False") apply (drule leadsto_false [temp_use, THEN iffD1, THEN STL2_gen [temp_use]]) apply (force simp: Init_defs) apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps) @@ -1065,7 +1061,7 @@ apply (auto simp: square_def angle_def) done -(* "wf r ==> |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *) +(* "wf r ==> |- \\[ (v`, $v) : #r ]_v --> \\[#False]_v" *) lemmas wf_not_dmd_box_decrease = wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps] @@ -1074,14 +1070,14 @@ *) lemma wf_box_dmd_decrease: assumes 1: "wf r" - shows "|- []<>((v`, $v) : #r) --> []<><(v`, $v) ~: #r>_v" + shows "|- \\((v`, $v) : #r) --> \\<(v`, $v) \ #r>_v" apply clarsimp apply (rule ccontr) apply (simp add: not_angle [try_rewrite] more_temp_simps) apply (drule 1 [THEN wf_not_dmd_box_decrease [temp_use]]) apply (drule BoxDmdDmdBox [temp_use]) apply assumption - apply (subgoal_tac "sigma |= []<> ((#False) ::action)") + apply (subgoal_tac "sigma |= \\ ((#False) ::action)") apply force apply (erule STL4E) apply (rule DmdImpl) @@ -1091,9 +1087,9 @@ (* In particular, for natural numbers, if n decreases infinitely often then it has to increase infinitely often. *) -lemma nat_box_dmd_decrease: "!!n::nat stfun. |- []<>(n` < $n) --> []<>($n < n`)" +lemma nat_box_dmd_decrease: "\n::nat stfun. |- \\(n` < $n) --> \\($n < n`)" apply clarsimp - apply (subgoal_tac "sigma |= []<><~ ((n`,$n) : #less_than) >_n") + apply (subgoal_tac "sigma |= \\<~ ((n`,$n) : #less_than) >_n") apply (erule thin_rl) apply (erule STL4E) apply (rule DmdImpl) @@ -1110,11 +1106,11 @@ lemma aallI: assumes 1: "basevars vs" - and 2: "(!!x. basevars (x,vs) ==> sigma |= F x)" - shows "sigma |= (AALL x. F x)" + and 2: "(\x. basevars (x,vs) ==> sigma |= F x)" + shows "sigma |= (\\x. F x)" by (auto simp: aall_def elim!: eexE [temp_use] intro!: 1 dest!: 2 [temp_use]) -lemma aallE: "|- (AALL x. F x) --> F x" +lemma aallE: "|- (\\x. F x) --> F x" apply (unfold aall_def) apply clarsimp apply (erule contrapos_np) @@ -1123,18 +1119,18 @@ (* monotonicity of quantification *) lemma eex_mono: - assumes 1: "sigma |= EEX x. F x" - and 2: "!!x. sigma |= F x --> G x" - shows "sigma |= EEX x. G x" + assumes 1: "sigma |= \\x. F x" + and 2: "\x. sigma |= F x --> G x" + shows "sigma |= \\x. G x" apply (rule unit_base [THEN 1 [THEN eexE]]) apply (rule eexI [temp_use]) apply (erule 2 [unfolded intensional_rews, THEN mp]) done lemma aall_mono: - assumes 1: "sigma |= AALL x. F(x)" - and 2: "!!x. sigma |= F(x) --> G(x)" - shows "sigma |= AALL x. G(x)" + assumes 1: "sigma |= \\x. F(x)" + and 2: "\x. sigma |= F(x) --> G(x)" + shows "sigma |= \\x. G(x)" apply (rule unit_base [THEN aallI]) apply (rule 2 [unfolded intensional_rews, THEN mp]) apply (rule 1 [THEN aallE [temp_use]]) @@ -1143,11 +1139,11 @@ (* Derived history introduction rule *) lemma historyI: assumes 1: "sigma |= Init I" - and 2: "sigma |= []N" + and 2: "sigma |= \N" and 3: "basevars vs" - and 4: "!!h. basevars(h,vs) ==> |- I & h = ha --> HI h" - and 5: "!!h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)" - shows "sigma |= EEX h. Init (HI h) & [](HN h)" + and 4: "\h. basevars(h,vs) ==> |- I & h = ha --> HI h" + and 5: "\h s t. [| basevars(h,vs); N (s,t); h t = hb (h s) (s,t) |] ==> HN h (s,t)" + shows "sigma |= \\h. Init (HI h) & \(HN h)" apply (rule history [temp_use, THEN eexE]) apply (rule 3) apply (rule eexI [temp_use]) @@ -1165,7 +1161,7 @@ example of a history variable: existence of a clock *) -lemma "|- EEX h. Init(h = #True) & [](h` = (~$h))" +lemma "|- \\h. Init(h = #True) & \(h` = (~$h))" apply (rule tempI) apply (rule historyI) apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+