theory Finalise_R

lemma thread_set_all_corresT:
  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow>
                         tcb_relation (f tcb) (f' tcb')"
  assumes y: "\<And>tcb. \<forall>(getF, setF) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb"
  assumes z: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (f' tcb) = getF tcb"
  assumes e: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow>
                         etcb_relation (g etcb) (f' tcb')"
  shows      "corres dc (tcb_at t and valid_etcbs)
                        (tcb_at' t)
                    (thread_set_all f g t) (threadSet f' t)" apply (simp add: thread_set_all_def threadSet_def bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split[OF thread_gets_the_all_corres]) apply (simp add: split_def) apply (rule tcb_update_all_corres') apply (erule x) apply (rule y) apply (clarsimp simp: bspec_split [OF spec [OF z]]) apply fastforce apply (erule e) apply (simp add: thread_gets_the_all_def, wp+) apply clarsimp apply (frule(1) tcb_at_is_etcb_at) apply (clarsimp simp add: tcb_at_def get_etcb_def obj_at_def) apply (drule get_tcb_SomeD) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_etcbs) (tcb_at' t) (thread_set_all f g t) (threadSet f' t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_etcbs) (tcb_at' t) (do (tcb, etcb) <- thread_gets_the_all t;
set_thread_all t (f tcb) (g etcb)
od) (do tcb <- getObject t;
setObject t (f' tcb)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do (tcb, etcb) <- thread_gets_the_all t;
set_thread_all t (f tcb) (g etcb)
od) (do tcb <- getObject t;
setObject t (f' tcb)
od)
 2. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv tcb. (case rv of (tcb, etcb) \<Rightarrow> \<lambda>tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb') tcb \<Longrightarrow> corres dc (?R4 rv) (?R'4 tcb) (case rv of (tcb, etcb) \<Rightarrow> set_thread_all t (f tcb) (g etcb)) (setObject t (f' tcb))
 2. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> corres dc (?R4 rv) (?R'4 tcb) (set_thread_all t (f (fst rv)) (g (snd rv))) (setObject t (f' tcb))
 2. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; tcb_relation (?tcb10 rv) (?tcb'14 tcb)\<rbrakk> \<Longrightarrow> tcb_relation (f (fst rv)) (f' tcb)
 2. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f (fst rv)) = getF (?tcb10 rv)
 3. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcb) = getF (?tcb'14 tcb)
 4. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> dc () ()
 5. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; etcb_relation (?etcb13 rv) (?tcb'14 tcb)\<rbrakk> \<Longrightarrow> etcb_relation (g (snd rv)) (f' tcb)
 6. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (?tcb10 rv)) t and (\<lambda>s. ekheap s t = Some (?etcb13 rv))\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' (?tcb'14 tcb) t\<rbrace>
 8. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 9. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f (fst rv)) = getF (fst rv)
 2. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcb) = getF tcb
 3. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> dc () ()
 4. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; etcb_relation (?etcb13 rv) tcb\<rbrakk> \<Longrightarrow> etcb_relation (g (snd rv)) (f' tcb)
 5. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (fst rv)) t and (\<lambda>s. ekheap s t = Some (?etcb13 rv))\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 7. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 8. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcb) = getF tcb
 2. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> dc () ()
 3. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; etcb_relation (?etcb13 rv) tcb\<rbrakk> \<Longrightarrow> etcb_relation (g (snd rv)) (f' tcb)
 4. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (fst rv)) t and (\<lambda>s. ekheap s t = Some (?etcb13 rv))\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 6. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 7. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv tcb. tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb \<Longrightarrow> dc () ()
 2. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; etcb_relation (?etcb13 rv) tcb\<rbrakk> \<Longrightarrow> etcb_relation (g (snd rv)) (f' tcb)
 3. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (fst rv)) t and (\<lambda>s. ekheap s t = Some (?etcb13 rv))\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 5. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv tcb. \<lbrakk>tcb_relation (fst rv) tcb \<and> etcb_relation (snd rv) tcb; etcb_relation (?etcb13 rv) tcb\<rbrakk> \<Longrightarrow> etcb_relation (g (snd rv)) (f' tcb)
 2. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (fst rv)) t and (\<lambda>s. ekheap s t = Some (?etcb13 rv))\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 4. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> thread_gets_the_all t \<lbrace>\<lambda>rv. ko_at (TCB (fst rv)) t and (\<lambda>s. ekheap s t = Some (snd rv))\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 3. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and ?Q4) s
 4. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (tcb_at t and is_etcb_at t and (\<lambda>s. get_tcb t s \<noteq> None \<longrightarrow> get_etcb t s \<noteq> None \<longrightarrow> (ko_at (TCB (fst (the (get_tcb t s), the (get_etcb t s)))) t and (\<lambda>sa. ekheap sa t = Some (snd (the (get_tcb t s), the (get_etcb t s))))) s)) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at t s; valid_etcbs s\<rbrakk> \<Longrightarrow> is_etcb_at t s \<and> ((\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. get_etcb t s = Some y) \<longrightarrow> ko_at (TCB (the (get_tcb t s))) t s \<and> ekheap s t = get_etcb t s)
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at t s; valid_etcbs s; is_etcb_at t s\<rbrakk> \<Longrightarrow> is_etcb_at t s \<and> ((\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. get_etcb t s = Some y) \<longrightarrow> ko_at (TCB (the (get_tcb t s))) t s \<and> ekheap s t = get_etcb t s)
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s ko y ya. \<lbrakk>valid_etcbs s; is_etcb_at t s; kheap s t = Some ko; is_tcb ko; get_tcb t s = Some y; ekheap s t = Some ya\<rbrakk> \<Longrightarrow> ko = TCB y
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s ko y ya. \<lbrakk>valid_etcbs s; is_etcb_at t s; kheap s t = Some ko; is_tcb ko; ekheap s t = Some ya; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ko = TCB y
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!