theory DetSchedSchedule_AI

lemma reschedule_required_valid_blocked:
  "\<lbrace>valid_blocked\<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 clarsimp apply (rule conjI) apply clarsimp apply (rule conjI) apply (force simp: etcb_at_def tcb_sched_enqueue_def valid_blocked_def valid_blocked_except_def split: option.splits) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<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. valid_blocked s \<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. valid_blocked s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<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 (1 subgoal):
 1. \<And>s. valid_blocked s \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> (\<forall>xa. etcb_at (\<lambda>t. etcb_at (\<lambda>ta. x = xa \<longrightarrow> (\<exists>d p. (d = tcb_domain t \<and> p = tcb_priority ta \<longrightarrow> xa \<in> set (tcb_sched_enqueue xa (ready_queues s (tcb_domain t) (tcb_priority ta)))) \<and> ((d = tcb_domain t \<longrightarrow> p \<noteq> tcb_priority ta) \<longrightarrow> xa \<in> set (ready_queues s d p)))) x s) x s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_blocked s \<Longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s)
 2. \<And>s. valid_blocked s \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> (\<forall>xa. etcb_at (\<lambda>t. etcb_at (\<lambda>ta. x = xa \<longrightarrow> (\<exists>d p. (d = tcb_domain t \<and> p = tcb_priority ta \<longrightarrow> xa \<in> set (tcb_sched_enqueue xa (ready_queues s (tcb_domain t) (tcb_priority ta)))) \<and> ((d = tcb_domain t \<longrightarrow> p \<noteq> tcb_priority ta) \<longrightarrow> xa \<in> set (ready_queues s d p)))) x s) x s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> (\<forall>xa. etcb_at (\<lambda>t. etcb_at (\<lambda>ta. x = xa \<longrightarrow> (\<exists>d p. (d = tcb_domain t \<and> p = tcb_priority ta \<longrightarrow> xa \<in> set (tcb_sched_enqueue xa (ready_queues s (tcb_domain t) (tcb_priority ta)))) \<and> ((d = tcb_domain t \<longrightarrow> p \<noteq> tcb_priority ta) \<longrightarrow> xa \<in> set (ready_queues s d p)))) x s) x s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_blocked s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> (\<forall>xa. etcb_at (\<lambda>t. etcb_at (\<lambda>ta. x = xa \<longrightarrow> (\<exists>d p. (d = tcb_domain t \<and> p = tcb_priority ta \<longrightarrow> xa \<in> set (tcb_sched_enqueue xa (ready_queues s (tcb_domain t) (tcb_priority ta)))) \<and> ((d = tcb_domain t \<longrightarrow> p \<noteq> tcb_priority ta) \<longrightarrow> xa \<in> set (ready_queues s d p)))) x s) x s)
 2. \<And>s. valid_blocked s \<Longrightarrow> scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<Longrightarrow> scheduler_action s = choose_new_thread \<longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal:
No subgoals!