moved lemmas for dvd on nat to theories Nat and Power
authorhaftmann
Wed Oct 28 17:44:03 2009 +0100 (2009-10-28)
changeset 33274b6ff7db522b5
parent 33273 9290fbf0a30e
child 33275 b497b2574bf6
moved lemmas for dvd on nat to theories Nat and Power
src/HOL/Divides.thy
src/HOL/Nat.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Oct 28 12:21:38 2009 +0000
     1.2 +++ b/src/HOL/Divides.thy	Wed Oct 28 17:44:03 2009 +0100
     1.3 @@ -178,6 +178,9 @@
     1.4  lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
     1.5  by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
     1.6  
     1.7 +lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b"
     1.8 +by (drule dvd_div_mult_self) (simp add: mult_commute)
     1.9 +
    1.10  lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a"
    1.11  apply (cases "a = 0")
    1.12   apply simp
    1.13 @@ -866,79 +869,6 @@
    1.14  apply (auto simp add: Suc_diff_le le_mod_geq)
    1.15  done
    1.16  
    1.17 -
    1.18 -subsubsection {* The Divides Relation *}
    1.19 -
    1.20 -lemma dvd_1_left [iff]: "Suc 0 dvd k"
    1.21 -  unfolding dvd_def by simp
    1.22 -
    1.23 -lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
    1.24 -by (simp add: dvd_def)
    1.25 -
    1.26 -lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
    1.27 -by (simp add: dvd_def)
    1.28 -
    1.29 -lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
    1.30 -  unfolding dvd_def
    1.31 -  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
    1.32 -
    1.33 -text {* @{term "op dvd"} is a partial order *}
    1.34 -
    1.35 -interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
    1.36 -  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    1.37 -
    1.38 -lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    1.39 -unfolding dvd_def
    1.40 -by (blast intro: diff_mult_distrib2 [symmetric])
    1.41 -
    1.42 -lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
    1.43 -  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    1.44 -  apply (blast intro: dvd_add)
    1.45 -  done
    1.46 -
    1.47 -lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
    1.48 -by (drule_tac m = m in dvd_diff_nat, auto)
    1.49 -
    1.50 -lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    1.51 -  apply (rule iffI)
    1.52 -   apply (erule_tac [2] dvd_add)
    1.53 -   apply (rule_tac [2] dvd_refl)
    1.54 -  apply (subgoal_tac "n = (n+k) -k")
    1.55 -   prefer 2 apply simp
    1.56 -  apply (erule ssubst)
    1.57 -  apply (erule dvd_diff_nat)
    1.58 -  apply (rule dvd_refl)
    1.59 -  done
    1.60 -
    1.61 -lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
    1.62 -  unfolding dvd_def
    1.63 -  apply (erule exE)
    1.64 -  apply (simp add: mult_ac)
    1.65 -  done
    1.66 -
    1.67 -lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
    1.68 -  apply auto
    1.69 -   apply (subgoal_tac "m*n dvd m*1")
    1.70 -   apply (drule dvd_mult_cancel, auto)
    1.71 -  done
    1.72 -
    1.73 -lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
    1.74 -  apply (subst mult_commute)
    1.75 -  apply (erule dvd_mult_cancel1)
    1.76 -  done
    1.77 -
    1.78 -lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
    1.79 -  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    1.80 -
    1.81 -lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
    1.82 -  by (simp add: dvd_eq_mod_eq_0 mult_div_cancel)
    1.83 -
    1.84 -lemma power_dvd_imp_le:
    1.85 -  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
    1.86 -  apply (rule power_le_imp_le_exp, assumption)
    1.87 -  apply (erule dvd_imp_le, simp)
    1.88 -  done
    1.89 -
    1.90  lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
    1.91  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    1.92  
    1.93 @@ -1162,9 +1092,4 @@
    1.94    with j show ?thesis by blast
    1.95  qed
    1.96  
    1.97 -lemma nat_dvd_not_less:
    1.98 -  fixes m n :: nat
    1.99 -  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
   1.100 -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.101 -
   1.102  end
     2.1 --- a/src/HOL/Nat.thy	Wed Oct 28 12:21:38 2009 +0000
     2.2 +++ b/src/HOL/Nat.thy	Wed Oct 28 17:44:03 2009 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Natural numbers *}
     2.5  
     2.6  theory Nat
     2.7 -imports Inductive Ring_and_Field
     2.8 +imports Inductive Product_Type Ring_and_Field
     2.9  uses
    2.10    "~~/src/Tools/rat.ML"
    2.11    "~~/src/Provers/Arith/cancel_sums.ML"
    2.12 @@ -1600,6 +1600,75 @@
    2.13  Least_Suc}, since there appears to be no need.*}
    2.14  
    2.15  
    2.16 +subsection {* The divides relation on @{typ nat} *}
    2.17 +
    2.18 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
    2.19 +unfolding dvd_def by simp
    2.20 +
    2.21 +lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
    2.22 +by (simp add: dvd_def)
    2.23 +
    2.24 +lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
    2.25 +by (simp add: dvd_def)
    2.26 +
    2.27 +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
    2.28 +  unfolding dvd_def
    2.29 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
    2.30 +
    2.31 +text {* @{term "op dvd"} is a partial order *}
    2.32 +
    2.33 +interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
    2.34 +  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    2.35 +
    2.36 +lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    2.37 +unfolding dvd_def
    2.38 +by (blast intro: diff_mult_distrib2 [symmetric])
    2.39 +
    2.40 +lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
    2.41 +  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    2.42 +  apply (blast intro: dvd_add)
    2.43 +  done
    2.44 +
    2.45 +lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
    2.46 +by (drule_tac m = m in dvd_diff_nat, auto)
    2.47 +
    2.48 +lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    2.49 +  apply (rule iffI)
    2.50 +   apply (erule_tac [2] dvd_add)
    2.51 +   apply (rule_tac [2] dvd_refl)
    2.52 +  apply (subgoal_tac "n = (n+k) -k")
    2.53 +   prefer 2 apply simp
    2.54 +  apply (erule ssubst)
    2.55 +  apply (erule dvd_diff_nat)
    2.56 +  apply (rule dvd_refl)
    2.57 +  done
    2.58 +
    2.59 +lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
    2.60 +  unfolding dvd_def
    2.61 +  apply (erule exE)
    2.62 +  apply (simp add: mult_ac)
    2.63 +  done
    2.64 +
    2.65 +lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
    2.66 +  apply auto
    2.67 +   apply (subgoal_tac "m*n dvd m*1")
    2.68 +   apply (drule dvd_mult_cancel, auto)
    2.69 +  done
    2.70 +
    2.71 +lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
    2.72 +  apply (subst mult_commute)
    2.73 +  apply (erule dvd_mult_cancel1)
    2.74 +  done
    2.75 +
    2.76 +lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
    2.77 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    2.78 +
    2.79 +lemma nat_dvd_not_less:
    2.80 +  fixes m n :: nat
    2.81 +  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
    2.82 +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
    2.83 +
    2.84 +
    2.85  subsection {* size of a datatype value *}
    2.86  
    2.87  class size =
     3.1 --- a/src/HOL/Power.thy	Wed Oct 28 12:21:38 2009 +0000
     3.2 +++ b/src/HOL/Power.thy	Wed Oct 28 17:44:03 2009 +0100
     3.3 @@ -452,6 +452,12 @@
     3.4    from power_strict_increasing_iff [OF this] less show ?thesis ..
     3.5  qed
     3.6  
     3.7 +lemma power_dvd_imp_le:
     3.8 +  "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
     3.9 +  apply (rule power_le_imp_le_exp, assumption)
    3.10 +  apply (erule dvd_imp_le, simp)
    3.11 +  done
    3.12 +
    3.13  
    3.14  subsection {* Code generator tweak *}
    3.15