theory DetSchedSchedule_AI

lemma next_thread_update:
  assumes a: "P(next_thread queues)"
  assumes b: "P t"
  shows
    "P(next_thread (queues((p :: word8) := t # (queues prio))))" proof - have imp_comp[simp]: "\<And>P Q. {x. P x \<longrightarrow> Q x} = {x. \<not> P x} \<union> {x. Q x}" by blast { assume c: "{prio. queues prio \<noteq> []} = {}" from a b c have ?thesis by (simp add: next_thread_def max_non_empty_queue_def) } moreover { assume d: "{prio. queues prio \<noteq> []} \<noteq> {}" from a b have ?thesis apply (clarsimp simp: next_thread_def
                            max_non_empty_queue_def
                            Max_insert[OF finite_word d]) apply (clarsimp simp add: max_def) done } ultimately show ?thesis by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (prove)
goal (1 subgoal):
 1. \<And>P Q. {x. P x \<longrightarrow> Q x} = {x. \<not> P x} \<union> {x. Q x} proof (state)
this:
{x. ?P x \<longrightarrow> ?Q x} = {x. \<not> ?P x} \<union> {x. ?Q x}

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{x. ?P x \<longrightarrow> ?Q x} = {x. \<not> ?P x} \<union> {x. ?Q x}

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} = {}

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (chain)
picking this:
P (next_thread queues)
P t
{prio. queues prio \<noteq> []} = {} proof (prove)
using this:
P (next_thread queues)
P t
{prio. queues prio \<noteq> []} = {}

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} = {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} = {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} = {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} \<noteq> {}

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (chain)
picking this:
P (next_thread queues)
P t proof (prove)
using this:
P (next_thread queues)
P t

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (hd (queues (Max {prio. queues prio \<noteq> []}))); P t; max p (Max {prio. queues prio \<noteq> []}) \<noteq> p\<rbrakk> \<Longrightarrow> P (hd (queues (max p (Max {prio. queues prio \<noteq> []})))) proof (prove)
goal:
No subgoals! proof (state)
this:
P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
{prio. queues prio \<noteq> []} \<noteq> {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (chain)
picking this:
{prio. queues prio \<noteq> []} = {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))
{prio. queues prio \<noteq> []} \<noteq> {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio))) proof (prove)
using this:
{prio. queues prio \<noteq> []} = {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))
{prio. queues prio \<noteq> []} \<noteq> {} \<Longrightarrow> P (next_thread (queues(p := t # queues prio)))

goal (1 subgoal):
 1. P (next_thread (queues(p := t # queues prio))) proof (state)
this:
P (next_thread (queues(p := t # queues prio)))

goal:
No subgoals!