theory Example2

lemma e0_caps_not_connected_to_e1:
  "\<not> (s \<turnstile> 0 \<leftrightarrow> 1)" apply (simp add: directly_tgs_connected_def4) apply (rule conjI) apply (simp add: cap_in_caps_def caps_of_s_e1) apply (rule conjI) apply (clarsimp simp add: cap_in_caps_def caps_of_s_e0_caps e0_caps_def) apply (erule disjE) apply (simp add: full_cap_def) apply clarsimp apply (rule conjI) apply (clarsimp simp add: cap_in_caps_def caps_of_s_e0_caps e0_caps_def) apply (erule disjE) apply (simp add: full_cap_def) apply clarsimp apply (rule conjI) apply (simp add: cap_in_caps_def caps_of_s_e1) apply (simp add: shares_caps_def) apply (simp add: store_connected_s) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> s \<turnstile> 0 \<leftrightarrow> 1 proof (prove)
goal (1 subgoal):
 1. take_cap 0 \<notin>cap caps_of s 1 \<and> take_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. take_cap 0 \<notin>cap caps_of s 1
 2. take_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (1 subgoal):
 1. take_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. take_cap 1 \<notin>cap caps_of s 0
 2. grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>c' = full_cap 0 \<or> c' \<in> range create_cap; c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (take_cap 1)) \<subseteq> rights (extra_rights c')\<rbrakk> \<Longrightarrow> False
 2. grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (take_cap 1)) \<subseteq> rights (extra_rights c'); c' = full_cap 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (take_cap 1)) \<subseteq> rights (extra_rights c'); c' \<in> range create_cap\<rbrakk> \<Longrightarrow> False
 3. grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (take_cap 1)) \<subseteq> rights (extra_rights c'); c' \<in> range create_cap\<rbrakk> \<Longrightarrow> False
 2. grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (1 subgoal):
 1. grant_cap 1 \<notin>cap caps_of s 0 \<and> grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. grant_cap 1 \<notin>cap caps_of s 0
 2. grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>c' = full_cap 0 \<or> c' \<in> range create_cap; c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (grant_cap 1)) \<subseteq> rights (extra_rights c')\<rbrakk> \<Longrightarrow> False
 2. grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (3 subgoals):
 1. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (grant_cap 1)) \<subseteq> rights (extra_rights c'); c' = full_cap 0\<rbrakk> \<Longrightarrow> False
 2. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (grant_cap 1)) \<subseteq> rights (extra_rights c'); c' \<in> range create_cap\<rbrakk> \<Longrightarrow> False
 3. grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>c' \<noteq> create_cap 1; c' \<noteq> create_cap 2; target c' = 1; rights (extra_rights (grant_cap 1)) \<subseteq> rights (extra_rights c'); c' \<in> range create_cap\<rbrakk> \<Longrightarrow> False
 2. grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (1 subgoal):
 1. grant_cap 0 \<notin>cap caps_of s 1 \<and> \<not> shares_caps s 1 0 proof (prove)
goal (2 subgoals):
 1. grant_cap 0 \<notin>cap caps_of s 1
 2. \<not> shares_caps s 1 0 proof (prove)
goal (1 subgoal):
 1. \<not> shares_caps s 1 0 proof (prove)
goal (1 subgoal):
 1. \<forall>e\<^sub>i. (1, e\<^sub>i) \<in> store_connected s \<longrightarrow> (0, e\<^sub>i) \<notin> store_connected s proof (prove)
goal:
No subgoals!