theory CSpace1_R

lemma is_derived_maskedAsFull[simp]:
  "is_derived' m slot c (maskedAsFull src_cap' a) =
   is_derived' m slot c src_cap'" apply (clarsimp simp: maskedAsFull_def isCap_simps split:if_splits) apply (case_tac c) apply (clarsimp simp:is_derived'_def vsCapRef_def isCap_simps badge_derived'_def )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived' m slot c (maskedAsFull src_cap' a) = is_derived' m slot c src_cap' proof (prove)
goal (1 subgoal):
 1. \<And>d f da v0a v1a fa. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f) proof (prove)
goal (12 subgoals):
 1. \<And>d f da v0a v1a fa x1. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 2. \<And>d f da v0a v1a fa. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.NullCap\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 3. \<And>d f da v0a v1a fa x31 x32 x33 x34. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 4. \<And>d f da v0a v1a fa x4. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 5. \<And>d f da v0a v1a fa x51 x52 x53 x54 x55 x56. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 6. \<And>d f da v0a v1a fa. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.DomainCap\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 7. \<And>d f da v0a v1a fa x71 x72 x73. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 8. \<And>d f da v0a v1a fa x8. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 9. \<And>d f da v0a v1a fa x91 x92 x93. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
 10. \<And>d f da v0a v1a fa x101 x102 x103 x104. \<lbrakk>src_cap' = capability.UntypedCap d v0a v1a f; a = capability.UntypedCap da v0a v1a fa; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> is_derived' m slot c (capability.UntypedCap d v0a v1a (max_free_index v1a)) = is_derived' m slot c (capability.UntypedCap d v0a v1a f)
A total of 12 subgoals... proof (prove)
goal:
No subgoals!