src/HOL/Enum.thy
 changeset 40651 9752ba7348b5 parent 40650 d40b347d5b0b child 40652 7bdfc1d6b143
```     1.1 --- a/src/HOL/Enum.thy	Mon Nov 22 11:34:56 2010 +0100
1.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:57 2010 +0100
1.3 @@ -50,6 +50,10 @@
1.4    "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
1.5    by (fact equal_refl)
1.6
1.7 +lemma [code]:
1.8 +  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
1.9 +by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
1.10 +
1.11  lemma order_fun [code]:
1.12    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
1.13    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
1.14 @@ -322,6 +326,25 @@
1.15
1.16  end
1.17
1.18 +instantiation finite_1 :: linorder
1.19 +begin
1.20 +
1.21 +definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
1.22 +where
1.23 +  "less_eq_finite_1 x y = True"
1.24 +
1.25 +definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
1.26 +where
1.27 +  "less_finite_1 x y = False"
1.28 +
1.29 +instance
1.30 +apply (intro_classes)
1.31 +apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
1.32 +apply (metis finite_1.exhaust)
1.33 +done
1.34 +
1.35 +end
1.36 +
1.37  datatype finite_2 = a\<^isub>1 | a\<^isub>2
1.38
1.39  instantiation finite_2 :: enum
1.40 @@ -335,6 +358,27 @@
1.41
1.42  end
1.43
1.44 +instantiation finite_2 :: linorder
1.45 +begin
1.46 +
1.47 +definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
1.48 +where
1.49 +  "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
1.50 +
1.51 +definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
1.52 +where
1.53 +  "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
1.54 +
1.55 +
1.56 +instance
1.57 +apply (intro_classes)
1.58 +apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
1.59 +apply (metis finite_2.distinct finite_2.nchotomy)+
1.60 +done
1.61 +
1.62 +end
1.63 +
1.64 +
1.65  datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
1.66
1.67  instantiation finite_3 :: enum
1.68 @@ -348,6 +392,25 @@
1.69
1.70  end
1.71
1.72 +instantiation finite_3 :: linorder
1.73 +begin
1.74 +
1.75 +definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
1.76 +where
1.77 +  "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
1.78 +     | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
1.79 +
1.80 +definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
1.81 +where
1.82 +  "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
1.83 +
1.84 +
1.85 +instance proof (intro_classes)
1.86 +qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
1.87 +
1.88 +end
1.89 +
1.90 +
1.91  datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
1.92
1.93  instantiation finite_4 :: enum
1.94 @@ -361,6 +424,8 @@
1.95
1.96  end
1.97
1.98 +
1.99 +
1.100  datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
1.101
1.102  instantiation finite_5 :: enum
1.103 @@ -375,5 +440,6 @@
1.104  end
1.105
1.106  hide_type finite_1 finite_2 finite_3 finite_4 finite_5
1.107 +hide_const (open) n_lists product
1.108
1.109  end
```