theory Scheduler_IF

lemma context_update_cur_thread_snippit_unobservable:
  "equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l)
                 (scheduler_affects_equiv aag l) (=)
                 (invs and silc_inv aag st and guarded_pas_domain aag
                       and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)
                       and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s))
                 (invs and silc_inv aag st and guarded_pas_domain aag
                       and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)
                       and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s))
                 (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)))
                 (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))" apply (rule equiv_valid_2_guard_imp) apply (simp add: op_eq_unit_dc) apply (rule equiv_valid_2_unobservable) apply (wp | elim conjE | simp add: dc_def)+ apply fastforce apply fastforce apply (fastforce simp: guarded_pas_domain_def silc_inv_not_cur_thread
                          cur_thread_idle disjoint_iff_not_equal)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) ?Q ?Q' (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))
 2. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) dc ?Q ?Q' (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))
 2. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>st. \<lbrace>?P4 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)) \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>?P'4 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>st. \<lbrace>?S4 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')) \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 4. \<And>st. \<lbrace>?S'4 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 5. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 6. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 7. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> (?P4 and ?P'4) s
 8. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> (?S4 and ?S'4) s proof (prove)
goal (4 subgoals):
 1. \<forall>s s'. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> scheduler_affects_equiv aag l s' s
 2. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 3. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s))) s
 4. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s))) s proof (prove)
goal (3 subgoals):
 1. \<forall>s s' s''. scheduler_equiv aag s s' \<and> scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> scheduler_affects_equiv aag l s s''
 2. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s))) s
 3. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc = idle_context s))) s
 2. \<And>s. (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s)) and (\<lambda>s. (cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l) \<and> (cur_thread s = idle_thread s \<longrightarrow> uc' = idle_context s))) s proof (prove)
goal:
No subgoals!