theory Schedule_C

lemma scheduleChooseNewThread_ccorres:
  "ccorres dc xfdc
     (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) UNIV hs
     (do domainTime \<leftarrow> getDomainTime;
         y \<leftarrow> when (domainTime = 0) nextDomain;
         chooseThread
      od)
     (Call scheduleChooseNewThread_'proc)" apply (cinit') apply (rule ccorres_pre_getDomainTime) apply (rule ccorres_split_nothrow) apply (rule_tac R="\<lambda>s. ksDomainTime s = domainTime" in ccorres_when) apply (fastforce simp: rf_sr_ksDomainTime) apply (rule_tac xf'=xfdc in ccorres_call[OF nextDomain_ccorres] ; simp) apply ceqv apply (ctac (no_vcg) add: chooseThread_ccorres) apply (wp nextDomain_invs_no_cicd') apply clarsimp apply (vcg exspec=nextDomain_modifies) apply (clarsimp simp: if_apply_def2 invs'_invs_no_cicd') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) UNIV hs (do domainTime <- getDomainTime;
y <- when (domainTime = 0) nextDomain;
chooseThread
od) (Call scheduleChooseNewThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 (SKIP # hs) (do domainTime <- getDomainTime;
y <- when (domainTime = 0) nextDomain;
chooseThread
od) (IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI;;
CALL chooseThread_'proc())
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. \<And>domainTime. ccorres dc xfdc (?P15 domainTime) (?P'15 domainTime) (SKIP # hs) (do y <- when (domainTime = 0) nextDomain;
chooseThread
od) (IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI;;
CALL chooseThread_'proc())
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ?P15 rv s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> ?P'15 rv} proof (prove)
goal (6 subgoals):
 1. \<And>domainTime. ccorres (?r'17 domainTime) (?xf'17 domainTime) (?P17 domainTime) (?P'17 domainTime) (SKIP # hs) (when (domainTime = 0) nextDomain) (IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI)
 2. \<And>domainTime rv' t t'. ceqv \<Gamma> (?xf'17 domainTime) rv' t t' (CALL chooseThread_'proc()) (?d'17 domainTime rv')
 3. \<And>domainTime y rv'. ?r'17 domainTime y rv' \<Longrightarrow> ccorres dc xfdc (?Q17 domainTime y) (?Q'17 domainTime y rv') (SKIP # hs) chooseThread (?d'17 domainTime rv')
 4. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>?Q17 domainTime\<rbrace>
 5. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. ?r'17 domainTime y (?xf'17 domainTime s) \<longrightarrow> s \<in> ?Q'17 domainTime y (?xf'17 domainTime s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> (?P17 rv and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> ?P'17 rv \<inter> ?R'17 rv} proof (prove)
goal (7 subgoals):
 1. \<And>domainTime. \<forall>s s'. (s, s') \<in> rf_sr \<and> ksDomainTime s = domainTime \<longrightarrow> (domainTime = 0) = (s' \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace>)
 2. \<And>domainTime. ccorres dc (?xf'17 domainTime) (?Pt23 domainTime) (?Rt23 domainTime) (SKIP # hs) nextDomain (CALL nextDomain_'proc())
 3. \<And>domainTime rv' t t'. ceqv \<Gamma> (?xf'17 domainTime) rv' t t' (CALL chooseThread_'proc()) (?d'17 domainTime rv')
 4. \<And>domainTime y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q17 domainTime y) (?Q'17 domainTime y rv') (SKIP # hs) chooseThread (?d'17 domainTime rv')
 5. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>?Q17 domainTime\<rbrace>
 6. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (?xf'17 domainTime s) \<longrightarrow> s \<in> ?Q'17 domainTime y (?xf'17 domainTime s)}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> ?Pt23 rv s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> ?Rt23 rv) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (6 subgoals):
 1. \<And>domainTime. ccorres dc (?xf'17 domainTime) (?Pt23 domainTime) (?Rt23 domainTime) (SKIP # hs) nextDomain (CALL nextDomain_'proc())
 2. \<And>domainTime rv' t t'. ceqv \<Gamma> (?xf'17 domainTime) rv' t t' (CALL chooseThread_'proc()) (?d'17 domainTime rv')
 3. \<And>domainTime y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q17 domainTime y) (?Q'17 domainTime y rv') (SKIP # hs) chooseThread (?d'17 domainTime rv')
 4. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>?Q17 domainTime\<rbrace>
 5. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (?xf'17 domainTime s) \<longrightarrow> s \<in> ?Q'17 domainTime y (?xf'17 domainTime s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> ?Pt23 rv s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> ?Rt23 rv) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (5 subgoals):
 1. \<And>domainTime rv' t t'. ceqv \<Gamma> xfdc rv' t t' (CALL chooseThread_'proc()) (?d'17 domainTime rv')
 2. \<And>domainTime y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q17 domainTime y) (?Q'17 domainTime y rv') (SKIP # hs) chooseThread (?d'17 domainTime rv')
 3. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>?Q17 domainTime\<rbrace>
 4. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'17 domainTime y (xfdc s)}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (4 subgoals):
 1. \<And>domainTime y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q17 domainTime y) (?Q'17 domainTime y rv') (SKIP # hs) chooseThread (CALL chooseThread_'proc())
 2. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>?Q17 domainTime\<rbrace>
 3. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> ?Q'17 domainTime y (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (3 subgoals):
 1. \<And>domainTime. \<lbrace>?R17 domainTime\<rbrace> when (domainTime = 0) nextDomain \<lbrace>\<lambda>y. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace>
 2. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and ?R17 rv) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (2 subgoals):
 1. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV}}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and (if rv = 0 then invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) else all_invs_but_ct_idle_or_in_cur_domain')) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (2 subgoals):
 1. \<And>domainTime. \<Gamma>\<turnstile>\<^bsub>/?F17 domainTime\<^esub> (?R'17 domainTime) IF \<acute>ksDomainTime = 0 THEN
  CALL nextDomain_'proc()
FI UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and (if rv = 0 then invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) else all_invs_but_ct_idle_or_in_cur_domain')) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> ?R'17 rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> ksSchedulerAction s = ChooseNewThread; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksDomainTime s = rv \<longrightarrow> ((\<lambda>s. ksDomainTime s = rv) and (\<lambda>s. rv = 0 \<longrightarrow> invs' s) and (\<lambda>s. rv \<noteq> 0 \<longrightarrow> True) and (if rv = 0 then invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) else all_invs_but_ct_idle_or_in_cur_domain')) s) \<and> s' \<in> {s. \<forall>rv. ksDomainTime_' (globals s) = rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>\<acute>ksDomainTime = 0\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(\<acute>ksDomainTime = 0 \<longrightarrow> True) \<and> (\<acute>ksDomainTime \<noteq> 0 \<longrightarrow> True)\<rbrace>} proof (prove)
goal:
No subgoals!