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.89    by (simp add: div_nat_def)
    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.94    by (simp add: mod_nat_def)
    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.99    by (simp add: prod_eq_iff)
   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