src/HOL/Enum.thy
 changeset 45140 339a8b3c4791 parent 45119 055c6ff9c5c3 child 45141 b2eb87bd541b
```     1.1 --- a/src/HOL/Enum.thy	Thu Oct 13 23:02:59 2011 +0200
1.2 +++ b/src/HOL/Enum.thy	Thu Oct 13 23:27:46 2011 +0200
1.3 @@ -758,69 +758,13 @@
1.4      unfolding enum_the_def by (auto split: list.split)
1.5  qed
1.6
1.7 +
1.8  subsection {* An executable card operator on finite types *}
1.9
1.10 -lemma
1.11 -  [code]: "card R = length (filter R enum)"
1.12 -by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
1.13 -
1.14 -subsection {* An executable (reflexive) transitive closure on finite relations *}
1.15 -
1.16 -text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
1.17 -
1.18 -definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
1.19 -where
1.20 - [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
1.21 -
1.22 -lemma [code]:
1.23 -  "ntrancl (R :: 'a * 'a => bool) 0 = R"
1.24 -proof
1.25 -  show "R <= ntrancl R 0"
1.26 -    unfolding ntrancl_def by fastforce
1.27 -next
1.28 -  {
1.29 -    fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
1.30 -  }
1.31 -  from this show "ntrancl R 0 <= R"
1.32 -    unfolding ntrancl_def by auto
1.33 -qed
1.34 -
1.35  lemma [code]:
1.36 -  "ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
1.37 -proof
1.38 -  {
1.39 -    fix a b
1.40 -    assume "(a, b) : ntrancl R (Suc n)"
1.41 -    from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
1.42 -      unfolding ntrancl_def by auto
1.43 -    have "(a, b) : ntrancl R n O (Id Un R)"
1.44 -    proof (cases "i = 1")
1.45 -      case True
1.46 -      from this `(a, b) : R ^^ i` show ?thesis
1.47 -        unfolding ntrancl_def by auto
1.48 -    next
1.49 -      case False
1.50 -      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
1.51 -        by (cases i) auto
1.52 -      from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
1.53 -        by auto
1.54 -      from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
1.55 -        unfolding ntrancl_def by fastforce
1.56 -      from this c2 show ?thesis by fastforce
1.57 -    qed
1.58 -  }
1.59 -  from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
1.60 -next
1.61 -  show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
1.62 -    unfolding ntrancl_def by fastforce
1.63 -qed
1.64 +  "card R = length (filter R enum)"
1.65 +  by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
1.66
1.67 -lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
1.68 -by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
1.69 -
1.70 -(* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
1.71 -lemma [code]: "r^* = (r^+)^="
1.72 -by simp
1.73
1.74  subsection {* Closing up *}
1.75
```