# HG changeset patch # User haftmann # Date 1256748243 -3600 # Node ID b6ff7db522b555c87517c5a3ceb0abdc576174f4 # Parent 9290fbf0a30e9a33afacd48535bf76bbbd0e7e2d moved lemmas for dvd on nat to theories Nat and Power diff -r 9290fbf0a30e -r b6ff7db522b5 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Oct 28 12:21:38 2009 +0000 +++ b/src/HOL/Divides.thy Wed Oct 28 17:44:03 2009 +0100 @@ -178,6 +178,9 @@ lemma dvd_div_mult_self: "a dvd b \ (b div a) * a = b" by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0) +lemma dvd_mult_div_cancel: "a dvd b \ a * (b div a) = b" +by (drule dvd_div_mult_self) (simp add: mult_commute) + lemma dvd_div_mult: "a dvd b \ (b div a) * c = b * c div a" apply (cases "a = 0") apply simp @@ -866,79 +869,6 @@ apply (auto simp add: Suc_diff_le le_mod_geq) done - -subsubsection {* The Divides Relation *} - -lemma dvd_1_left [iff]: "Suc 0 dvd k" - unfolding dvd_def by simp - -lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)" -by (simp add: dvd_def) - -lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \ m = 1" -by (simp add: dvd_def) - -lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)" - unfolding dvd_def - by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) - -text {* @{term "op dvd"} is a partial order *} - -interpretation dvd: order "op dvd" "\n m \ nat. n dvd m \ \ m dvd n" - proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) - -lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" -unfolding dvd_def -by (blast intro: diff_mult_distrib2 [symmetric]) - -lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\m |] ==> k dvd (m::nat)" - apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) - apply (blast intro: dvd_add) - done - -lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\m |] ==> k dvd (n::nat)" -by (drule_tac m = m in dvd_diff_nat, auto) - -lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" - apply (rule iffI) - apply (erule_tac [2] dvd_add) - apply (rule_tac [2] dvd_refl) - apply (subgoal_tac "n = (n+k) -k") - prefer 2 apply simp - apply (erule ssubst) - apply (erule dvd_diff_nat) - apply (rule dvd_refl) - done - -lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0 m dvd n" - unfolding dvd_def - apply (erule exE) - apply (simp add: mult_ac) - done - -lemma dvd_mult_cancel1: "0 (m*n dvd m) = (n = (1::nat))" - apply auto - apply (subgoal_tac "m*n dvd m*1") - apply (drule dvd_mult_cancel, auto) - done - -lemma dvd_mult_cancel2: "0 (n*m dvd m) = (n = (1::nat))" - apply (subst mult_commute) - apply (erule dvd_mult_cancel1) - done - -lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \ (n::nat)" - by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) - -lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)" - by (simp add: dvd_eq_mod_eq_0 mult_div_cancel) - -lemma power_dvd_imp_le: - "i ^ m dvd i ^ n \ (1::nat) < i \ m \ n" - apply (rule power_le_imp_le_exp, assumption) - apply (erule dvd_imp_le, simp) - done - lemma mod_eq_0_iff: "(m mod d = 0) = (\q::nat. m = d*q)" by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) @@ -1162,9 +1092,4 @@ with j show ?thesis by blast qed -lemma nat_dvd_not_less: - fixes m n :: nat - shows "0 < m \ m < n \ \ n dvd m" -by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) - end diff -r 9290fbf0a30e -r b6ff7db522b5 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Oct 28 12:21:38 2009 +0000 +++ b/src/HOL/Nat.thy Wed Oct 28 17:44:03 2009 +0100 @@ -8,7 +8,7 @@ header {* Natural numbers *} theory Nat -imports Inductive Ring_and_Field +imports Inductive Product_Type Ring_and_Field uses "~~/src/Tools/rat.ML" "~~/src/Provers/Arith/cancel_sums.ML" @@ -1600,6 +1600,75 @@ Least_Suc}, since there appears to be no need.*} +subsection {* The divides relation on @{typ nat} *} + +lemma dvd_1_left [iff]: "Suc 0 dvd k" +unfolding dvd_def by simp + +lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)" +by (simp add: dvd_def) + +lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \ m = 1" +by (simp add: dvd_def) + +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)" + unfolding dvd_def + by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff) + +text {* @{term "op dvd"} is a partial order *} + +interpretation dvd: order "op dvd" "\n m \ nat. n dvd m \ \ m dvd n" + proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym) + +lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)" +unfolding dvd_def +by (blast intro: diff_mult_distrib2 [symmetric]) + +lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\m |] ==> k dvd (m::nat)" + apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) + apply (blast intro: dvd_add) + done + +lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\m |] ==> k dvd (n::nat)" +by (drule_tac m = m in dvd_diff_nat, auto) + +lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))" + apply (rule iffI) + apply (erule_tac [2] dvd_add) + apply (rule_tac [2] dvd_refl) + apply (subgoal_tac "n = (n+k) -k") + prefer 2 apply simp + apply (erule ssubst) + apply (erule dvd_diff_nat) + apply (rule dvd_refl) + done + +lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0 m dvd n" + unfolding dvd_def + apply (erule exE) + apply (simp add: mult_ac) + done + +lemma dvd_mult_cancel1: "0 (m*n dvd m) = (n = (1::nat))" + apply auto + apply (subgoal_tac "m*n dvd m*1") + apply (drule dvd_mult_cancel, auto) + done + +lemma dvd_mult_cancel2: "0 (n*m dvd m) = (n = (1::nat))" + apply (subst mult_commute) + apply (erule dvd_mult_cancel1) + done + +lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \ (n::nat)" +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) + +lemma nat_dvd_not_less: + fixes m n :: nat + shows "0 < m \ m < n \ \ n dvd m" +by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) + + subsection {* size of a datatype value *} class size = diff -r 9290fbf0a30e -r b6ff7db522b5 src/HOL/Power.thy --- a/src/HOL/Power.thy Wed Oct 28 12:21:38 2009 +0000 +++ b/src/HOL/Power.thy Wed Oct 28 17:44:03 2009 +0100 @@ -452,6 +452,12 @@ from power_strict_increasing_iff [OF this] less show ?thesis .. qed +lemma power_dvd_imp_le: + "i ^ m dvd i ^ n \ (1::nat) < i \ m \ n" + apply (rule power_le_imp_le_exp, assumption) + apply (erule dvd_imp_le, simp) + done + subsection {* Code generator tweak *}