src/HOL/Divides.thy
changeset 54226 e3df2a4e02fc
parent 54221 56587960e444
child 54227 63b441f49645
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -509,6 +509,26 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class semiring_div_parity = semiring_div + semiring_numeral +
     1.8 +  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     1.9 +begin
    1.10 +
    1.11 +lemma parity_cases [case_names even odd]:
    1.12 +  assumes "a mod 2 = 0 \<Longrightarrow> P"
    1.13 +  assumes "a mod 2 = 1 \<Longrightarrow> P"
    1.14 +  shows P
    1.15 +  using assms parity by blast
    1.16 +
    1.17 +lemma not_mod_2_eq_0_eq_1 [simp]:
    1.18 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
    1.19 +  by (cases a rule: parity_cases) simp_all
    1.20 +
    1.21 +lemma not_mod_2_eq_1_eq_0 [simp]:
    1.22 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    1.23 +  by (cases a rule: parity_cases) simp_all
    1.24 +
    1.25 +end
    1.26 +
    1.27  
    1.28  subsection {* Generic numeral division with a pragmatic type class *}
    1.29  
    1.30 @@ -520,7 +540,6 @@
    1.31    and less technical class hierarchy.
    1.32  *}
    1.33  
    1.34 -
    1.35  class semiring_numeral_div = linordered_semidom + minus + semiring_div +
    1.36    assumes diff_invert_add1: "a + b = c \<Longrightarrow> a = c - b"
    1.37      and le_add_diff_inverse2: "b \<le> a \<Longrightarrow> a - b + b = a"
    1.38 @@ -540,18 +559,21 @@
    1.39    "a - 0 = a"
    1.40    by (rule diff_invert_add1 [symmetric]) simp
    1.41  
    1.42 -lemma parity:
    1.43 -  "a mod 2 = 0 \<or> a mod 2 = 1"
    1.44 -proof (rule ccontr)
    1.45 -  assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
    1.46 -  then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
    1.47 -  have "0 < 2" by simp
    1.48 -  with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
    1.49 -  with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
    1.50 -  with discrete have "1 \<le> a mod 2" by simp
    1.51 -  with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
    1.52 -  with discrete have "2 \<le> a mod 2" by simp
    1.53 -  with `a mod 2 < 2` show False by simp
    1.54 +subclass semiring_div_parity
    1.55 +proof
    1.56 +  fix a
    1.57 +  show "a mod 2 = 0 \<or> a mod 2 = 1"
    1.58 +  proof (rule ccontr)
    1.59 +    assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
    1.60 +    then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
    1.61 +    have "0 < 2" by simp
    1.62 +    with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
    1.63 +    with `a mod 2 \<noteq> 0` have "0 < a mod 2" by simp
    1.64 +    with discrete have "1 \<le> a mod 2" by simp
    1.65 +    with `a mod 2 \<noteq> 1` have "1 < a mod 2" by simp
    1.66 +    with discrete have "2 \<le> a mod 2" by simp
    1.67 +    with `a mod 2 < 2` show False by simp
    1.68 +  qed
    1.69  qed
    1.70  
    1.71  lemma divmod_digit_1: