theory Example

lemma sc:
  "store_connected example_state = {(id0,id1)} \<union> Id" apply simp apply (rule equalityI) apply (insert scd) apply (simp add: store_connected_def) apply clarsimp apply (erule converse_rtranclE) apply simp apply clarsimp apply (erule rtranclE) apply simp apply clarsimp apply (fastforce simp: store_connected_def) done

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