kings-crown/FVELER_Isabelle huggingface dataset:
theory Example2

lemma extra_rights_create_cap:
  "extra_rights (create_cap i) = full_cap i" by (simp add: create_cap_def full_cap_def extra_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (create_cap i) = full_cap i
theory Example2

lemma extra_rights_full_cap:
  "extra_rights (full_cap i) = full_cap i" by (simp add: full_cap_def extra_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (full_cap i) = full_cap i
theory Example2

lemma extra_rights_take_cap:
  "extra_rights (take_cap i) = take_cap i" by (simp add: take_cap_def extra_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (take_cap i) = take_cap i
theory Example2

lemma extra_rights_grant_cap:
  "extra_rights (grant_cap i) = grant_cap i" by (simp add: take_cap_def extra_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (grant_cap i) = grant_cap i
theory Example2

lemma caps_of'_s_e0_caps_helper:
  "extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) =
  range full_cap - {full_cap 1, full_cap 2}" apply rule apply (fastforce simp: create_cap_def extra_rights_def all_rights_def full_cap_def) apply rule apply (erule DiffE) apply clarsimp apply (rule image_eqI) apply (rule extra_rights_create_cap [THEN sym]) apply (simp add: full_cap_def create_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) = range full_cap - {full_cap 1, full_cap 2} proof (prove)
goal (2 subgoals):
 1. extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) \<subseteq> range full_cap - {full_cap 1, full_cap 2}
 2. range full_cap - {full_cap 1, full_cap 2} \<subseteq> extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) proof (prove)
goal (1 subgoal):
 1. range full_cap - {full_cap 1, full_cap 2} \<subseteq> extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> range full_cap - {full_cap 1, full_cap 2} \<Longrightarrow> x \<in> extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> range full_cap; x \<notin> {full_cap 1, full_cap 2}\<rbrakk> \<Longrightarrow> x \<in> extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>full_cap xa \<noteq> full_cap 1; full_cap xa \<noteq> full_cap 2\<rbrakk> \<Longrightarrow> full_cap xa \<in> extra_rights ` (range create_cap - {create_cap 1, create_cap 2}) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>full_cap xa \<noteq> full_cap 1; full_cap xa \<noteq> full_cap 2\<rbrakk> \<Longrightarrow> full_cap xa = extra_rights (?x27 xa)
 2. \<And>xa. \<lbrakk>full_cap xa \<noteq> full_cap 1; full_cap xa \<noteq> full_cap 2\<rbrakk> \<Longrightarrow> ?x27 xa \<in> range create_cap - {create_cap 1, create_cap 2} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>full_cap xa \<noteq> full_cap 1; full_cap xa \<noteq> full_cap 2\<rbrakk> \<Longrightarrow> create_cap xa \<in> range create_cap - {create_cap 1, create_cap 2} proof (prove)
goal:
No subgoals!
theory Example2

lemma cap_in_caps_take_cap:
  "\<lbrakk>create_cap x \<in> caps_of s y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y" apply (auto simp: cap_in_caps_def caps_of_def extra_rights_take_cap) apply (rule exI, rule conjI, assumption) apply (rule rev_bexI, simp) apply (rule conjI) apply (subgoal_tac "target (full_cap x) = x", simp+) apply (simp add: extra_rights_create_cap all_rights_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap x \<in> caps_of s y \<Longrightarrow> take_cap x \<in>cap caps_of s y proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> \<exists>ya. (y, ya) \<in> store_connected s \<and> (\<exists>c'\<in>direct_caps_of s ya. x = target c' \<and> Take \<in> rights (extra_rights c')) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> \<exists>c'\<in>direct_caps_of s xa. x = target c' \<and> Take \<in> rights (extra_rights c') proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> x = target (create_cap x) \<and> Take \<in> rights (extra_rights (create_cap x)) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> x = target (create_cap x)
 2. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> Take \<in> rights (extra_rights (create_cap x)) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(y, xa) \<in> store_connected s; create_cap x \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> Take \<in> rights (extra_rights (create_cap x)) proof (prove)
goal:
No subgoals!
theory Example2

lemma e0_connected_to:
  "\<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> s \<turnstile> 0 \<leftrightarrow> x" apply (rule directly_tgs_connected_comm) apply (simp add: directly_tgs_connected_def4) apply (rule disjI1) apply (rule cap_in_caps_take_cap) apply (simp add: caps_of_s_e0_caps e0_caps_def create_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> s \<turnstile> 0 \<leftrightarrow> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s 0 \<or> take_cap 0 \<in>cap caps_of s x \<or> grant_cap 0 \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s 0 \<or> shares_caps s 0 x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> create_cap x \<in> caps_of s 0 proof (prove)
goal:
No subgoals!
theory Example2

lemma e1_connected_trans_to_e2:
  "s \<turnstile> 1 \<leftrightarrow>* 2" apply (insert e1_connected_to_e2) apply (simp add: tgs_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 1 \<leftrightarrow>* 2 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 1 \<leftrightarrow> 2 \<Longrightarrow> s \<turnstile> 1 \<leftrightarrow>* 2 proof (prove)
goal:
No subgoals!
theory Example2

lemma caps_of_to_e1:
  "\<lbrakk>c \<in> caps_of s x; target c = 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2" apply (case_tac "x = 0") apply (fastforce simp: caps_of_s_e0_caps_2) apply (case_tac "x = 1") apply (fastforce simp: caps_of_s_e1) apply (fastforce simp: caps_of_s_e3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s x; target c = 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s x; target c = 1; x = 0\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2
 2. \<lbrakk>c \<in> caps_of s x; target c = 1; x \<noteq> 0\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s x; target c = 1; x \<noteq> 0\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s x; target c = 1; x \<noteq> 0; x = 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2
 2. \<lbrakk>c \<in> caps_of s x; target c = 1; x \<noteq> 0; x \<noteq> 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s x; target c = 1; x \<noteq> 0; x \<noteq> 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal:
No subgoals!
theory Example2

lemma cap_in_caps_caps_of_e1:
  "c \<in>cap caps_of s 1 \<Longrightarrow> target c = 1 \<or> target c = 2" by (clarsimp simp: cap_in_caps_def caps_of_s_e1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in>cap caps_of s 1 \<Longrightarrow> target c = 1 \<or> target c = 2
theory Example2

lemma cap_in_caps_caps_of_e2:
  "c \<in>cap caps_of s 2 \<Longrightarrow> False" by (clarsimp simp: cap_in_caps_def caps_of_s_e2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in>cap caps_of s 2 \<Longrightarrow> False
theory Example2

lemma cap_in_caps_caps_of_to_e1:
  "\<lbrakk>c \<in>cap caps_of s x; target c = 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2" apply (clarsimp simp: cap_in_caps_def) apply (drule (1) caps_of_to_e1, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in>cap caps_of s x; target c = 1\<rbrakk> \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>target c = 1; c' \<in> caps_of s x; target c' = 1; rights (extra_rights c) \<subseteq> rights (extra_rights c'); x \<noteq> 2\<rbrakk> \<Longrightarrow> x = 1 proof (prove)
goal:
No subgoals!
theory Example2

lemma cap_in_caps_caps_of_to_e2:
  "\<lbrakk>c \<in>cap caps_of s x; target c = 2\<rbrakk> \<Longrightarrow> x = 1" apply (clarsimp simp: cap_in_caps_def) apply (erule (1) caps_of_to_e2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in>cap caps_of s x; target c = 2\<rbrakk> \<Longrightarrow> x = 1 proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>target c = 2; c' \<in> caps_of s x; target c' = 2; rights (extra_rights c) \<subseteq> rights (extra_rights c')\<rbrakk> \<Longrightarrow> x = 1 proof (prove)
goal:
No subgoals!
theory Example2

lemma e1_connected_to:
  "s \<turnstile> 1 \<leftrightarrow> x \<Longrightarrow> x = 1 \<or> x = 2" apply (simp add: directly_tgs_connected_def4) apply (erule disjE) apply (erule cap_in_caps_caps_of_to_e1, simp) apply (erule disjE) apply (drule cap_in_caps_caps_of_e1, simp) apply (erule disjE) apply (drule cap_in_caps_caps_of_e1, simp) apply (erule disjE) apply (erule cap_in_caps_caps_of_to_e1, simp) apply (fastforce simp: shares_caps_def store_connected_s) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 1 \<leftrightarrow> x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. take_cap 1 \<in>cap caps_of s x \<or> take_cap x \<in>cap caps_of s 1 \<or> grant_cap x \<in>cap caps_of s 1 \<or> grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. take_cap 1 \<in>cap caps_of s x \<Longrightarrow> x = 1 \<or> x = 2
 2. take_cap x \<in>cap caps_of s 1 \<or> grant_cap x \<in>cap caps_of s 1 \<or> grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. take_cap x \<in>cap caps_of s 1 \<or> grant_cap x \<in>cap caps_of s 1 \<or> grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. take_cap x \<in>cap caps_of s 1 \<Longrightarrow> x = 1 \<or> x = 2
 2. grant_cap x \<in>cap caps_of s 1 \<or> grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. grant_cap x \<in>cap caps_of s 1 \<or> grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. grant_cap x \<in>cap caps_of s 1 \<Longrightarrow> x = 1 \<or> x = 2
 2. grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. grant_cap 1 \<in>cap caps_of s x \<or> shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. grant_cap 1 \<in>cap caps_of s x \<Longrightarrow> x = 1 \<or> x = 2
 2. shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. shares_caps s 1 x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal:
No subgoals!
theory Example2

lemma e2_connected_to:
  "s \<turnstile> 2 \<leftrightarrow> x \<Longrightarrow> x = 1 \<or> x = 2" apply (simp add: directly_tgs_connected_def4) apply (erule disjE, rule disjI1) apply (erule cap_in_caps_caps_of_to_e2, simp) apply (erule disjE, rule disjI1) apply (drule cap_in_caps_caps_of_e2, simp) apply (erule disjE, rule disjI1) apply (drule cap_in_caps_caps_of_e2, simp) apply (erule disjE, rule disjI1) apply (erule cap_in_caps_caps_of_to_e2, simp) apply (clarsimp simp: shares_caps_def store_connected_s) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 2 \<leftrightarrow> x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. take_cap 2 \<in>cap caps_of s x \<or> take_cap x \<in>cap caps_of s 2 \<or> grant_cap x \<in>cap caps_of s 2 \<or> grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. take_cap 2 \<in>cap caps_of s x \<Longrightarrow> x = 1
 2. take_cap x \<in>cap caps_of s 2 \<or> grant_cap x \<in>cap caps_of s 2 \<or> grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. take_cap x \<in>cap caps_of s 2 \<or> grant_cap x \<in>cap caps_of s 2 \<or> grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. take_cap x \<in>cap caps_of s 2 \<Longrightarrow> x = 1
 2. grant_cap x \<in>cap caps_of s 2 \<or> grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. grant_cap x \<in>cap caps_of s 2 \<or> grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. grant_cap x \<in>cap caps_of s 2 \<Longrightarrow> x = 1
 2. grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. grant_cap 2 \<in>cap caps_of s x \<or> shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (2 subgoals):
 1. grant_cap 2 \<in>cap caps_of s x \<Longrightarrow> x = 1
 2. shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. shares_caps s x 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal:
No subgoals!
theory Example2

lemma directly_tgs_connected_in_inv_image:
  "(directly_tgs_connected s) \<subseteq> inv_image Id (\<lambda> x. x=1 \<or> x=2)" by (fastforce simp: inv_image_def
              dest!: e1_connected_to e1_connected_to [OF directly_tgs_connected_comm]
                     e2_connected_to e2_connected_to [OF directly_tgs_connected_comm])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. directly_tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)
theory Example2

lemma eq_inv_image_connected:
  "(inv_image Id (\<lambda> x. x=1 \<or> x=2))\<^sup>= = inv_image Id (\<lambda> x. x=1 \<or> x=2)" by (fastforce simp: inv_image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)))\<^sup>= = inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a))
theory Example2

lemma rtrancl_inv_image_connected:
  "(inv_image Id (\<lambda> x. x=1 \<or> x=2))\<^sup>* = inv_image Id (\<lambda> x. x=1 \<or> x=2)" apply (subst trancl_reflcl [symmetric]) apply (subst eq_inv_image_connected) apply (rule trancl_id) apply (rule connected_inv_image_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)))\<^sup>* = inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)) proof (prove)
goal (1 subgoal):
 1. ((inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)))\<^sup>=)\<^sup>+ = inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)) proof (prove)
goal (1 subgoal):
 1. (inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)))\<^sup>+ = inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a)) proof (prove)
goal (1 subgoal):
 1. trans (inv_image Id (\<lambda>x. x = (1::'a) \<or> x = (2::'a))) proof (prove)
goal:
No subgoals!
theory Example2

lemma tgs_connected_in_inv_image:
  "(tgs_connected s) \<subseteq> inv_image Id (\<lambda> x. x=1 \<or> x=2)" apply (simp add: tgs_connected_def) apply (subst rtrancl_inv_image_connected [symmetric]) apply (rule rtrancl_mono) apply (rule directly_tgs_connected_in_inv_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) proof (prove)
goal (1 subgoal):
 1. (directly_tgs_connected s)\<^sup>* \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) proof (prove)
goal (1 subgoal):
 1. (directly_tgs_connected s)\<^sup>* \<subseteq> (inv_image Id (\<lambda>x. x = 1 \<or> x = 2))\<^sup>* proof (prove)
goal (1 subgoal):
 1. directly_tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) proof (prove)
goal:
No subgoals!
theory Example2

lemma e0_not_connected_trans_e1:
  "\<not> s \<turnstile> 0 \<leftrightarrow>* 1" apply clarsimp apply (drule set_mp [OF tgs_connected_in_inv_image]) apply (simp add: inv_image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> s \<turnstile> 0 \<leftrightarrow>* 1 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 0 \<leftrightarrow>* 1 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (0, 1) \<in> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma e0_e1_leakage:
  "s' \<in> execute cmds s \<Longrightarrow> \<not> leak s' 0 1" apply (insert e0_not_connected_trans_e1) apply (drule (2) leakage_rule) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 0 \<rightarrow> 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; \<not> s \<turnstile> 0 \<leftrightarrow>* 1\<rbrakk> \<Longrightarrow> \<not> s' \<turnstile> 0 \<rightarrow> 1 proof (prove)
goal:
No subgoals!
theory Example2

lemma island_e0:
  "island s 0 = {i. i \<noteq> 1 \<and> i \<noteq> 2}" apply rule apply (clarsimp simp: island_def) apply (insert tgs_connected_in_inv_image)[1] apply fastforce apply (clarsimp simp: island_def) apply (drule (1) e0_connected_to) apply (drule directly_tgs_connected_comm) by (metis directly_tgs_connected_def2 tgs_connected_comm leakImplyConnectedTrans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. island s 0 = {i. i \<noteq> 1 \<and> i \<noteq> 2} proof (prove)
goal (2 subgoals):
 1. island s 0 \<subseteq> {i. i \<noteq> 1 \<and> i \<noteq> 2}
 2. {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s 0 proof (prove)
goal (2 subgoals):
 1. \<And>x. s \<turnstile> 0 \<leftrightarrow>* x \<Longrightarrow> x \<noteq> 1 \<and> x \<noteq> 2
 2. {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s 0 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>s \<turnstile> 0 \<leftrightarrow>* x; tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> x \<noteq> 1 \<and> x \<noteq> 2
 2. {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s 0 proof (prove)
goal (1 subgoal):
 1. {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> s \<turnstile> 0 \<leftrightarrow>* x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> 2; s \<turnstile> 0 \<leftrightarrow> x\<rbrakk> \<Longrightarrow> s \<turnstile> 0 \<leftrightarrow>* x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> 2; s \<turnstile> x \<leftrightarrow> 0\<rbrakk> \<Longrightarrow> s \<turnstile> 0 \<leftrightarrow>* x
theory Example2

lemma island_e1:
  "island s 1 = {1,2}" apply rule apply (clarsimp simp: island_def) apply (insert tgs_connected_in_inv_image)[1] apply fastforce apply (clarsimp simp: island_def) apply (rule e1_connected_trans_to_e2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. island s 1 = {1, 2} proof (prove)
goal (2 subgoals):
 1. island s 1 \<subseteq> {1, 2}
 2. {1, 2} \<subseteq> island s 1 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> 1; s \<turnstile> 1 \<leftrightarrow>* x\<rbrakk> \<Longrightarrow> x = 2
 2. {1, 2} \<subseteq> island s 1 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> 1; s \<turnstile> 1 \<leftrightarrow>* x; tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> x = 2
 2. {1, 2} \<subseteq> island s 1 proof (prove)
goal (1 subgoal):
 1. {1, 2} \<subseteq> island s 1 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 1 \<leftrightarrow>* 2 proof (prove)
goal:
No subgoals!
theory Example2

lemma island_e2:
  "island s 2 = {1,2}" apply rule apply (clarsimp simp: island_def) apply (insert tgs_connected_in_inv_image)[1] apply fastforce apply (clarsimp simp: island_def) apply (rule e1_connected_trans_to_e2  [THEN tgs_connected_comm]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. island s 2 = {1, 2} proof (prove)
goal (2 subgoals):
 1. island s 2 \<subseteq> {1, 2}
 2. {1, 2} \<subseteq> island s 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> 1; s \<turnstile> 2 \<leftrightarrow>* x\<rbrakk> \<Longrightarrow> x = 2
 2. {1, 2} \<subseteq> island s 2 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> 1; s \<turnstile> 2 \<leftrightarrow>* x; tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> x = 2
 2. {1, 2} \<subseteq> island s 2 proof (prove)
goal (1 subgoal):
 1. {1, 2} \<subseteq> island s 2 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 2 \<leftrightarrow>* 1 proof (prove)
goal:
No subgoals!