author bulwahn Mon, 22 Nov 2010 11:34:57 +0100 changeset 40651 9752ba7348b5 parent 40650 d40b347d5b0b child 40652 7bdfc1d6b143
adding code equation for function equality; adding some instantiations for the finite types
 src/HOL/Enum.thy file | annotate | diff | comparison | revisions
```--- 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```