src/HOL/Nat.thy
 changeset 33274 b6ff7db522b5 parent 32772 50d090ca93f8 child 33364 2bd12592c5e8
```     1.1 --- a/src/HOL/Nat.thy	Wed Oct 28 12:21:38 2009 +0000
1.2 +++ b/src/HOL/Nat.thy	Wed Oct 28 17:44:03 2009 +0100
1.3 @@ -8,7 +8,7 @@
1.4  header {* Natural numbers *}
1.5
1.6  theory Nat
1.7 -imports Inductive Ring_and_Field
1.8 +imports Inductive Product_Type Ring_and_Field
1.9  uses
1.10    "~~/src/Tools/rat.ML"
1.11    "~~/src/Provers/Arith/cancel_sums.ML"
1.12 @@ -1600,6 +1600,75 @@
1.13  Least_Suc}, since there appears to be no need.*}
1.14
1.15
1.16 +subsection {* The divides relation on @{typ nat} *}
1.17 +
1.18 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
1.19 +unfolding dvd_def by simp
1.20 +
1.21 +lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
1.23 +
1.24 +lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
1.26 +
1.27 +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
1.28 +  unfolding dvd_def
1.29 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
1.30 +
1.31 +text {* @{term "op dvd"} is a partial order *}
1.32 +
1.33 +interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
1.34 +  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
1.35 +
1.36 +lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
1.37 +unfolding dvd_def
1.38 +by (blast intro: diff_mult_distrib2 [symmetric])
1.39 +
1.40 +lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
1.41 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
1.42 +  apply (blast intro: dvd_add)
1.43 +  done
1.44 +
1.45 +lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
1.46 +by (drule_tac m = m in dvd_diff_nat, auto)
1.47 +
1.48 +lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
1.49 +  apply (rule iffI)
1.50 +   apply (erule_tac [2] dvd_add)
1.51 +   apply (rule_tac [2] dvd_refl)
1.52 +  apply (subgoal_tac "n = (n+k) -k")
1.53 +   prefer 2 apply simp
1.54 +  apply (erule ssubst)
1.55 +  apply (erule dvd_diff_nat)
1.56 +  apply (rule dvd_refl)
1.57 +  done
1.58 +
1.59 +lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
1.60 +  unfolding dvd_def
1.61 +  apply (erule exE)
1.62 +  apply (simp add: mult_ac)
1.63 +  done
1.64 +
1.65 +lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
1.66 +  apply auto
1.67 +   apply (subgoal_tac "m*n dvd m*1")
1.68 +   apply (drule dvd_mult_cancel, auto)
1.69 +  done
1.70 +
1.71 +lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
1.72 +  apply (subst mult_commute)
1.73 +  apply (erule dvd_mult_cancel1)
1.74 +  done
1.75 +
1.76 +lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
1.77 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
1.78 +
1.79 +lemma nat_dvd_not_less:
1.80 +  fixes m n :: nat
1.81 +  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
1.82 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
1.83 +
1.84 +
1.85  subsection {* size of a datatype value *}
1.86
1.87  class size =
```