# HG changeset patch
# User haftmann
# Date 1412963732 -7200
# Node ID cd63a4b12a33909e901c937aed73a5717d769fe4
# Parent  94bef115c08f2764bdcebb51d399a499b1fbdd49
specialized specification: avoid trivial instances

diff -r 94bef115c08f -r cd63a4b12a33 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 09 22:43:48 2014 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 10 19:55:32 2014 +0200
@@ -506,6 +506,7 @@
 
 class semiring_div_parity = semiring_div + semiring_numeral +
   assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
+  assumes one_mod_two_eq_one: "1 mod 2 = 1"
 begin
 
 lemma parity_cases [case_names even odd]:
@@ -569,6 +570,9 @@
     with discrete have "2 \<le> a mod 2" by simp
     with `a mod 2 < 2` show False by simp
   qed
+next
+  show "1 mod 2 = 1"
+    by (rule mod_less) simp_all
 qed
 
 lemma divmod_digit_1:
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) \<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 =