theory Finalise_R

lemma threadSet_ct_idle_or_in_cur_domain':
  "\<lbrace>ct_idle_or_in_cur_domain' and (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)\<rbrace>
    threadSet F t
   \<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 (wp hoare_vcg_disj_lift hoare_vcg_imp_lift) apply wps apply wp apply wps apply wp apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)\<rbrace> threadSet F t \<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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)\<rbrace> threadSet F t \<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 (3 subgoals):
 1. \<lbrace>?P6\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace>
 2. \<lbrace>?P'6\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s\<rbrace>
 3. \<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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)) s \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ?P6 s \<or> ?P'6 s proof (prove)
goal (3 subgoals):
 1. \<And>prev_s. \<lbrace>?P7 prev_s\<rbrace> threadSet F t \<lbrace>\<lambda>rv s'. ksCurThread prev_s = ksIdleThread prev_s\<rbrace>
 2. \<lbrace>?P'6\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s\<rbrace>
 3. \<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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)) s \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ?P7 s s \<or> ?P'6 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. 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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)) s \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ksCurThread s = ksIdleThread s \<or> ?P'6 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P16 prev_s\<rbrace> threadSet F t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) (ksCurThread prev_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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)) s \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ksCurThread s = ksIdleThread s \<or> ?P16 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 (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)) s \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>obj. if t = ksCurThread s then ksCurDomain s = tcbDomain (F obj) else ksCurDomain s = tcbDomain obj) (ksCurThread s) s proof (prove)
goal:
No subgoals!