theory Example2

lemma store_connected_s: "store_connected s = {(1,2)} \<union> Id" apply simp apply (rule equalityI) apply (insert store_connected_direct_s) apply (simp add: store_connected_def) apply clarsimp apply (erule converse_rtranclE) apply simp apply clarsimp apply (erule rtranclE) apply fastforce apply (simp add: store_connected_id) apply (drule rtranclD) apply (safe, simp_all, (erule tranclE, simp, fastforce)+) apply (fastforce simp: store_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. store_connected s = {(1, 2)}\<^sup>= proof (prove)
goal (1 subgoal):
 1. store_connected s = insert (1, 2) Id proof (prove)
goal (2 subgoals):
 1. store_connected s \<subseteq> insert (1, 2) Id
 2. insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> store_connected s \<subseteq> insert (1, 2) Id
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> {(0, 0), (1, 1), (1, 2)}\<^sup>* \<subseteq> insert (1, 2) Id
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*; a \<noteq> b\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = b\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. \<And>a b y. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; (a, y) \<in> {(0, 0), (1, 1), (1, 2)}; (y, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 3. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; (a, y) \<in> {(0, 0), (1, 1), (1, 2)}; (y, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; (y, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (3 subgoals):
 1. \<And>a b y. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; y = b\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. \<And>a b y ya. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; (y, ya) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*; (ya, b) \<in> {(0, 0), (1, 1), (1, 2)}\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 3. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b y ya. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; (y, ya) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*; (ya, b) \<in> {(0, 0), (1, 1), (1, 2)}\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b y ya. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; (y, ya) \<in> {(1, 2)}\<^sup>*; ya = 0 \<and> b = 0 \<or> ya = 1 \<and> b = 1 \<or> ya = 1 \<and> b = 2\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>a b y ya. \<lbrakk>store_connected_direct s = {(0, 0), (1, 1), (1, 2)}; a \<noteq> b; a = 0 \<and> y = 0 \<or> a = 1 \<and> y = 1 \<or> a = 1 \<and> y = 2; ya = 0 \<and> b = 0 \<or> ya = 1 \<and> b = 1 \<or> ya = 1 \<and> b = 2; y = ya \<or> y \<noteq> ya \<and> (y, ya) \<in> {(1, 2)}\<^sup>+\<rbrakk> \<Longrightarrow> a = 1 \<and> b = 2
 2. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> insert (1, 2) Id \<subseteq> store_connected s proof (prove)
goal (1 subgoal):
 1. store_connected_direct s = {(0, 0), (1, 1), (1, 2)} \<Longrightarrow> (1, 2) \<in> store_connected s proof (prove)
goal:
No subgoals!