--- a/src/HOL/IntDiv.thy Wed Jul 25 17:05:50 2007 +0200
+++ b/src/HOL/IntDiv.thy Wed Jul 25 18:10:28 2007 +0200
@@ -758,6 +758,15 @@
done
+lemma zmod_zdiff1_eq: fixes a::int
+ shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
+proof -
+ have "?l = (c + (a mod c - b mod c)) mod c"
+ using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
+ also have "\<dots> = ?r" by simp
+ finally show ?thesis .
+qed
+
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but
--- a/src/HOL/Library/GCD.thy Wed Jul 25 17:05:50 2007 +0200
+++ b/src/HOL/Library/GCD.thy Wed Jul 25 18:10:28 2007 +0200
@@ -419,7 +419,12 @@
definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
-(* ilcm_dvd12 are needed later *)
+lemma dvd_ilcm_self1[simp]: "i dvd ilcm i j"
+by(simp add:ilcm_def dvd_int_iff)
+
+lemma dvd_ilcm_self2[simp]: "j dvd ilcm i j"
+by(simp add:ilcm_def dvd_int_iff)
+
lemma ilcm_dvd1:
assumes anz: "a \<noteq> 0"
and bnz: "b \<noteq> 0"
@@ -446,6 +451,22 @@
thus ?thesis by (simp add: ilcm_def dvd_int_iff)
qed
+lemma dvd_imp_dvd_ilcm1:
+ assumes "k dvd i" shows "k dvd (ilcm i j)"
+proof -
+ have "nat(abs k) dvd nat(abs i)" using `k dvd i`
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric]IntDiv.zdvd_abs1)
+ thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
+qed
+
+lemma dvd_imp_dvd_ilcm2:
+ assumes "k dvd j" shows "k dvd (ilcm i j)"
+proof -
+ have "nat(abs k) dvd nat(abs j)" using `k dvd j`
+ by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric]IntDiv.zdvd_abs1)
+ thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
+qed
+
lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
by (case_tac "d <0", simp_all)
@@ -478,14 +499,14 @@
qed
lemma ilcm_pos:
- assumes apos: " 0 < a"
- and bpos: "0 < b"
- shows "0 < ilcm a b"
+ assumes anz: "a \<noteq> 0"
+ and bnz: "b \<noteq> 0"
+ shows "0 < ilcm a b"
proof-
let ?na = "nat (abs a)"
let ?nb = "nat (abs b)"
- have nap: "?na >0" using apos by simp
- have nbp: "?nb >0" using bpos by simp
+ have nap: "?na >0" using anz by simp
+ have nbp: "?nb >0" using bnz by simp
have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
thus ?thesis by (simp add: ilcm_def)
qed
--- a/src/HOL/List.thy Wed Jul 25 17:05:50 2007 +0200
+++ b/src/HOL/List.thy Wed Jul 25 18:10:28 2007 +0200
@@ -983,6 +983,9 @@
lemma set_concat [simp]: "set (concat xs) = \<Union>(set ` set xs)"
by (induct xs) auto
+lemma set_concat_map: "set(concat(map f xs)) = (UN x:set xs. set(f x))"
+by(auto)
+
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
by (induct xs) auto
@@ -1556,6 +1559,10 @@
"(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
by (induct xs ys rule:list_induct2') auto
+lemma in_set_zipE:
+ "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
+by(blast dest: set_zip_leftD set_zip_rightD)
+
subsubsection {* @{text list_all2} *}
lemma list_all2_lengthD [intro?]: