theory Schedule_C

lemma switchToIdleThread_ccorres:
  "ccorres dc xfdc invs_no_cicd' UNIV []
           switchToIdleThread (Call switchToIdleThread_'proc)" apply (cinit) apply (rule ccorres_symb_exec_l) apply (ctac (no_vcg) add: Arch_switchToIdleThread_ccorres) apply (simp add: setCurThread_def) apply (rule_tac P="\<lambda>s. thread = ksIdleThread s" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                             carch_state_relation_def cmachine_state_relation_def) apply (simp add: ARM_H.switchToIdleThread_def) apply wp+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] global.switchToIdleThread (Call switchToIdleThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (do thread <- getIdleThread;
y <- Arch.switchToIdleThread;
setCurThread thread
od) (CALL Arch_switchToIdleThread_'proc();;
\<acute>ksCurThread :== \<acute>ksIdleThread)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (5 subgoals):
 1. \<And>thread. ccorres dc xfdc (?Q15 thread) (?Q'15 thread) [SKIP] (do y <- Arch.switchToIdleThread;
setCurThread thread
od) (CALL Arch_switchToIdleThread_'proc();;
\<acute>ksCurThread :== \<acute>ksIdleThread)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>?Q15\<rbrace>
 4. empty_fail getIdleThread
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q22 thread rv) (?Q'22 thread rv xfdca) [SKIP] (setCurThread thread) (\<acute>ksCurThread :== \<acute>ksIdleThread)
 2. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>?Q22 thread\<rbrace>
 3. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 5. empty_fail getIdleThread
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'22 rv rva (xfdc t)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread xfdca. ccorres dc xfdc (?Q22 thread ()) (?Q'22 thread () xfdca) [SKIP] (modify (ksCurThread_update (\<lambda>_. thread))) (\<acute>ksCurThread :== \<acute>ksIdleThread)
 2. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>?Q22 thread\<rbrace>
 3. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 5. empty_fail getIdleThread
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'22 rv rva (xfdc t)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread xfdca. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. thread = ksIdleThread \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksCurThread :== \<acute>ksIdleThread {s. \<exists>(rv, \<sigma>')\<in>fst (modify (ksCurThread_update (\<lambda>_. thread)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>a b. thread = ksIdleThread b\<rbrace>
 3. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 5. empty_fail getIdleThread
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (6 subgoals):
 1. \<And>thread xfdca \<sigma>. {s. thread = ksIdleThread \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (modify (ksCurThread_update (\<lambda>_. thread)) \<sigma>). (\<sigma>', globals_update (ksCurThread_'_update (\<lambda>_. ksIdleThread_' (globals s))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksCurThread_'_update (\<lambda>_. ksIdleThread_' (globals s))) s))}
 2. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>a b. thread = ksIdleThread b\<rbrace>
 3. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 5. empty_fail getIdleThread
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksCurThread := ksIdleThread \<sigma>\<rparr>, globals_update (ksCurThread_'_update (\<lambda>_. ksIdleThread_' (globals x))) x) \<in> rf_sr
 2. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>a b. thread = ksIdleThread b\<rbrace>
 3. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 5. empty_fail getIdleThread
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>?R22 thread\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>a b. thread = ksIdleThread b\<rbrace>
 2. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 4. empty_fail getIdleThread
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>?R22 thread\<rbrace> getIdleThread >>= setVMRoot \<lbrace>\<lambda>a b. thread = ksIdleThread b\<rbrace>
 2. \<And>s. \<lbrace>(=) s\<rbrace> getIdleThread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getIdleThread \<lbrace>\<lambda>thread. all_invs_but_ct_idle_or_in_cur_domain' and ?R22 thread\<rbrace>
 4. empty_fail getIdleThread
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and ?R22 rv) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (2 subgoals):
 1. empty_fail getIdleThread
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>sa. ksIdleThread s = ksIdleThread sa)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. rv = ksIdleThread s)) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>sa. ksIdleThread s = ksIdleThread sa)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. rv = ksIdleThread s)) s \<longrightarrow> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal:
No subgoals!