theory ADT_IF_Refine

lemma doUserOp_if_ex_abs[wp]:
  "\<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs (einvs)\<rbrace>
   doUserOp_if f tc
   \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" apply (rule hoare_pre) apply (rule corres_ex_abs_lift'[OF do_user_op_if_corres']) apply (rule_tac Q="\<lambda>a. invs and ct_running and valid_list and valid_sched" in hoare_strengthen_post) apply (wp do_user_op_if_invs) apply clarsimp apply (clarsimp simp: ex_abs_def) apply (rule_tac x=sa in exI) apply (clarsimp simp: active_from_running ct_running_related schedaction_related)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P3\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_. einvs\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<Longrightarrow> (ex_abs (?P3 and (einvs and ct_running)) and (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>a. invs and ct_running and valid_list and valid_sched\<rbrace>
 2. \<And>rv s. (invs and ct_running and valid_list and valid_sched) s \<Longrightarrow> einvs s
 3. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<Longrightarrow> (ex_abs (?P3 and (einvs and ct_running)) and (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (invs and ct_running and valid_list and valid_sched) s \<Longrightarrow> einvs s
 2. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<Longrightarrow> (ex_abs ((\<lambda>s. (invs and ct_running) s \<and> valid_list s \<and> valid_sched s) and (einvs and ct_running)) and (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<Longrightarrow> (ex_abs ((\<lambda>s. (invs and ct_running) s \<and> valid_list s \<and> valid_sched s) and (einvs and ct_running)) and (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running')) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread; ct_running' 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> ct_running sa \<and> valid_list sa \<and> valid_sched sa \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; ksSchedulerAction s = ResumeCurrentThread; ct_running' 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> ct_running sa \<and> valid_list sa \<and> valid_sched sa \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> ct_running sa proof (prove)
goal:
No subgoals!