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.22 +by (simp add: dvd_def)
    1.23 +
    1.24 +lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
    1.25 +by (simp add: dvd_def)
    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 =