theory Finalise_R

lemma valid_inQ_queues_lift:
  assumes tat: "\<And>d p tcb. \<lbrace>obj_at' (inQ d p) tcb\<rbrace> f \<lbrace>\<lambda>_. obj_at' (inQ d p) tcb\<rbrace>"
  and     prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  shows   "\<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" proof - show ?thesis apply (clarsimp simp: valid_def valid_inQ_queues_def) apply safe apply (rule use_valid [OF _ tat], assumption) apply (drule spec, drule spec, erule conjE, erule bspec) apply (rule ccontr) apply (erule notE[rotated], erule(1) use_valid [OF _ prq]) apply (erule use_valid [OF _ prq]) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> (\<forall>t\<in>set (ksReadyQueues b (d, p)). obj_at' (inQ d p) t b) \<and> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s); t \<in> set (ksReadyQueues b (d, p))\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t b
 2. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s); t \<in> set (ksReadyQueues b (d, p))\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) t s
 2. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); t \<in> set (ksReadyQueues b (d, p)); distinct (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> t \<in> set (ksReadyQueues s (d, p))
 2. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b d p t. \<lbrakk>(a, b) \<in> fst (f s); t \<in> set (ksReadyQueues b (d, p)); distinct (ksReadyQueues s (d, p)); t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> distinct (ksReadyQueues b (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b d p. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)) \<Longrightarrow> distinct (ksReadyQueues s (d, p)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>

goal:
No subgoals!