theory Noninterference

lemma ready_queues_alters_kheap:
  assumes a: "valid_queues s"
  assumes b: "valid_blocked s"
  assumes c: "valid_idle s'"
  shows "\<lbrakk> ready_queues s d a \<noteq> ready_queues s' d a;
           threads @ ready_queues s d a = ready_queues s' d a; valid_queues s';
           valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t;
           t \<noteq> idle_thread s \<longrightarrow> (t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s');
           scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s' \<rbrakk>
           \<Longrightarrow> kheap s t \<noteq> kheap s' t" apply (frule prefix_helper) using a apply ((simp add: valid_queues_def)+)[2] apply clarsimp apply (drule(1) set_mp) apply (drule(1) orthD1) apply (erule(1) valid_queuesE) apply (subgoal_tac "tcb_at t s") apply (frule valid_blocked_imp[OF b]) apply (rule valid_queues_not_in_place[OF a],assumption) apply (simp add: etcb_at_def) apply (simp add: is_etcb_at_def) using c apply (auto simp: pred_tcb_at_def tcb_at_st_tcb_at obj_at_def valid_idle_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> kheap s t \<noteq> kheap s' t proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> distinct (ready_queues s d a)
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> distinct (ready_queues s' d a)
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; set threads \<inter> set (ready_queues s d a) = {} \<and> set threads \<subseteq> set (ready_queues s' d a)\<rbrakk> \<Longrightarrow> kheap s t \<noteq> kheap s' t proof (prove)
using this:
valid_queues s

goal (3 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> distinct (ready_queues s d a)
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> distinct (ready_queues s' d a)
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; set threads \<inter> set (ready_queues s d a) = {} \<and> set threads \<subseteq> set (ready_queues s' d a)\<rbrakk> \<Longrightarrow> kheap s t \<noteq> kheap s' t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; set threads \<inter> set (ready_queues s d a) = {} \<and> set threads \<subseteq> set (ready_queues s' d a)\<rbrakk> \<Longrightarrow> kheap s t \<noteq> kheap s' t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; set threads \<inter> set (ready_queues s d a) = {}; set threads \<subseteq> set (ready_queues s' d a); kheap s t = kheap s' t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; set threads \<inter> set (ready_queues s d a) = {}; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_queues s'; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> not_queued t s
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> cur_thread s
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> scheduler_action s \<noteq> switch_thread t
 4. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s; st_tcb_at (\<lambda>s. \<not> runnable s) t s\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> is_etcb_at t s
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> cur_thread s
 4. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> scheduler_action s \<noteq> switch_thread t
 5. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s; st_tcb_at (\<lambda>s. \<not> runnable s) t s\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> is_etcb_at t s
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> cur_thread s
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> scheduler_action s \<noteq> switch_thread t
 4. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s; st_tcb_at (\<lambda>s. \<not> runnable s) t s\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> cur_thread s
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> scheduler_action s \<noteq> switch_thread t
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s; st_tcb_at (\<lambda>s. \<not> runnable s) t s\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
using this:
valid_idle s'

goal (4 subgoals):
 1. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> cur_thread s
 2. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s\<rbrakk> \<Longrightarrow> scheduler_action s \<noteq> switch_thread t
 3. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a); tcb_at t s; st_tcb_at (\<lambda>s. \<not> runnable s) t s\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>ready_queues s d a \<noteq> ready_queues s' d a; threads @ ready_queues s d a = ready_queues s' d a; valid_etcbs s; valid_etcbs s'; t \<in> set threads; ekheap s t = ekheap s' t; t \<noteq> idle_thread s' \<longrightarrow> t \<noteq> cur_thread s \<and> t \<noteq> cur_thread s'; scheduler_action s \<noteq> switch_thread t; idle_thread s = idle_thread s'; kheap s t = kheap s' t; t \<in> set (ready_queues s' d a); t \<notin> set (ready_queues s d a); is_etcb_at t s'; etcb_at (\<lambda>t. tcb_priority t = a \<and> tcb_domain t = d) t s'; st_tcb_at runnable t s'; distinct (ready_queues s' d a)\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal:
No subgoals!