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