# HG changeset patch
# User wenzelm
# Date 1452547383 -3600
# Node ID 324bc1ffba12e06bafb3a8b5428da04dbfe47a04
# Parent 5b946c81dfbf586806f8008c2e2adf52af61cfc8
eliminated old defs;
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Action.thy Mon Jan 11 22:23:03 2016 +0100
@@ -9,25 +9,19 @@
imports Stfun
begin
-
-(** abstract syntax **)
-
-type_synonym 'a trfun = "(state * state) \<Rightarrow> 'a"
-type_synonym action = "bool trfun"
+type_synonym 'a trfun = "state \<times> state \<Rightarrow> 'a"
+type_synonym action = "bool trfun"
instance prod :: (world, world) world ..
-consts
- (** abstract syntax **)
- before :: "'a stfun \<Rightarrow> 'a trfun"
- after :: "'a stfun \<Rightarrow> 'a trfun"
- unch :: "'a stfun \<Rightarrow> action"
+definition enabled :: "action \<Rightarrow> stpred"
+ where "enabled A s \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+
- SqAct :: "[action, 'a stfun] \<Rightarrow> action"
- AnAct :: "[action, 'a stfun] \<Rightarrow> action"
- enabled :: "action \<Rightarrow> stpred"
-
-(** concrete syntax **)
+consts
+ before :: "'a stfun \<Rightarrow> 'a trfun"
+ after :: "'a stfun \<Rightarrow> 'a trfun"
+ unch :: "'a stfun \<Rightarrow> action"
syntax
(* Syntax for writing action expressions in arbitrary contexts *)
@@ -40,8 +34,6 @@
(*** Priming: same as "after" ***)
"_prime" :: "lift \<Rightarrow> lift" ("(_`)" [100] 99)
- "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0,1000] 99)
- "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0,1000] 99)
"_Enabled" :: "lift \<Rightarrow> lift" ("(Enabled _)" [100] 100)
translations
@@ -50,25 +42,30 @@
"_after" == "CONST after"
"_prime" => "_after"
"_unchanged" == "CONST unch"
- "_SqAct" == "CONST SqAct"
- "_AnAct" == "CONST AnAct"
"_Enabled" == "CONST enabled"
- "w \<Turnstile> [A]_v" <= "_SqAct A v w"
- "w \<Turnstile> <A>_v" <= "_AnAct A v w"
"s \<Turnstile> Enabled A" <= "_Enabled A s"
"w \<Turnstile> unchanged f" <= "_unchanged f w"
axiomatization where
unl_before: "(ACT $v) (s,t) \<equiv> v s" and
unl_after: "(ACT v$) (s,t) \<equiv> v t" and
-
unchanged_def: "(s,t) \<Turnstile> unchanged v \<equiv> (v t = v s)"
-defs
- square_def: "ACT [A]_v \<equiv> ACT (A \<or> unchanged v)"
- angle_def: "ACT <A>_v \<equiv> ACT (A \<and> \<not> unchanged v)"
+
+definition SqAct :: "[action, 'a stfun] \<Rightarrow> action"
+ where square_def: "SqAct A v \<equiv> ACT (A \<or> unchanged v)"
+
+definition AnAct :: "[action, 'a stfun] \<Rightarrow> action"
+ where angle_def: "AnAct A v \<equiv> ACT (A \<and> \<not> unchanged v)"
- enabled_def: "s \<Turnstile> Enabled A \<equiv> \<exists>u. (s,u) \<Turnstile> A"
+syntax
+ "_SqAct" :: "[lift, lift] \<Rightarrow> lift" ("([_]'_(_))" [0, 1000] 99)
+ "_AnAct" :: "[lift, lift] \<Rightarrow> lift" ("(<_>'_(_))" [0, 1000] 99)
+translations
+ "_SqAct" == "CONST SqAct"
+ "_AnAct" == "CONST AnAct"
+ "w \<Turnstile> [A]_v" \<leftharpoondown> "_SqAct A v w"
+ "w \<Turnstile> <A>_v" \<leftharpoondown> "_AnAct A v w"
(* The following assertion specializes "intI" for any world type
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Init.thy Mon Jan 11 22:23:03 2016 +0100
@@ -16,25 +16,22 @@
type_synonym temporal = "behavior form"
-
consts
- Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
first_world :: "behavior \<Rightarrow> ('w::world)"
st1 :: "behavior \<Rightarrow> state"
st2 :: "behavior \<Rightarrow> state"
+definition Initial :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+ where Init_def: "Initial F sigma = F (first_world sigma)"
+
syntax
"_TEMP" :: "lift \<Rightarrow> 'a" ("(TEMP _)")
"_Init" :: "lift \<Rightarrow> lift" ("(Init _)"[40] 50)
-
translations
"TEMP F" => "(F::behavior \<Rightarrow> _)"
"_Init" == "CONST Initial"
"sigma \<Turnstile> Init F" <= "_Init F sigma"
-defs
- Init_def: "sigma \<Turnstile> Init F == (first_world sigma) \<Turnstile> F"
-
overloading
fw_temp \<equiv> "first_world :: behavior \<Rightarrow> behavior"
fw_stp \<equiv> "first_world :: behavior \<Rightarrow> state"
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Mon Jan 11 22:23:03 2016 +0100
@@ -74,10 +74,10 @@
unanswered call for that process.
*)
lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
- by (auto simp: Return_def MC_action_defs)
+ by (auto simp: AReturn_def MC_action_defs)
lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
- by (auto simp: Call_def MC_action_defs)
+ by (auto simp: ACall_def MC_action_defs)
(* Enabledness of actions *)
@@ -86,7 +86,7 @@
\<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA
\<longrightarrow> Enabled (MClkFwd send rcv cst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
- @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow>
@@ -103,7 +103,7 @@
apply (tactic \<open>action_simp_tac @{context}
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
apply (tactic \<open>action_simp_tac (@{context} addsimps
- [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
+ [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
done
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy Mon Jan 11 22:23:03 2016 +0100
@@ -178,7 +178,7 @@
*)
lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
- by (auto simp: Return_def RM_action_defs)
+ by (auto simp: AReturn_def RM_action_defs)
(* Enabledness conditions *)
@@ -191,7 +191,7 @@
apply (tactic
\<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+ \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
@{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
done
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Jan 11 22:23:03 2016 +0100
@@ -320,7 +320,7 @@
(* ==================== Lemmas about the environment ============================== *)
lemma Envbusy: "\<turnstile> $(Calling memCh p) \<longrightarrow> \<not>ENext p"
- by (auto simp: ENext_def Call_def)
+ by (auto simp: ENext_def ACall_def)
(* ==================== Lemmas about the implementation's states ==================== *)
@@ -333,7 +333,7 @@
lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
\<longrightarrow> (S2 rmhist p)$"
- by (force simp: ENext_def Call_def c_def r_def m_def
+ by (force simp: ENext_def ACall_def c_def r_def m_def
caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
@@ -352,7 +352,7 @@
\<longrightarrow> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
@{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
- @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
+ @{thm AReturn_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
(* ------------------------------ State S2 ---------------------------------------- *)
@@ -367,7 +367,7 @@
\<and> unchanged (e p, r p, m p, rmhist!p)
\<longrightarrow> (S3 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
- @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
+ @{thm ACall_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
@{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
@@ -380,7 +380,7 @@
\<longrightarrow> unchanged (rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S2_def)
+ MClkReply_def AReturn_def S_def S2_def)
(* ------------------------------ State S3 ---------------------------------------- *)
@@ -405,7 +405,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
@{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
- @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
+ @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ACall_def}, @{thm e_def},
@{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -413,7 +413,7 @@
\<and> unchanged (e p, c p, m p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
+ @{thm RPCFail_def}, @{thm AReturn_def}, @{thm e_def}, @{thm c_def},
@{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
@{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -422,7 +422,7 @@
lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
- Return_def r_def rtrner_def S_def S3_def Calling_def)
+ AReturn_def r_def rtrner_def S_def S3_def Calling_def)
(* ------------------------------ State S4 ---------------------------------------- *)
@@ -441,7 +441,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
@{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
- @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
@{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
@{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
@@ -455,7 +455,7 @@
\<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
@{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
- @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
+ @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm AReturn_def}, @{thm e_def},
@{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
@{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -471,12 +471,12 @@
lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
\<and> HNext rmhist p
\<longrightarrow> (S5 rmhist p)$"
- by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
+ by (auto simp: HNext_def MemReturn_def AReturn_def e_def c_def r_def
rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
- Return_def m_def rtrner_def S_def S4_def Calling_def)
+ AReturn_def m_def rtrner_def S_def S4_def Calling_def)
(* ------------------------------ State S5 ---------------------------------------- *)
@@ -493,14 +493,14 @@
lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
+ @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
@{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
\<longrightarrow> (S6 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
- @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
+ @{thm AReturn_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
@{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -511,7 +511,7 @@
\<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
using [[fast_solver]]
by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
- MClkReply_def Return_def S_def S5_def)
+ MClkReply_def AReturn_def S_def S5_def)
(* ------------------------------ State S6 ---------------------------------------- *)
@@ -526,7 +526,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
+ @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm ACall_def}, @{thm AReturn_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -534,7 +534,7 @@
\<and> unchanged (e p,r p,m p)
\<longrightarrow> (S1 rmhist p)$"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
- @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
+ @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm AReturn_def}, @{thm MClkReply_def},
@{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
@{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
@@ -545,7 +545,7 @@
by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
- by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
+ by (auto simp: HNext_def MClkReply_def AReturn_def c_def rtrner_def S_def S6_def Calling_def)
section "Correctness of predicate-action diagram"
@@ -676,7 +676,7 @@
apply (drule S6_excl [temp_use])
apply (auto simp: RPCFail_def MemFail_def e_def c_def m_def resbar_def)
apply (force simp: S3_def S_def)
- apply (auto simp: Return_def)
+ apply (auto simp: AReturn_def)
done
lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
@@ -724,7 +724,7 @@
@{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply (drule S4_excl [temp_use] S5_excl [temp_use])+
using [[fast_solver]]
- apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
+ apply (auto elim!: squareE [temp_use] simp: MemReturn_def AReturn_def)
done
lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -733,7 +733,7 @@
apply clarsimp
apply (drule S5_excl [temp_use] S6_excl [temp_use])+
apply (auto simp: e_def c_def m_def resbar_def)
- apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
+ apply (auto simp: RPCReply_def AReturn_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
done
lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
@@ -741,7 +741,7 @@
\<longrightarrow> MemFail memCh (resbar rmhist) p"
apply clarsimp
apply (drule S6_excl [temp_use])
- apply (auto simp: e_def c_def m_def RPCFail_def Return_def MemFail_def resbar_def)
+ apply (auto simp: e_def c_def m_def RPCFail_def AReturn_def MemFail_def resbar_def)
apply (auto simp: S5_def S_def)
done
@@ -752,7 +752,7 @@
apply (drule S6_excl [temp_use])+
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
@{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
+ @{thm AReturn_def}, @{thm resbar_def}]) [] [] 1\<close>)
apply simp_all (* simplify if-then-else *)
apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
[@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
@@ -909,7 +909,7 @@
lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
\<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
- @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
+ @{thm AReturn_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
\<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1088,7 +1088,7 @@
lemma MClkReplyS6:
"\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
- @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
+ @{thm MClkReply_def}, @{thm AReturn_def}, @{thm ImpInv_def}, @{thm S_def},
@{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Mon Jan 11 22:23:03 2016 +0100
@@ -37,14 +37,13 @@
(* slice through array-valued state function *)
-consts
- slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+definition slice :: "('a \<Rightarrow> 'b) stfun \<Rightarrow> 'a \<Rightarrow> 'b stfun"
+ where "slice x i s \<equiv> x s i"
+
syntax
- "_slice" :: "[lift, 'a] \<Rightarrow> lift" ("(_!_)" [70,70] 70)
+ "_slice" :: "[lift, 'a] \<Rightarrow> lift" ("(_!_)" [70,70] 70)
translations
- "_slice" == "CONST slice"
-defs
- slice_def: "(PRED (x!i)) s == x s i"
+ "_slice" \<rightleftharpoons> "CONST slice"
(* state predicates *)
@@ -55,22 +54,24 @@
(* actions *)
-consts
- ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
- AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+definition ACall :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'a stfun \<Rightarrow> action"
+ where "ACall ch p v \<equiv> ACT
+ \<not> $Calling ch p
+ \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+ \<and> (arg<ch!p>$ = $v)"
+
+definition AReturn :: "('a,'r) channel \<Rightarrow> PrIds \<Rightarrow> 'r stfun \<Rightarrow> action"
+ where "AReturn ch p v == ACT
+ $Calling ch p
+ \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+ \<and> (res<ch!p>$ = $v)"
+
syntax
- "_Call" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Call _ _ _)" [90,90,90] 90)
- "_Return" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Return _ _ _)" [90,90,90] 90)
+ "_Call" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Call _ _ _)" [90,90,90] 90)
+ "_Return" :: "['a, 'b, lift] \<Rightarrow> lift" ("(Return _ _ _)" [90,90,90] 90)
translations
- "_Call" == "CONST ACall"
- "_Return" == "CONST AReturn"
-defs
- Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p
- \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
- \<and> (arg<ch!p>$ = $v)"
- Return_def: "(ACT Return ch p v) == ACT $Calling ch p
- \<and> (rbit<ch!p>$ = $cbit<ch!p>)
- \<and> (res<ch!p>$ = $v)"
+ "_Call" \<rightleftharpoons> "CONST ACall"
+ "_Return" \<rightleftharpoons> "CONST AReturn"
(* temporal formulas *)
@@ -91,14 +92,14 @@
declare slice_def [simp]
-lemmas Procedure_defs = caller_def rtrner_def Calling_def Call_def Return_def
+lemmas Procedure_defs = caller_def rtrner_def Calling_def ACall_def AReturn_def
PLegalCaller_def LegalCaller_def PLegalReturner_def LegalReturner_def
(* Calls and returns change their subchannel *)
lemma Call_changed: "\<turnstile> Call ch p v \<longrightarrow> <Call ch p v>_((caller ch)!p)"
- by (auto simp: angle_def Call_def caller_def Calling_def)
+ by (auto simp: angle_def ACall_def caller_def Calling_def)
lemma Return_changed: "\<turnstile> Return ch p v \<longrightarrow> <Return ch p v>_((rtrner ch)!p)"
- by (auto simp: angle_def Return_def rtrner_def Calling_def)
+ by (auto simp: angle_def AReturn_def rtrner_def Calling_def)
end
diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Mon Jan 11 22:23:03 2016 +0100
@@ -83,7 +83,7 @@
*)
lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
- by (auto simp: Return_def RPC_action_defs)
+ by (auto simp: AReturn_def RPC_action_defs)
lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)
@@ -101,14 +101,14 @@
lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
- @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB
\<longrightarrow> Enabled (RPCReply send rcv rst p)"
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
- @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
+ @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
end