theory Confine_S

lemma create_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysCreate e c\<^sub>1 c\<^sub>2)\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s" apply(clarsimp simp: step_def split: if_split_asm) apply (erule disjE, fastforce simp: tgs_connected_def, clarsimp) apply (drule create_directly_tgs_connected, clarsimp, assumption) apply (simp add: tgs_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2; s' = s \<or> s' = createOperation e c\<^sub>1 c\<^sub>2 s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2; Store \<in> rights c\<^sub>1 \<longrightarrow> Write \<in> rights c\<^sub>1 \<longrightarrow> c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> is_entity s (target c\<^sub>2) \<or> Create \<notin> rights c\<^sub>2; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>createOperation e c\<^sub>1 c\<^sub>2 s \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2; s' = createOperation e c\<^sub>1 c\<^sub>2 s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2; Store \<in> rights c\<^sub>1 \<longrightarrow> Write \<in> rights c\<^sub>1 \<longrightarrow> c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> is_entity s (target c\<^sub>2) \<or> Create \<notin> rights c\<^sub>2; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCreate e c\<^sub>1 c\<^sub>2; Store \<in> rights c\<^sub>1 \<longrightarrow> Write \<in> rights c\<^sub>1 \<longrightarrow> c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> is_entity s (target c\<^sub>2) \<or> Create \<notin> rights c\<^sub>2; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!