theory Lib

lemma union_trans:
  assumes SR: "\<And>x y z. \<lbrakk> (x,y) \<in> S; (y,z) \<in> R \<rbrakk> \<Longrightarrow> (x,z) \<in> S^*"
  shows "(R \<union> S)^* = R^* \<union> R^* O S^*" apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (erule rtrancl_induct; simp) apply (erule disjE) apply (erule disjE) apply (drule (1) rtrancl_into_rtrancl) apply blast apply clarsimp apply (drule rtranclD [where R=S]) apply (erule disjE) apply simp apply (erule conjE) apply (drule tranclD2) apply (elim exE conjE) apply (drule (1) SR) apply (drule (1) rtrancl_trans) apply blast apply (rule disjI2) apply (erule disjE) apply (blast intro: in_rtrancl_UnI) apply clarsimp apply (drule (1) rtrancl_into_rtrancl) apply (erule (1) relcompI) apply (erule disjE) apply (blast intro: in_rtrancl_UnI) apply clarsimp apply (blast intro: in_rtrancl_UnI rtrancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (R \<union> S)\<^sup>* = R\<^sup>* \<union> R\<^sup>* O S\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> (R \<union> S)\<^sup>*) = (x \<in> R\<^sup>* \<union> R\<^sup>* O S\<^sup>*) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ((a, b) \<in> (R \<union> S)\<^sup>*) = ((a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>*) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> (R \<union> S)\<^sup>* \<Longrightarrow> (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R \<or> (y, z) \<in> S; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> R\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R; (a, y) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R; (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 4. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R; (a, z) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R; (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 4. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> R; (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (ya, za) \<in> S\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya = za \<or> ya \<noteq> za \<and> (ya, za) \<in> S\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (4 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya = za\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za \<and> (ya, za) \<in> S\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 3. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 4. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za \<and> (ya, za) \<in> S\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za; (ya, za) \<in> S\<^sup>+\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za; \<exists>z. (ya, z) \<in> S\<^sup>* \<and> (z, za) \<in> S\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za zb. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za; (ya, zb) \<in> S\<^sup>*; (zb, za) \<in> S\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za zb. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za; (ya, zb) \<in> S\<^sup>*; (zb, z) \<in> S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>z x ya za zb. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> R; (x, ya) \<in> R\<^sup>*; (x, z) \<notin> R\<^sup>* O S\<^sup>*; ya \<noteq> za; (zb, z) \<in> S\<^sup>*; (ya, z) \<in> S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* \<or> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (a, y) \<in> R\<^sup>* \<or> (a, y) \<in> R\<^sup>* O S\<^sup>*; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> S; (a, y) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> S; (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* O S\<^sup>*
 3. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a y z. \<lbrakk>(a, y) \<in> (R \<union> S)\<^sup>*; (y, z) \<in> S; (a, y) \<in> R\<^sup>* O S\<^sup>*\<rbrakk> \<Longrightarrow> (a, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> S; (x, ya) \<in> R\<^sup>*; (ya, za) \<in> S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>z x ya za. \<lbrakk>(x, za) \<in> (R \<union> S)\<^sup>*; (za, z) \<in> S; (x, ya) \<in> R\<^sup>*; (ya, z) \<in> S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> R\<^sup>* O S\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> R\<^sup>* \<or> (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>*
 2. \<And>a b. (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> R\<^sup>* O S\<^sup>* \<Longrightarrow> (a, b) \<in> (R \<union> S)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> R\<^sup>*; (y, z) \<in> S\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (R \<union> S)\<^sup>* proof (prove)
goal:
No subgoals!