# HG changeset patch
# User haftmann
# Date 1383216260 -3600
# Node ID e3df2a4e02fc4dc6894fab06ce22e9daebd4a4fd
# Parent  8a49a5a302840909a31df7409ee36ec78ace691e
explicit type class for modelling even/odd parity

diff -r 8a49a5a30284 -r e3df2a4e02fc src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -509,6 +509,26 @@
 
 end
 
+class semiring_div_parity = semiring_div + semiring_numeral +
+  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
+begin
+
+lemma parity_cases [case_names even odd]:
+  assumes "a mod 2 = 0 \<Longrightarrow> P"
+  assumes "a mod 2 = 1 \<Longrightarrow> P"
+  shows P
+  using assms parity by blast
+
+lemma not_mod_2_eq_0_eq_1 [simp]:
+  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
+  by (cases a rule: parity_cases) simp_all
+
+lemma not_mod_2_eq_1_eq_0 [simp]:
+  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
+  by (cases a rule: parity_cases) simp_all
+
+end
+
 
 subsection {* Generic numeral division with a pragmatic type class *}
 
@@ -520,7 +540,6 @@
   and less technical class hierarchy.
 *}
 
-
 class semiring_numeral_div = linordered_semidom + minus + semiring_div +
   assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
     and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
@@ -540,18 +559,21 @@
   "a - 0 = a"
   by (rule diff_invert_add1 [symmetric]) simp
 
-lemma parity:
-  "a mod 2 = 0 \<or> a mod 2 = 1"
-proof (rule ccontr)
-  assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
-  then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
-  have "0 < 2" by simp
-  with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
-  with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
-  with discrete have "1 \<le> a mod 2" by simp
-  with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
-  with discrete have "2 \<le> a mod 2" by simp
-  with `a mod 2 < 2` show False by simp
+subclass semiring_div_parity
+proof
+  fix a
+  show "a mod 2 = 0 \<or> a mod 2 = 1"
+  proof (rule ccontr)
+    assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
+    then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
+    have "0 < 2" by simp
+    with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
+    with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
+    with discrete have "1 \<le> a mod 2" by simp
+    with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
+    with discrete have "2 \<le> a mod 2" by simp
+    with `a mod 2 < 2` show False by simp
+  qed
 qed
 
 lemma divmod_digit_1: