# HG changeset patch
# User nipkow
# Date 1185379828 -7200
# Node ID 79dc793bec4344013278370cb091fcc4d68736f0
# Parent  e3c4c0b9ae0544614fa8cfdcb0be6d30ba0e3dec
Added lemmas

diff -r e3c4c0b9ae05 -r 79dc793bec43 src/HOL/IntDiv.thy
--- 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
diff -r e3c4c0b9ae05 -r 79dc793bec43 src/HOL/Library/GCD.thy
--- 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
diff -r e3c4c0b9ae05 -r 79dc793bec43 src/HOL/List.thy
--- 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?]: