theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_valid_blocked':
  "\<lbrace>valid_blocked and (\<lambda>s. scheduler_action s = switch_thread t \<and>
      (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace>
   set_scheduler_action choose_new_thread  \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: valid_blocked_def, wp set_scheduler_action_wp) apply clarsimp apply (erule_tac x=ta in allE) apply (erule impCE) apply force apply (erule_tac x=st in allE) apply (force simp: not_queued_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and (\<lambda>s. scheduler_action s = switch_thread t \<and> (\<exists>d p. t \<in> set (ready_queues s d p)))\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)) and (\<lambda>s. scheduler_action s = switch_thread t \<and> (\<exists>d p. t \<in> set (ready_queues s d p)))) s \<Longrightarrow> \<forall>t. not_queued t (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> t \<noteq> cur_thread (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> scheduler_action (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart) proof (prove)
goal (1 subgoal):
 1. \<And>s ta d p st. \<lbrakk>\<forall>ta. not_queued ta s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) ta s \<longrightarrow> ta \<noteq> cur_thread s \<longrightarrow> t \<noteq> ta \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s ta d p st. \<lbrakk>scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s; not_queued ta s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) ta s \<longrightarrow> ta \<noteq> cur_thread s \<longrightarrow> t \<noteq> ta \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s ta d p st. \<lbrakk>scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s; \<not> not_queued ta s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s ta d p st. \<lbrakk>scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s; \<forall>st. st_tcb_at ((=) st) ta s \<longrightarrow> ta \<noteq> cur_thread s \<longrightarrow> t \<noteq> ta \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s ta d p st. \<lbrakk>scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s; \<forall>st. st_tcb_at ((=) st) ta s \<longrightarrow> ta \<noteq> cur_thread s \<longrightarrow> t \<noteq> ta \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s ta d p st. \<lbrakk>scheduler_action s = switch_thread t; t \<in> set (ready_queues s d p); not_queued ta s; st_tcb_at ((=) st) ta s; ta \<noteq> cur_thread s; st_tcb_at ((=) st) ta s \<longrightarrow> ta \<noteq> cur_thread s \<longrightarrow> t \<noteq> ta \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!