# HG changeset patch
# User bulwahn
# Date 1327681325 -3600
# Node ID 54870ad19af454d96c54b2a777463eb7937c24bc
# Parent  10c18630612a71a0f2a96e116438366449f97016
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well

diff -r 10c18630612a -r 54870ad19af4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Jan 27 17:02:08 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Jan 27 17:22:05 2012 +0100
@@ -1003,7 +1003,7 @@
     unfolding ntrancl_def by auto
 qed
 
-lemma ntrancl_Suc [simp, code]:
+lemma ntrancl_Suc [simp]:
   "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"
 proof
   {
@@ -1034,6 +1034,10 @@
     unfolding ntrancl_def by fastforce
 qed
 
+lemma [code]:
+  "ntrancl (Suc n) r = (let r' = ntrancl n r in r' Un r' O r)"
+unfolding Let_def by auto
+
 lemma finite_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)