specialized specification: avoid trivial instances
authorhaftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646cd63a4b12a33
parent 58645 94bef115c08f
child 58647 fce800afeec7
specialized specification: avoid trivial instances
src/HOL/Divides.thy
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 09 22:43:48 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 10 19:55:32 2014 +0200
     1.3 @@ -506,6 +506,7 @@
     1.4  
     1.5  class semiring_div_parity = semiring_div + semiring_numeral +
     1.6    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     1.7 +  assumes one_mod_two_eq_one: "1 mod 2 = 1"
     1.8  begin
     1.9  
    1.10  lemma parity_cases [case_names even odd]:
    1.11 @@ -569,6 +570,9 @@
    1.12      with discrete have "2 \<le> a mod 2" by simp
    1.13      with `a mod 2 < 2` show False by simp
    1.14    qed
    1.15 +next
    1.16 +  show "1 mod 2 = 1"
    1.17 +    by (rule mod_less) simp_all
    1.18  qed
    1.19  
    1.20  lemma divmod_digit_1:
     2.1 --- a/src/HOL/Enum.thy	Thu Oct 09 22:43:48 2014 +0200
     2.2 +++ b/src/HOL/Enum.thy	Fri Oct 10 19:55:32 2014 +0200
     2.3 @@ -681,7 +681,7 @@
     2.4  
     2.5  instance finite_2 :: complete_linorder ..
     2.6  
     2.7 -instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, semiring_div_parity, sgn_if}" begin
     2.8 +instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, sgn_if, semiring_div}" begin
     2.9  definition [simp]: "0 = a\<^sub>1"
    2.10  definition [simp]: "1 = a\<^sub>2"
    2.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)"
    2.12 @@ -701,6 +701,14 @@
    2.13       split: finite_2.splits)
    2.14  end
    2.15  
    2.16 +lemma two_finite_2 [simp]:
    2.17 +  "2 = a\<^sub>1"
    2.18 +  by (simp add: numeral.simps plus_finite_2_def)
    2.19 +  
    2.20 +instance finite_2 :: semiring_div_parity
    2.21 +by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
    2.22 +
    2.23 +
    2.24  hide_const (open) a\<^sub>1 a\<^sub>2
    2.25  
    2.26  datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    2.27 @@ -826,6 +834,8 @@
    2.28       split: finite_3.splits)
    2.29  end
    2.30  
    2.31 +
    2.32 +
    2.33  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    2.34  
    2.35  datatype (plugins only: code "quickcheck*" extraction) finite_4 =