theory Finalise_DR

lemma do_machine_op_wp:
  "\<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
    \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op mop \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" apply (clarsimp simp:do_machine_op_def gets_def get_def return_def bind_def select_f_def simpler_modify_def) apply (clarsimp simp:valid_def) apply (drule_tac x = "(machine_state s)" in spec) apply (drule_tac x = "(a,b)" in bspec) apply simp apply clarsimp apply (clarsimp simp:transform_def transform_current_thread_def) apply (simp add: transform_objects_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op mop \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> \<lambda>s. (\<Union>a\<in>fst (mop (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa), (\<exists>x\<in>fst (mop (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) s)) \<or> snd (mop (machine_state s))) \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. \<forall>x\<in>fst (mop s). case x of (r, s') \<Rightarrow> underlying_memory s' = underlying_memory s; cs = transform s; (a, b) \<in> fst (mop (machine_state s))\<rbrakk> \<Longrightarrow> transform (update_machine b s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cs = transform s; (a, b) \<in> fst (mop (machine_state s)); \<forall>x\<in>fst (mop (machine_state s)). case x of (r, s') \<Rightarrow> underlying_memory s' = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> transform (update_machine b s) = transform s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>cs = transform s; (a, b) \<in> fst (mop (machine_state s))\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (mop (machine_state s))
 2. \<And>s a b. \<lbrakk>cs = transform s; (a, b) \<in> fst (mop (machine_state s)); case (a, b) of (r, s') \<Rightarrow> underlying_memory s' = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> transform (update_machine b s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cs = transform s; (a, b) \<in> fst (mop (machine_state s)); case (a, b) of (r, s') \<Rightarrow> underlying_memory s' = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> transform (update_machine b s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cs = transform s; (a, b) \<in> fst (mop (machine_state s)); underlying_memory b = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> transform (update_machine b s) = transform s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cs = \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = transform_cdt s, cdl_current_thread = if cur_thread s \<noteq> idle_thread s then Some (cur_thread s) else None, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr>; (a, b) \<in> fst (mop (machine_state s)); underlying_memory b = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> transform_objects (update_machine b s) = transform_objects s proof (prove)
goal:
No subgoals!