theory ArchRetype_IF

lemma dmo_no_mem_globals_equiv:
  "\<lbrakk> \<And>P. f \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace>;
     \<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>;
     \<And>P. f \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> \<rbrakk>
     \<Longrightarrow> do_machine_op f \<lbrace>globals_equiv s\<rbrace>" unfolding do_machine_op_def apply (wp | simp add: split_def)+ apply atomize apply (erule_tac x="(=) (underlying_memory (machine_state sa))" in allE) apply (erule_tac x="(=) (device_state (machine_state sa))" in allE) apply (erule_tac x="(=) (exclusive_state (machine_state sa))" in allE) apply (fastforce simp: valid_def globals_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> do_machine_op f \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<And>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>; \<And>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>; globals_equiv s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>P. \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (underlying_memory ms)\<rbrace>; \<forall>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>; \<forall>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>; globals_equiv s sa\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>; \<forall>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>; globals_equiv s sa; \<lbrace>\<lambda>ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace> f \<lbrace>\<lambda>_ ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>P. \<lbrace>\<lambda>ms. P (exclusive_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (exclusive_state ms)\<rbrace>; globals_equiv s sa; \<lbrace>\<lambda>ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace> f \<lbrace>\<lambda>_ ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace>; \<lbrace>\<lambda>ms. device_state (machine_state sa) = device_state ms\<rbrace> f \<lbrace>\<lambda>_ ms. device_state (machine_state sa) = device_state ms\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>globals_equiv s sa; \<lbrace>\<lambda>ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace> f \<lbrace>\<lambda>_ ms. underlying_memory (machine_state sa) = underlying_memory ms\<rbrace>; \<lbrace>\<lambda>ms. device_state (machine_state sa) = device_state ms\<rbrace> f \<lbrace>\<lambda>_ ms. device_state (machine_state sa) = device_state ms\<rbrace>; \<lbrace>\<lambda>ms. exclusive_state (machine_state sa) = exclusive_state ms\<rbrace> f \<lbrace>\<lambda>_ ms. exclusive_state (machine_state sa) = exclusive_state ms\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!