theory DetSchedSchedule_AI

lemma reschedule_preserves_valid_sched: "\<lbrace> valid_sched \<rbrace> reschedule_required \<lbrace> \<lambda>rv. valid_sched \<rbrace>" unfolding reschedule_required_def set_scheduler_action_def tcb_sched_action_def apply (rule hoare_pre) apply (wp|wpc)+ apply clarsimp apply (rule conjI) apply (clarsimp simp: valid_sched_2_def ct_not_in_q_2_def valid_blocked_2_def) apply (rule conjI) defer apply (clarsimp simp: valid_sched_2_def ct_not_in_q_2_def valid_blocked_2_def) apply (clarsimp simp only: etcb_at_def) apply (case_tac "ekheap s x"; simp) apply (clarsimp simp: valid_sched_2_def) apply (rule conjI) apply (clarsimp simp: valid_queues_2_def valid_sched_action_2_def tcb_sched_enqueue_def
     weak_valid_sched_action_2_def etcb_at_conj_is_etcb_at) apply (rule conjI) apply (clarsimp simp: ct_not_in_q_2_def) apply (clarsimp simp:  valid_blocked_2_def) apply (clarsimp simp:  not_queued_def) apply (erule_tac x=t in allE; simp) by (clarsimp simp:  set_nonmember_if_cong tcb_sched_enqueue_def split: if_split_asm; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> reschedule_required \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do action <- gets scheduler_action;
case action of switch_thread t \<Rightarrow> do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od | _ \<Rightarrow> return ();
modify (scheduler_action_update (\<lambda>_. choose_new_thread))
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do action <- gets scheduler_action;
case action of switch_thread t \<Rightarrow> do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue t queue)
od | _ \<Rightarrow> return ();
modify (scheduler_action_update (\<lambda>_. choose_new_thread))
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>s. valid_sched s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> valid_sched (scheduler_action_update (\<lambda>_. choose_new_thread) s)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched (scheduler_action_update (\<lambda>_. choose_new_thread) (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))) x s) x s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched (scheduler_action_update (\<lambda>_. choose_new_thread) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_sched s \<Longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)
 2. \<And>s. valid_sched s \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_sched s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s
 2. \<And>s. valid_sched s \<Longrightarrow> scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_sched s \<Longrightarrow> scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)
 2. \<And>s. valid_sched s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue x (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) x s) x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> case ekheap s x of None \<Rightarrow> True | Some xa \<Rightarrow> case ekheap s x of None \<Rightarrow> True | Some xb \<Rightarrow> valid_sched_2 (\<lambda>a aa. if a = tcb_domain xa \<and> aa = tcb_priority xb then tcb_sched_enqueue x (ready_queues s (tcb_domain xa) (tcb_priority xb)) else ready_queues s a aa) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); scheduler_action s = switch_thread x; ekheap s x = Some a\<rbrakk> \<Longrightarrow> valid_sched_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> valid_queues_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (ekheap s) (kheap s) \<and> ct_not_in_q_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) choose_new_thread (cur_thread s) \<and> valid_blocked_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> valid_queues_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (ekheap s) (kheap s)
 2. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) choose_new_thread (cur_thread s) \<and> valid_blocked_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) choose_new_thread (cur_thread s) \<and> valid_blocked_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> ct_not_in_q_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) choose_new_thread (cur_thread s)
 2. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> valid_blocked_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s\<rbrakk> \<Longrightarrow> valid_blocked_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) (kheap s) choose_new_thread (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a t st. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> x \<noteq> t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); valid_idle_etcb s; not_queued_2 (\<lambda>b c. if b = tcb_domain a \<and> c = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s b c) t; st_tcb_at ((=) st) t s; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x a t st. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); \<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> x \<noteq> t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); valid_idle_etcb s; \<forall>d p. t \<notin> set (if d = tcb_domain a \<and> p = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s d p); st_tcb_at ((=) st) t s; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x a t st. \<lbrakk>scheduler_action s = switch_thread x; ekheap s x = Some a; valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s); valid_idle_etcb s; \<forall>d p. t \<notin> set (if d = tcb_domain a \<and> p = tcb_priority a then tcb_sched_enqueue x (ready_queues s (tcb_domain a) (tcb_priority a)) else ready_queues s d p); st_tcb_at ((=) st) t s; t \<noteq> cur_thread s; (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> x \<noteq> t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart