# 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 "\ = ?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 = (\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 \ 0" and bnz: "b \ 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 \ 0" + and bnz: "b \ 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) = \(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)\ set (zip xs ys) \ y \ set ys" by (induct xs ys rule:list_induct2') auto +lemma in_set_zipE: + "(x,y) : set(zip xs ys) \ (\ x : set xs; y : set ys \ \ R) \ R" +by(blast dest: set_zip_leftD set_zip_rightD) + subsubsection {* @{text list_all2} *} lemma list_all2_lengthD [intro?]: