adding code equation for function equality; adding some instantiations for the finite types
authorbulwahn
Mon Nov 22 11:34:57 2010 +0100 (2010-11-22)
changeset 406519752ba7348b5
parent 40650 d40b347d5b0b
child 40652 7bdfc1d6b143
adding code equation for function equality; adding some instantiations for the finite types
src/HOL/Enum.thy
     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