187 |
187 |
188 lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
188 lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
189 \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult) |
189 \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult) |
190 \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))" |
190 \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))" |
191 apply (tactic |
191 apply (tactic |
192 \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>) |
192 \<open>action_simp_tac \<^context> [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>) |
193 apply (tactic |
193 apply (tactic |
194 \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def}, |
194 \<open>action_simp_tac (\<^context> addsimps [@{thm MemReturn_def}, @{thm AReturn_def}, |
195 @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
195 @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
196 done |
196 done |
197 |
197 |
198 lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
198 lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
199 \<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)" |
199 \<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)" |
233 lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) \<Longrightarrow> |
233 lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) \<Longrightarrow> |
234 \<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l) |
234 \<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l) |
235 \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" |
235 \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" |
236 apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use]) |
236 apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use]) |
237 apply (case_tac "arg (ch w p)") |
237 apply (case_tac "arg (ch w p)") |
238 apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Read_def}, |
238 apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Read_def}, |
239 temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>) |
239 temp_rewrite \<^context> @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>) |
240 apply (force dest: base_pair [temp_use]) |
240 apply (force dest: base_pair [temp_use]) |
241 apply (erule contrapos_np) |
241 apply (erule contrapos_np) |
242 apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Write_def}, |
242 apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Write_def}, |
243 temp_rewrite @{context} @{thm enabled_ex}]) |
243 temp_rewrite \<^context> @{thm enabled_ex}]) |
244 [@{thm WriteInner_enabled}, exI] [] 1\<close>) |
244 [@{thm WriteInner_enabled}, exI] [] 1\<close>) |
245 done |
245 done |
246 |
246 |
247 end |
247 end |