1 (* Title: HOL/TLA/Memory/MemClerk.thy |
1 (* Title: HOL/TLA/Memory/MemClerk.thy |
2 Author: Stephan Merz, University of Munich |
2 Author: Stephan Merz, University of Munich |
3 *) |
3 *) |
4 |
4 |
5 section {* RPC-Memory example: specification of the memory clerk *} |
5 section \<open>RPC-Memory example: specification of the memory clerk\<close> |
6 |
6 |
7 theory MemClerk |
7 theory MemClerk |
8 imports Memory RPC MemClerkParameters |
8 imports Memory RPC MemClerkParameters |
9 begin |
9 begin |
10 |
10 |
83 (* Enabledness of actions *) |
83 (* Enabledness of actions *) |
84 |
84 |
85 lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow> |
85 lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow> |
86 \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA |
86 \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA |
87 \<longrightarrow> Enabled (MClkFwd send rcv cst p)" |
87 \<longrightarrow> Enabled (MClkFwd send rcv cst p)" |
88 by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, |
88 by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, |
89 @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
89 @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
90 [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
90 [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
91 |
91 |
92 lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow> |
92 lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow> |
93 Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
93 Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
94 by (auto elim!: enabled_mono simp: angle_def MClkFwd_def) |
94 by (auto elim!: enabled_mono simp: angle_def MClkFwd_def) |
95 |
95 |
98 by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use]) |
98 by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use]) |
99 |
99 |
100 lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow> |
100 lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow> |
101 \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB |
101 \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB |
102 \<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
102 \<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
103 apply (tactic {* action_simp_tac @{context} |
103 apply (tactic \<open>action_simp_tac @{context} |
104 [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *}) |
104 [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>) |
105 apply (tactic {* action_simp_tac (@{context} addsimps |
105 apply (tactic \<open>action_simp_tac (@{context} addsimps |
106 [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) |
106 [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) |
107 [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
107 [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
108 done |
108 done |
109 |
109 |
110 lemma MClkReplyNotRetry: "\<turnstile> MClkReply send rcv cst p \<longrightarrow> \<not>MClkRetry send rcv cst p" |
110 lemma MClkReplyNotRetry: "\<turnstile> MClkReply send rcv cst p \<longrightarrow> \<not>MClkRetry send rcv cst p" |
111 by (auto simp: MClkReply_def MClkRetry_def) |
111 by (auto simp: MClkReply_def MClkRetry_def) |
112 |
112 |