# HG changeset patch
# User haftmann
# Date 1318541266 -7200
# Node ID 339a8b3c479197d6be767da24f90db7f684e6c8e
# Parent  bdcaa3f3a2f418a389d7cee78bf7f9f02309cbe8
bouned transitive closure

diff -r bdcaa3f3a2f4 -r 339a8b3c4791 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Thu Oct 13 23:02:59 2011 +0200
+++ b/src/HOL/Enum.thy	Thu Oct 13 23:27:46 2011 +0200
@@ -758,69 +758,13 @@
     unfolding enum_the_def by (auto split: list.split)
 qed
 
+
 subsection {* An executable card operator on finite types *}
 
-lemma
-  [code]: "card R = length (filter R enum)"
-by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
-
-subsection {* An executable (reflexive) transitive closure on finite relations *}
-
-text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
-
-definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
-where
- [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
-
-lemma [code]:
-  "ntrancl (R :: 'a * 'a => bool) 0 = R"
-proof
-  show "R <= ntrancl R 0"
-    unfolding ntrancl_def by fastforce
-next
-  { 
-    fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
-  }
-  from this show "ntrancl R 0 <= R"
-    unfolding ntrancl_def by auto
-qed
-
 lemma [code]:
-  "ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
-proof
-  {
-    fix a b
-    assume "(a, b) : ntrancl R (Suc n)"
-    from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
-      unfolding ntrancl_def by auto
-    have "(a, b) : ntrancl R n O (Id Un R)"
-    proof (cases "i = 1")
-      case True
-      from this `(a, b) : R ^^ i` show ?thesis
-        unfolding ntrancl_def by auto
-    next
-      case False
-      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
-        by (cases i) auto
-      from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
-        by auto
-      from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
-        unfolding ntrancl_def by fastforce
-      from this c2 show ?thesis by fastforce
-    qed
-  }
-  from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
-next
-  show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
-    unfolding ntrancl_def by fastforce
-qed
+  "card R = length (filter R enum)"
+  by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
 
-lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
-by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
-
-(* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
-lemma [code]: "r^* = (r^+)^="
-by simp
 
 subsection {* Closing up *}
 
diff -r bdcaa3f3a2f4 -r 339a8b3c4791 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Oct 13 23:02:59 2011 +0200
+++ b/src/HOL/Nitpick.thy	Thu Oct 13 23:27:46 2011 +0200
@@ -63,7 +63,7 @@
 by (auto simp: mem_def)
 
 lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
-by simp
+  by (simp only: rtrancl_trancl_reflcl)
 
 lemma rtranclp_unfold [nitpick_unfold, no_atp]:
 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
diff -r bdcaa3f3a2f4 -r 339a8b3c4791 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:02:59 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:27:46 2011 +0200
@@ -576,6 +576,9 @@
    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
   done
 
+lemma rtrancl_trancl_reflcl [code]: "r^* = (r^+)^="
+  by simp
+
 lemma trancl_empty [simp]: "{}^+ = {}"
   by (auto elim: trancl_induct)
 
@@ -980,6 +983,65 @@
 apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
 done
 
+
+subsection {* Bounded transitive closure *}
+
+definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
+where
+  "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)"
+
+lemma ntrancl_Zero [simp, code]:
+  "ntrancl 0 R = R"
+proof
+  show "R \<subseteq> ntrancl 0 R"
+    unfolding ntrancl_def by fastforce
+next
+  { 
+    fix i have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" by auto
+  }
+  from this show "ntrancl 0 R \<le> R"
+    unfolding ntrancl_def by auto
+qed
+
+lemma ntrancl_Suc [simp, code]:
+  "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"
+proof
+  {
+    fix a b
+    assume "(a, b) \<in> ntrancl (Suc n) R"
+    from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
+      unfolding ntrancl_def by auto
+    have "(a, b) \<in> ntrancl n R O (Id \<union> R)"
+    proof (cases "i = 1")
+      case True
+      from this `(a, b) \<in> R ^^ i` show ?thesis
+        unfolding ntrancl_def by auto
+    next
+      case False
+      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
+        by (cases i) auto
+      from this `(a, b) \<in> R ^^ i` obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
+        by auto
+      from c1 j `i \<le> Suc (Suc n)` have "(a, c) \<in> ntrancl n R"
+        unfolding ntrancl_def by fastforce
+      from this c2 show ?thesis by fastforce
+    qed
+  }
+  from this show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)"
+    by auto
+next
+  show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R"
+    unfolding ntrancl_def by fastforce
+qed
+
+lemma finnite_trancl_ntranl:
+  "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
+  by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
+
+lemma [code]: "trancl (R :: (('a :: finite) \<times> 'a) set) = ntrancl (card R - 1) R"
+  by (simp add: finnite_trancl_ntranl)
+
+
 subsection {* Acyclic relations *}
 
 definition acyclic :: "('a * 'a) set => bool" where