kings-crown/FVELER_Isabelle huggingface dataset:
theory Scheduler_IF

lemma silc_dom_equiv_states_equiv_lift:
  assumes a: "\<And>P Q R S st. f \<lbrace>states_equiv_for P Q R S st\<rbrace>"
  shows "f \<lbrace>silc_dom_equiv aag st\<rbrace>" apply (simp add: silc_dom_equiv_as_states_equiv[abs_def]) apply (clarsimp simp add: valid_def) apply (frule use_valid[OF _ a]) apply assumption apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s\<rbrace> f \<lbrace>\<lambda>_ s. states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>kheap := kheap st\<rparr>) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> states_equiv_for (?P9 s a b) (?Q9 s a b) (?R9 s a b) (?S9 s a b) (?st9 s a b) s
 2. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s; (a, b) \<in> fst (f s); states_equiv_for (?P9 s a b) (?Q9 s a b) (?R9 s a b) (?S9 s a b) (?st9 s a b) b\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>kheap := kheap st\<rparr>) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) s; (a, b) \<in> fst (f s); states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>kheap := kheap st\<rparr>) b\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>kheap := kheap st\<rparr>) b proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma store_cur_thread_midstrength_reads_respects:
  "equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
               (scheduler_affects_equiv aag l) (invs and (\<lambda>s. t = idle_thread s))
               (do x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
                   set_scheduler_action resume_cur_thread
                od)" apply (clarsimp simp: do_machine_op_def bind_def gets_def get_def return_def select_f_def
                        set_scheduler_action_def assert_def simpler_modify_def fail_def) apply (fold simpler_modify_def) apply (rule ev_modify) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
                        scheduler_affects_equiv_def states_equiv_for_def idle_equiv_def equiv_for_def
                        equiv_asids_def scheduler_globals_frame_equiv_def silc_dom_equiv_def
                        weak_scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and (\<lambda>s. t = idle_thread s)) (do x <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and (\<lambda>s. t = idle_thread s)) (\<lambda>s. ({((), s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>)}, False)) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and (\<lambda>s. t = idle_thread s)) (modify (\<lambda>s. s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>(invs and (\<lambda>s. t = idle_thread s)) s; (invs and (\<lambda>s. t = idle_thread s)) ta; midstrength_scheduler_affects_equiv aag l s ta; scheduler_equiv aag s ta\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) (ta\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) (ta\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma thread_get_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l (K (pasObjectAbs aag t \<in> reads_scheduler aag l)) (thread_get f t)" apply (rule gen_asm_ev) apply (simp add: thread_get_def) apply (wpsimp simp: scheduler_affects_equiv_def states_equiv_for_def equiv_for_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (pasObjectAbs aag t \<in> reads_scheduler aag l)) (thread_get f t) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (thread_get f t) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do tcb <- gets_the (get_tcb t);
return (f tcb)
od) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma silc_dom_lift:
  assumes a: "\<And>P. f \<lbrace>\<lambda>s. P (kheap s)\<rbrace>"
  shows "f \<lbrace>silc_dom_equiv aag st\<rbrace>" by (wpsimp wp: a simp: silc_dom_equiv_def equiv_for_def[abs_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>
theory Scheduler_IF

lemma dmo_silc_dom[wp]:
  "do_machine_op mop \<lbrace>silc_dom_equiv aag st\<rbrace>" by (wp silc_dom_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_dom_equiv aag st\<rbrace> do_machine_op mop \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>
theory Scheduler_IF

lemma asahi_scheduler_affects_equiv_sym[elim]:
  "asahi_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_scheduler_affects_equiv aag l s' s" apply (simp add: asahi_scheduler_affects_equiv_def) apply (auto simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asahi_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_scheduler_affects_equiv aag l s' s proof (prove)
goal (1 subgoal):
 1. states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s') \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed s' = work_units_completed s \<and> scheduler_globals_frame_equiv s' s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma midstrength_weak[intro]:
  "midstrength_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s s'" by (auto simp: midstrength_scheduler_affects_equiv_def weak_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s s'
theory Scheduler_IF

lemma asahi_ex_scheduler_affects_equiv_sym[elim]:
  "asahi_ex_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l s' s" apply (simp add: asahi_ex_scheduler_affects_equiv_def) apply (auto simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asahi_ex_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l s' s proof (prove)
goal (1 subgoal):
 1. states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and> arch_scheduler_affects_equiv s s') \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed s' = work_units_completed s \<and> scheduler_globals_frame_equiv s' s \<and> arch_scheduler_affects_equiv s' s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma ev_asahi_ex_to_full_fragement:
  "equiv_valid (scheduler_equiv aag) (asahi_ex_scheduler_affects_equiv aag l)
               (scheduler_affects_equiv aag l) \<top>
               (do x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
                   set_scheduler_action resume_cur_thread
                od)" apply (clarsimp simp: gets_def get_def return_def select_f_def  bind_def
                        set_scheduler_action_def assert_def simpler_modify_def fail_def) apply (fold simpler_modify_def) apply (rule ev_modify) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def states_equiv_for_def
                        globals_equiv_scheduler_def scheduler_affects_equiv_def
                        equiv_for_def equiv_asids_def
                        scheduler_globals_frame_equiv_def silc_dom_equiv_def
                        weak_scheduler_affects_equiv_def
                        asahi_ex_scheduler_affects_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (asahi_ex_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do x <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (asahi_ex_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>_. True) (\<lambda>s. ({((), s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>)}, False)) proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (asahi_ex_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>True; True; asahi_ex_scheduler_affects_equiv aag l s ta; scheduler_equiv aag s ta\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) (ta\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) (ta\<lparr>scheduler_action := resume_cur_thread, cur_thread := t\<rparr>) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma cur_thread_update_idle_reads_respects_scheduler:
  "reads_respects_scheduler aag l (\<lambda>s. t = idle_thread s) (modify (cur_thread_update (\<lambda>_. t)))" apply (rule ev_modify) apply (clarsimp simp add: scheduler_affects_equiv_def
                   scheduler_equiv_def domain_fields_equiv_def
                   globals_equiv_scheduler_def states_equiv_for_def
                   equiv_for_def equiv_asids_def
                   scheduler_globals_frame_equiv_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. t = idle_thread s) (modify (cur_thread_update (\<lambda>_. t))) proof (prove)
goal (1 subgoal):
 1. \<And>s ta. \<lbrakk>t = idle_thread s; t = idle_thread ta; scheduler_affects_equiv aag l s ta; scheduler_equiv aag s ta\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) \<and> scheduler_affects_equiv aag l (s\<lparr>cur_thread := t\<rparr>) (ta\<lparr>cur_thread := t\<rparr>) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma thread_get_weak_reads_respects_scheduler[wp]:
  "weak_reads_respects_scheduler aag l (K (pasObjectAbs aag t \<in> reads_scheduler aag l))
                                 (thread_get f t)" apply (rule gen_asm_ev) apply (simp add: thread_get_def) apply wp apply (simp add: weak_scheduler_affects_equiv_def states_equiv_for_def equiv_for_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_reads_respects_scheduler aag l (K (pasObjectAbs aag t \<in> reads_scheduler aag l)) (thread_get f t) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> weak_reads_respects_scheduler aag l (\<lambda>_. True) (thread_get f t) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> weak_reads_respects_scheduler aag l (\<lambda>_. True) (do tcb <- gets_the (get_tcb t);
return (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; True\<rbrakk> \<Longrightarrow> K (\<forall>s ta. scheduler_equiv aag s ta \<and> weak_scheduler_affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta) s \<and> (get_tcb t s \<noteq> None \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma weak_reads_respects_scheduler_to_midstrength:
  assumes w: "weak_reads_respects_scheduler aag l P f"
  assumes i: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "equiv_valid_inv (scheduler_equiv aag)
        (midstrength_scheduler_affects_equiv aag l) P f" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) apply (rule conjI) apply (insert w)[1] apply (fastforce simp: equiv_valid_def2 equiv_valid_2_def) apply (blast dest: state_unchanged[OF i]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) P f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> a = aa \<and> scheduler_equiv aag b ba \<and> midstrength_scheduler_affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> midstrength_scheduler_affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t; weak_reads_respects_scheduler aag l P f\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> midstrength_scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; scheduler_equiv aag s t; midstrength_scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> midstrength_scheduler_affects_equiv aag l b ba proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma midstrength_scheduler_affects_equiv_trans[elim]:
  "\<lbrakk> scheduler_equiv aag s s'; midstrength_scheduler_affects_equiv aag l s s';
     scheduler_equiv aag s' s''; midstrength_scheduler_affects_equiv aag l s' s'' \<rbrakk>
     \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s s''" apply (simp add: midstrength_scheduler_affects_equiv_def
                   scheduler_equiv_def domain_fields_equiv_def) apply (fastforce intro: states_equiv_for_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>scheduler_equiv aag s s'; midstrength_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s' s''; midstrength_scheduler_affects_equiv aag l s' s''\<rbrakk> \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_domain s = cur_domain s'' \<and> domain_time s = domain_time s'' \<and> domain_index s = domain_index s'' \<and> domain_list s = domain_list s'' \<and> idle_thread s = idle_thread s'' \<and> globals_equiv_scheduler s s' \<and> silc_dom_equiv aag s s' \<and> equiv_irq_state (machine_state s) (machine_state s''); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s' \<and> (reads_scheduler_cur_domain aag l s'' \<longrightarrow> work_units_completed s = work_units_completed s''); cur_domain s' = cur_domain s'' \<and> domain_time s' = domain_time s'' \<and> domain_index s' = domain_index s'' \<and> domain_list s' = domain_list s'' \<and> idle_thread s' = idle_thread s'' \<and> globals_equiv_scheduler s' s'' \<and> silc_dom_equiv aag s' s'' \<and> equiv_irq_state (machine_state s') (machine_state s''); states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s'' \<and> (reads_scheduler_cur_domain aag l s'' \<longrightarrow> work_units_completed s' = work_units_completed s'')\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'' proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_evrv':
  "equiv_valid_rv I A B R (K (\<forall>s t. I s t \<and> A s t  \<longrightarrow> R (f s) (f t) \<and> B s t)) (gets f)" apply (auto simp: equiv_valid_2_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (f s) (f t) \<and> B s t)) (gets f) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_ev_no_inv:
  shows "equiv_valid I A B (\<lambda> s. \<forall>s t. I s t \<and> A s t  \<longrightarrow> f s = f t \<and> B s t) (gets f)" apply (simp add: equiv_valid_def2) apply (auto intro: equiv_valid_rv_guard_imp[OF gets_evrv']) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B (\<lambda>s. \<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t \<and> B s t) (gets f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B (=) (\<lambda>s. \<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t \<and> B s t) (gets f) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma weak_scheduler_affects_equiv_trans[elim]:
  "\<lbrakk> weak_scheduler_affects_equiv aag l s s'; weak_scheduler_affects_equiv aag l s' s'' \<rbrakk>
     \<Longrightarrow> weak_scheduler_affects_equiv aag l s s''" apply (simp add: weak_scheduler_affects_equiv_def) apply (fastforce intro: states_equiv_for_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weak_scheduler_affects_equiv aag l s s'; weak_scheduler_affects_equiv aag l s' s''\<rbrakk> \<Longrightarrow> weak_scheduler_affects_equiv aag l s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s''\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s'' proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma weak_scheduler_affects_equiv_sym[elim]:
  "weak_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s' s" apply (simp add: weak_scheduler_affects_equiv_def) apply (fastforce intro: states_equiv_for_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s' s proof (prove)
goal (1 subgoal):
 1. states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s s' \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) s' s proof (prove)
goal:
No subgoals!