theory Retype_R

lemma sch_act_wf_lift_asm_futz:
  assumes tcb: "\<And>P t. \<lbrace>st_tcb_at' P t and Q \<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>"
  assumes tcbDomain: "\<And>P t. \<lbrace>obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> P (tcbDomain tcb)) t and Q\<rbrace> f \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> P (tcbDomain tcb)) t\<rbrace>"
  assumes kCT: "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>"
  assumes kCD: "\<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain 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 \<and> Q s\<rbrace>
  f
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (clarsimp simp: valid_def) apply (frule use_valid [OF _ ksA]) prefer 2 apply assumption apply (frule_tac P1="(=) (ksCurThread s)" in use_valid [OF _ kCT]) apply (rule refl) apply (frule_tac P1="(=) (ksCurDomain s)" in use_valid [OF _ kCD]) apply (rule refl) apply (case_tac "ksSchedulerAction s") apply (simp add: ct_in_state'_def) apply (drule use_valid [OF _ tcb]) apply simp apply simp apply simp apply (clarsimp simp: tcb_in_cur_domain'_def) apply (frule use_valid [OF _ tcb], fastforce) apply simp apply (rename_tac word) apply (subgoal_tac "(obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word and Q) s") apply (drule use_valid [OF _ tcbDomain], fastforce) apply (auto simp: st_tcb_at'_def o_def obj_at'_def ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> Q 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>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s\<rbrakk> \<Longrightarrow> ?P10 s a b (ksSchedulerAction s)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ?P10 s a b (ksSchedulerAction b)\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ?P10 s a b (ksSchedulerAction b)\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s\<rbrakk> \<Longrightarrow> ?P10 s a b (ksSchedulerAction s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s\<rbrakk> \<Longrightarrow> ksCurThread s = ksCurThread s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b\<rbrakk> \<Longrightarrow> ksCurDomain s = ksCurDomain s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 3. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); st_tcb_at' activatable' (ksCurThread b) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> st_tcb_at' activatable' (ksCurThread b) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 3. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (4 subgoals):
 1. \<And>s a b. \<lbrakk>st_tcb_at' activatable' (ksCurThread b) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (st_tcb_at' (?P26 s a b) (?t26 s a b) and Q) s
 2. \<And>s a b. \<lbrakk>st_tcb_at' activatable' (ksCurThread b) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' (?P26 s a b) (?t26 s a b) b\<rbrakk> \<Longrightarrow> st_tcb_at' activatable' (ksCurThread b) b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 4. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>st_tcb_at' activatable' (ksCurThread b) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' activatable' (ksCurThread b) b\<rbrakk> \<Longrightarrow> st_tcb_at' activatable' (ksCurThread b) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 3. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b
 2. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); sch_act_wf (ksSchedulerAction s) s; Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3; st_tcb_at' runnable' x3 s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3; st_tcb_at' runnable' x3 s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 s; st_tcb_at' runnable' x3 b\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x3 b \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x3. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread x3; st_tcb_at' runnable' x3 s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 s; st_tcb_at' runnable' x3 b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s a b word. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread word; st_tcb_at' runnable' word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; st_tcb_at' runnable' word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b proof (prove)
goal (2 subgoals):
 1. \<And>s a b word. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread word; st_tcb_at' runnable' word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; st_tcb_at' runnable' word b; (obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word and Q) s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b
 2. \<And>s a b word. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread word; st_tcb_at' runnable' word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; st_tcb_at' runnable' word b\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word and Q) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b word. \<lbrakk>Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread word; st_tcb_at' runnable' word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; st_tcb_at' runnable' word b; (obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word and Q) s; obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b
 2. \<And>s a b word. \<lbrakk>(a, b) \<in> fst (f s); Q s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction s = SwitchToThread word; st_tcb_at' runnable' word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; st_tcb_at' runnable' word b\<rbrakk> \<Longrightarrow> (obj_at' (\<lambda>tcb. runnable' (tcbState tcb) \<longrightarrow> ksCurDomain b = tcbDomain tcb) word and Q) s proof (prove)
goal:
No subgoals!