theory Abstract_Separation_D

lemma add_to_slots_assoc:
  "add_to_slots x (add_to_slots (y ++ z) obj) =
   add_to_slots (x ++ y) (add_to_slots z obj)" apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def) apply (fastforce simp: cdl_tcb.splits cdl_cnode.splits
                 split: cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abstract_Separation_D.add_to_slots x (Abstract_Separation_D.add_to_slots (y ++ z) obj) = Abstract_Separation_D.add_to_slots (x ++ y) (Abstract_Separation_D.add_to_slots z obj) proof (prove)
goal (1 subgoal):
 1. (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := x ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := y ++ z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>)) = (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | Tcb xa \<Rightarrow> Tcb (xa\<lparr>cdl_tcb_caps := x ++ y ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode xa \<Rightarrow> CNode (xa\<lparr>cdl_cnode_caps := x ++ y ++ (case case obj of Endpoint \<Rightarrow> obj | Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_caps := z ++ (case obj of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>) of Endpoint \<Rightarrow> \<lambda>x. None | Tcb x \<Rightarrow> cdl_tcb_caps x | CNode x \<Rightarrow> cdl_cnode_caps x)\<rparr>)) proof (prove)
goal:
No subgoals!