kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma mdb_cte_at_cdt_null:
  "\<lbrakk>caps_of_state s p = Some cap.NullCap;
    mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk>
   \<Longrightarrow> (cdt s) p = None" apply (rule ccontr) apply (clarsimp) apply (drule_tac src=p in mdb_cte_at_cte_wp_at) apply (fastforce) apply (clarsimp simp:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some NullCap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some NullCap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); cdt s p \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some NullCap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); cdt s p = Some (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some NullCap; cdt s p = Some (a, b)\<rbrakk> \<Longrightarrow> p \<in> dom (cdt s) \<or> p \<in> ran (cdt s)
 2. \<And>a b. \<lbrakk>caps_of_state s p = Some NullCap; cdt s p = Some (a, b); cte_wp_at ((\<noteq>) NullCap) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some NullCap; cdt s p = Some (a, b); cte_wp_at ((\<noteq>) NullCap) p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_untyped_cap_as_full_cdt[wp]:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>_ s'. P (cdt s')\<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def) apply (wp set_cap_rvk_cdt_ct_ms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>_ s'. P (cdt s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>_ s'. P (cdt s')\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_untyped_cap_as_full_is_original[wp]:
  "\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s'. P (is_original_cap s') \<rbrace>" apply (simp add:set_untyped_cap_as_full_def split del:if_split) apply (rule hoare_pre) apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s'. P (is_original_cap s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>rv s'. P (is_original_cap s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>rv s'. P (is_original_cap s')\<rbrace>
 2. \<And>s. P (is_original_cap s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (is_original_cap s) \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> P (is_original_cap s)) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> P (is_original_cap s)) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma imp_rev: "\<lbrakk>a\<longrightarrow>b;\<not>b\<rbrakk> \<Longrightarrow> \<not> a" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<longrightarrow> b; \<not> b\<rbrakk> \<Longrightarrow> \<not> a
theory CSpace_AI

lemma mdb_cte_at_more_swp[simp]: "mdb_cte_at
            (swp (cte_wp_at P)
              (trans_state f s)) =
       mdb_cte_at
            (swp (cte_wp_at P)
              (s))" apply (simp add: swp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at P) (trans_state f s)) = mdb_cte_at (swp (cte_wp_at P) s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma usable_untyped_range_empty[simp]:
  "is_untyped_cap cap \<Longrightarrow> usable_untyped_range (max_free_index_update cap) = {}" by (clarsimp simp:is_cap_simps free_index_update_def cap_aligned_def max_free_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap cap \<Longrightarrow> usable_untyped_range (max_free_index_update cap) = {}
theory CSpace_AI

lemma reply_cap_id_free_index:
 "\<lbrakk>m src = Some capa; m' = m (src \<mapsto> capa\<lparr>free_index :=x\<rparr>)\<rbrakk> \<Longrightarrow>
   m' ptr = Some (ReplyCap t master rights) \<longleftrightarrow> m ptr = Some (ReplyCap t master rights)" by (rule iffI)
    (clarsimp simp add: free_index_update_def split:if_splits cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa)\<rbrakk> \<Longrightarrow> (m' ptr = Some (ReplyCap t master rights)) = (m ptr = Some (ReplyCap t master rights))
theory CSpace_AI

lemma reply_mdb_update_free_index:
  "\<lbrakk>m src = Some capa; m' = m (src \<mapsto> capa\<lparr>free_index :=x\<rparr>)\<rbrakk> \<Longrightarrow>
   reply_mdb c m'  = reply_mdb c m" by (rule iffI)
     (simp only: reply_mdb_def reply_caps_mdb_def reply_masters_mdb_def reply_cap_id_free_index)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa)\<rbrakk> \<Longrightarrow> reply_mdb c m' = reply_mdb c m
theory CSpace_AI

lemma cap_aligned_free_index_update[simp]:
  "cap_aligned capa \<Longrightarrow> cap_aligned (capa\<lparr>free_index :=x\<rparr>)" apply (case_tac capa) apply (clarsimp simp: cap_aligned_def free_index_update_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_aligned capa \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_aligned capa; capa = NullCap\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_aligned capa; capa = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 3. \<And>x31 x32 x33. \<lbrakk>cap_aligned capa; capa = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 4. \<And>x41 x42 x43. \<lbrakk>cap_aligned capa; capa = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 5. \<And>x51 x52 x53. \<lbrakk>cap_aligned capa; capa = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 6. \<And>x61 x62 x63. \<lbrakk>cap_aligned capa; capa = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 7. \<And>x7. \<lbrakk>cap_aligned capa; capa = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 8. \<lbrakk>cap_aligned capa; capa = DomainCap\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 9. \<lbrakk>cap_aligned capa; capa = IRQControlCap\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
 10. \<And>x10. \<lbrakk>cap_aligned capa; capa = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_aligned (free_index_update (\<lambda>_. x) capa)
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma upd_commute:
  "src \<noteq> dest \<Longrightarrow> (m(dest \<mapsto> cap, src \<mapsto> capa))
  = (m(src \<mapsto> capa, dest \<mapsto> cap))" apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<noteq> dest \<Longrightarrow> m(dest \<mapsto> cap, src \<mapsto> capa) = m(src \<mapsto> capa, dest \<mapsto> cap) proof (prove)
goal (1 subgoal):
 1. \<And>x. src \<noteq> dest \<Longrightarrow> (m(dest \<mapsto> cap, src \<mapsto> capa)) x = (m(src \<mapsto> capa, dest \<mapsto> cap)) x proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_class_free_index_upd[simp]:
  "cap_class (free_index_update f cap) = cap_class cap" by (simp add:free_index_update_def split:cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_class (free_index_update f cap) = cap_class cap
theory CSpace_AI

lemma cap_range_free_index_update[simp]:
  "cap_range (capa\<lparr>free_index:=x\<rparr>) = cap_range capa" by(auto simp:cap_range_def free_index_update_def split:cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range (free_index_update (\<lambda>_. x) capa) = cap_range capa
theory CSpace_AI

lemma cap_range_free_index_update2[simp]:
  "cap_range (free_index_update f cap) = cap_range cap" by (auto simp:cap_range_def free_index_update_def split:cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range (free_index_update f cap) = cap_range cap
theory CSpace_AI

lemma swp_cte_at_cdt_update [iff]:
  "swp cte_at (cdt_update f s) = swp cte_at s" by (simp add: swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp (cte_wp_at (\<lambda>_. True)) (cdt_update f s) = swp (cte_wp_at (\<lambda>_. True)) s
theory CSpace_AI

lemma swp_cte_at_mdb_rev_update [iff]:
  "swp cte_at (is_original_cap_update f s) = swp cte_at s" by (simp add: swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp (cte_wp_at (\<lambda>_. True)) (is_original_cap_update f s) = swp (cte_wp_at (\<lambda>_. True)) s
theory CSpace_AI

lemma derived_not_Null [simp]:
  "\<not>is_derived m p c cap.NullCap"
  "\<not>is_derived m p cap.NullCap c" by (auto simp: is_derived_def cap_master_cap_simps dest!: cap_master_cap_eqDs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_derived m p c NullCap &&& \<not> is_derived m p NullCap c
theory CSpace_AI

lemma set_untyped_cap_as_full_impact:
  "\<lbrace>cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap c src
   \<lbrace>\<lambda>r. cte_wp_at ((=) (masked_as_full src_cap c)) src\<rbrace>" apply (simp only: set_untyped_cap_as_full_def) apply (rule hoare_pre) apply (wp set_cap_cte_wp_at) apply (auto simp:masked_as_full_def elim:cte_wp_at_weakenE split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap c src \<lbrace>\<lambda>r. cte_wp_at ((=) (masked_as_full src_cap c)) src\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) src_cap) src\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>r. cte_wp_at ((=) (masked_as_full src_cap c)) src\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>r. cte_wp_at ((=) (masked_as_full src_cap c)) src\<rbrace>
 2. \<And>s. cte_wp_at ((=) src_cap) src s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at ((=) src_cap) src s \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<longrightarrow> ((\<lambda>s. if src = src then masked_as_full src_cap c = max_free_index_update src_cap else cte_wp_at ((=) (masked_as_full src_cap c)) src s) and cte_wp_at (\<lambda>_. True) src) s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c) \<longrightarrow> cte_wp_at ((=) (masked_as_full src_cap c)) src s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma is_derived_masked_as_full[simp]:
  "is_derived (cdt a) src c (masked_as_full src_cap c) =
   is_derived (cdt a) src c src_cap" apply (case_tac c) apply (simp_all add:masked_as_full_def) apply (clarsimp simp:is_cap_simps split:if_splits) apply (auto simp add:is_derived_def cap_master_cap_simps is_cap_simps intro!: is_derived_arch_non_arch) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap proof (prove)
goal (12 subgoals):
 1. c = NullCap \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 2. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 3. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 4. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 5. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 6. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 7. \<And>x7. c = ThreadCap x7 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 8. c = DomainCap \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 9. c = IRQControlCap \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
 10. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> is_derived (cdt a) src c (masked_as_full src_cap c) = is_derived (cdt a) src c src_cap
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> is_untyped_cap src_cap \<and> obj_ref_of src_cap = x22 \<and> cap_bits_untyped src_cap = x23 \<longrightarrow> is_derived (cdt a) src (UntypedCap x21 x22 x23 x24) (max_free_index_update src_cap) = is_derived (cdt a) src (UntypedCap x21 x22 x23 x24) src_cap proof (prove)
goal (1 subgoal):
 1. \<And>x21 x24 dev r bits f. \<lbrakk>c = UntypedCap x21 r bits x24; src_cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> is_derived (cdt a) src (UntypedCap x21 r bits x24) (UntypedCap dev r bits (max_free_index bits)) = is_derived (cdt a) src (UntypedCap x21 r bits x24) (UntypedCap dev r bits f) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_range_maskedAsFull[simp]:
  "cap_range (masked_as_full src_cap cap) = cap_range src_cap" apply (clarsimp simp:masked_as_full_def is_cap_simps split:cap.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range (masked_as_full src_cap cap) = cap_range src_cap proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma connect_eqv_singleE:
  assumes single:"\<And>p p'. ((p,p') \<in> m) = ((p,p')\<in> m')"
  shows "((p,p')\<in> m\<^sup>+) = ((p,p')\<in> m'\<^sup>+)" apply (rule iffI) apply (erule trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp:single) apply (drule iffD1[OF single]) apply simp apply (erule trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp:single) apply (drule iffD2[OF single]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((p, p') \<in> m\<^sup>+) = ((p, p') \<in> m'\<^sup>+) proof (prove)
goal (2 subgoals):
 1. (p, p') \<in> m\<^sup>+ \<Longrightarrow> (p, p') \<in> m'\<^sup>+
 2. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>y. (p, y) \<in> m \<Longrightarrow> (p, y) \<in> m'\<^sup>+
 2. \<And>y z. \<lbrakk>(p, y) \<in> m\<^sup>+; (y, z) \<in> m; (p, y) \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m'\<^sup>+
 3. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>y. (p, y) \<in> m \<Longrightarrow> (p, y) \<in> m'
 2. \<And>y z. \<lbrakk>(p, y) \<in> m\<^sup>+; (y, z) \<in> m; (p, y) \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m'\<^sup>+
 3. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(p, y) \<in> m\<^sup>+; (y, z) \<in> m; (p, y) \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m'\<^sup>+
 2. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(p, y) \<in> m\<^sup>+; (p, y) \<in> m'\<^sup>+; (y, z) \<in> m'\<rbrakk> \<Longrightarrow> (p, z) \<in> m'\<^sup>+
 2. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (1 subgoal):
 1. (p, p') \<in> m'\<^sup>+ \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y. (p, y) \<in> m' \<Longrightarrow> (p, y) \<in> m\<^sup>+
 2. \<And>y z. \<lbrakk>(p, y) \<in> m'\<^sup>+; (y, z) \<in> m'; (p, y) \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>y. (p, y) \<in> m' \<Longrightarrow> (p, y) \<in> m
 2. \<And>y z. \<lbrakk>(p, y) \<in> m'\<^sup>+; (y, z) \<in> m'; (p, y) \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(p, y) \<in> m'\<^sup>+; (y, z) \<in> m'; (p, y) \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, z) \<in> m\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(p, y) \<in> m'\<^sup>+; (p, y) \<in> m\<^sup>+; (y, z) \<in> m\<rbrakk> \<Longrightarrow> (p, z) \<in> m\<^sup>+ proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma connect_eqv_singleE':
  assumes single:"\<And>p p'. ((p,p') \<in> m) = ((p,p')\<in> m')"
  shows "((p,p')\<in> m\<^sup>*) = ((p,p')\<in> m'\<^sup>*)" apply (case_tac "p = p'") apply simp apply (rule iffI) apply (drule rtranclD) apply clarsimp apply (rule trancl_into_rtrancl) apply (simp add:connect_eqv_singleE[OF single]) apply (drule rtranclD) apply clarsimp apply (rule trancl_into_rtrancl) apply (simp add:connect_eqv_singleE[OF single]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((p, p') \<in> m\<^sup>*) = ((p, p') \<in> m'\<^sup>*) proof (prove)
goal (2 subgoals):
 1. p = p' \<Longrightarrow> ((p, p') \<in> m\<^sup>*) = ((p, p') \<in> m'\<^sup>*)
 2. p \<noteq> p' \<Longrightarrow> ((p, p') \<in> m\<^sup>*) = ((p, p') \<in> m'\<^sup>*) proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> ((p, p') \<in> m\<^sup>*) = ((p, p') \<in> m'\<^sup>*) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m'\<^sup>*
 2. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> p'; p = p' \<or> p \<noteq> p' \<and> (p, p') \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m'\<^sup>*
 2. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m'\<^sup>*
 2. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m'\<^sup>+
 2. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>*\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> p'; p = p' \<or> p \<noteq> p' \<and> (p, p') \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> p'; (p, p') \<in> m'\<^sup>+\<rbrakk> \<Longrightarrow> (p, p') \<in> m\<^sup>+ proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma identity_eq :"((=) x) = (\<lambda>c. c = x)" by (rule ext) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) x = (\<lambda>c. c = x)
theory CSpace_AI

lemma forall_eq: "(\<forall>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>b. Q b)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. P x = Q x \<Longrightarrow> (\<forall>x. P x) = (\<forall>b. Q b)
theory CSpace_AI

lemma ran_dom:"(\<forall>x\<in> ran m. P x) = (\<forall>y\<in> dom m. P (the (m y)))" by (auto simp:ran_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>ran m. P x) = (\<forall>y\<in>dom m. P (the (m y)))
theory CSpace_AI

lemma dom_in:
  "(\<exists>x. c a = Some x) = (a\<in> dom c)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. c a = Some x) = (a \<in> dom c)
theory CSpace_AI

lemma same_region_as_masked_as_full[simp]:
  "same_region_as (masked_as_full src_cap c) = same_region_as src_cap" apply (rule ext)+ apply (case_tac src_cap;
         clarsimp simp:masked_as_full_def is_cap_simps free_index_update_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_region_as (masked_as_full src_cap c) = same_region_as src_cap proof (prove)
goal (1 subgoal):
 1. \<And>x. same_region_as (masked_as_full src_cap c) x = same_region_as src_cap x proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma should_be_parent_of_masked_as_full[simp]:
  "should_be_parent_of (masked_as_full src_cap c) = should_be_parent_of src_cap" apply (rule ext)+ apply (clarsimp simp:should_be_parent_of_def) apply (case_tac src_cap; simp add:masked_as_full_def is_cap_simps free_index_update_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. should_be_parent_of (masked_as_full src_cap c) = should_be_parent_of src_cap proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. should_be_parent_of (masked_as_full src_cap c) x xa xb = should_be_parent_of src_cap x xa xb proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. (x \<and> same_region_as src_cap xa \<and> (case masked_as_full src_cap c of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge xa = badge \<and> \<not> xb | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge xa = badge \<and> \<not> xb | _ \<Rightarrow> True)) = (x \<and> same_region_as src_cap xa \<and> (case src_cap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge xa = badge \<and> \<not> xb | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge xa = badge \<and> \<not> xb | _ \<Rightarrow> True)) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cte_at_get_cap:
  "cte_at p s \<Longrightarrow> \<exists>c. (c, s) \<in> fst (get_cap p s)" by (clarsimp simp add: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> \<exists>c. (c, s) \<in> fst (get_cap p s)