# HG changeset patch
# User nipkow
# Date 1402044813 -7200
# Node ID 276befcd90d9c691b5a7161f7fb80668a29ba259
# Parent  dce365931721669fc81360bf01bb82eb31460d2b
added lemmas

diff -r dce365931721 -r 276befcd90d9 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Jun 05 19:39:38 2014 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Jun 06 10:53:33 2014 +0200
@@ -460,19 +460,6 @@
 
 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]
 
-lemma trancl_insert:
-  "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
-  -- {* primitive recursion for @{text trancl} over finite relations *}
-  apply (rule equalityI)
-   apply (rule subsetI)
-   apply (simp only: split_tupled_all)
-   apply (erule trancl_induct, blast)
-   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
-  apply (rule subsetI)
-  apply (blast intro: trancl_mono rtrancl_mono
-    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
-  done
-
 lemma tranclp_converseI: "(r^++)^--1 x y ==> (r^--1)^++ x y"
   apply (drule conversepD)
   apply (erule tranclp_induct)
@@ -603,6 +590,28 @@
 lemma trancl_unfold_left: "r^+ = r O r^*"
 by (auto dest: tranclD intro: rtrancl_into_trancl2)
 
+lemma trancl_insert:
+  "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
+  -- {* primitive recursion for @{text trancl} over finite relations *}
+  apply (rule equalityI)
+   apply (rule subsetI)
+   apply (simp only: split_tupled_all)
+   apply (erule trancl_induct, blast)
+   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
+  apply (rule subsetI)
+  apply (blast intro: trancl_mono rtrancl_mono
+    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
+  done
+
+lemma trancl_insert2:
+  "(insert (a,b) r)^+ = r^+ \<union> {(x,y). ((x,a) : r^+ \<or> x=a) \<and> ((b,y) \<in> r^+ \<or> y=b)}"
+by(auto simp add: trancl_insert rtrancl_eq_or_trancl)
+
+lemma rtrancl_insert:
+  "(insert (a,b) r)^* = r^* \<union> {(x,y). (x,a) : r^* \<and> (b,y) \<in> r^*}"
+using trancl_insert[of a b r]
+by(simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast
+
 
 text {* Simplifying nested closures *}