theory Scheduler_IF

lemma strong_cur_domain_unobservable:
  "reads_respects_scheduler aag l (P and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) f
   \<Longrightarrow> strong_reads_respects_scheduler aag l (P and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) f" apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def scheduler_affects_equiv_def
                        equiv_valid_def2 equiv_valid_2_def weak_scheduler_affects_equiv_def) apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply clarsimp apply (drule_tac x="(a,b)" in bspec,clarsimp+) apply (drule_tac x="(aa,ba)" in bspec,clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (P and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) f \<Longrightarrow> strong_reads_respects_scheduler aag l (P and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> P t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> cur_domain s = cur_domain t \<and> domain_time s = domain_time t \<and> domain_index s = domain_index t \<and> domain_list s = domain_list t \<and> idle_thread s = idle_thread t \<and> globals_equiv_scheduler s t \<and> silc_dom_equiv aag s t \<and> equiv_irq_state (machine_state s) (machine_state t) \<and> 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 t \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t) \<longrightarrow> cur_thread s = cur_thread t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> scheduler_globals_frame_equiv s t \<and> idle_thread s = idle_thread t \<and> (cur_thread s \<noteq> idle_thread t \<longrightarrow> arch_scheduler_affects_equiv s t)) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> cur_domain s' = cur_domain t' \<and> domain_time s' = domain_time t' \<and> domain_index s' = domain_index t' \<and> domain_list s' = domain_list t' \<and> idle_thread s' = idle_thread t' \<and> globals_equiv_scheduler s' t' \<and> silc_dom_equiv aag s' t' \<and> equiv_irq_state (machine_state s') (machine_state t') \<and> 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' t' \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t') \<longrightarrow> cur_thread s' = cur_thread t' \<and> scheduler_action s' = scheduler_action t' \<and> work_units_completed s' = work_units_completed t' \<and> scheduler_globals_frame_equiv s' t' \<and> idle_thread s' = idle_thread t' \<and> (cur_thread s' \<noteq> idle_thread t' \<longrightarrow> arch_scheduler_affects_equiv s' t'))); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); P s; P t; pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}; cur_domain s = cur_domain t; domain_time s = domain_time t; domain_index s = domain_index t; domain_list s = domain_list t; idle_thread s = idle_thread t; globals_equiv_scheduler s t; silc_dom_equiv aag s t; equiv_irq_state (machine_state s) (machine_state t); 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 t\<rbrakk> \<Longrightarrow> a = aa \<and> cur_domain b = cur_domain ba \<and> domain_time b = domain_time ba \<and> domain_index b = domain_index ba \<and> domain_list b = domain_list ba \<and> idle_thread b = idle_thread ba \<and> globals_equiv_scheduler b ba \<and> silc_dom_equiv aag b ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> 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) b ba \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l ba) \<longrightarrow> cur_thread b = cur_thread ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> scheduler_globals_frame_equiv b ba \<and> idle_thread b = idle_thread ba \<and> (cur_thread b \<noteq> idle_thread ba \<longrightarrow> arch_scheduler_affects_equiv 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; pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}; cur_domain s = cur_domain t; domain_time s = domain_time t; domain_index s = domain_index t; domain_list s = domain_list t; idle_thread s = idle_thread t; globals_equiv_scheduler s t; silc_dom_equiv aag s t; equiv_irq_state (machine_state s) (machine_state t); 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 t; \<forall>t. P s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> P t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> cur_domain s = cur_domain t \<and> domain_time s = domain_time t \<and> domain_index s = domain_index t \<and> domain_list s = domain_list t \<and> idle_thread s = idle_thread t \<and> globals_equiv_scheduler s t \<and> silc_dom_equiv aag s t \<and> equiv_irq_state (machine_state s) (machine_state t) \<and> 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 t \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t) \<longrightarrow> cur_thread s = cur_thread t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> scheduler_globals_frame_equiv s t \<and> idle_thread s = idle_thread t \<and> (cur_thread s \<noteq> idle_thread t \<longrightarrow> arch_scheduler_affects_equiv s t)) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> cur_domain s' = cur_domain t' \<and> domain_time s' = domain_time t' \<and> domain_index s' = domain_index t' \<and> domain_list s' = domain_list t' \<and> idle_thread s' = idle_thread t' \<and> globals_equiv_scheduler s' t' \<and> silc_dom_equiv aag s' t' \<and> equiv_irq_state (machine_state s') (machine_state t') \<and> 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' t' \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t') \<longrightarrow> cur_thread s' = cur_thread t' \<and> scheduler_action s' = scheduler_action t' \<and> work_units_completed s' = work_units_completed t' \<and> scheduler_globals_frame_equiv s' t' \<and> idle_thread s' = idle_thread t' \<and> (cur_thread s' \<noteq> idle_thread t' \<longrightarrow> arch_scheduler_affects_equiv s' t')))\<rbrakk> \<Longrightarrow> a = aa \<and> cur_domain b = cur_domain ba \<and> domain_time b = domain_time ba \<and> domain_index b = domain_index ba \<and> domain_list b = domain_list ba \<and> idle_thread b = idle_thread ba \<and> globals_equiv_scheduler b ba \<and> silc_dom_equiv aag b ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> 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) b ba \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l ba) \<longrightarrow> cur_thread b = cur_thread ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> scheduler_globals_frame_equiv b ba \<and> idle_thread b = idle_thread ba \<and> (cur_thread b \<noteq> idle_thread ba \<longrightarrow> arch_scheduler_affects_equiv 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; pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}; cur_domain s = cur_domain t; domain_time s = domain_time t; domain_index s = domain_index t; domain_list s = domain_list t; idle_thread s = idle_thread t; globals_equiv_scheduler s t; silc_dom_equiv aag s t; equiv_irq_state (machine_state s) (machine_state t); 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 t; P s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> P t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> cur_domain s = cur_domain t \<and> domain_time s = domain_time t \<and> domain_index s = domain_index t \<and> domain_list s = domain_list t \<and> idle_thread s = idle_thread t \<and> globals_equiv_scheduler s t \<and> silc_dom_equiv aag s t \<and> equiv_irq_state (machine_state s) (machine_state t) \<and> 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 t \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t) \<longrightarrow> cur_thread s = cur_thread t \<and> scheduler_action s = scheduler_action t \<and> work_units_completed s = work_units_completed t \<and> scheduler_globals_frame_equiv s t \<and> idle_thread s = idle_thread t \<and> (cur_thread s \<noteq> idle_thread t \<longrightarrow> arch_scheduler_affects_equiv s t)) \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> cur_domain s' = cur_domain t' \<and> domain_time s' = domain_time t' \<and> domain_index s' = domain_index t' \<and> domain_list s' = domain_list t' \<and> idle_thread s' = idle_thread t' \<and> globals_equiv_scheduler s' t' \<and> silc_dom_equiv aag s' t' \<and> equiv_irq_state (machine_state s') (machine_state t') \<and> 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' t' \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t') \<longrightarrow> cur_thread s' = cur_thread t' \<and> scheduler_action s' = scheduler_action t' \<and> work_units_completed s' = work_units_completed t' \<and> scheduler_globals_frame_equiv s' t' \<and> idle_thread s' = idle_thread t' \<and> (cur_thread s' \<noteq> idle_thread t' \<longrightarrow> arch_scheduler_affects_equiv s' t')))\<rbrakk> \<Longrightarrow> a = aa \<and> cur_domain b = cur_domain ba \<and> domain_time b = domain_time ba \<and> domain_index b = domain_index ba \<and> domain_list b = domain_list ba \<and> idle_thread b = idle_thread ba \<and> globals_equiv_scheduler b ba \<and> silc_dom_equiv aag b ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> 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) b ba \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l ba) \<longrightarrow> cur_thread b = cur_thread ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> scheduler_globals_frame_equiv b ba \<and> idle_thread b = idle_thread ba \<and> (cur_thread b \<noteq> idle_thread ba \<longrightarrow> arch_scheduler_affects_equiv 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; pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}; cur_domain s = cur_domain t; domain_time s = domain_time t; domain_index s = domain_index t; domain_list s = domain_list t; idle_thread s = idle_thread t; globals_equiv_scheduler s t; silc_dom_equiv aag s t; equiv_irq_state (machine_state s) (machine_state t); 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 t; \<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> cur_domain s' = cur_domain t' \<and> domain_time s' = domain_time t' \<and> domain_index s' = domain_index t' \<and> domain_list s' = domain_list t' \<and> idle_thread s' = idle_thread t' \<and> globals_equiv_scheduler s' t' \<and> silc_dom_equiv aag s' t' \<and> equiv_irq_state (machine_state s') (machine_state t') \<and> 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' t' \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t') \<longrightarrow> cur_thread s' = cur_thread t' \<and> scheduler_action s' = scheduler_action t' \<and> work_units_completed s' = work_units_completed t' \<and> scheduler_globals_frame_equiv s' t' \<and> idle_thread s' = idle_thread t' \<and> (cur_thread s' \<noteq> idle_thread t' \<longrightarrow> arch_scheduler_affects_equiv s' t'))\<rbrakk> \<Longrightarrow> a = aa \<and> cur_domain b = cur_domain ba \<and> domain_time b = domain_time ba \<and> domain_index b = domain_index ba \<and> domain_list b = domain_list ba \<and> idle_thread b = idle_thread ba \<and> globals_equiv_scheduler b ba \<and> silc_dom_equiv aag b ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> 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) b ba \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l ba) \<longrightarrow> cur_thread b = cur_thread ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> scheduler_globals_frame_equiv b ba \<and> idle_thread b = idle_thread ba \<and> (cur_thread b \<noteq> idle_thread ba \<longrightarrow> arch_scheduler_affects_equiv 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; pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}; cur_domain s = cur_domain t; domain_time s = domain_time t; domain_index s = domain_index t; domain_list s = domain_list t; idle_thread s = idle_thread t; globals_equiv_scheduler s t; silc_dom_equiv aag s t; equiv_irq_state (machine_state s) (machine_state t); 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 t; \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> a = rvb \<and> cur_domain b = cur_domain t' \<and> domain_time b = domain_time t' \<and> domain_index b = domain_index t' \<and> domain_list b = domain_list t' \<and> idle_thread b = idle_thread t' \<and> globals_equiv_scheduler b t' \<and> silc_dom_equiv aag b t' \<and> equiv_irq_state (machine_state b) (machine_state t') \<and> 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) b t' \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l t') \<longrightarrow> cur_thread b = cur_thread t' \<and> scheduler_action b = scheduler_action t' \<and> work_units_completed b = work_units_completed t' \<and> scheduler_globals_frame_equiv b t' \<and> idle_thread b = idle_thread t' \<and> (cur_thread b \<noteq> idle_thread t' \<longrightarrow> arch_scheduler_affects_equiv b t'))\<rbrakk> \<Longrightarrow> a = aa \<and> cur_domain b = cur_domain ba \<and> domain_time b = domain_time ba \<and> domain_index b = domain_index ba \<and> domain_list b = domain_list ba \<and> idle_thread b = idle_thread ba \<and> globals_equiv_scheduler b ba \<and> silc_dom_equiv aag b ba \<and> equiv_irq_state (machine_state b) (machine_state ba) \<and> 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) b ba \<and> ((pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l ba) \<longrightarrow> cur_thread b = cur_thread ba \<and> scheduler_action b = scheduler_action ba \<and> work_units_completed b = work_units_completed ba \<and> scheduler_globals_frame_equiv b ba \<and> idle_thread b = idle_thread ba \<and> (cur_thread b \<noteq> idle_thread ba \<longrightarrow> arch_scheduler_affects_equiv b ba)) proof (prove)
goal:
No subgoals!