kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma rescheduleRequired_valid_queues_sch_act_simple:
  "\<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp | fastforce simp: Invariants_H.valid_queues_def sch_act_simple_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and sch_act_simple\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_valid_bitmapQ_sch_act_simple:
  "\<lbrace> valid_bitmapQ and sch_act_simple\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" including no_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\<lambda>rv s. valid_bitmapQ s \<and>
                            (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)" in hoare_seq_ext) apply wpsimp apply (case_tac x; simp) apply (wp, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. valid_bitmapQ s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> do y <- case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace>
 2. \<lbrace>valid_bitmapQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. valid_bitmapQ s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y. valid_bitmapQ\<rbrace>
 2. \<lbrace>valid_bitmapQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. valid_bitmapQ s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple:
  "\<lbrace> bitmapQ_no_L1_orphans and sch_act_simple\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" including no_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\<lambda>rv s. bitmapQ_no_L1_orphans s \<and>
                            (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)" in hoare_seq_ext) apply wpsimp apply (case_tac x; simp) apply (wp, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. bitmapQ_no_L1_orphans s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> do y <- case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace>
 2. \<lbrace>bitmapQ_no_L1_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L1_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. bitmapQ_no_L1_orphans s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y. bitmapQ_no_L1_orphans\<rbrace>
 2. \<lbrace>bitmapQ_no_L1_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L1_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L1_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple:
  "\<lbrace> bitmapQ_no_L2_orphans and sch_act_simple\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" including no_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\<lambda>rv s. bitmapQ_no_L2_orphans s \<and>
                            (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)" in hoare_seq_ext) apply wpsimp apply (case_tac x; simp) apply (wp, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. bitmapQ_no_L2_orphans s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> do y <- case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace>
 2. \<lbrace>bitmapQ_no_L2_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L2_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. bitmapQ_no_L2_orphans s \<and> (x = ResumeCurrentThread \<or> x = ChooseNewThread)\<rbrace> case x of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y. bitmapQ_no_L2_orphans\<rbrace>
 2. \<lbrace>bitmapQ_no_L2_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L2_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread)\<rbrace> getSchedulerAction \<lbrace>\<lambda>rv s. bitmapQ_no_L2_orphans s \<and> (rv = ResumeCurrentThread \<or> rv = ChooseNewThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_bitmapQ_sch_act_simple:
  "\<lbrace>valid_bitmapQ and sch_act_simple\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_valid_bitmapQ_sch_act_simple
            threadSet_valid_bitmapQ [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and sch_act_simple\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_bitmapQ s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then valid_bitmapQ and sch_act_simple else valid_bitmapQ) s
 2. \<And>s. (valid_bitmapQ and sch_act_simple) s \<Longrightarrow> valid_bitmapQ s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_bitmapQ_no_L2_orphans_sch_act_simple:
  "\<lbrace> bitmapQ_no_L2_orphans and sch_act_simple\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple
            threadSet_valid_bitmapQ_no_L2_orphans [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans and sch_act_simple\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. bitmapQ_no_L2_orphans s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then bitmapQ_no_L2_orphans and sch_act_simple else bitmapQ_no_L2_orphans) s
 2. \<And>s. (bitmapQ_no_L2_orphans and sch_act_simple) s \<Longrightarrow> bitmapQ_no_L2_orphans s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_bitmapQ_no_L1_orphans_sch_act_simple:
  "\<lbrace> bitmapQ_no_L1_orphans and sch_act_simple\<rbrace>
    setThreadState st t
   \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple
            threadSet_valid_bitmapQ_no_L1_orphans [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and sch_act_simple\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. bitmapQ_no_L1_orphans s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then bitmapQ_no_L1_orphans and sch_act_simple else bitmapQ_no_L1_orphans) s
 2. \<And>s. (bitmapQ_no_L1_orphans and sch_act_simple) s \<Longrightarrow> bitmapQ_no_L1_orphans s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_valid_queues:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and>
    ((\<exists>p. t \<in> set(ksReadyQueues s p)) \<longrightarrow> runnable' st)\<rbrace>
   setThreadState st t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_valid_queues_sch_act_simple
            threadSet_valid_queues [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Invariants_H.valid_queues s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then Invariants_H.valid_queues and sch_act_simple else Invariants_H.valid_queues) s
 2. \<And>s. Invariants_H.valid_queues s \<and> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<Longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. st) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. st) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. st) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. st) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sbn_valid_queues:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s\<rbrace>
   setBoundNotification ntfn t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_valid_queues [THEN hoare_strengthen_post]) apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<Longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbBoundNotification_update (\<lambda>_. ntfn) tcb) \<and> runnable' (tcbState (tcbBoundNotification_update (\<lambda>_. ntfn) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbBoundNotification_update (\<lambda>_. ntfn) tcb) \<and> runnable' (tcbState (tcbBoundNotification_update (\<lambda>_. ntfn) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_valid_queues'_weak[wp]:
  "\<lbrace>\<lambda>s. valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. valid_queues'\<rbrace>" apply (simp add: rescheduleRequired_def) apply wpsimp apply (clarsimp simp: weak_sch_act_wf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_queues' s; weak_sch_act_wf (SwitchToThread x) s; ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma rescheduleRequired_valid_queues'_sch_act_simple:
  "\<lbrace>valid_queues' and sch_act_simple\<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. valid_queues'\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp | fastforce simp: valid_queues'_def sch_act_simple_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and sch_act_simple\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and sch_act_simple\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setThreadState_valid_queues'[wp]:
  "\<lbrace>\<lambda>s. valid_queues' s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_valid_queues'_sch_act_simple) apply (rule_tac Q="\<lambda>_. valid_queues'" in hoare_post_imp) apply (clarsimp simp: sch_act_simple_def) apply (wp threadSet_valid_queues') apply (fastforce simp: inQ_def obj_at'_def pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then valid_queues' and sch_act_simple else valid_queues') s\<rbrace>
 2. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. valid_queues' s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then valid_queues' and sch_act_simple else valid_queues') s
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 3. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbState_update (\<lambda>_. st) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_valid_queues'[wp]:
  "\<lbrace>\<lambda>s. valid_queues' s\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_valid_queues') apply (fastforce simp: inQ_def obj_at'_def pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbBoundNotification_update (\<lambda>_. ntfn) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma valid_tcb'_tcbState_update:
  "\<lbrakk> valid_tcb_state' st s; valid_tcb' tcb s \<rbrakk> \<Longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s" apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def valid_tcb_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tcb_state' st s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s proof (prove)
goal:
No subgoals!