theory CSpace_AI

lemma is_derived_cap_class_range:
  "is_derived m src cap capa
  \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa" apply (clarsimp simp:is_derived_def split:if_splits) apply (frule master_cap_cap_range) apply (drule master_cap_class) apply simp apply (frule master_cap_cap_range) apply (drule master_cap_class) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m src cap capa \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of src m = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa
 2. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; descendants_of src m = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; cap_range capa = cap_range cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa
 2. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; descendants_of src m = {}; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; cap_range capa = cap_range cap; cap_class capa = cap_class cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa
 2. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; cap_range capa = cap_range cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap capa; cap \<noteq> NullCap; \<not> is_zombie capa; cap \<noteq> IRQControlCap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; cap_range capa = cap_range cap; cap_class capa = cap_class cap\<rbrakk> \<Longrightarrow> cap_class cap = cap_class capa \<and> cap_range cap \<subseteq> cap_range capa proof (prove)
goal:
No subgoals!