theory ADT_C

lemma tcb_queue_rel_unique:
  "hp NULL = None \<Longrightarrow>
   tcb_queue_relation gn gp hp as pp cp \<Longrightarrow>
   tcb_queue_relation gn gp hp as' pp cp \<Longrightarrow> as' = as" proof (induct as arbitrary: as' pp cp) case Nil thus ?case by (cases as', simp+) next case (Cons x xs) thus ?case by (cases as') (clarsimp simp: tcb_ptr_to_ctcb_ptr_def)+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as proof (state)
goal (2 subgoals):
 1. \<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp [] pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = []
 2. \<And>x1 as as' pp cp. \<lbrakk>\<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as; hp NULL = None; tcb_queue_relation gn gp hp (x1 # as) pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = x1 # as proof (state)
this:
hp NULL = None
tcb_queue_relation gn gp hp [] pp cp
tcb_queue_relation gn gp hp as' pp cp

goal (2 subgoals):
 1. \<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp [] pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = []
 2. \<And>x1 as as' pp cp. \<lbrakk>\<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as; hp NULL = None; tcb_queue_relation gn gp hp (x1 # as) pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = x1 # as proof (prove)
using this:
hp NULL = None
tcb_queue_relation gn gp hp [] pp cp
tcb_queue_relation gn gp hp as' pp cp

goal (1 subgoal):
 1. as' = [] proof (state)
this:
as' = []

goal (1 subgoal):
 1. \<And>x1 as as' pp cp. \<lbrakk>\<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as; hp NULL = None; tcb_queue_relation gn gp hp (x1 # as) pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = x1 # as proof (state)
goal (1 subgoal):
 1. \<And>x1 as as' pp cp. \<lbrakk>\<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as; hp NULL = None; tcb_queue_relation gn gp hp (x1 # as) pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = x1 # as proof (state)
this:
\<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp xs ?pp ?cp; tcb_queue_relation gn gp hp ?as' ?pp ?cp\<rbrakk> \<Longrightarrow> ?as' = xs
hp NULL = None
tcb_queue_relation gn gp hp (x # xs) pp cp
tcb_queue_relation gn gp hp as' pp cp

goal (1 subgoal):
 1. \<And>x1 as as' pp cp. \<lbrakk>\<And>as' pp cp. \<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp as pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = as; hp NULL = None; tcb_queue_relation gn gp hp (x1 # as) pp cp; tcb_queue_relation gn gp hp as' pp cp\<rbrakk> \<Longrightarrow> as' = x1 # as proof (prove)
using this:
\<lbrakk>hp NULL = None; tcb_queue_relation gn gp hp xs ?pp ?cp; tcb_queue_relation gn gp hp ?as' ?pp ?cp\<rbrakk> \<Longrightarrow> ?as' = xs
hp NULL = None
tcb_queue_relation gn gp hp (x # xs) pp cp
tcb_queue_relation gn gp hp as' pp cp

goal (1 subgoal):
 1. as' = x # xs proof (state)
this:
as' = x # xs

goal:
No subgoals!