kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma cte_at_get_cap_wp:
  "cte_at p s \<Longrightarrow> \<exists>c. (c, s) \<in> fst (get_cap p s) \<and> cte_wp_at ((=) c) p s" by (clarsimp simp: 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) \<and> cte_wp_at ((=) c) p s
theory CSpace_AI

lemma s_d_swap_0 [simp]: "\<lbrakk> a \<noteq>0; b \<noteq> 0 \<rbrakk> \<Longrightarrow> s_d_swap 0 a b = 0" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (0::'a); b \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> s_d_swap (0::'a) a b = (0::'a)
theory CSpace_AI

lemma s_d_swap_inv [simp]: "s_d_swap (s_d_swap p a b) a b = p" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_d_swap (s_d_swap p a b) a b = p
theory CSpace_AI

lemma s_d_fst [simp]:
  "s_d_swap b a b = a" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_d_swap b a b = a
theory CSpace_AI

lemma s_d_snd [simp]:
  "s_d_swap a a b = b" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_d_swap a a b = b
theory CSpace_AI

lemma s_d_swap_0_eq [simp]:
  "\<lbrakk> src \<noteq> 0; dest \<noteq> 0 \<rbrakk> \<Longrightarrow> (s_d_swap c src dest = 0) = (c = 0)" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<noteq> (0::'a); dest \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> (s_d_swap c src dest = (0::'a)) = (c = (0::'a))
theory CSpace_AI

lemma s_d_swap_eq_src [simp]:
  "(s_d_swap p src dest = src) = (p = dest)" by (auto simp: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s_d_swap p src dest = src) = (p = dest)
theory CSpace_AI

lemma s_d_swap_eq_dest:
  "src \<noteq> dest \<Longrightarrow> (s_d_swap p src dest = dest) = (p = src)" by (simp add: s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. src \<noteq> dest \<Longrightarrow> (s_d_swap p src dest = dest) = (p = src)
theory CSpace_AI

lemma no_mloop:
  "no_mloop m" using valid_mdb by (simp add: valid_mdb_def m)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop m proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. no_mloop m
theory CSpace_AI

lemma no_loops [iff]:
  "m \<Turnstile> p \<rightarrow> p = False" using no_mloop by (cases p) (clarsimp simp add: no_mloop_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p = False proof (prove)
using this:
no_mloop m

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p = False
theory CSpace_AI

lemma no_loops_d [iff]:
  "m \<Turnstile> p \<leadsto> p = False" by (fastforce dest: r_into_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<leadsto> p = False
theory CSpace_AI

lemma no_loops_m [iff]:
  "(m p = Some p) = False" apply clarsimp apply (fold cdt_parent_defs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m p = Some p) = False proof (prove)
goal (1 subgoal):
 1. m p = Some p \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<leadsto> p \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma parency:
  "n \<Turnstile> p \<rightarrow> p' = m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p'" by (blast intro: parency_n_m parency_m_n')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> p \<rightarrow> p' = m \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p'
theory CSpace_AI

lemma descendants:
  "descendants_of p n =
  (let swap = \<lambda>S. S - {src,dest} \<union>
                (if src \<in> S then {dest} else {}) \<union>
                (if dest \<in> S then {src} else {}) in
  swap (descendants_of (s_d_swp p) m))" apply (simp add: Let_def parency descendants_of_def s_d_swap_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of p n = (let swap = \<lambda>S. S - {src, dest} \<union> (if src \<in> S then {dest} else {}) \<union> (if dest \<in> S then {src} else {}) in swap (descendants_of (s_d_swp p) m)) proof (prove)
goal (1 subgoal):
 1. (p = dest \<longrightarrow> (m \<Turnstile> src \<rightarrow> dest \<longrightarrow> {q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<longrightarrow> m \<Turnstile> src \<rightarrow> q)} = insert src ({q. m \<Turnstile> src \<rightarrow> q} - {dest})) \<and> ((src, dest) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> {q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m \<Turnstile> src \<rightarrow> q))} = {q. m \<Turnstile> src \<rightarrow> q})) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (m \<Turnstile> dest \<rightarrow> src \<longrightarrow> {q. q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m \<Turnstile> dest \<rightarrow> q)} = insert dest ({q. m \<Turnstile> dest \<rightarrow> q} - {src, dest})) \<and> ((dest, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> {q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m \<Turnstile> dest \<rightarrow> q))} = {q. m \<Turnstile> dest \<rightarrow> q})) \<and> (p \<noteq> src \<longrightarrow> (m \<Turnstile> p \<rightarrow> src \<longrightarrow> (m \<Turnstile> p \<rightarrow> dest \<longrightarrow> {q. q \<noteq> dest \<longrightarrow> q \<noteq> src \<longrightarrow> m \<Turnstile> p \<rightarrow> q} = insert src (insert dest ({q. m \<Turnstile> p \<rightarrow> q} - {src, dest}))) \<and> ((p, dest) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> {q. q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m \<Turnstile> p \<rightarrow> q)} = insert dest ({q. m \<Turnstile> p \<rightarrow> q} - {src, dest}))) \<and> ((p, src) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> (m \<Turnstile> p \<rightarrow> dest \<longrightarrow> {q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<longrightarrow> m \<Turnstile> p \<rightarrow> q)} = insert src ({q. m \<Turnstile> p \<rightarrow> q} - {dest})) \<and> ((p, dest) \<notin> (cdt_parent_rel m)\<^sup>+ \<longrightarrow> {q. q \<noteq> dest \<and> (q \<noteq> dest \<longrightarrow> q \<noteq> src \<and> (q \<noteq> src \<longrightarrow> m \<Turnstile> p \<rightarrow> q))} = {q. m \<Turnstile> p \<rightarrow> q})))) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma copy_of_commute:
  "copy_of c' c = copy_of c c'" apply (subgoal_tac "!c c'. copy_of c' c --> copy_of c c'") apply (rule iffI) apply (erule_tac x=c in allE, erule_tac x=c' in allE, simp) apply (erule_tac x=c' in allE, erule_tac x=c in allE, simp) apply clarsimp apply (clarsimp simp: copy_of_def is_reply_cap_def is_master_reply_cap_def
                      same_object_as_commute
                split: if_splits cap.splits) by (simp_all add: same_object_as_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of c' c = copy_of c c' proof (prove)
goal (2 subgoals):
 1. \<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c' \<Longrightarrow> copy_of c' c = copy_of c c'
 2. \<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c'; copy_of c' c\<rbrakk> \<Longrightarrow> copy_of c c'
 2. \<lbrakk>\<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c'; copy_of c c'\<rbrakk> \<Longrightarrow> copy_of c' c
 3. \<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c'; copy_of c c'\<rbrakk> \<Longrightarrow> copy_of c' c
 2. \<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c' proof (prove)
goal (1 subgoal):
 1. \<forall>c c'. copy_of c' c \<longrightarrow> copy_of c c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. copy_of c' c \<Longrightarrow> copy_of c c' proof (prove)
goal (10 subgoals):
 1. \<And>x21 x22 x23 x24. same_object_as NullCap (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 2. \<And>x21 x22 x23 x24 x31 x32 x33. same_object_as (EndpointCap x31 x32 x33) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 3. \<And>x21 x22 x23 x24 x41 x42 x43. same_object_as (NotificationCap x41 x42 x43) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 4. \<And>x21 x22 x23 x24 x61 x62 x63. same_object_as (CNodeCap x61 x62 x63) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 5. \<And>x21 x22 x23 x24 x7. same_object_as (ThreadCap x7) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 6. \<And>x21 x22 x23 x24. same_object_as DomainCap (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 7. \<And>x21 x22 x23 x24. same_object_as IRQControlCap (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 8. \<And>x21 x22 x23 x24 x10. same_object_as (IRQHandlerCap x10) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 9. \<And>x21 x22 x23 x24 x111 x112 x113. same_object_as (Zombie x111 x112 x113) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
 10. \<And>x21 x22 x23 x24 x12. same_object_as (ArchObjectCap x12) (UntypedCap x21 x22 x23 x24) \<Longrightarrow> False
theory CSpace_AI

lemma weak_derived_commute:
  "weak_derived c' c = weak_derived c c'" by (auto simp: weak_derived_def copy_of_commute split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c' c = weak_derived c c'
theory CSpace_AI

lemma weak_derived_Null:
  "weak_derived c' c \<Longrightarrow> (c' = cap.NullCap) = (c = cap.NullCap)" apply (clarsimp simp: weak_derived_def) apply (erule disjE) apply (clarsimp simp: copy_of_def split: if_split_asm) apply (auto simp: is_cap_simps same_object_as_def
              split: cap.splits)[1] apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived c' c \<Longrightarrow> (c' = NullCap) = (c = NullCap) proof (prove)
goal (1 subgoal):
 1. copy_of c' c \<and> cap_asid c' = cap_asid c \<and> cap_asid_base c' = cap_asid_base c \<and> cap_vptr c' = cap_vptr c \<or> c = c' \<Longrightarrow> (c' = NullCap) = (c = NullCap) proof (prove)
goal (2 subgoals):
 1. copy_of c' c \<and> cap_asid c' = cap_asid c \<and> cap_asid_base c' = cap_asid_base c \<and> cap_vptr c' = cap_vptr c \<Longrightarrow> (c' = NullCap) = (c = NullCap)
 2. c = c' \<Longrightarrow> (c' = NullCap) = (c = NullCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> is_untyped_cap c; same_object_as c c'; is_reply_cap c = is_reply_cap c'; is_master_reply_cap c = is_master_reply_cap c'; cap_asid c' = cap_asid c; cap_asid_base c' = cap_asid_base c; cap_vptr c' = cap_vptr c\<rbrakk> \<Longrightarrow> (c' = NullCap) = (c = NullCap)
 2. c = c' \<Longrightarrow> (c' = NullCap) = (c = NullCap) proof (prove)
goal (1 subgoal):
 1. c = c' \<Longrightarrow> (c' = NullCap) = (c = NullCap) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma ensure_no_children_descendants:
  "ensure_no_children p =
  (\<lambda>s. if descendants_of p (cdt s) = {}
   then returnOk () s
   else throwError ExceptionTypes_A.RevokeFirst s)" apply (rule ext) apply (simp add: ensure_no_children_def bindE_def liftE_def gets_def
                   get_def bind_def return_def lift_def whenE_def) apply (rule conjI) apply (clarsimp simp: descendants_of_def cdt_parent_defs) apply fastforce apply (clarsimp simp: descendants_of_def cdt_parent_defs) apply (drule tranclD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ensure_no_children p = (\<lambda>s. if descendants_of p (cdt s) = {} then returnOk () s else throwError RevokeFirst s) proof (prove)
goal (1 subgoal):
 1. \<And>s. ensure_no_children p s = (if descendants_of p (cdt s) = {} then returnOk () s else throwError RevokeFirst s) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>a b. cdt s (a, b) = Some p) \<longrightarrow> descendants_of p (cdt s) = {} \<longrightarrow> throwError RevokeFirst s = returnOk () s) \<and> ((\<forall>a b. cdt s (a, b) \<noteq> Some p) \<longrightarrow> descendants_of p (cdt s) \<noteq> {} \<longrightarrow> returnOk () s = throwError RevokeFirst s) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<exists>a b. cdt s (a, b) = Some p) \<longrightarrow> descendants_of p (cdt s) = {} \<longrightarrow> throwError RevokeFirst s = returnOk () s
 2. \<And>s. (\<forall>a b. cdt s (a, b) \<noteq> Some p) \<longrightarrow> descendants_of p (cdt s) \<noteq> {} \<longrightarrow> returnOk () s = throwError RevokeFirst s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>cdt s (a, b) = Some p; \<forall>a b. (p, a, b) \<notin> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> throwError RevokeFirst s = returnOk () s
 2. \<And>s. (\<forall>a b. cdt s (a, b) \<noteq> Some p) \<longrightarrow> descendants_of p (cdt s) \<noteq> {} \<longrightarrow> returnOk () s = throwError RevokeFirst s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b. cdt s (a, b) \<noteq> Some p) \<longrightarrow> descendants_of p (cdt s) \<noteq> {} \<longrightarrow> returnOk () s = throwError RevokeFirst s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>a b. cdt s (a, b) \<noteq> Some p; (p, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> returnOk () s = throwError RevokeFirst s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>a b. cdt s (a, b) \<noteq> Some p; \<exists>z. (p, z) \<in> {(p, c). cdt s c = Some p} \<and> (z, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>*\<rbrakk> \<Longrightarrow> returnOk () s = throwError RevokeFirst s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma desc_dest [intro?, simp]:
  "dest \<notin> descendants_of x m" using dest_None apply (clarsimp simp add: descendants_of_def) apply (drule tranclD2) apply (clarsimp simp: cdt_parent_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest \<notin> descendants_of x m proof (prove)
using this:
m dest = None

goal (1 subgoal):
 1. dest \<notin> descendants_of x m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = None; m \<Turnstile> x \<rightarrow> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = None; \<exists>z. m \<Turnstile> x \<rightarrow>* z \<and> m \<Turnstile> z \<leadsto> dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma no_src_parent' [iff]:
  "m' \<Turnstile> src \<leadsto> p = False" by (simp add: m'_def m''_def cdt_parent_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<Turnstile> src \<leadsto> p = False
theory CSpace_AI

lemma no_src_parent_trans' [iff]:
  "m' \<Turnstile> src \<rightarrow> p = False" by (clarsimp dest!: tranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<Turnstile> src \<rightarrow> p = False
theory CSpace_AI

lemma no_dest_parent_trans [iff]:
  "m \<Turnstile> dest \<rightarrow> p = False" using dest_desc by (fastforce simp add: descendants_of_def cdt_parent_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> dest \<rightarrow> p = False proof (prove)
using this:
descendants_of dest m = {}

goal (1 subgoal):
 1. m \<Turnstile> dest \<rightarrow> p = False
theory CSpace_AI

lemma no_dest_parent [iff]:
  "m \<turnstile> dest cdt_parent_of p = False" by (fastforce dest: r_into_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> dest \<leadsto> p = False
theory CSpace_AI

lemma no_dest_parent_unfold [iff]:
  "(m x = Some dest) = False" using no_dest_parent unfolding cdt_parent_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m x = Some dest) = False proof (prove)
using this:
m \<Turnstile> dest \<leadsto> ?p = False

goal (1 subgoal):
 1. (m x = Some dest) = False proof (prove)
using this:
((dest, ?p) \<in> {(p, c). m c = Some p}) = False

goal (1 subgoal):
 1. (m x = Some dest) = False
theory CSpace_AI

lemma no_src_child_trans [iff]:
  "m' \<turnstile> p cdt_parent_of\<^sup>+ src = False" by (clarsimp dest!: tranclD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<Turnstile> p \<rightarrow> src = False
theory CSpace_AI

lemma direct_src_loop_unfolded [iff]:
  "(m src = Some src) = False" by (fold cdt_parent_defs) (fastforce dest: r_into_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m src = Some src) = False
theory CSpace_AI

lemma mdb_cte_at:
  "mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) m" using valid_mdb by (simp add: valid_mdb_def m)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) m proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) m
theory CSpace_AI

lemma to_dest_direct [simp]:
  "m' \<Turnstile> x \<leadsto> dest = m \<Turnstile> x \<leadsto> src" by (clarsimp simp add: m'_def m''_def cdt_parent_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<Turnstile> x \<leadsto> dest = m \<Turnstile> x \<leadsto> src
theory CSpace_AI

lemma from_dest_direct [simp]:
  "m' \<Turnstile> dest \<leadsto> x = m \<Turnstile> src \<leadsto> x" by (clarsimp simp add: m'_def m''_def cdt_parent_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<Turnstile> dest \<leadsto> x = m \<Turnstile> src \<leadsto> x
theory CSpace_AI

lemma copy_untyped1:
  "\<lbrakk> copy_of cap cap'; is_untyped_cap cap' \<rbrakk> \<Longrightarrow> cap' = cap" by (simp add: copy_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>copy_of cap cap'; is_untyped_cap cap'\<rbrakk> \<Longrightarrow> cap' = cap
theory CSpace_AI

lemma copy_untyped2:
  "\<lbrakk> copy_of cap cap'; is_untyped_cap cap \<rbrakk> \<Longrightarrow> cap' = cap" apply (cases cap) apply (auto simp: copy_of_def same_object_as_def is_cap_simps
              split: if_split_asm cap.splits) done

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

lemma copy_of_Null [simp]:
  "\<not>copy_of cap.NullCap c" by (auto simp add: copy_of_def same_object_as_def is_cap_simps
              split: cap.splits)

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

lemma copy_of_Null2 [simp]:
  "\<not>copy_of c cap.NullCap" by (auto simp add: copy_of_def same_object_as_def is_cap_simps)

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

lemma weak_derived_untyped_range:
  "weak_derived dcap cap \<Longrightarrow> untyped_range dcap = untyped_range cap" by (cases dcap, auto simp: is_cap_simps weak_derived_def copy_of_def
                             same_object_as_def
                       split: if_split_asm cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived dcap cap \<Longrightarrow> untyped_range dcap = untyped_range cap
theory CSpace_AI

lemma weak_derived_cap_range:
  "\<And>dcap cap. weak_derived dcap cap \<Longrightarrow> cap_range dcap = cap_range cap" by (simp add:cap_range_def weak_derived_untyped_range weak_derived_obj_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>dcap cap. weak_derived dcap cap \<Longrightarrow> cap_range dcap = cap_range cap
theory CSpace_AI

lemma weak_derived_untyped2:
  "\<lbrakk> weak_derived cap cap'; is_untyped_cap cap \<rbrakk> \<Longrightarrow> cap' = cap" by (auto simp: weak_derived_def copy_untyped2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weak_derived cap cap'; is_untyped_cap cap\<rbrakk> \<Longrightarrow> cap' = cap
theory CSpace_AI

lemma weak_derived_Null_eq [simp]:
  "(weak_derived NullCap cap) = (cap = NullCap)" by (auto simp: weak_derived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived NullCap cap = (cap = NullCap)
theory CSpace_AI

lemma weak_derived_is_untyped:
  "weak_derived dcap cap \<Longrightarrow> is_untyped_cap dcap = is_untyped_cap cap" by (cases dcap, auto simp: is_cap_simps weak_derived_def copy_of_def
                             same_object_as_def
                       split: if_split_asm cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived dcap cap \<Longrightarrow> is_untyped_cap dcap = is_untyped_cap cap
theory CSpace_AI

lemma weak_derived_irq [simp]:
  "weak_derived IRQControlCap cap = (cap = IRQControlCap)" by (auto simp add: weak_derived_def copy_of_def same_object_as_def
           split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived IRQControlCap cap = (cap = IRQControlCap)
theory CSpace_AI

lemma weak_derived_is_reply:
  "weak_derived dcap cap \<Longrightarrow> is_reply_cap dcap = is_reply_cap cap" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def is_cap_simps
         split: if_split_asm cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived dcap cap \<Longrightarrow> is_reply_cap dcap = is_reply_cap cap
theory CSpace_AI

lemma weak_derived_is_reply_master:
  "weak_derived dcap cap \<Longrightarrow> is_master_reply_cap dcap = is_master_reply_cap cap" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def is_cap_simps
         split: if_split_asm cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived dcap cap \<Longrightarrow> is_master_reply_cap dcap = is_master_reply_cap cap
theory CSpace_AI

lemma non_arch_cap_asid_vptr_None:
  assumes "\<not> is_arch_cap cap"
  shows "cap_asid cap = None"
    and "cap_asid_base cap = None"
    and "cap_vptr cap = None" using assms by (cases cap; simp add: is_cap_simps cap_asid_def cap_asid_base_def cap_vptr_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid cap = None &&& cap_asid_base cap = None &&& cap_vptr cap = None proof (prove)
using this:
\<not> is_arch_cap cap

goal (1 subgoal):
 1. cap_asid cap = None &&& cap_asid_base cap = None &&& cap_vptr cap = None
theory CSpace_AI

lemma weak_derived_Reply:
  "weak_derived (cap.ReplyCap t m R) c = (\<exists> R'. (c = cap.ReplyCap t m R'))"
  "weak_derived c (cap.ReplyCap t m R) = (\<exists> R'. (c = cap.ReplyCap t m R'))" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def is_cap_simps
                 non_arch_cap_asid_vptr_None[simplified is_cap_simps]
          split: if_split_asm cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived (ReplyCap t m R) c = (\<exists>R'. c = ReplyCap t m R') &&& weak_derived c (ReplyCap t m R) = (\<exists>R'. c = ReplyCap t m R')