diff -r 94bef115c08f -r cd63a4b12a33 src/HOL/Enum.thy --- 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) \ a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \ a\<^sub>1 | _ \ 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 =