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 \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, |
88 by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm MClkFwd_def}, |
89 @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
89 @{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
90 [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
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))" |
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 \<open>action_simp_tac @{context} |
103 apply (tactic \<open>action_simp_tac \<^context> |
104 [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>) |
104 [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>) |
105 apply (tactic \<open>action_simp_tac (@{context} addsimps |
105 apply (tactic \<open>action_simp_tac (\<^context> addsimps |
106 [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) |
106 [@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) |
107 [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
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" |