src/HOL/GCD.thy
 changeset 69785 9e326f6f8a24 parent 69768 7e4966eaf781 child 69906 55534affe445
```     1.1 --- a/src/HOL/GCD.thy	Sat Feb 02 15:52:14 2019 +0100
1.2 +++ b/src/HOL/GCD.thy	Mon Feb 04 12:16:03 2019 +0100
1.3 @@ -682,6 +682,12 @@
1.4      by simp
1.5  qed
1.6
1.7 +lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
1.8 +  by (simp add: gcd_dvdI1 gcd_dvdI2)
1.9 +
1.10 +lemma lcm_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> lcm a b dvd lcm c d"
1.11 +  by (simp add: dvd_lcmI1 dvd_lcmI2)
1.12 +
1.13  lemma dvd_productE:
1.14    assumes "p dvd a * b"
1.15    obtains x y where "p = x * y" "x dvd a" "y dvd b"
1.16 @@ -1081,6 +1087,29 @@
1.17  lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
1.18    by simp
1.19
1.20 +lemma Gcd_mono:
1.21 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
1.22 +  shows   "(GCD x\<in>A. f x) dvd (GCD x\<in>A. g x)"
1.23 +proof (intro Gcd_greatest, safe)
1.24 +  fix x assume "x \<in> A"
1.25 +  hence "(GCD x\<in>A. f x) dvd f x"
1.26 +    by (intro Gcd_dvd) auto
1.27 +  also have "f x dvd g x"
1.28 +    using \<open>x \<in> A\<close> assms by blast
1.29 +  finally show "(GCD x\<in>A. f x) dvd \<dots>" .
1.30 +qed
1.31 +
1.32 +lemma Lcm_mono:
1.33 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x"
1.34 +  shows   "(LCM x\<in>A. f x) dvd (LCM x\<in>A. g x)"
1.35 +proof (intro Lcm_least, safe)
1.36 +  fix x assume "x \<in> A"
1.37 +  hence "f x dvd g x" by (rule assms)
1.38 +  also have "g x dvd (LCM x\<in>A. g x)"
1.39 +    using \<open>x \<in> A\<close> by (intro dvd_Lcm) auto
1.40 +  finally show "f x dvd \<dots>" .
1.41 +qed
1.42 +
1.43  end
1.44
1.45
```