src/HOL/Divides.thy
 changeset 61433 a4c0de1df3d8 parent 61275 053ec04ea866 child 61649 268d88ec9087
```     1.1 --- a/src/HOL/Divides.thy	Thu Oct 15 12:39:51 2015 +0200
1.2 +++ b/src/HOL/Divides.thy	Sat Oct 17 13:18:43 2015 +0200
1.3 @@ -813,6 +813,9 @@
1.4
1.5  subsection \<open>Division on @{typ nat}\<close>
1.6
1.7 +context
1.8 +begin
1.9 +
1.10  text \<open>
1.11    We define @{const divide} and @{const mod} on @{typ nat} by means
1.12    of a characteristic relation with two input arguments
1.13 @@ -827,7 +830,7 @@
1.14
1.15  text \<open>@{const divmod_nat_rel} is total:\<close>
1.16
1.17 -lemma divmod_nat_rel_ex:
1.18 +qualified lemma divmod_nat_rel_ex:
1.19    obtains q r where "divmod_nat_rel m n (q, r)"
1.20  proof (cases "n = 0")
1.21    case True  with that show thesis
1.22 @@ -860,7 +863,7 @@
1.23
1.24  text \<open>@{const divmod_nat_rel} is injective:\<close>
1.25
1.26 -lemma divmod_nat_rel_unique:
1.27 +qualified lemma divmod_nat_rel_unique:
1.28    assumes "divmod_nat_rel m n qr"
1.29      and "divmod_nat_rel m n qr'"
1.30    shows "qr = qr'"
1.31 @@ -887,10 +890,10 @@
1.32    means of @{const divmod_nat_rel}:
1.33  \<close>
1.34
1.35 -definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.36 +qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
1.37    "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
1.38
1.39 -lemma divmod_nat_rel_divmod_nat:
1.40 +qualified lemma divmod_nat_rel_divmod_nat:
1.41    "divmod_nat_rel m n (divmod_nat m n)"
1.42  proof -
1.43    from divmod_nat_rel_ex
1.44 @@ -899,63 +902,65 @@
1.45    by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
1.46  qed
1.47
1.48 -lemma divmod_nat_unique:
1.49 +qualified lemma divmod_nat_unique:
1.50    assumes "divmod_nat_rel m n qr"
1.51    shows "divmod_nat m n = qr"
1.52    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
1.53
1.54 +qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
1.55 +  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
1.56 +
1.57 +qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
1.58 +  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
1.59 +
1.60 +qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
1.61 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.62 +
1.63 +qualified lemma divmod_nat_step:
1.64 +  assumes "0 < n" and "n \<le> m"
1.65 +  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
1.66 +proof (rule divmod_nat_unique)
1.67 +  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
1.68 +    by (fact divmod_nat_rel_divmod_nat)
1.69 +  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
1.70 +    unfolding divmod_nat_rel_def using assms by auto
1.71 +qed
1.72 +
1.73 +end
1.74 +
1.75  instantiation nat :: semiring_div
1.76  begin
1.77
1.78  definition divide_nat where
1.79 -  div_nat_def: "m div n = fst (divmod_nat m n)"
1.80 +  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
1.81
1.82  definition mod_nat where
1.83 -  "m mod n = snd (divmod_nat m n)"
1.84 +  "m mod n = snd (Divides.divmod_nat m n)"
1.85
1.86  lemma fst_divmod_nat [simp]:
1.87 -  "fst (divmod_nat m n) = m div n"
1.88 +  "fst (Divides.divmod_nat m n) = m div n"
1.90
1.91  lemma snd_divmod_nat [simp]:
1.92 -  "snd (divmod_nat m n) = m mod n"
1.93 +  "snd (Divides.divmod_nat m n) = m mod n"
1.95
1.96  lemma divmod_nat_div_mod:
1.97 -  "divmod_nat m n = (m div n, m mod n)"
1.98 +  "Divides.divmod_nat m n = (m div n, m mod n)"
1.100
1.101  lemma div_nat_unique:
1.102    assumes "divmod_nat_rel m n (q, r)"
1.103    shows "m div n = q"
1.104 -  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
1.105 +  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.106
1.107  lemma mod_nat_unique:
1.108    assumes "divmod_nat_rel m n (q, r)"
1.109    shows "m mod n = r"
1.110 -  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
1.111 +  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.112
1.113  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
1.114 -  using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
1.115 -
1.116 -lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
1.117 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.118 -
1.119 -lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
1.120 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.121 -
1.122 -lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
1.123 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.124 -
1.125 -lemma divmod_nat_step:
1.126 -  assumes "0 < n" and "n \<le> m"
1.127 -  shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
1.128 -proof (rule divmod_nat_unique)
1.129 -  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
1.130 -    by (rule divmod_nat_rel)
1.131 -  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
1.132 -    unfolding divmod_nat_rel_def using assms by auto
1.133 -qed
1.134 +  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
1.135
1.136  text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
1.137
1.138 @@ -963,25 +968,25 @@
1.139    fixes m n :: nat
1.140    assumes "m < n"
1.141    shows "m div n = 0"
1.142 -  using assms divmod_nat_base by (simp add: prod_eq_iff)
1.143 +  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
1.144
1.145  lemma le_div_geq:
1.146    fixes m n :: nat
1.147    assumes "0 < n" and "n \<le> m"
1.148    shows "m div n = Suc ((m - n) div n)"
1.149 -  using assms divmod_nat_step by (simp add: prod_eq_iff)
1.150 +  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
1.151
1.152  lemma mod_less [simp]:
1.153    fixes m n :: nat
1.154    assumes "m < n"
1.155    shows "m mod n = m"
1.156 -  using assms divmod_nat_base by (simp add: prod_eq_iff)
1.157 +  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
1.158
1.159  lemma le_mod_geq:
1.160    fixes m n :: nat
1.161    assumes "n \<le> m"
1.162    shows "m mod n = (m - n) mod n"
1.163 -  using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
1.164 +  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
1.165
1.166  instance proof
1.167    fix m n :: nat
1.168 @@ -1003,10 +1008,10 @@
1.169    thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
1.170  next
1.171    fix n :: nat show "n div 0 = 0"
1.172 -    by (simp add: div_nat_def divmod_nat_zero)
1.173 +    by (simp add: div_nat_def Divides.divmod_nat_zero)
1.174  next
1.175    fix n :: nat show "0 div n = 0"
1.176 -    by (simp add: div_nat_def divmod_nat_zero_left)
1.177 +    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
1.178  qed
1.179
1.180  end
1.181 @@ -1030,8 +1035,9 @@
1.182
1.183  end
1.184
1.185 -lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1.186 -  let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
1.187 +lemma divmod_nat_if [code]:
1.188 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1.189 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
1.190    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1.191
1.192  text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
1.193 @@ -1347,15 +1353,15 @@
1.194    assume P: ?lhs
1.195    then have "divmod_nat_rel m n (q, m - n * q)"
1.196      unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
1.197 -  with divmod_nat_rel_unique divmod_nat_rel [of m n]
1.198 -  have "(q, m - n * q) = (m div n, m mod n)" by auto
1.199 +  then have "m div n = q"
1.200 +    by (rule div_nat_unique)
1.201    then show ?rhs by simp
1.202  qed
1.203
1.204  theorem split_div':
1.205    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
1.206     (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
1.207 -  apply (case_tac "0 < n")
1.208 +  apply (cases "0 < n")
1.209    apply (simp only: add: split_div_lemma)
1.210    apply simp_all
1.211    done
```