theory KHeap_R

lemma ct_idle_or_in_cur_domain'_lift:
  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 a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace>
                            f
                       \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace>"
  shows "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> f \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) apply (rule_tac f="ksCurThread" in  hoare_lift_Pf) apply (rule_tac f="ksIdleThread" in hoare_lift_Pf) apply (rule_tac f="ksSchedulerAction" in  hoare_lift_Pf) apply (rule_tac f="ksCurDomain" in  hoare_lift_Pf) apply (wp hoare_vcg_imp_lift) apply (rule e) apply simp apply (rule a) apply (rule b) apply (rule c) apply (rule d) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<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\<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. \<And>x. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> x = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) x s\<rbrace> f \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> x = ksIdleThread a \<or> obj_at' (\<lambda>tcb. ksCurDomain a = tcbDomain tcb) x a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) x s\<rbrace> f \<lbrace>\<lambda>_ a. ksSchedulerAction a = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. ksCurDomain a = tcbDomain tcb) x a\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x xa xb. \<lbrace>\<lambda>s. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) x s\<rbrace> f \<lbrace>\<lambda>_ a. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. ksCurDomain a = tcbDomain tcb) x a\<rbrace>
 2. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc. \<lbrace>\<lambda>s. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x s\<rbrace> f \<lbrace>\<lambda>_ a. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x a\<rbrace>
 2. \<And>x xa xb P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 4. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x xa xb xc. \<lbrace>?Q'13 x xa xb xc\<rbrace> f \<lbrace>\<lambda>rv s. x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x s\<rbrace>
 2. \<And>x xa xb xc s. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x s \<Longrightarrow> xb \<noteq> ResumeCurrentThread \<or> ?Q'13 x xa xb xc s
 3. \<And>x xa xb P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 4. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 5. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 6. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc s. xb = ResumeCurrentThread \<longrightarrow> x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x s \<Longrightarrow> xb \<noteq> ResumeCurrentThread \<or> x = xa \<or> obj_at' (\<lambda>tcb. xc = tcbDomain tcb) x s
 2. \<And>x xa xb P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 3. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 4. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x xa xb P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!