theory Scheduler_IF

lemma any_valid_thread:
  "queues p \<noteq> [] \<Longrightarrow> (\<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x)
   \<Longrightarrow> P (hd (max_non_empty_queue queues))" apply (simp add: max_non_empty_queue_def) apply (rule Max_prop) prefer 2 apply simp apply blast apply (drule_tac x="hd (queues (Max {prio. queues prio \<noteq> []}))" in meta_spec) apply (drule_tac x="Max {prio. queues prio \<noteq> []}" in meta_spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (hd (max_non_empty_queue queues)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []})))
 2. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> {prio. queues prio \<noteq> []} \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> {prio. queues prio \<noteq> []} \<noteq> {}
 2. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x. queues x \<noteq> []
 2. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queues p \<noteq> []; \<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queues p \<noteq> []; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}; \<And>prio. hd (queues (Max {prio. queues prio \<noteq> []})) \<in> set (queues prio) \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []})))\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queues p \<noteq> []; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}; hd (queues (Max {prio. queues prio \<noteq> []})) \<in> set (queues (Max {prio. queues prio \<noteq> []})) \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []})))\<rbrakk> \<Longrightarrow> P (hd (queues (Max {prio. queues prio \<noteq> []}))) proof (prove)
goal:
No subgoals!