# HG changeset patch
# User bulwahn
# Date 1317645794 -7200
# Node ID 3911cf09899a87bd119d59f3af63b24d99872e8b
# Parent  f947eeef6b6fe02e15461b45e2b7a84d45468826
adding code equations for cardinality and (reflexive) transitive closure on finite types

diff -r f947eeef6b6f -r 3911cf09899a src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Oct 03 14:43:13 2011 +0200
+++ b/src/HOL/Enum.thy	Mon Oct 03 14:43:14 2011 +0200
@@ -758,12 +758,78 @@
     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 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
+
+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 *}
+
 code_abort enum_the
 
 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
 
 
 hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
-hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
+hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
 
 end