src/HOL/Divides.thy
 changeset 66815 93c6632ddf44 parent 66814 a24cde9588bb child 66816 212a3334e7da
```     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -6,7 +6,7 @@
1.4  section \<open>More on quotient and remainder\<close>
1.5
1.6  theory Divides
1.7 -imports Parity
1.8 +imports Parity Nat_Transfer
1.9  begin
1.10
1.11  subsection \<open>Numeral division with a pragmatic type class\<close>
1.12 @@ -19,7 +19,7 @@
1.13    and less technical class hierarchy.
1.14  \<close>
1.15
1.16 -class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
1.17 +class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
1.18    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
1.19      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
1.20      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
1.21 @@ -40,29 +40,6 @@
1.22      yields a significant speedup.\<close>
1.23  begin
1.24
1.25 -subclass unique_euclidean_semiring_parity
1.26 -proof
1.27 -  fix a
1.28 -  show "a mod 2 = 0 \<or> a mod 2 = 1"
1.29 -  proof (rule ccontr)
1.30 -    assume "\<not> (a mod 2 = 0 \<or> a mod 2 = 1)"
1.31 -    then have "a mod 2 \<noteq> 0" and "a mod 2 \<noteq> 1" by simp_all
1.32 -    have "0 < 2" by simp
1.33 -    with pos_mod_bound pos_mod_sign have "0 \<le> a mod 2" "a mod 2 < 2" by simp_all
1.34 -    with \<open>a mod 2 \<noteq> 0\<close> have "0 < a mod 2" by simp
1.35 -    with discrete have "1 \<le> a mod 2" by simp
1.36 -    with \<open>a mod 2 \<noteq> 1\<close> have "1 < a mod 2" by simp
1.37 -    with discrete have "2 \<le> a mod 2" by simp
1.38 -    with \<open>a mod 2 < 2\<close> show False by simp
1.39 -  qed
1.40 -next
1.41 -  show "1 mod 2 = 1"
1.42 -    by (rule mod_less) simp_all
1.43 -next
1.44 -  show "0 \<noteq> 2"
1.45 -    by simp
1.46 -qed
1.47 -
1.48  lemma divmod_digit_1:
1.49    assumes "0 \<le> a" "0 < b" and "b \<le> a mod (2 * b)"
1.50    shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
1.51 @@ -74,7 +51,7 @@
1.52    then have [simp]: "1 \<le> a div b" by (simp add: discrete)
1.53    with \<open>0 < b\<close> have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
1.54    define w where "w = a div b mod 2"
1.55 -  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
1.56 +  then have w_exhaust: "w = 0 \<or> w = 1" by auto
1.57    have mod_w: "a mod (2 * b) = a mod b + b * w"
1.58      by (simp add: w_def mod_mult2_eq ac_simps)
1.59    from assms w_exhaust have "w = 1"
1.60 @@ -93,7 +70,7 @@
1.61      and "a mod (2 * b) = a mod b" (is "?Q")
1.62  proof -
1.63    define w where "w = a div b mod 2"
1.64 -  with parity have w_exhaust: "w = 0 \<or> w = 1" by auto
1.65 +  then have w_exhaust: "w = 0 \<or> w = 1" by auto
1.66    have mod_w: "a mod (2 * b) = a mod b + b * w"
1.67      by (simp add: w_def mod_mult2_eq ac_simps)
1.68    moreover have "b \<le> a mod b + b"
1.69 @@ -318,60 +295,6 @@
1.70
1.71  declare divmod_algorithm_code [where ?'a = nat, code]
1.72
1.73 -lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
1.74 -  by (auto elim: oddE)
1.75 -
1.76 -lemma even_Suc_div_two [simp]:
1.77 -  "even n \<Longrightarrow> Suc n div 2 = n div 2"
1.78 -  using even_succ_div_two [of n] by simp
1.79 -
1.80 -lemma odd_Suc_div_two [simp]:
1.81 -  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1.82 -  using odd_succ_div_two [of n] by simp
1.83 -
1.84 -lemma odd_two_times_div_two_nat [simp]:
1.85 -  assumes "odd n"
1.86 -  shows "2 * (n div 2) = n - (1 :: nat)"
1.87 -proof -
1.88 -  from assms have "2 * (n div 2) + 1 = n"
1.89 -    by (rule odd_two_times_div_two_succ)
1.90 -  then have "Suc (2 * (n div 2)) - 1 = n - 1"
1.91 -    by simp
1.92 -  then show ?thesis
1.93 -    by simp
1.94 -qed
1.95 -
1.96 -lemma parity_induct [case_names zero even odd]:
1.97 -  assumes zero: "P 0"
1.98 -  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1.99 -  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1.100 -  shows "P n"
1.101 -proof (induct n rule: less_induct)
1.102 -  case (less n)
1.103 -  show "P n"
1.104 -  proof (cases "n = 0")
1.105 -    case True with zero show ?thesis by simp
1.106 -  next
1.107 -    case False
1.108 -    with less have hyp: "P (n div 2)" by simp
1.109 -    show ?thesis
1.110 -    proof (cases "even n")
1.111 -      case True
1.112 -      with hyp even [of "n div 2"] show ?thesis
1.113 -        by simp
1.114 -    next
1.115 -      case False
1.116 -      with hyp odd [of "n div 2"] show ?thesis
1.117 -        by simp
1.118 -    qed
1.119 -  qed
1.120 -qed
1.121 -
1.122 -lemma mod_2_not_eq_zero_eq_one_nat:
1.123 -  fixes n :: nat
1.124 -  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
1.125 -  by (fact not_mod_2_eq_0_eq_1)
1.126 -
1.127  lemma Suc_0_div_numeral [simp]:
1.128    fixes k l :: num
1.129    shows "Suc 0 div numeral k = fst (divmod Num.One k)"
1.130 @@ -708,6 +631,39 @@
1.131
1.132  text\<open>There is no \<open>mod_neg_pos_trivial\<close>.\<close>
1.133
1.134 +instance int :: ring_parity
1.135 +proof
1.136 +  fix k l :: int
1.137 +  show "k mod 2 = 1" if "\<not> 2 dvd k"
1.138 +  proof (rule order_antisym)
1.139 +    have "0 \<le> k mod 2" and "k mod 2 < 2"
1.140 +      by auto
1.141 +    moreover have "k mod 2 \<noteq> 0"
1.142 +      using that by (simp add: dvd_eq_mod_eq_0)
1.143 +    ultimately have "0 < k mod 2"
1.144 +      by (simp only: less_le) simp
1.145 +    then show "1 \<le> k mod 2"
1.146 +      by simp
1.147 +    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
1.148 +      by (simp only: less_le) simp
1.149 +  qed
1.150 +qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
1.151 +
1.152 +lemma even_diff_iff [simp]:
1.153 +  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
1.154 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.155 +
1.156 +lemma even_abs_add_iff [simp]:
1.157 +  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
1.158 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
1.159 +
1.160 +lemma even_add_abs_iff [simp]:
1.161 +  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
1.162 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
1.163 +
1.164 +lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
1.165 +  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
1.166 +
1.167
1.168  subsubsection \<open>Laws for div and mod with Unary Minus\<close>
1.169
1.170 @@ -1495,4 +1451,18 @@
1.171    then show ?thesis ..
1.172  qed
1.173
1.174 +lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
1.175 +
1.176 +lemma mod_2_not_eq_zero_eq_one_nat:
1.177 +  fixes n :: nat
1.178 +  shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
1.179 +  by (fact not_mod_2_eq_0_eq_1)
1.180 +
1.181 +lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
1.182 +  by (fact even_of_nat)
1.183 +
1.184 +text \<open>Tool setup\<close>
1.185 +
1.186 +declare transfer_morphism_int_nat [transfer add return: even_int_iff]
1.187 +
1.188  end
```