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