kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_D

lemma use_option_form_bind:
  "f x >>= g = (\<lambda>s. monadic_option_dest
       ((monadic_rel_optionation_form f O monadic_rel_optionation_form g) `` {Some (x, s)}))" apply (rule ext) apply (simp add: monadic_rel_optionation_form_def monadic_option_dest_def
                   bind_def split_def) apply (simp add: relcomp_unfold ex_option image_def prod_eq_iff Bex_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x >>= g = (\<lambda>s. monadic_option_dest ((monadic_rel_optionation_form f O monadic_rel_optionation_form g) `` {Some (x, s)})) proof (prove)
goal (1 subgoal):
 1. \<And>s. (f x >>= g) s = monadic_option_dest ((monadic_rel_optionation_form f O monadic_rel_optionation_form g) `` {Some (x, s)}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>fst (f x s). fst (g (fst x) (snd x))) = Some -` ({p. (\<exists>a b. fst p = Some (a, b)) \<and> (\<exists>a b. snd p = Some (a, b)) \<and> the (snd p) \<in> fst (f (fst (the (fst p))) (snd (the (fst p)))) \<or> (\<exists>a b. fst p = Some (a, b)) \<and> snd p = None \<and> snd (f (fst (the (fst p))) (snd (the (fst p)))) \<or> fst p = None \<and> snd p = None} O {p. (\<exists>a b. fst p = Some (a, b)) \<and> (\<exists>a b. snd p = Some (a, b)) \<and> the (snd p) \<in> fst (g (fst (the (fst p))) (snd (the (fst p)))) \<or> (\<exists>a b. fst p = Some (a, b)) \<and> snd p = None \<and> snd (g (fst (the (fst p))) (snd (the (fst p)))) \<or> fst p = None \<and> snd p = None}) `` {Some (x, s)} \<and> ((\<exists>x\<in>fst (f x s). snd (g (fst x) (snd x))) \<or> snd (f x s)) = ((Some (x, s), None) \<in> {p. (\<exists>a b. fst p = Some (a, b)) \<and> (\<exists>a b. snd p = Some (a, b)) \<and> the (snd p) \<in> fst (f (fst (the (fst p))) (snd (the (fst p)))) \<or> (\<exists>a b. fst p = Some (a, b)) \<and> snd p = None \<and> snd (f (fst (the (fst p))) (snd (the (fst p)))) \<or> fst p = None \<and> snd p = None} O {p. (\<exists>a b. fst p = Some (a, b)) \<and> (\<exists>a b. snd p = Some (a, b)) \<and> the (snd p) \<in> fst (g (fst (the (fst p))) (snd (the (fst p)))) \<or> (\<exists>a b. fst p = Some (a, b)) \<and> snd p = None \<and> snd (g (fst (the (fst p))) (snd (the (fst p)))) \<or> fst p = None \<and> snd p = None}) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Union> {y. \<exists>a b. (a, b) \<in> fst (f x s) \<and> y = fst (g a b)} = {y. \<exists>a b. (a, b) \<in> fst (f x s) \<and> y \<in> fst (g a b)} proof (prove)
goal:
No subgoals!
theory System_S

lemma all_rights_def2:
  "all_rights = {Read, Write, Take, Grant, Create, Store}" apply (clarsimp simp: all_rights_def, rule, simp_all, rule, simp) apply (metis right.exhaust) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_rights = {Read, Write, Take, Grant, Create, Store} proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Read \<or> x = Write \<or> x = Take \<or> x = Grant \<or> x = Create \<or> x = Store proof (prove)
goal:
No subgoals!
theory System_S

lemma caps_rel:
  "caps_of s e = \<Union>(direct_caps_of s ` store_connected s `` {e})" by (simp add: caps_of_def Image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s e = \<Union> (direct_caps_of s ` store_connected s `` {e})
theory System_S

lemma createOperation_def2:
  "createOperation e c\<^sub>1 c\<^sub>2 s \<equiv>
  let new_cap = \<lparr> target = target c\<^sub>2, rights = all_rights \<rparr>;
      newTarget = ({new_cap} \<union> direct_caps_of s (target c\<^sub>1) )
  in
  s (target c\<^sub>1 \<mapsto> Entity newTarget, target c\<^sub>2 \<mapsto> null_entity)" by (simp add: createOperation_def Let_def full_cap_def null_entity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. createOperation e c\<^sub>1 c\<^sub>2 s \<equiv> let new_cap = \<lparr>target = target c\<^sub>2, rights = all_rights\<rparr>; newTarget = {new_cap} \<union> direct_caps_of s (target c\<^sub>1) in s(target c\<^sub>1 \<mapsto> Entity newTarget, target c\<^sub>2 \<mapsto> null_entity)
theory System_S

lemma grantOperation_def2:
  "grantOperation e c\<^sub>1 c\<^sub>2 R s \<equiv>
  s (target c\<^sub>1 \<mapsto> Entity ( {diminish R c\<^sub>2} \<union> direct_caps_of s (target c\<^sub>1)))" by (clarsimp simp: grantOperation_def caps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. grantOperation e c\<^sub>1 c\<^sub>2 R s \<equiv> s(target c\<^sub>1 \<mapsto> Entity ({diminish R c\<^sub>2} \<union> direct_caps_of s (target c\<^sub>1)))
theory System_S

lemma removeOperation_simpler:
  "removeOperation e c\<^sub>1 c\<^sub>2 s \<equiv>
  (case s (target c\<^sub>1) of
    None \<Rightarrow> s
  | Some (Entity caps) \<Rightarrow> s (target c\<^sub>1 \<mapsto> Entity (caps - {c\<^sub>2})))" by (rule eq_reflection, simp add: removeOperation_def is_entity_def direct_caps_of_def
                             split: if_split_asm option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. removeOperation e c\<^sub>1 c\<^sub>2 s \<equiv> case s (target c\<^sub>1) of None \<Rightarrow> s | Some (Entity caps) \<Rightarrow> s(target c\<^sub>1 \<mapsto> Entity (caps - {c\<^sub>2}))
theory System_S

lemma removeSetOperation_simpler:
  "removeSetOperation e c caps s \<equiv>
  (case s (target c) of
    None \<Rightarrow> s
  | Some (Entity caps') \<Rightarrow> s (target c \<mapsto> Entity (caps' - caps)))" by (auto simp: removeSetOperation_def is_entity_def direct_caps_of_def
         intro!: eq_reflection
          split: if_split_asm option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. removeSetOperation e c caps s \<equiv> case s (target c) of None \<Rightarrow> s | Some (Entity caps') \<Rightarrow> s(target c \<mapsto> Entity (caps' - caps))
theory System_S

lemma removeSetOperation_fold_removeOperation:
  "removeSetOperation e c (set caps) s = fold (removeOperation e c) caps s" apply (subst foldr_fold [symmetric]) apply (fastforce simp: removeOperation_def direct_caps_of_def is_entity_def) apply (rule sym) apply (induct caps) apply (fastforce simp: removeSetOperation_def removeOperation_def direct_caps_of_def is_entity_def) apply (fastforce simp: removeSetOperation_def removeOperation_def direct_caps_of_def is_entity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. removeSetOperation e c (set caps) s = fold (removeOperation e c) caps s proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set caps; y \<in> set caps\<rbrakk> \<Longrightarrow> removeOperation e c y \<circ> removeOperation e c x = removeOperation e c x \<circ> removeOperation e c y
 2. removeSetOperation e c (set caps) s = foldr (removeOperation e c) caps s proof (prove)
goal (1 subgoal):
 1. removeSetOperation e c (set caps) s = foldr (removeOperation e c) caps s proof (prove)
goal (1 subgoal):
 1. foldr (removeOperation e c) caps s = removeSetOperation e c (set caps) s proof (prove)
goal (2 subgoals):
 1. foldr (removeOperation e c) [] s = removeSetOperation e c (set []) s
 2. \<And>a caps. foldr (removeOperation e c) caps s = removeSetOperation e c (set caps) s \<Longrightarrow> foldr (removeOperation e c) (a # caps) s = removeSetOperation e c (set (a # caps)) s proof (prove)
goal (1 subgoal):
 1. \<And>a caps. foldr (removeOperation e c) caps s = removeSetOperation e c (set caps) s \<Longrightarrow> foldr (removeOperation e c) (a # caps) s = removeSetOperation e c (set (a # caps)) s proof (prove)
goal:
No subgoals!
theory System_S

lemma is_entity_dom: "is_entity s e = (e \<in> dom s)" by (simp add: is_entity_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s e = (e \<in> dom s)
theory System_S

lemma is_entity_imp_not_None:
  "is_entity s e \<Longrightarrow> s e \<noteq> None" by (simp add: is_entity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s e \<Longrightarrow> s e \<noteq> None
theory System_S

lemma store_connected_refl [simp]:
  "(e, e) \<in> store_connected s" by (simp add: store_connected_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (e, e) \<in> store_connected s
theory System_S

lemma no_caps_of_imp_not_connected [rule_format]:
  "\<lbrakk>(e, x) \<in> store_connected s\<rbrakk>
  \<Longrightarrow> direct_caps_of s e = {} \<longrightarrow> x = e" apply (unfold store_connected_def) apply (erule rtrancl.induct) apply simp apply (clarsimp simp: store_connected_direct_def direct_caps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (e, x) \<in> store_connected s \<Longrightarrow> direct_caps_of s e = {} \<longrightarrow> x = e proof (prove)
goal (1 subgoal):
 1. (e, x) \<in> (store_connected_direct s)\<^sup>* \<Longrightarrow> direct_caps_of s e = {} \<longrightarrow> x = e proof (prove)
goal (2 subgoals):
 1. \<And>a. direct_caps_of s a = {} \<longrightarrow> a = a
 2. \<And>a b c. \<lbrakk>(a, b) \<in> (store_connected_direct s)\<^sup>*; direct_caps_of s a = {} \<longrightarrow> b = a; (b, c) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> direct_caps_of s a = {} \<longrightarrow> c = a proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> (store_connected_direct s)\<^sup>*; direct_caps_of s a = {} \<longrightarrow> b = a; (b, c) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> direct_caps_of s a = {} \<longrightarrow> c = a proof (prove)
goal:
No subgoals!
theory System_S

lemma no_direct_caps_of_no_caps_of:
  "(direct_caps_of s e = {}) = (caps_of s e = {})" apply (rule iffI) apply (clarsimp simp add: caps_of_def) apply (drule (1) no_caps_of_imp_not_connected) apply simp apply (clarsimp simp add: caps_of_def store_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (direct_caps_of s e = {}) = (caps_of s e = {}) proof (prove)
goal (2 subgoals):
 1. direct_caps_of s e = {} \<Longrightarrow> caps_of s e = {}
 2. caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>direct_caps_of s e = {}; (e, x) \<in> store_connected s\<rbrakk> \<Longrightarrow> direct_caps_of s x = {}
 2. caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>direct_caps_of s e = {}; x = e\<rbrakk> \<Longrightarrow> direct_caps_of s x = {}
 2. caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {} proof (prove)
goal (1 subgoal):
 1. caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {} proof (prove)
goal:
No subgoals!
theory System_S

lemma no_direct_caps_of_imp_no_caps_of:
  "direct_caps_of s e = {} \<Longrightarrow> caps_of s e = {}" by (rule no_direct_caps_of_no_caps_of [THEN iffD1])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s e = {} \<Longrightarrow> caps_of s e = {}
theory System_S

lemma no_caps_of_imp_no_direct_caps_of:
  "caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {}" by (rule no_direct_caps_of_no_caps_of [THEN iffD2])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s e = {} \<Longrightarrow> direct_caps_of s e = {}
theory System_S

lemma store_connected_direct_in_store_connected:
  "(x, y) \<in> store_connected_direct s \<Longrightarrow> (x, y) \<in> store_connected s" by (simp add: store_connected_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected_direct s \<Longrightarrow> (x, y) \<in> store_connected s
theory System_S

lemma no_diminish [simp]:
  "diminish all_rights c = c" by (simp add: diminish_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish all_rights c = c
theory System_S

lemma no_diminish_image [simp]:
  "diminish all_rights ` C = C" by (fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish all_rights ` C = C
theory System_S

lemma diminish_diminish [simp]:
  "diminish dimR2 (diminish dimR1 sc) = diminish (dimR1 \<inter> dimR2) sc" by (clarsimp simp add: diminish_def Int_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish dimR2 (diminish dimR1 sc) = diminish (dimR1 \<inter> dimR2) sc
theory System_S

lemma diminish_range_diminish [simp]:
  "diminish dimR2 ` diminish dimR1 ` ssc = diminish (dimR1 \<inter> dimR2) ` ssc" apply (rule set_eqI) apply (rule iffI) apply (clarsimp) apply (clarsimp simp del: diminish_diminish simp add: diminish_diminish [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish dimR2 ` diminish dimR1 ` ssc = diminish (dimR1 \<inter> dimR2) ` ssc proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> diminish dimR2 ` diminish dimR1 ` ssc) = (x \<in> diminish (dimR1 \<inter> dimR2) ` ssc) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> diminish dimR2 ` diminish dimR1 ` ssc \<Longrightarrow> x \<in> diminish (dimR1 \<inter> dimR2) ` ssc
 2. \<And>x. x \<in> diminish (dimR1 \<inter> dimR2) ` ssc \<Longrightarrow> x \<in> diminish dimR2 ` diminish dimR1 ` ssc proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> diminish (dimR1 \<inter> dimR2) ` ssc \<Longrightarrow> x \<in> diminish dimR2 ` diminish dimR1 ` ssc proof (prove)
goal:
No subgoals!
theory System_S

lemma execute_not_empty:
  "execute ops s \<noteq> {}" apply (induct ops) apply (simp) apply (simp add: step_def del: if_image_distrib, fast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. execute ops s \<noteq> {} proof (prove)
goal (2 subgoals):
 1. execute [] s \<noteq> {}
 2. \<And>a ops. execute ops s \<noteq> {} \<Longrightarrow> execute (a # ops) s \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>a ops. execute ops s \<noteq> {} \<Longrightarrow> execute (a # ops) s \<noteq> {} proof (prove)
goal:
No subgoals!
theory System_S

lemma execute_append [intro]:
  "\<And> s s' s'' opsA. \<lbrakk> s'' \<in> execute opsA s; s' \<in> execute opsB s'' \<rbrakk> \<Longrightarrow> s' \<in> execute (opsB @ opsA) s" apply (induct opsB) apply (simp) apply (atomize) apply (clarsimp) apply (rule bexI) apply (assumption) by (drule spec | drule(1) mp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'' opsA. \<lbrakk>s'' \<in> execute opsA s; s' \<in> execute opsB s''\<rbrakk> \<Longrightarrow> s' \<in> execute (opsB @ opsA) s proof (prove)
goal (2 subgoals):
 1. \<And>s s' s'' opsA. \<lbrakk>s'' \<in> execute opsA s; s' \<in> execute [] s''\<rbrakk> \<Longrightarrow> s' \<in> execute ([] @ opsA) s
 2. \<And>a opsB s s' s'' opsA. \<lbrakk>\<And>s s' s'' opsA. \<lbrakk>s'' \<in> execute opsA s; s' \<in> execute opsB s''\<rbrakk> \<Longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; s' \<in> execute (a # opsB) s''\<rbrakk> \<Longrightarrow> s' \<in> execute ((a # opsB) @ opsA) s proof (prove)
goal (1 subgoal):
 1. \<And>a opsB s s' s'' opsA. \<lbrakk>\<And>s s' s'' opsA. \<lbrakk>s'' \<in> execute opsA s; s' \<in> execute opsB s''\<rbrakk> \<Longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; s' \<in> execute (a # opsB) s''\<rbrakk> \<Longrightarrow> s' \<in> execute ((a # opsB) @ opsA) s proof (prove)
goal (1 subgoal):
 1. \<And>a opsB s s' s'' opsA. \<lbrakk>\<forall>s s' s'' opsA. s'' \<in> execute opsA s \<longrightarrow> s' \<in> execute opsB s'' \<longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; s' \<in> execute (a # opsB) s''\<rbrakk> \<Longrightarrow> s' \<in> execute ((a # opsB) @ opsA) s proof (prove)
goal (1 subgoal):
 1. \<And>a opsB s s' s'' opsA x. \<lbrakk>\<forall>s s' s'' opsA. s'' \<in> execute opsA s \<longrightarrow> s' \<in> execute opsB s'' \<longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; x \<in> execute opsB s''; s' \<in> step a x\<rbrakk> \<Longrightarrow> \<exists>x\<in>execute (opsB @ opsA) s. s' \<in> step a x proof (prove)
goal (2 subgoals):
 1. \<And>a opsB s s' s'' opsA x. \<lbrakk>\<forall>s s' s'' opsA. s'' \<in> execute opsA s \<longrightarrow> s' \<in> execute opsB s'' \<longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; x \<in> execute opsB s''; s' \<in> step a x\<rbrakk> \<Longrightarrow> s' \<in> step a (?x9 a opsB s s' s'' opsA x)
 2. \<And>a opsB s s' s'' opsA x. \<lbrakk>\<forall>s s' s'' opsA. s'' \<in> execute opsA s \<longrightarrow> s' \<in> execute opsB s'' \<longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; x \<in> execute opsB s''; s' \<in> step a x\<rbrakk> \<Longrightarrow> ?x9 a opsB s s' s'' opsA x \<in> execute (opsB @ opsA) s proof (prove)
goal (1 subgoal):
 1. \<And>a opsB s s' s'' opsA x. \<lbrakk>\<forall>s s' s'' opsA. s'' \<in> execute opsA s \<longrightarrow> s' \<in> execute opsB s'' \<longrightarrow> s' \<in> execute (opsB @ opsA) s; s'' \<in> execute opsA s; x \<in> execute opsB s''; s' \<in> step a x\<rbrakk> \<Longrightarrow> x \<in> execute (opsB @ opsA) s
theory System_S

lemma heapAdd_read_cap [simp]:
  "target (read_cap e) = e" by (simp add: read_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (read_cap e) = e
theory System_S

lemma heapAdd_write_cap [simp]:
  "target (write_cap e) = e" by (simp add: write_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (write_cap e) = e
theory System_S

lemma rights_write_cap [simp]:
  "rights (write_cap e) = {Write}" by (simp add: write_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (write_cap e) = {Write}
theory System_S

lemma heapAdd_take_cap [simp]:
  "target (take_cap e) = e" by (simp add: take_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (take_cap e) = e
theory System_S

lemma rights_take_cap [simp]:
  "rights (take_cap e) = {Take}" by (simp add: take_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (take_cap e) = {Take}
theory System_S

lemma heapAdd_grant_cap [simp]:
  "target (grant_cap e) = e" by (simp add: grant_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (grant_cap e) = e
theory System_S

lemma rights_grant_cap [simp]:
  "rights (grant_cap e) = {Grant}" by (simp add: grant_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (grant_cap e) = {Grant}
theory System_S

lemma rights_create_cap [simp]:
  "rights (create_cap e) = {Create}" by (simp add: create_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (create_cap e) = {Create}
theory System_S

lemma heapAdd_store_cap [simp]:
  "target (store_cap e) = e" by (simp add: store_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (store_cap e) = e
theory System_S

lemma heapAdd_full_cap [simp]:
  "target (full_cap e) = e" by (simp add: full_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (full_cap e) = e
theory System_S

lemma rights_full_cap [simp]:
  "rights (full_cap e) = all_rights" by (simp add: full_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (full_cap e) = all_rights
theory System_S

lemma entity_diminish [simp]:
  "target (diminish R c) = target c" by (simp add: diminish_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (diminish R c) = target c
theory System_S

lemma rights_diminish [simp]:
  "rights (diminish R c) = rights c \<inter> R" by (simp add: diminish_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (diminish R c) = rights c \<inter> R
theory System_S

lemma caps_of_imp_some_direct_cap:
  "c \<in> caps_of s e \<Longrightarrow> \<exists>e'. c \<in> direct_caps_of s e'" by (auto simp: caps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> caps_of s e \<Longrightarrow> \<exists>e'. c \<in> direct_caps_of s e'
theory System_S

lemma caps_of_imp_some_store_connected_direct_cap:
  "c \<in> caps_of s e \<Longrightarrow> \<exists>e'. (e, e') \<in> store_connected s \<and> c \<in> direct_caps_of s e'" by (auto simp: caps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> caps_of s e \<Longrightarrow> \<exists>e'. (e, e') \<in> store_connected s \<and> c \<in> direct_caps_of s e'
theory System_S

lemma direct_cap_in_cap:
  "c \<in> direct_caps_of s e \<Longrightarrow> c \<in> caps_of s e" by (auto simp: caps_of_def store_connected_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> direct_caps_of s e \<Longrightarrow> c \<in> caps_of s e
theory System_S

lemma all_caps_ofE [elim!]:
  "\<lbrakk> c \<in> all_caps_of s; \<And>e'. c \<in> direct_caps_of s e' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (fastforce simp add: all_caps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> all_caps_of s; \<And>e'. c \<in> direct_caps_of s e' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory System_S

lemma entity_not_not_entity:
  "\<lbrakk>is_entity s e\<^sub>1; \<not> is_entity s e\<^sub>2\<rbrakk> \<Longrightarrow> e\<^sub>1 \<noteq> e\<^sub>2" by (auto simp: is_entity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s e\<^sub>1; \<not> is_entity s e\<^sub>2\<rbrakk> \<Longrightarrow> e\<^sub>1 \<noteq> e\<^sub>2
theory System_S

lemma no_direct_caps_of_in_nonEntity:
  "\<not> is_entity s e \<Longrightarrow> direct_caps_of s e = {}" by (auto simp: direct_caps_of_def is_entity_def split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s e \<Longrightarrow> direct_caps_of s e = {}
theory System_S

lemma not_is_entity_imp_no_direct_caps_of:
  "\<not> is_entity s e \<Longrightarrow> caps_of s e = {}" by (drule no_direct_caps_of_in_nonEntity, erule no_direct_caps_of_imp_no_caps_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s e \<Longrightarrow> caps_of s e = {}
theory System_S

lemma direct_caps_of_imp_is_entity:
  "c \<in> direct_caps_of s e \<Longrightarrow> is_entity s e" by (auto intro: classical dest: no_direct_caps_of_in_nonEntity)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> direct_caps_of s e \<Longrightarrow> is_entity s e
theory System_S

lemma caps_of_imp_is_entity:
  "c \<in> caps_of s e \<Longrightarrow> is_entity s e" by (auto intro: classical dest: not_is_entity_imp_no_direct_caps_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> caps_of s e \<Longrightarrow> is_entity s e
theory System_S

lemma store_caps_of_store_connected_direct:
  "\<lbrakk>c \<in> direct_caps_of s e; Store \<in> rights c\<rbrakk>
  \<Longrightarrow> (e, target c) \<in> store_connected_direct s" by (fastforce simp: store_connected_direct_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> direct_caps_of s e; Store \<in> rights c\<rbrakk> \<Longrightarrow> (e, target c) \<in> store_connected_direct s
theory System_S

lemma store_caps_store_connected:
  "\<lbrakk>c \<in> caps_of s e; Store \<in> rights c\<rbrakk> \<Longrightarrow> (e, target c) \<in> store_connected s" apply (clarsimp simp: store_connected_def caps_of_def) by (frule (1) store_caps_of_store_connected_direct, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e; Store \<in> rights c\<rbrakk> \<Longrightarrow> (e, target c) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Store \<in> rights c; (e, x) \<in> (store_connected_direct s)\<^sup>*; c \<in> direct_caps_of s x\<rbrakk> \<Longrightarrow> (e, target c) \<in> (store_connected_direct s)\<^sup>*
theory Confine_S

lemma extra_rights_idem [simp]:
  "(extra_rights (extra_rights c)) = (extra_rights c)" apply (clarsimp simp add: extra_rights_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (extra_rights c) = extra_rights c proof (prove)
goal:
No subgoals!
theory Confine_S

lemma extra_rights_image_idem [simp]:
  "(extra_rights ` (extra_rights ` S)) = (extra_rights ` S)" by (rule set_eqI) (simp add: image_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights ` extra_rights ` S = extra_rights ` S
theory Confine_S

lemma extra_rights_empty_rights_ident [simp]:
   "extra_rights \<lparr> target = e, rights = {} \<rparr> = \<lparr> target = e, rights = {} \<rparr>" by (simp add: extra_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights \<lparr>target = e, rights = {}\<rparr> = \<lparr>target = e, rights = {}\<rparr>