src/HOL/GCD.thy
changeset 62346 97f2ed240431
parent 62345 e66d7841d5a2
child 62347 2230b7047376
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -582,6 +582,20 @@
     1.4      by (auto intro: associated_eqI)
     1.5  qed
     1.6  
     1.7 +lemma Gcd_eqI:
     1.8 +  assumes "normalize a = a"
     1.9 +  assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
    1.10 +    and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
    1.11 +  shows "Gcd A = a"
    1.12 +  using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
    1.13 +
    1.14 +lemma Lcm_eqI:
    1.15 +  assumes "normalize a = a"
    1.16 +  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
    1.17 +    and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
    1.18 +  shows "Lcm A = a"
    1.19 +  using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
    1.20 +
    1.21  end  
    1.22  
    1.23  
    1.24 @@ -656,6 +670,14 @@
    1.25  
    1.26  (* specific to int *)
    1.27  
    1.28 +lemma gcd_eq_int_iff:
    1.29 +  "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
    1.30 +  by (simp add: gcd_int_def)
    1.31 +
    1.32 +lemma lcm_eq_int_iff:
    1.33 +  "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
    1.34 +  by (simp add: lcm_int_def)
    1.35 +
    1.36  lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
    1.37    by (simp add: gcd_int_def)
    1.38  
    1.39 @@ -1874,6 +1896,10 @@
    1.40  
    1.41  end
    1.42  
    1.43 +lemma Gcd_nat_eq_one:
    1.44 +  "1 \<in> N \<Longrightarrow> Gcd N = (1::nat)"
    1.45 +  by (rule Gcd_eq_1_I) auto
    1.46 +
    1.47  text\<open>Alternative characterizations of Gcd:\<close>
    1.48  
    1.49  lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
    1.50 @@ -1940,10 +1966,10 @@
    1.51  begin
    1.52  
    1.53  definition
    1.54 -  "Lcm M = int (Lcm (nat ` abs ` M))"
    1.55 +  "Lcm M = int (Lcm m\<in>M. (nat \<circ> abs) m)"
    1.56  
    1.57  definition
    1.58 -  "Gcd M = int (Gcd (nat ` abs ` M))"
    1.59 +  "Gcd M = int (Gcd m\<in>M. (nat \<circ> abs) m)"
    1.60  
    1.61  instance by standard
    1.62    (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
    1.63 @@ -1951,6 +1977,24 @@
    1.64  
    1.65  end
    1.66  
    1.67 +lemma abs_Gcd [simp]:
    1.68 +  fixes K :: "int set"
    1.69 +  shows "\<bar>Gcd K\<bar> = Gcd K"
    1.70 +  using normalize_Gcd [of K] by simp
    1.71 +
    1.72 +lemma abs_Lcm [simp]:
    1.73 +  fixes K :: "int set"
    1.74 +  shows "\<bar>Lcm K\<bar> = Lcm K"
    1.75 +  using normalize_Lcm [of K] by simp
    1.76 +
    1.77 +lemma Gcm_eq_int_iff:
    1.78 +  "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
    1.79 +  by (simp add: Gcd_int_def comp_def image_image)
    1.80 +
    1.81 +lemma Lcm_eq_int_iff:
    1.82 +  "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
    1.83 +  by (simp add: Lcm_int_def comp_def image_image)
    1.84 +
    1.85  
    1.86  subsection \<open>GCD and LCM on @{typ integer}\<close>
    1.87