theory ADT_IF_Refine

lemma scheduler'_if_ex_abs[wp]:
  "\<lbrace>invs' and ex_abs (einvs) and valid_domain_list'
          and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)\<rbrace>
   schedule'_if tc
   \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" apply (rule hoare_pre) apply (rule corres_ex_abs_lift[OF schedule_if_corres]) apply wp apply (clarsimp simp: ex_abs_def) apply (rule exI, rule conjI, assumption) apply (frule state_relation_schact) apply (auto simp: domain_list_rel_eq domain_time_rel_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P3\<rbrace> schedule_if tc \<lbrace>\<lambda>_. einvs\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (ex_abs (?P3 and (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (ex_abs ((\<lambda>s. invs s \<and> valid_list s \<and> (valid_sched and valid_idle) s) and (invs and valid_sched and valid_list and valid_domain_list and (\<lambda>s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread; (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> valid_list sa \<and> valid_sched sa \<and> valid_idle sa \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> valid_idle sa \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; sched_act_relation (scheduler_action sa) (ksSchedulerAction s)\<rbrakk> \<Longrightarrow> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> valid_idle sa \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread) proof (prove)
goal:
No subgoals!