--- a/src/HOL/Enum.thy Thu Oct 09 22:43:48 2014 +0200
+++ b/src/HOL/Enum.thy Fri Oct 10 19:55:32 2014 +0200
@@ -681,7 +681,7 @@
instance finite_2 :: complete_linorder ..
-instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, semiring_div_parity, sgn_if}" begin
+instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
definition [simp]: "0 = a\<^sub>1"
definition [simp]: "1 = a\<^sub>2"
definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
@@ -701,6 +701,14 @@
split: finite_2.splits)
end
+lemma two_finite_2 [simp]:
+ "2 = a\<^sub>1"
+ by (simp add: numeral.simps plus_finite_2_def)
+
+instance finite_2 :: semiring_div_parity
+by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
+
+
hide_const (open) a\<^sub>1 a\<^sub>2
datatype (plugins only: code "quickcheck*" extraction) finite_3 =
@@ -826,6 +834,8 @@
split: finite_3.splits)
end
+
+
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
datatype (plugins only: code "quickcheck*" extraction) finite_4 =