src/HOL/Enum.thy

 end
 
 lemma [code nbe]:
   "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"
     and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"

 instance proof
 qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
 
 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
 begin
 

 instance proof
 qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
 
 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
 begin
 

 instance proof
 qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
 
 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
 begin
 

 instance proof
 qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
 
 end
 
+
+
 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
 
 instantiation finite_5 :: enum
 begin
 

 qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
 
 end
 
 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
-
-end
+hide_const (open) n_lists product
+
+end