theory Scheduler_IF

lemma dmo_no_mem_globals_equiv_scheduler:
  assumes a: "\<And>P. f \<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace>"
      and b: "\<And>P. f \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace>"
  shows "do_machine_op f \<lbrace>globals_equiv_scheduler s\<rbrace>" unfolding do_machine_op_def apply (rule hoare_pre) apply (wp | simp add: split_def)+ apply clarsimp apply (frule_tac P4 = "\<lambda>um. um = underlying_memory (machine_state sa)" in use_valid[OF _ a]) apply simp apply (frule_tac P4 = "\<lambda>um. um = device_state (machine_state sa)" in use_valid[OF _ b]) apply simp apply (fastforce simp: valid_def globals_equiv_scheduler_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler s\<rbrace> do_machine_op f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler 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_scheduler s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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_scheduler s\<rbrace>
 2. \<And>sa. globals_equiv_scheduler s sa \<Longrightarrow> ?Q sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv_scheduler s sa \<Longrightarrow> \<forall>x\<in>fst (f (machine_state sa)). globals_equiv_scheduler s (sa\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> underlying_memory (machine_state sa) = underlying_memory (machine_state sa)
 2. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa)); underlying_memory b = underlying_memory (machine_state sa)\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa)); underlying_memory b = underlying_memory (machine_state sa)\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa)); underlying_memory b = underlying_memory (machine_state sa)\<rbrakk> \<Longrightarrow> device_state (machine_state sa) = device_state (machine_state sa)
 2. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa)); underlying_memory b = underlying_memory (machine_state sa); device_state b = device_state (machine_state sa)\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a b. \<lbrakk>globals_equiv_scheduler s sa; (a, b) \<in> fst (f (machine_state sa)); underlying_memory b = underlying_memory (machine_state sa); device_state b = device_state (machine_state sa)\<rbrakk> \<Longrightarrow> globals_equiv_scheduler s (sa\<lparr>machine_state := b\<rparr>) proof (prove)
goal:
No subgoals!