capitalized GCD and LCM syntax
authorhaftmann
Mon Apr 18 20:56:13 2016 +0200 (2016-04-18)
changeset 6302592680537201f
parent 63024 adeac19dd410
child 63026 9a9c2d846d4a
capitalized GCD and LCM syntax
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Mon Apr 18 20:56:11 2016 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Apr 18 20:56:13 2016 +0200
     1.3 @@ -44,39 +44,39 @@
     1.4  end
     1.5  
     1.6  class Gcd = gcd +
     1.7 -  fixes Gcd :: "'a set \<Rightarrow> 'a" ("Gcd")
     1.8 -    and Lcm :: "'a set \<Rightarrow> 'a" ("Lcm")
     1.9 +  fixes Gcd :: "'a set \<Rightarrow> 'a"
    1.10 +    and Lcm :: "'a set \<Rightarrow> 'a"
    1.11  begin
    1.12  
    1.13 -abbreviation GCD :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.14 +abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.15  where
    1.16 -  "GCD A f \<equiv> Gcd (f ` A)"
    1.17 +  "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
    1.18  
    1.19 -abbreviation LCM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.20 +abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.21  where
    1.22 -  "LCM A f \<equiv> Lcm (f ` A)"
    1.23 +  "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
    1.24  
    1.25  end
    1.26  
    1.27  syntax
    1.28 -  "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3Gcd _./ _)" [0, 10] 10)
    1.29 -  "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3Gcd _\<in>_./ _)" [0, 0, 10] 10)
    1.30 -  "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3Lcm _./ _)" [0, 10] 10)
    1.31 -  "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3Lcm _\<in>_./ _)" [0, 0, 10] 10)
    1.32 +  "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
    1.33 +  "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
    1.34 +  "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
    1.35 +  "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
    1.36  
    1.37  translations
    1.38 -  "Gcd x y. B"   \<rightleftharpoons> "Gcd x. Gcd y. B"
    1.39 -  "Gcd x. B"     \<rightleftharpoons> "CONST GCD CONST UNIV (\<lambda>x. B)"
    1.40 -  "Gcd x. B"     \<rightleftharpoons> "Gcd x \<in> CONST UNIV. B"
    1.41 -  "Gcd x\<in>A. B"   \<rightleftharpoons> "CONST GCD A (\<lambda>x. B)"
    1.42 -  "Lcm x y. B"   \<rightleftharpoons> "Lcm x. Lcm y. B"
    1.43 -  "Lcm x. B"     \<rightleftharpoons> "CONST LCM CONST UNIV (\<lambda>x. B)"
    1.44 -  "Lcm x. B"     \<rightleftharpoons> "Lcm x \<in> CONST UNIV. B"
    1.45 -  "Lcm x\<in>A. B"   \<rightleftharpoons> "CONST LCM A (\<lambda>x. B)"
    1.46 +  "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
    1.47 +  "GCD x. B"     \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)"
    1.48 +  "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
    1.49 +  "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
    1.50 +  "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
    1.51 +  "LCM x. B"     \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. B)"
    1.52 +  "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
    1.53 +  "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
    1.54  
    1.55  print_translation \<open>
    1.56 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GCD} @{syntax_const "_GCD"},
    1.57 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LCM} @{syntax_const "_LCM"}]
    1.58 +  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"},
    1.59 +    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}]
    1.60  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    1.61  
    1.62  class semiring_gcd = normalization_semidom + gcd +
    1.63 @@ -2166,10 +2166,10 @@
    1.64  begin
    1.65  
    1.66  definition
    1.67 -  "Lcm M = int (Lcm m\<in>M. (nat \<circ> abs) m)"
    1.68 +  "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
    1.69  
    1.70  definition
    1.71 -  "Gcd M = int (Gcd m\<in>M. (nat \<circ> abs) m)"
    1.72 +  "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
    1.73  
    1.74  instance by standard
    1.75    (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def