--- 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:
--- 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 =