src/HOL/GCD.thy
changeset 62350 66a381d3f88f
parent 62349 7c23469b5118
child 62353 7f927120b5a2
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -44,8 +44,40 @@
     1.4  end
     1.5  
     1.6  class Gcd = gcd +
     1.7 -  fixes Gcd :: "'a set \<Rightarrow> 'a"
     1.8 -    and Lcm :: "'a set \<Rightarrow> 'a"
     1.9 +  fixes Gcd :: "'a set \<Rightarrow> 'a" ("Gcd")
    1.10 +    and Lcm :: "'a set \<Rightarrow> 'a" ("Lcm")
    1.11 +begin
    1.12 +
    1.13 +abbreviation GCD :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.14 +where
    1.15 +  "GCD A f \<equiv> Gcd (f ` A)"
    1.16 +
    1.17 +abbreviation LCM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.18 +where
    1.19 +  "LCM A f \<equiv> Lcm (f ` A)"
    1.20 +
    1.21 +end
    1.22 +
    1.23 +syntax
    1.24 +  "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3Gcd _./ _)" [0, 10] 10)
    1.25 +  "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3Gcd _\<in>_./ _)" [0, 0, 10] 10)
    1.26 +  "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3Lcm _./ _)" [0, 10] 10)
    1.27 +  "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3Lcm _\<in>_./ _)" [0, 0, 10] 10)
    1.28 +
    1.29 +translations
    1.30 +  "Gcd x y. B"   \<rightleftharpoons> "Gcd x. Gcd y. B"
    1.31 +  "Gcd x. B"     \<rightleftharpoons> "CONST GCD CONST UNIV (\<lambda>x. B)"
    1.32 +  "Gcd x. B"     \<rightleftharpoons> "Gcd x \<in> CONST UNIV. B"
    1.33 +  "Gcd x\<in>A. B"   \<rightleftharpoons> "CONST GCD A (\<lambda>x. B)"
    1.34 +  "Lcm x y. B"   \<rightleftharpoons> "Lcm x. Lcm y. B"
    1.35 +  "Lcm x. B"     \<rightleftharpoons> "CONST LCM CONST UNIV (\<lambda>x. B)"
    1.36 +  "Lcm x. B"     \<rightleftharpoons> "Lcm x \<in> CONST UNIV. B"
    1.37 +  "Lcm x\<in>A. B"   \<rightleftharpoons> "CONST LCM A (\<lambda>x. B)"
    1.38 +
    1.39 +print_translation \<open>
    1.40 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GCD} @{syntax_const "_GCD"},
    1.41 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LCM} @{syntax_const "_LCM"}]
    1.42 +\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    1.43  
    1.44  class semiring_gcd = normalization_semidom + gcd +
    1.45    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    1.46 @@ -571,7 +603,7 @@
    1.47    have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
    1.48    proof -
    1.49      from that obtain B where "A = insert a B" by blast
    1.50 -    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
    1.51 +    moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
    1.52        by (rule gcd_dvd1)
    1.53      ultimately show "Gcd (normalize ` A) dvd a"
    1.54        by simp
    1.55 @@ -596,8 +628,7 @@
    1.56    shows "Lcm A = a"
    1.57    using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
    1.58  
    1.59 -end  
    1.60 -
    1.61 +end
    1.62  
    1.63  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
    1.64