src/HOL/Enum.thy
changeset 58646 cd63a4b12a33
parent 58350 919149921e46
child 58659 6c9821c32dd5
     1.1 --- a/src/HOL/Enum.thy	Thu Oct 09 22:43:48 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Oct 10 19:55:32 2014 +0200
     1.3 @@ -681,7 +681,7 @@
     1.4  
     1.5  instance finite_2 :: complete_linorder ..
     1.6  
     1.7 -instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, semiring_div_parity, sgn_if}" begin
     1.8 +instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
     1.9  definition [simp]: "0 = a\<^sub>1"
    1.10  definition [simp]: "1 = a\<^sub>2"
    1.11  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)"
    1.12 @@ -701,6 +701,14 @@
    1.13       split: finite_2.splits)
    1.14  end
    1.15  
    1.16 +lemma two_finite_2 [simp]:
    1.17 +  "2 = a\<^sub>1"
    1.18 +  by (simp add: numeral.simps plus_finite_2_def)
    1.19 +  
    1.20 +instance finite_2 :: semiring_div_parity
    1.21 +by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
    1.22 +
    1.23 +
    1.24  hide_const (open) a\<^sub>1 a\<^sub>2
    1.25  
    1.26  datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    1.27 @@ -826,6 +834,8 @@
    1.28       split: finite_3.splits)
    1.29  end
    1.30  
    1.31 +
    1.32 +
    1.33  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    1.34  
    1.35  datatype (plugins only: code "quickcheck*" extraction) finite_4 =