theory ADT_IF_Refine

lemma kernelEntry_ex_abs[wp]:
  "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle')
          and arch_extras
          and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
          and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'
          and ex_abs (einvs)\<rbrace>
   kernelEntry_if e tc
   \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" apply (rule hoare_pre) apply (rule corres_ex_abs_lift[OF kernel_entry_if_corres]) apply (wp kernel_entry_if_invs kernel_entry_if_valid_sched) apply (clarsimp simp: ex_abs_def) apply (rule_tac x=sa in exI) apply (clarsimp simp: domain_time_rel_eq domain_list_rel_eq) by (fastforce simp: ct_running_related ct_idle_related schedaction_related
                      active_from_running' active_from_running)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P3\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. einvs\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs) s \<Longrightarrow> (ex_abs (?P3 and (einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list)) and (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs) s \<Longrightarrow> (ex_abs ((\<lambda>s. (invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<and> valid_list s \<and> (valid_sched and invs and (ct_active or ct_idle) and (\<lambda>s. (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> scheduler_action s = resume_cur_thread)) s) and (einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list)) and (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; arch_extras s; ksSchedulerAction s = ResumeCurrentThread; 0 < ksDomainTime s; valid_domain_list' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> valid_list sa \<and> valid_sched sa \<and> invs sa \<and> (ct_active sa \<or> ct_idle sa) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> scheduler_action sa = resume_cur_thread \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; arch_extras s; ksSchedulerAction s = ResumeCurrentThread; 0 < ksDomainTime s; valid_domain_list' s; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> (sa, s) \<in> state_relation \<and> invs sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> valid_list sa \<and> valid_sched sa \<and> invs sa \<and> (ct_active sa \<or> ct_idle sa) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> scheduler_action sa = resume_cur_thread \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; arch_extras s; ksSchedulerAction s = ResumeCurrentThread; 0 < domain_time sa; valid_domain_list sa; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> (ct_active sa \<or> ct_idle sa) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active sa) \<and> scheduler_action sa = resume_cur_thread \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> scheduler_action sa = resume_cur_thread