author bulwahn Mon Oct 03 14:43:14 2011 +0200 (2011-10-03 ago) changeset 45117 3911cf09899a parent 45116 f947eeef6b6f child 45118 7462f287189a
adding code equations for cardinality and (reflexive) transitive closure on finite types
 src/HOL/Enum.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Enum.thy	Mon Oct 03 14:43:13 2011 +0200
1.2 +++ b/src/HOL/Enum.thy	Mon Oct 03 14:43:14 2011 +0200
1.3 @@ -758,12 +758,78 @@
1.4      unfolding enum_the_def by (auto split: list.split)
1.5  qed
1.6
1.7 +subsection {* An executable card operator on finite types *}
1.8 +
1.9 +lemma
1.10 +  [code]: "card R = length (filter R enum)"
1.11 +by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
1.12 +
1.13 +subsection {* An executable (reflexive) transitive closure on finite relations *}
1.14 +
1.15 +text {* Definitions could be moved to Transitive_Closure if they are of more general use. *}
1.16 +
1.17 +definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
1.18 +where
1.19 + [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
1.20 +
1.21 +lemma [code]:
1.22 +  "ntrancl (R :: 'a * 'a => bool) 0 = R"
1.23 +proof
1.24 +  show "R <= ntrancl R 0"
1.25 +    unfolding ntrancl_def by fastforce
1.26 +next
1.27 +  {
1.28 +    fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
1.29 +  }
1.30 +  from this show "ntrancl R 0 <= R"
1.31 +    unfolding ntrancl_def by auto
1.32 +qed
1.33 +
1.34 +lemma [code]:
1.35 +  "ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
1.36 +proof
1.37 +  {
1.38 +    fix a b
1.39 +    assume "(a, b) : ntrancl R (Suc n)"
1.40 +    from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
1.41 +      unfolding ntrancl_def by auto
1.42 +    have "(a, b) : ntrancl R n O (Id Un R)"
1.43 +    proof (cases "i = 1")
1.44 +      case True
1.45 +      from this `(a, b) : R ^^ i` show ?thesis
1.46 +        unfolding ntrancl_def by auto
1.47 +    next
1.48 +      case False
1.49 +      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
1.50 +        by (cases i) auto
1.51 +      from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
1.52 +        by auto
1.53 +      from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
1.54 +        unfolding ntrancl_def by fastforce
1.55 +      from this c2 show ?thesis by fastforce
1.56 +    qed
1.57 +  }
1.58 +  from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
1.59 +next
1.60 +  show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
1.61 +    unfolding ntrancl_def by fastforce
1.62 +qed
1.63 +
1.64 +lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
1.65 +by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
1.66 +
1.67 +(* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
1.68 +lemma [code]: "r^* = (r^+)^="
1.69 +by simp
1.70 +
1.71 +subsection {* Closing up *}
1.72 +
1.73  code_abort enum_the
1.74
1.75  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
1.76
1.77
1.78  hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
1.79 -hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
1.80 +hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
1.81
1.82  end
```