--- 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 \<Longrightarrow> (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 \<Longrightarrow> a * (b div a) = b"
+by (drule dvd_div_mult_self) (simp add: mult_commute)
+
lemma dvd_div_mult: "a dvd b \<Longrightarrow> (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) \<longleftrightarrow> 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" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> 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\<le>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\<le>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<k |] ==> m dvd n"
- unfolding dvd_def
- apply (erule exE)
- apply (simp add: mult_ac)
- done
-
-lemma dvd_mult_cancel1: "0<m ==> (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<m ==> (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 \<le> (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 \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> 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) = (\<exists>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 \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
-by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
-
end
--- 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) \<longleftrightarrow> 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" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> 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\<le>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\<le>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<k |] ==> m dvd n"
+ unfolding dvd_def
+ apply (erule exE)
+ apply (simp add: mult_ac)
+ done
+
+lemma dvd_mult_cancel1: "0<m ==> (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<m ==> (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 \<le> (n::nat)"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
+lemma nat_dvd_not_less:
+ fixes m n :: nat
+ shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
+by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
+
+
subsection {* size of a datatype value *}
class size =
--- 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 \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n"
+ apply (rule power_le_imp_le_exp, assumption)
+ apply (erule dvd_imp_le, simp)
+ done
+
subsection {* Code generator tweak *}