kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma set_cap_caps_of_state_monad:
  "(v, s') \<in> fst (set_cap cap p s) \<Longrightarrow> caps_of_state s' = (caps_of_state s)(p \<mapsto> cap)" apply (drule use_valid) apply (rule set_cap_caps_of_state [where P="(=) ((caps_of_state s)(p\<mapsto>cap))"]) apply (rule refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v, s') \<in> fst (set_cap cap p s) \<Longrightarrow> caps_of_state s' = (caps_of_state s)(p \<mapsto> cap) proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> set_cap cap p \<lbrace>?Q\<rbrace>
 2. ?P s
 3. ?Q v s' \<Longrightarrow> caps_of_state s' = (caps_of_state s)(p \<mapsto> cap) proof (prove)
goal (2 subgoals):
 1. (caps_of_state s)(p \<mapsto> cap) = (caps_of_state s)(p \<mapsto> cap)
 2. (caps_of_state s)(p \<mapsto> cap) = caps_of_state s' \<Longrightarrow> caps_of_state s' = (caps_of_state s)(p \<mapsto> cap) proof (prove)
goal (1 subgoal):
 1. (caps_of_state s)(p \<mapsto> cap) = caps_of_state s' \<Longrightarrow> caps_of_state s' = (caps_of_state s)(p \<mapsto> cap) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants_of_empty:
  "(descendants_of d m = {}) = (\<forall>c. \<not>m \<turnstile> d cdt_parent_of c)" apply (simp add: descendants_of_def) apply (rule iffI) apply clarsimp apply (erule allE, erule allE) apply (erule notE) apply fastforce apply clarsimp apply (drule tranclD) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (descendants_of d m = {}) = (\<forall>c. (d, c) \<notin> cdt_parent_rel m) proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+) = (\<forall>a b. (d, a, b) \<notin> cdt_parent_rel m) proof (prove)
goal (2 subgoals):
 1. \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m
 2. \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+; m \<Turnstile> d \<leadsto> (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m \<Turnstile> d \<leadsto> (a, b); (d, ?a8 a b, ?b10 a b) \<notin> (cdt_parent_rel m)\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. m \<Turnstile> d \<leadsto> (a, b) \<Longrightarrow> m \<Turnstile> d \<rightarrow> (?a8 a b, ?b10 a b)
 2. \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<forall>a b. (d, a, b) \<notin> cdt_parent_rel m \<Longrightarrow> \<forall>a b. (d, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (d, a, b) \<notin> cdt_parent_rel m; m \<Turnstile> d \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (d, a, b) \<notin> cdt_parent_rel m; \<exists>z. m \<Turnstile> d \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants_of_None:
  "(\<forall>c. d \<notin> descendants_of c m) = (m d = None)" apply (simp add: descendants_of_def cdt_parent_defs) apply (rule iffI) prefer 2 apply clarsimp apply (drule tranclD2) apply clarsimp apply (erule contrapos_pp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>c. d \<notin> descendants_of c m) = (m d = None) proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+) = (m d = None) proof (prove)
goal (2 subgoals):
 1. \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> m d = None
 2. m d = None \<Longrightarrow> \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. m d = None \<Longrightarrow> \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+
 2. \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> m d = None proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m d = None; ((a, b), d) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> m d = None proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m d = None; \<exists>z. ((a, b), z) \<in> {(p, c). m c = Some p}\<^sup>* \<and> (z, d) \<in> {(p, c). m c = Some p}\<rbrakk> \<Longrightarrow> False
 2. \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> m d = None proof (prove)
goal (1 subgoal):
 1. \<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+ \<Longrightarrow> m d = None proof (prove)
goal (1 subgoal):
 1. m d \<noteq> None \<Longrightarrow> \<not> (\<forall>a b. ((a, b), d) \<notin> {(p, c). m c = Some p}\<^sup>+) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma not_should_be_parent_Null [simp]:
  "should_be_parent_of cap.NullCap a b c = False" by (simp add: should_be_parent_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. should_be_parent_of NullCap a b c = False
theory CSpace_AI

lemma mdb_None_no_parent:
  "m p = None \<Longrightarrow> m \<Turnstile> c \<leadsto> p = False" by (clarsimp simp: cdt_parent_defs)

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

lemma descendants_of_self_None:
  assumes "descendants_of dest m = {}"
  assumes n: "m dest = None"
  shows "descendants_of x (m(dest \<mapsto> dest)) =
   (if x = dest then {dest} else descendants_of x m)" apply (subst descendants_of_self[OF assms(1)]) apply clarsimp apply (subgoal_tac "dest \<notin> descendants_of x m") apply simp apply (insert n) apply (simp add: descendants_of_None [symmetric] del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> dest)) = (if x = dest then {dest} else descendants_of x m) proof (prove)
goal (1 subgoal):
 1. (if x = dest then {dest} else descendants_of x m - {dest}) = (if x = dest then {dest} else descendants_of x m) proof (prove)
goal (1 subgoal):
 1. x \<noteq> dest \<Longrightarrow> descendants_of x m - {dest} = descendants_of x m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> dest; dest \<notin> descendants_of x m\<rbrakk> \<Longrightarrow> descendants_of x m - {dest} = descendants_of x m
 2. x \<noteq> dest \<Longrightarrow> dest \<notin> descendants_of x m proof (prove)
goal (1 subgoal):
 1. x \<noteq> dest \<Longrightarrow> dest \<notin> descendants_of x m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> dest; m dest = None\<rbrakk> \<Longrightarrow> dest \<notin> descendants_of x m proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants_of_NoneD:
  "\<lbrakk> m p = None; p \<in> descendants_of x m \<rbrakk> \<Longrightarrow> False" by (simp add: descendants_of_None [symmetric] del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = None; p \<in> descendants_of x m\<rbrakk> \<Longrightarrow> False
theory CSpace_AI

lemma descendants_of_insert_child':
  assumes d: "descendants_of dest m = {}"
  assumes s: "src \<noteq> dest"
  assumes m: "m dest = None"
  shows
  "descendants_of x (m (dest \<mapsto> src)) =
   (if src \<in> descendants_of x m \<or> x = src
    then descendants_of x m \<union> {dest} else descendants_of x m)" apply (subst descendants_of_insert_child [OF d s]) apply clarsimp apply (subgoal_tac "dest \<notin> descendants_of x m") apply clarsimp apply (rule notI) apply (rule descendants_of_NoneD, rule m, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> src)) = (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m) proof (prove)
goal (1 subgoal):
 1. (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m - {dest}) = (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<notin> descendants_of x m; x \<noteq> src\<rbrakk> \<Longrightarrow> descendants_of x m - {dest} = descendants_of x m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>src \<notin> descendants_of x m; x \<noteq> src; dest \<notin> descendants_of x m\<rbrakk> \<Longrightarrow> descendants_of x m - {dest} = descendants_of x m
 2. \<lbrakk>src \<notin> descendants_of x m; x \<noteq> src\<rbrakk> \<Longrightarrow> dest \<notin> descendants_of x m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<notin> descendants_of x m; x \<noteq> src\<rbrakk> \<Longrightarrow> dest \<notin> descendants_of x m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>src \<notin> descendants_of x m; x \<noteq> src; dest \<in> descendants_of x m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma no_mloop [intro!]: "no_mloop m" using valid_mdb by (simp add: valid_mdb_def m_def)

(* 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 [simp, intro!]: "\<not>m \<Turnstile> p \<rightarrow> p" using no_mloop by (cases p) (simp add: no_mloop_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p, p) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
using this:
no_mloop m

goal (1 subgoal):
 1. (p, p) \<notin> (cdt_parent_rel m)\<^sup>+
theory CSpace_AI

lemma no_mdb_loop [simp, intro!]: "m p \<noteq> Some p" proof assume "m p = Some p" hence "m \<Turnstile> p \<leadsto> p" by (simp add: cdt_parent_of_def) hence "m \<Turnstile> p \<rightarrow> p" .. thus False by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p \<noteq> Some p proof (state)
goal (1 subgoal):
 1. m p = Some p \<Longrightarrow> False proof (state)
this:
m p = Some p

goal (1 subgoal):
 1. m p = Some p \<Longrightarrow> False proof (prove)
using this:
m p = Some p

goal (1 subgoal):
 1. m \<Turnstile> p \<leadsto> p proof (state)
this:
m \<Turnstile> p \<leadsto> p

goal (1 subgoal):
 1. m p = Some p \<Longrightarrow> False proof (prove)
using this:
m \<Turnstile> p \<leadsto> p

goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p proof (state)
this:
m \<Turnstile> p \<rightarrow> p

goal (1 subgoal):
 1. m p = Some p \<Longrightarrow> False proof (prove)
using this:
m \<Turnstile> p \<rightarrow> p

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!
theory CSpace_AI

lemma untyped_inc:
  "untyped_inc m cs" using valid_mdb by (simp add: valid_mdb_def m_def cs_def)

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

goal (1 subgoal):
 1. untyped_inc m cs
theory CSpace_AI

lemma untyped_mdb:
  "untyped_mdb m cs" using valid_mdb by (simp add: valid_mdb_def m_def cs_def)

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

goal (1 subgoal):
 1. untyped_mdb m cs
theory CSpace_AI

lemma null_no_mdb:
  "cs p = Some cap.NullCap \<Longrightarrow> \<not> m \<Turnstile> p \<rightarrow> p' \<and> \<not> m \<Turnstile> p' \<rightarrow> p" using valid_mdb_no_null [OF valid_mdb] by (simp add: m_def cs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cs p = Some NullCap \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel m)\<^sup>+ \<and> (p', p) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
using this:
caps_of_state s ?p = Some NullCap \<Longrightarrow> (?p, ?p') \<notin> (cdt_parent_rel (cdt s))\<^sup>+ \<and> (?p', ?p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+

goal (1 subgoal):
 1. cs p = Some NullCap \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel m)\<^sup>+ \<and> (p', p) \<notin> (cdt_parent_rel m)\<^sup>+
theory CSpace_AI

lemma the_arch_cap_ArchObjectCap[simp]:
  "the_arch_cap (cap.ArchObjectCap cap) = cap" by (simp add: the_arch_cap_def)

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

lemma cap_master_cap_simps:
  "cap_master_cap (cap.EndpointCap ref bdg rghts)      = cap.EndpointCap ref 0 UNIV"
  "cap_master_cap (cap.NotificationCap ref bdg rghts) = cap.NotificationCap ref 0 UNIV"
  "cap_master_cap (cap.CNodeCap ref bits gd)           = cap.CNodeCap ref bits []"
  "cap_master_cap (cap.ThreadCap ref)                  = cap.ThreadCap ref"
  "cap_master_cap (cap.NullCap)           = cap.NullCap"
  "cap_master_cap (cap.DomainCap)         = cap.DomainCap"
  "cap_master_cap (cap.UntypedCap dev r n f)  = cap.UntypedCap dev r n 0"
  "cap_master_cap (cap.ReplyCap r m rights)      = cap.ReplyCap r True UNIV"
  "cap_master_cap (cap.IRQControlCap)     = cap.IRQControlCap"
  "cap_master_cap (cap.IRQHandlerCap irq) = cap.IRQHandlerCap irq"
  "cap_master_cap (cap.Zombie r a b)      = cap.Zombie r a b"
  "cap_master_cap (ArchObjectCap ac) = ArchObjectCap (cap_master_arch_cap ac)" by (simp_all add: cap_master_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_master_cap (EndpointCap ref bdg rghts) = EndpointCap ref 0 UNIV &&& cap_master_cap (NotificationCap ref bdg rghts) = NotificationCap ref 0 UNIV &&& cap_master_cap (CNodeCap ref bits gd) = CNodeCap ref bits []) &&& cap_master_cap (ThreadCap ref) = ThreadCap ref &&& cap_master_cap NullCap = NullCap &&& cap_master_cap DomainCap = DomainCap) &&& (cap_master_cap (UntypedCap dev r n f) = UntypedCap dev r n 0 &&& cap_master_cap (ReplyCap r m rights) = ReplyCap r True UNIV &&& cap_master_cap IRQControlCap = IRQControlCap) &&& cap_master_cap (IRQHandlerCap irq) = IRQHandlerCap irq &&& cap_master_cap (Zombie r a b) = Zombie r a b &&& cap_master_cap (ArchObjectCap ac) = ArchObjectCap (cap_master_arch_cap ac)
theory CSpace_AI

lemma is_original_cap_set_cap:
  "(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> is_original_cap s' = is_original_cap s" by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
               split: if_split_asm Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (set_cap p c s) \<Longrightarrow> is_original_cap s' = is_original_cap s
theory CSpace_AI

lemma mdb_set_cap:
  "(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> cdt s' = cdt s" by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
               split: if_split_asm Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (set_cap p c s) \<Longrightarrow> cdt s' = cdt s
theory CSpace_AI

lemma master_cap_obj_refs:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> obj_refs c = obj_refs c'" by (clarsimp simp add: cap_master_cap_def
                 intro!: master_arch_cap_obj_refs[THEN arg_cong[where f=set_option]]
                  split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> obj_refs c = obj_refs c'
theory CSpace_AI

lemma master_cap_untyped_range:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> untyped_range c = untyped_range c'" by (simp add: cap_master_cap_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> untyped_range c = untyped_range c'
theory CSpace_AI

lemma master_cap_cap_range:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> cap_range c = cap_range c'" by (simp add: cap_range_def cong: master_cap_untyped_range master_cap_obj_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> cap_range c = cap_range c'
theory CSpace_AI

lemma master_cap_ep:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ep_cap c = is_ep_cap c'" by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ep_cap c = is_ep_cap c'
theory CSpace_AI

lemma master_cap_ntfn:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ntfn_cap c = is_ntfn_cap c'" by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_ntfn_cap c = is_ntfn_cap c'
theory CSpace_AI

lemma cap_master_cap_zombie:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_zombie c = is_zombie c'" by (simp add: cap_master_cap_def is_cap_simps split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> is_zombie c = is_zombie c'
theory CSpace_AI

lemma zobj_refs_def2:
  "zobj_refs c = (case c of Zombie _ _ _ \<Rightarrow> {} | _ \<Rightarrow> obj_refs c)" by (cases c; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zobj_refs c = (case c of Zombie x xa xb \<Rightarrow> {} | _ \<Rightarrow> obj_refs c)
theory CSpace_AI

lemma cap_master_cap_zobj_refs:
  "cap_master_cap c = cap_master_cap c' \<Longrightarrow> zobj_refs c = zobj_refs c'" by (clarsimp simp add: cap_master_cap_def
                 intro!: master_arch_cap_obj_refs[THEN arg_cong[where f=set_option]]
                  split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap c' \<Longrightarrow> zobj_refs c = zobj_refs c'
theory CSpace_AI

lemma caps_of_state_obj_refs:
  "\<lbrakk> caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s \<rbrakk>
  \<Longrightarrow> \<exists>ko. kheap s r = Some ko" apply (subgoal_tac "valid_cap cap s") prefer 2 apply (rule cte_wp_valid_cap) apply (erule caps_of_state_cteD) apply assumption apply (cases cap, auto simp: valid_cap_def obj_at_def
                         dest: obj_ref_is_arch
                         split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko
 2. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) ?p1 s
 2. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s r = Some ko proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma dest_no_parent_trancl [iff]:
  "(m \<Turnstile> dest \<rightarrow> p) = False" using desc by (simp add: descendants_of_def del: split_paired_All)

(* 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 dest_no_parent [iff]:
  "(m \<Turnstile> dest \<leadsto> 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 dest_no_parent_d [iff]:
  "(m p = Some dest) = False" apply clarsimp apply (fold cdt_parent_defs) apply simp done

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

lemma dest_no_child [iff]:
  "(m \<Turnstile> p \<leadsto> dest) = False" using dest by (simp add: cdt_parent_defs)

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

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

lemma dest_no_child_trancl [iff]:
  "(m \<Turnstile> p \<rightarrow> dest) = False" by (clarsimp dest!: tranclD2)

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

lemma descendants_child:
  "descendants_of x (m(dest \<mapsto> src)) =
  (if src \<in> descendants_of x m \<or> x = src
   then descendants_of x m \<union> {dest} else descendants_of x m)" apply (rule descendants_of_insert_child') apply (rule desc) apply (rule neq) apply (rule dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of x (m(dest \<mapsto> src)) = (if src \<in> descendants_of x m \<or> x = src then descendants_of x m \<union> {dest} else descendants_of x m) proof (prove)
goal (3 subgoals):
 1. descendants_of dest m = {}
 2. src \<noteq> dest
 3. m dest = None proof (prove)
goal (2 subgoals):
 1. src \<noteq> dest
 2. m dest = None proof (prove)
goal (1 subgoal):
 1. m dest = None proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_option_empty_inter:
  "(set_option X \<inter> Y = {}) = (\<forall>x. X = Some x \<longrightarrow> x \<notin> Y)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (set_option X \<inter> Y = {}) = (\<forall>x. X = Some x \<longrightarrow> x \<notin> Y)
theory CSpace_AI

lemma dest_no_parent_d_n [iff]:
  "(n p = Some dest) = False" by (simp add: n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n p = Some dest) = False
theory CSpace_AI

lemma dest_no_parent_n [iff]:
  "n \<Turnstile> dest \<leadsto> z = False" by (simp add: cdt_parent_defs)

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

lemma dest_no_parent_n_trancl [iff]:
  "n \<Turnstile> dest \<rightarrow> z = False" by (clarsimp dest!: tranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> dest \<rightarrow> z = False
theory CSpace_AI

lemma n_to_dest [iff]:
  "(n \<Turnstile> p \<leadsto> dest) = (m \<Turnstile> p \<leadsto> src)" by (simp add: n_def cdt_parent_defs)

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

lemma dest_neq_Some [iff]:
  "(m dest = Some p) = False" using dest by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m dest = Some p) = False proof (prove)
using this:
m dest = None

goal (1 subgoal):
 1. (m dest = Some p) = False