theory DetSchedSchedule_AI

lemma set_thread_state_not_runnable_valid_blocked:
  "\<lbrace>valid_blocked and K (\<not> runnable ts)\<rbrace>
      set_thread_state ref ts \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp)+ apply (rule hoare_strengthen_post) apply (rule set_scheduler_action_cnt_valid_blocked_weak) apply simp apply (wp gts_wp)+ apply (clarsimp simp: valid_blocked_def valid_blocked_except_def st_tcb_at_def obj_at_def get_tcb_def) apply (case_tac ts, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and K (\<not> runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and (\<lambda>y. \<not> runnable ts)\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tcb ts. \<not> runnable ts \<Longrightarrow> \<lbrace>?Q6 tcb () ts ref resume_cur_thread\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 2. \<And>tcb y ts cur. \<lbrace>?B4 tcb y ts cur\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then ?Q6 tcb y ts cur action else valid_blocked\<rbrace>
 3. \<And>tcb y ts. \<lbrace>?B3 tcb y ts\<rbrace> gets cur_thread \<lbrace>?B4 tcb y ts\<rbrace>
 4. \<And>tcb y. \<lbrace>?B2 tcb y\<rbrace> get_thread_state ref \<lbrace>?B3 tcb y\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ref = Some y);
return (the (kh ref))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the (get_tcb ref) \<lbrace>?B1\<rbrace>
 7. \<And>s. (valid_blocked and (\<lambda>y. \<not> runnable ts)) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>tcb ts. \<not> runnable ts \<Longrightarrow> \<lbrace>?Q6 tcb () ts ref resume_cur_thread\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q7 tcb ts\<rbrace>
 2. \<And>tcb ts rv s. \<lbrakk>\<not> runnable ts; ?Q7 tcb ts rv s\<rbrakk> \<Longrightarrow> valid_blocked s
 3. \<And>tcb y ts cur. \<lbrace>?B4 tcb y ts cur\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then ?Q6 tcb y ts cur action else valid_blocked\<rbrace>
 4. \<And>tcb y ts. \<lbrace>?B3 tcb y ts\<rbrace> gets cur_thread \<lbrace>?B4 tcb y ts\<rbrace>
 5. \<And>tcb y. \<lbrace>?B2 tcb y\<rbrace> get_thread_state ref \<lbrace>?B3 tcb y\<rbrace>
 6. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ref = Some y);
return (the (kh ref))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od \<lbrace>?B2 tcb\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets_the (get_tcb ref) \<lbrace>?B1\<rbrace>
 8. \<And>s. (valid_blocked and (\<lambda>y. \<not> runnable ts)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>tcb ts rv s. \<lbrakk>\<not> runnable ts; valid_blocked s\<rbrakk> \<Longrightarrow> valid_blocked s
 2. \<And>tcb y ts cur. \<lbrace>?B4 tcb y ts cur\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then valid_blocked and simple_sched_action else valid_blocked\<rbrace>
 3. \<And>tcb y ts. \<lbrace>?B3 tcb y ts\<rbrace> gets cur_thread \<lbrace>?B4 tcb y ts\<rbrace>
 4. \<And>tcb y. \<lbrace>?B2 tcb y\<rbrace> get_thread_state ref \<lbrace>?B3 tcb y\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ref = Some y);
return (the (kh ref))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the (get_tcb ref) \<lbrace>?B1\<rbrace>
 7. \<And>s. (valid_blocked and (\<lambda>y. \<not> runnable ts)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>tcb y ts cur. \<lbrace>?B4 tcb y ts cur\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then valid_blocked and simple_sched_action else valid_blocked\<rbrace>
 2. \<And>tcb y ts. \<lbrace>?B3 tcb y ts\<rbrace> gets cur_thread \<lbrace>?B4 tcb y ts\<rbrace>
 3. \<And>tcb y. \<lbrace>?B2 tcb y\<rbrace> get_thread_state ref \<lbrace>?B3 tcb y\<rbrace>
 4. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh ref = Some y);
return (the (kh ref))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od \<lbrace>?B2 tcb\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets_the (get_tcb ref) \<lbrace>?B1\<rbrace>
 6. \<And>s. (valid_blocked and (\<lambda>y. \<not> runnable ts)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_blocked and (\<lambda>y. \<not> runnable ts)) s \<Longrightarrow> get_tcb ref s \<noteq> None \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) ref (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>))\<rparr>) \<longrightarrow> (if \<not> runnable st \<and> cur_thread (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>))\<rparr>) = ref \<and> scheduler_action (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>))\<rparr>) = resume_cur_thread then valid_blocked and simple_sched_action else valid_blocked) (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<forall>t. not_queued t s \<longrightarrow> (\<forall>st. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> st = tcb_state tcb)) \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); \<not> runnable ts; kheap s ref = Some (TCB y); not_queued ref s; ref \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread ref\<rbrakk> \<Longrightarrow> ts \<noteq> Running \<and> ts \<noteq> Restart proof (prove)
goal:
No subgoals!