author nipkow Fri, 06 Jun 2014 10:53:33 +0200 changeset 57178 276befcd90d9 parent 57177 dce365931721 child 57179 011955e7846b
```--- 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)}"