theory KHeap_R

lemma sch_act_wf_lift:
  assumes tcb: "\<And>P t. \<lbrace>st_tcb_at' P t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
  assumes tcb_cd: "\<And>P t. \<lbrace> tcb_in_cur_domain' t\<rbrace> f \<lbrace>\<lambda>_ . tcb_in_cur_domain' t \<rbrace>"
  assumes kCT: "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>"
  assumes ksA: "\<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>"
  shows
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  f
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (clarsimp simp: valid_def) apply (frule (1) use_valid [OF _ ksA]) apply (case_tac "ksSchedulerAction b", simp_all) apply (drule (2) use_valid [OF _ ct_in_state_thread_state_lift' [OF kCT tcb]]) apply (clarsimp) apply (rule conjI) apply (drule (2) use_valid [OF _ tcb]) apply (drule (2) use_valid [OF _ tcb_cd]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> f \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction b) s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); ct_in_state' activatable' s; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> ct_in_state' activatable' b
 2. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); ksSchedulerAction b = SwitchToThread x3; st_tcb_at' runnable' x3 s; tcb_in_cur_domain' x3 s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); ksSchedulerAction b = SwitchToThread x3; st_tcb_at' runnable' x3 s; tcb_in_cur_domain' x3 s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b
 2. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); ksSchedulerAction b = SwitchToThread x3; st_tcb_at' runnable' x3 s; tcb_in_cur_domain' x3 s\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>sch_act_wf (ksSchedulerAction s) s; (a, b) \<in> fst (f s); ksSchedulerAction b = SwitchToThread x3; st_tcb_at' runnable' x3 s; tcb_in_cur_domain' x3 s\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' x3 b proof (prove)
goal:
No subgoals!