theory DetSchedSchedule_AI

lemma reschedule_required_switch_valid_blocked:
  "\<lbrace>\<lambda>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False\<rbrace>
    reschedule_required \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: reschedule_required_def | wp set_scheduler_action_cnt_valid_blocked tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift | wpc)+ apply (simp add: tcb_sched_action_def) apply wp+ apply (force simp: etcb_at_def tcb_sched_enqueue_def valid_blocked_def valid_blocked_except_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>action x2 t. action = switch_thread x2 \<Longrightarrow> \<lbrace>\<lambda>a. ?P27 (switch_thread x2) x2 a t\<rbrace> tcb_sched_action tcb_sched_enqueue x2 \<lbrace>\<lambda>a b. scheduler_action b = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues b d p))\<rbrace>
 2. \<And>action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R9 action\<rbrace> return () \<lbrace>\<lambda>y s. valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> valid_blocked_except x s \<and> (\<forall>xa. ?P27 action x s xa)) \<and> (action = choose_new_thread \<longrightarrow> ?R9 action s)\<rbrace>
 4. \<And>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>action x2 t. action = switch_thread x2 \<Longrightarrow> \<lbrace>\<lambda>a. ?P27 (switch_thread x2) x2 a t\<rbrace> do d <- ethread_get tcb_domain x2;
prio <- ethread_get tcb_priority x2;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue x2 queue)
od \<lbrace>\<lambda>a b. scheduler_action b = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues b d p))\<rbrace>
 2. \<And>action. action = choose_new_thread \<Longrightarrow> \<lbrace>?R9 action\<rbrace> return () \<lbrace>\<lambda>y s. valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets scheduler_action \<lbrace>\<lambda>action s. (action = resume_cur_thread \<longrightarrow> valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))) \<and> (\<forall>x. action = switch_thread x \<longrightarrow> valid_blocked_except x s \<and> (\<forall>xa. ?P27 action x s xa)) \<and> (action = choose_new_thread \<longrightarrow> ?R9 action s)\<rbrace>
 4. \<And>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. case scheduler_action s of switch_thread t \<Rightarrow> valid_blocked_except t s | _ \<Rightarrow> False \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except x s \<and> (\<forall>xa. etcb_at (\<lambda>t. etcb_at (\<lambda>ta. scheduler_action (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s) = switch_thread xa \<longrightarrow> (\<exists>d p. xa \<in> set (ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s) d p))) x s) x s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>d p. t \<in> set (ready_queues s d p)))) proof (prove)
goal:
No subgoals!