kings-crown/FVELER_Isabelle huggingface dataset:
theory Confine_S

lemma shares_caps_remove:
  "shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y
  \<Longrightarrow> shares_caps s x y" apply (clarsimp simp: shares_caps_def removeOperation_simpler
                 split:option.splits) apply (frule (1) store_connected_remove [where x=x], clarsimp) apply (drule (1) store_connected_remove [where x=y], clarsimp) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y \<Longrightarrow> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c\<^sub>1) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xa - {c\<^sub>2}))); (y, e\<^sub>i) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xa - {c\<^sub>2})))\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c\<^sub>1) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xa - {c\<^sub>2}))); (y, e\<^sub>i) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xa - {c\<^sub>2}))); (x, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c\<^sub>1) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xa - {c\<^sub>2}))); (x, e\<^sub>i) \<in> store_connected s; (y, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s
theory Confine_S

lemma direct_caps_of_removeSet:
  "c' \<in> direct_caps_of (removeSetOperation e c C s) x \<Longrightarrow>
  c' \<in> direct_caps_of s x" by (clarsimp simp: removeSetOperation_simpler direct_caps_of_def
              split: option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c' \<in> direct_caps_of (removeSetOperation e c C s) x \<Longrightarrow> c' \<in> direct_caps_of s x
theory Confine_S

lemma caps_of_removeSet:
  "c' \<in> caps_of (removeSetOperation e c C s) x \<Longrightarrow>
  c' \<in> caps_of s x" apply (clarsimp simp: caps_of_def) apply (rule_tac x=xa in exI) apply (drule direct_caps_of_removeSet) apply (simp add: removeSetOperation_simpler split: option.splits) apply (erule (1) store_connected_remove) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c' \<in> caps_of (removeSetOperation e c C s) x \<Longrightarrow> c' \<in> caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeSetOperation e c C s); c' \<in> direct_caps_of (removeSetOperation e c C s) xa\<rbrakk> \<Longrightarrow> \<exists>xa. (x, xa) \<in> store_connected s \<and> c' \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeSetOperation e c C s); c' \<in> direct_caps_of (removeSetOperation e c C s) xa\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s \<and> c' \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeSetOperation e c C s); c' \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s \<and> c' \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa x2 xaa. \<lbrakk>c' \<in> direct_caps_of s xa; s (target c) = Some (Entity xaa); x2 = Entity xaa; (x, xa) \<in> store_connected (s(target c \<mapsto> Entity (xaa - C)))\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>x x2 xa. \<lbrakk>c' \<in> direct_caps_of s x; s (target c) = Some (Entity xa); x2 = Entity xa\<rbrakk> \<Longrightarrow> xa - C \<subseteq> xa proof (prove)
goal:
No subgoals!
theory Confine_S

lemma shares_caps_removeSet:
  "shares_caps (removeSetOperation e c C s) x y
  \<Longrightarrow> shares_caps s x y" apply (clarsimp simp: shares_caps_def removeSetOperation_simpler split:option.splits) apply (frule (1) store_connected_remove [where x=x], clarsimp) apply (drule (1) store_connected_remove [where x=y], clarsimp) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shares_caps (removeSetOperation e c C s) x y \<Longrightarrow> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c \<mapsto> Entity (xa - C))); (y, e\<^sub>i) \<in> store_connected (s(target c \<mapsto> Entity (xa - C)))\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c \<mapsto> Entity (xa - C))); (y, e\<^sub>i) \<in> store_connected (s(target c \<mapsto> Entity (xa - C))); (x, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>xa e\<^sub>i. \<lbrakk>s (target c) = Some (Entity xa); (x, e\<^sub>i) \<in> store_connected (s(target c \<mapsto> Entity (xa - C))); (x, e\<^sub>i) \<in> store_connected s; (y, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s
theory Confine_S

lemma removeSet_conTrans:
  "\<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = (SysRemoveSet n c C)\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y" by(auto dest!: removeSet_connected)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysRemoveSet n c C\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y
theory Confine_S

lemma direct_caps_of_removeSetOfCaps:
  "c' \<in> direct_caps_of (removeSetOfCaps cap_map s) x \<Longrightarrow>
  c' \<in> direct_caps_of s x" by (clarsimp simp: removeSetOfCaps_def direct_caps_of_def
              split: option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c' \<in> direct_caps_of (removeSetOfCaps cap_map s) x \<Longrightarrow> c' \<in> direct_caps_of s x
theory Confine_S

lemma caps_of_revoke:
  "\<lbrakk>s' \<in> revokeOperation sub c\<^sub>1 s ;  c \<in> caps_of s' e \<rbrakk>
  \<Longrightarrow> c \<in> caps_of s e" apply (clarsimp simp: revokeOperation_def
                 split: if_split_asm) apply (drule (1) caps_of_removeSetOfCaps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> revokeOperation sub c\<^sub>1 s; c \<in> caps_of s' e\<rbrakk> \<Longrightarrow> c \<in> caps_of s e proof (prove)
goal (1 subgoal):
 1. \<And>cap_map. \<lbrakk>c \<in> caps_of (removeSetOfCaps cap_map s) e; \<forall>e'. cap_map e' \<subseteq> caps_to_entity (target c\<^sub>1) e' s; s' = removeSetOfCaps cap_map s\<rbrakk> \<Longrightarrow> c \<in> caps_of s e proof (prove)
goal:
No subgoals!
theory Confine_S

lemma direct_caps_of_revoke:
  "\<lbrakk>s' \<in> revokeOperation e c s; c' \<in> direct_caps_of s' x\<rbrakk>
   \<Longrightarrow> c' \<in> direct_caps_of s x" apply (clarsimp simp: revokeOperation_def
                 split: if_split_asm) apply (drule (1) direct_caps_of_removeSetOfCaps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> revokeOperation e c s; c' \<in> direct_caps_of s' x\<rbrakk> \<Longrightarrow> c' \<in> direct_caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>cap_map. \<lbrakk>c' \<in> direct_caps_of (removeSetOfCaps cap_map s) x; \<forall>e'. cap_map e' \<subseteq> caps_to_entity (target c) e' s; s' = removeSetOfCaps cap_map s\<rbrakk> \<Longrightarrow> c' \<in> direct_caps_of s x proof (prove)
goal:
No subgoals!
theory Confine_S

lemma store_connected_revoke:
 "\<lbrakk>(x, y) \<in> store_connected s'; s' \<in> revokeOperation e c s\<rbrakk>
  \<Longrightarrow> (x, y) \<in> store_connected s" apply (simp add: store_connected_def) apply (erule rtrancl_induct) apply simp apply (fold store_connected_def) apply (subgoal_tac "(y,z) \<in> store_connected_direct s") apply (fastforce simp: store_connected_def) apply (clarsimp simp: store_connected_direct_def) apply (metis direct_caps_of_revoke) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> store_connected s'; s' \<in> revokeOperation e c s\<rbrakk> \<Longrightarrow> (x, y) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> (store_connected_direct s')\<^sup>*; s' \<in> revokeOperation e c s\<rbrakk> \<Longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. s' \<in> revokeOperation e c s \<Longrightarrow> (x, x) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> (store_connected_direct s')\<^sup>*; (y, z) \<in> store_connected_direct s'; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> (store_connected_direct s')\<^sup>*; (y, z) \<in> store_connected_direct s'; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> store_connected s'; (y, z) \<in> store_connected_direct s'; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> store_connected s'; (y, z) \<in> store_connected_direct s'; (x, y) \<in> store_connected s; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s
 2. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> store_connected s'; (y, z) \<in> store_connected_direct s'; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> store_connected s'; (y, z) \<in> store_connected_direct s'; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y cap. \<lbrakk>s' \<in> revokeOperation e c s; (x, y) \<in> store_connected s'; (x, y) \<in> store_connected s; cap \<in> direct_caps_of s' y; Store \<in> rights cap\<rbrakk> \<Longrightarrow> \<exists>capa. capa \<in> direct_caps_of s y \<and> Store \<in> rights capa \<and> target capa = target cap proof (prove)
goal:
No subgoals!
theory Confine_S

lemma shares_caps_revoke:
  "\<lbrakk>shares_caps s' x y; s' \<in> revokeOperation e c s\<rbrakk>
  \<Longrightarrow> shares_caps s x y" apply (clarsimp simp: shares_caps_def) apply (frule (1) store_connected_revoke [where x=x]) apply (drule (1) store_connected_revoke [where x=y]) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>shares_caps s' x y; s' \<in> revokeOperation e c s\<rbrakk> \<Longrightarrow> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> revokeOperation e c s; (x, e\<^sub>i) \<in> store_connected s'; (y, e\<^sub>i) \<in> store_connected s'\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> revokeOperation e c s; (x, e\<^sub>i) \<in> store_connected s'; (y, e\<^sub>i) \<in> store_connected s'; (x, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> revokeOperation e c s; (x, e\<^sub>i) \<in> store_connected s'; (x, e\<^sub>i) \<in> store_connected s; (y, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s
theory Confine_S

lemma removeOperation_entity_ids [simp]:
  "is_entity (removeOperation e c c' s) e' = is_entity s e'" by (simp add: is_entity_def removeOperation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity (removeOperation e c c' s) e' = is_entity s e'
theory Confine_S

lemma removeSetOfCaps_entity_ids [simp]:
  "is_entity (removeSetOfCaps cap_map s) e' = is_entity s e'" by (simp add: is_entity_def removeSetOfCaps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity (removeSetOfCaps cap_map s) e' = is_entity s e'
theory Confine_S

lemma revoke_entities:
  "s' \<in> revokeOperation sub c\<^sub>1 s \<Longrightarrow> is_entity s' e = is_entity s e" by (clarsimp simp: revokeOperation_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<in> revokeOperation sub c\<^sub>1 s \<Longrightarrow> is_entity s' e = is_entity s e
theory Confine_S

lemma revoke_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysRevoke n c\<^sub>1)\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s" by(auto dest!: revoke_directly_tgs_connected)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysRevoke n c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y
theory Confine_S

lemma is_entity_destroy:
  "is_entity (destroyOperation e' c s) e \<Longrightarrow> is_entity s e" by (simp add: destroyOperation_def is_entity_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity (destroyOperation e' c s) e \<Longrightarrow> is_entity s e
theory Confine_S

lemma leakImplyConnected:
  "leak s\<^sub>i e\<^sub>x e\<^sub>i \<Longrightarrow> (e\<^sub>x, e\<^sub>i) \<in> directly_tgs_connected s\<^sub>i" by(simp add: directly_tgs_connected_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s\<^sub>i \<turnstile> e\<^sub>x \<rightarrow> e\<^sub>i \<Longrightarrow> s\<^sub>i \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>i
theory Confine_S

lemma leakImplyConnectedTrans:
  "leak s\<^sub>i e\<^sub>x e\<^sub>i \<Longrightarrow> (e\<^sub>x, e\<^sub>i) \<in> tgs_connected s\<^sub>i" by(simp add: tgs_connected_def, frule leakImplyConnected, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s\<^sub>i \<turnstile> e\<^sub>x \<rightarrow> e\<^sub>i \<Longrightarrow> s\<^sub>i \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i
theory Confine_S

lemma tgs_connected_preserved [rule_format]:
  "\<forall>s'. s' \<in> execute cmds s \<longrightarrow>
    s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow>
    s \<turnstile> x \<leftrightarrow>* y" apply(induct_tac cmds, simp) apply clarsimp apply(rename_tac cmd cmds s'' s') apply(erule_tac x=s' in allE) apply(simp add: tgs_connected_preserved_step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. s' \<in> execute cmds s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<forall>s'. s' \<in> execute list s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y \<Longrightarrow> \<forall>s'. s' \<in> execute (a # list) s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>a list s' xa. \<lbrakk>\<forall>s'. s' \<in> execute list s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y; xa \<in> execute list s; s' \<in> step a xa; s' \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>cmd cmds s'' s'. \<lbrakk>\<forall>s'. s' \<in> execute cmds s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y; s' \<in> execute cmds s; s'' \<in> step cmd s'; s'' \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>cmd cmds s'' s'. \<lbrakk>s' \<in> execute cmds s; s'' \<in> step cmd s'; s'' \<turnstile> x \<leftrightarrow>* y; s' \<in> execute cmds s \<longrightarrow> s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow> s \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

lemma leak_conTrans [rule_format]:
  "\<lbrakk>s \<in> execute cmds s\<^sub>0; leak s x y\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s\<^sub>0" by (auto intro: leakImplyConnectedTrans tgs_connected_preserved)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> execute cmds s\<^sub>0; s \<turnstile> x \<rightarrow> y\<rbrakk> \<Longrightarrow> s\<^sub>0 \<turnstile> x \<leftrightarrow>* y
theory Confine_S

lemma leakage_rule:
  "\<lbrakk>s' \<in> execute cmds s; \<not> s \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> \<not> (s' \<turnstile> x \<rightarrow> y)" by(auto simp add: leak_conTrans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; \<not> s \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> \<not> s' \<turnstile> x \<rightarrow> y
theory Confine_S

lemma authority_confinement_induct_step:
  "\<lbrakk>s' \<in> step cmd s;
    \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk>
  \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c" apply (clarsimp simp: caps_dominated_by_def) apply (drule (1) caps_of_op) apply (fastforce simp: cap_in_caps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk> \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>cap' x. \<lbrakk>s' \<in> step cmd s; \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> (\<forall>cap'\<in>caps_of s e\<^sub>i. target cap' = target c \<longrightarrow> rights (extra_rights cap') \<subseteq> rights (extra_rights c)); cap' \<in> caps_of s' e\<^sub>x; target cap' = target c; x \<in> rights (extra_rights cap')\<rbrakk> \<Longrightarrow> x \<in> rights (extra_rights c) proof (prove)
goal (1 subgoal):
 1. \<And>cap' x. \<lbrakk>\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> (\<forall>cap'\<in>caps_of s e\<^sub>i. target cap' = target c \<longrightarrow> rights (extra_rights cap') \<subseteq> rights (extra_rights c)); cap' \<in> caps_of s' e\<^sub>x; target cap' = target c; x \<in> rights (extra_rights cap'); \<exists>z. s \<turnstile> e\<^sub>x \<leftrightarrow>* z \<and> cap' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> x \<in> rights (extra_rights c) proof (prove)
goal:
No subgoals!
theory Confine_S

lemma authority_confinement:
  "\<lbrakk>s' \<in> execute cmds s;
    \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk>
  \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c" by (erule authority_confinement_helper [rule_format, where e\<^sub>x=e\<^sub>x], simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk> \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c
theory Islands_S

lemma island_caps_def2:
  "island_caps s x \<equiv> \<Union> e \<in> island s x. caps_of s e" by(simp add: island_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. island_caps s x \<equiv> \<Union> (caps_of s ` island s x)
theory Islands_S

lemma island_caps_def3:
  "island_caps s x =  \<Union>(direct_caps_of s ` island s x)" apply (clarsimp simp: island_caps_def) apply rule apply (clarsimp simp: island_def caps_of_def) apply (drule store_connected_directly_tgs_connected) apply (metis directly_tgs_connected_rtrancl_into_rtrancl) apply (fastforce simp: caps_of_def store_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. island_caps s x = \<Union> (direct_caps_of s ` island s x) proof (prove)
goal (1 subgoal):
 1. \<Union> (caps_of s ` island s x) = \<Union> (direct_caps_of s ` island s x) proof (prove)
goal (2 subgoals):
 1. \<Union> (caps_of s ` island s x) \<subseteq> \<Union> (direct_caps_of s ` island s x)
 2. \<Union> (direct_caps_of s ` island s x) \<subseteq> \<Union> (caps_of s ` island s x) proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa xb. \<lbrakk>xa \<in> direct_caps_of s xb; s \<turnstile> x \<leftrightarrow>* xaa; (xaa, xb) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>xb. s \<turnstile> x \<leftrightarrow>* xb \<and> xa \<in> direct_caps_of s xb
 2. \<Union> (direct_caps_of s ` island s x) \<subseteq> \<Union> (caps_of s ` island s x) proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa xb. \<lbrakk>xa \<in> direct_caps_of s xb; s \<turnstile> x \<leftrightarrow>* xaa; s \<turnstile> xaa \<leftrightarrow> xb\<rbrakk> \<Longrightarrow> \<exists>xb. s \<turnstile> x \<leftrightarrow>* xb \<and> xa \<in> direct_caps_of s xb
 2. \<Union> (direct_caps_of s ` island s x) \<subseteq> \<Union> (caps_of s ` island s x) proof (prove)
goal (1 subgoal):
 1. \<Union> (direct_caps_of s ` island s x) \<subseteq> \<Union> (caps_of s ` island s x) proof (prove)
goal:
No subgoals!
theory Islands_S

lemma island_caps_dom:
  "island_caps s e\<^sub>x \<le>cap c =
  (\<forall>e\<^sub>i. (e\<^sub>x, e\<^sub>i) \<in> tgs_connected s \<longrightarrow> caps_of s e\<^sub>i \<le>cap c)" by (auto simp add: island_caps_def caps_dominated_by_def island_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (island_caps s e\<^sub>x \<le>cap c) = (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c)
theory Isolation_S

lemma set_flow_def2:
  "(X, Y) \<in> set_flow s = (\<exists>x \<in> X. \<exists>y \<in> Y.
                        (read_cap x \<in>cap caps_of s y \<or>
                        write_cap y \<in>cap caps_of s x))" by (simp add: set_flow_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((X, Y) \<in> set_flow s) = (\<exists>x\<in>X. \<exists>y\<in>Y. read_cap x \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s x)
theory Isolation_S

lemma flow_def2:
  "(x, y) \<in> flow s = ((island s x, island s y) \<in> set_flow s)" by (simp add: flow_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> flow s) = ((island s x, island s y) \<in> set_flow s)
theory Isolation_S

lemma rights_extra_rights_read_cap [simp]:
  "rights (extra_rights (read_cap e)) = {Read}" by (simp add: rights_extra_rights)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (extra_rights (read_cap e)) = {Read}
theory Isolation_S

lemma rights_extra_rights_write_cap [simp]:
  "rights (extra_rights (write_cap e)) = {Write}" by (simp add: rights_extra_rights)

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