# HG changeset patch
# User bulwahn
# Date 1290422097 -3600
# Node ID 9752ba7348b5dd7c437328c3aad8e32bb01c45a6
# Parent  d40b347d5b0b8c2f8b904b0b1b260fa46349858b
adding code equation for function equality; adding some instantiations for the finite types

diff -r d40b347d5b0b -r 9752ba7348b5 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Nov 22 11:34:56 2010 +0100
+++ b/src/HOL/Enum.thy	Mon Nov 22 11:34:57 2010 +0100
@@ -50,6 +50,10 @@
   "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
   by (fact equal_refl)
 
+lemma [code]:
+  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
+by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
+
 lemma order_fun [code]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -322,6 +326,25 @@
 
 end
 
+instantiation finite_1 :: linorder
+begin
+
+definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
+where
+  "less_eq_finite_1 x y = True"
+
+definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
+where
+  "less_finite_1 x y = False"
+
+instance
+apply (intro_classes)
+apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
+apply (metis finite_1.exhaust)
+done
+
+end
+
 datatype finite_2 = a\<^isub>1 | a\<^isub>2
 
 instantiation finite_2 :: enum
@@ -335,6 +358,27 @@
 
 end
 
+instantiation finite_2 :: linorder
+begin
+
+definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
+where
+  "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
+
+definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
+where
+  "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
+
+
+instance
+apply (intro_classes)
+apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
+apply (metis finite_2.distinct finite_2.nchotomy)+
+done
+
+end
+
+
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
 instantiation finite_3 :: enum
@@ -348,6 +392,25 @@
 
 end
 
+instantiation finite_3 :: linorder
+begin
+
+definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
+where
+  "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
+     | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
+
+definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
+where
+  "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
+
+
+instance proof (intro_classes)
+qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
+
+end
+
+
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
 instantiation finite_4 :: enum
@@ -361,6 +424,8 @@
 
 end
 
+
+
 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
 
 instantiation finite_5 :: enum
@@ -375,5 +440,6 @@
 end
 
 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
+hide_const (open) n_lists product
 
 end