theory ArchScheduler_IF

lemma reads_respects_scheduler_clearExMonitor[wp]:
  "reads_respects_scheduler aag l \<top> (do_machine_op clearExMonitor)" apply (simp add: clearExMonitor_def) apply (wp dmo_ev) apply (rule ev_modify) apply clarsimp apply (rule conjI) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
                         silc_dom_equiv_def equiv_for_def) apply (clarsimp simp: scheduler_affects_equiv_def arch_scheduler_affects_equiv_def
                        states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def
                        scheduler_globals_frame_equiv_def
              simp del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do_machine_op clearExMonitor) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. equiv_valid_inv (\<lambda>ms ms'. scheduler_equiv aag (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (\<lambda>ms ms'. scheduler_affects_equiv aag l (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (K (True \<and> True)) (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>K (True \<and> True) sa; K (True \<and> True) t; scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa t. \<lbrakk>scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>)
 2. \<And>s s' sa t. \<lbrakk>scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!