theory Retype_R

lemma ct_idle_or_in_cur_domain'_lift_futz:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace>       f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>"
  assumes b: "\<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace>      f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
  assumes d: "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace>       f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>"
  assumes e: "\<And>d t. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Inactive \<and> d = tcbDomain tcb) t s \<and> Q s\<rbrace>
                            f
                     \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Inactive \<and> d = tcbDomain tcb) t\<rbrace>"
  shows "\<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" proof - from e have e':
    "\<And>d t. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Inactive \<and> d = tcbDomain tcb) t s \<and> Q s\<rbrace>
              f
            \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. d = tcbDomain tcb) t\<rbrace>" apply (rule hoare_strengthen_post) apply (auto simp: obj_at'_def) done show ?thesis apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) apply (rule hoare_pre) apply (wps a b c d) apply (wp hoare_weak_lift_imp e' hoare_vcg_disj_lift) apply (auto simp: obj_at'_def ct_in_state'_def projectKOs st_tcb_at'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (chain)
picking this:
\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ?d = tcbDomain tcb) ?t s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ?d = tcbDomain tcb) ?t\<rbrace> proof (prove)
using this:
\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ?d = tcbDomain tcb) ?t s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ?d = tcbDomain tcb) ?t\<rbrace>

goal (1 subgoal):
 1. \<And>d t. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. d = tcbDomain tcb) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d t rv s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> d = tcbDomain tcb) t s \<Longrightarrow> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ?d = tcbDomain tcb) ?t s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. ?d = tcbDomain tcb) ?t\<rbrace>

goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> f \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s\<rbrace>
 2. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) and ct_active' and Q) s \<Longrightarrow> ?Q3 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P6 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. ksSchedulerAction prev_s = ResumeCurrentThread \<longrightarrow> ksCurThread prev_s = ksIdleThread prev_s \<or> obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) (ksCurThread prev_s) s'\<rbrace>
 2. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) and ct_active' and Q) s \<Longrightarrow> ?P6 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) and ct_active' and Q) s \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> ksCurDomain s = tcbDomain tcb) (ksCurThread s) s \<and> Q s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_idle_or_in_cur_domain' and ct_active' and Q\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>

goal:
No subgoals!