simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
authorhaftmann
Thu Aug 23 17:09:39 2018 +0000 (15 months ago)
changeset 687969ca183045102
parent 68795 210b687cdbbe
child 68797 e79c771c0619
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
NEWS
src/HOL/Analysis/Starlike.thy
src/HOL/Complete_Lattices.thy
src/HOL/GCD.thy
src/HOL/Lattices_Big.thy
     1.1 --- a/NEWS	Thu Aug 23 17:09:37 2018 +0000
     1.2 +++ b/NEWS	Thu Aug 23 17:09:39 2018 +0000
     1.3 @@ -14,6 +14,15 @@
     1.4  specified in seconds; a negative value means it is disabled (default).
     1.5  
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Simplified syntax setup for big operators under image. In rare
    1.10 +situations, type conversions are not inserted implicitly any longer
    1.11 +and need to be given explicitly. Auxiliary abbreviations INFIMUM,
    1.12 +SUPREMUM, UNION, INTER should now rarely occur in output and are just
    1.13 +retained as migration auxiliary. INCOMPATIBILITY.
    1.14 +
    1.15 +
    1.16  New in Isabelle2018 (August 2018)
    1.17  ---------------------------------
    1.18  
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:37 2018 +0000
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:39 2018 +0000
     2.3 @@ -1355,7 +1355,7 @@
     2.4      proof safe
     2.5        fix i :: 'a
     2.6        assume i: "i \<in> Basis"
     2.7 -      have "norm (x - y) < MINIMUM Basis ((\<bullet>) x)"
     2.8 +      have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
     2.9          using y by (auto simp: dist_norm less_eq_real_def)
    2.10        also have "... \<le> x\<bullet>i"
    2.11          using i by auto
     3.1 --- a/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:37 2018 +0000
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:39 2018 +0000
     3.3 @@ -18,7 +18,7 @@
     3.4    fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
     3.5  begin
     3.6  
     3.7 -abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     3.8 +abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
     3.9    where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
    3.10  
    3.11  lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
    3.12 @@ -43,7 +43,7 @@
    3.13    fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
    3.14  begin
    3.15  
    3.16 -abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    3.17 +abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
    3.18    where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
    3.19  
    3.20  lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
    3.21 @@ -64,12 +64,6 @@
    3.22  
    3.23  end
    3.24  
    3.25 -text \<open>
    3.26 -  Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of
    3.27 -  \<open>INF\<close> and \<open>SUP\<close> to allow the following syntax coexist
    3.28 -  with the plain constant names.
    3.29 -\<close>
    3.30 -
    3.31  syntax (ASCII)
    3.32    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    3.33    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    3.34 @@ -89,17 +83,12 @@
    3.35    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    3.36  
    3.37  translations
    3.38 -  "\<Sqinter>x y. B"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. B"
    3.39 -  "\<Sqinter>x. B"     \<rightleftharpoons> "\<Sqinter>x \<in> CONST UNIV. B"
    3.40 -  "\<Sqinter>x\<in>A. B"   \<rightleftharpoons> "CONST INFIMUM A (\<lambda>x. B)"
    3.41 -  "\<Squnion>x y. B"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. B"
    3.42 -  "\<Squnion>x. B"     \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
    3.43 -  "\<Squnion>x\<in>A. B"   \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
    3.44 -
    3.45 -print_translation \<open>
    3.46 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
    3.47 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
    3.48 -\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    3.49 +  "\<Sqinter>x y. f"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
    3.50 +  "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
    3.51 +  "\<Sqinter>x\<in>A. f"   \<rightleftharpoons> "CONST Inf ((\<lambda>x. f) ` A)"
    3.52 +  "\<Squnion>x y. f"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. f"
    3.53 +  "\<Squnion>x. f"     \<rightleftharpoons> "\<Squnion>CONST range (\<lambda>x. f)"
    3.54 +  "\<Squnion>x\<in>A. f"   \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) `  A)"
    3.55  
    3.56  
    3.57  subsection \<open>Abstract complete lattices\<close>
    3.58 @@ -852,14 +841,9 @@
    3.59  
    3.60  subsubsection \<open>Intersections of families\<close>
    3.61  
    3.62 -abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    3.63 +abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
    3.64    where "INTER \<equiv> INFIMUM"
    3.65  
    3.66 -text \<open>
    3.67 -  Note: must use name @{const INTER} here instead of \<open>INT\<close>
    3.68 -  to allow the following syntax coexist with the plain constant name.
    3.69 -\<close>
    3.70 -
    3.71  syntax (ASCII)
    3.72    "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3INT _./ _)" [0, 10] 10)
    3.73    "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
    3.74 @@ -873,13 +857,9 @@
    3.75    "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
    3.76  
    3.77  translations
    3.78 -  "\<Inter>x y. B"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. B"
    3.79 -  "\<Inter>x. B"    \<rightleftharpoons> "\<Inter>x \<in> CONST UNIV. B"
    3.80 -  "\<Inter>x\<in>A. B"  \<rightleftharpoons> "CONST INTER A (\<lambda>x. B)"
    3.81 -
    3.82 -print_translation \<open>
    3.83 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    3.84 -\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    3.85 +  "\<Inter>x y. f"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
    3.86 +  "\<Inter>x. f"    \<rightleftharpoons> "\<Inter>CONST range (\<lambda>x. f)"
    3.87 +  "\<Inter>x\<in>A. f"  \<rightleftharpoons> "CONST Inter ((\<lambda>x. f) ` A)"
    3.88  
    3.89  lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
    3.90    by (auto intro!: INF_eqI)
    3.91 @@ -1021,14 +1001,9 @@
    3.92  
    3.93  subsubsection \<open>Unions of families\<close>
    3.94  
    3.95 -abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    3.96 +abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
    3.97    where "UNION \<equiv> SUPREMUM"
    3.98  
    3.99 -text \<open>
   3.100 -  Note: must use name @{const UNION} here instead of \<open>UN\<close>
   3.101 -  to allow the following syntax coexist with the plain constant name.
   3.102 -\<close>
   3.103 -
   3.104  syntax (ASCII)
   3.105    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   3.106    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
   3.107 @@ -1042,9 +1017,9 @@
   3.108    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
   3.109  
   3.110  translations
   3.111 -  "\<Union>x y. B"   \<rightleftharpoons> "\<Union>x. \<Union>y. B"
   3.112 -  "\<Union>x. B"     \<rightleftharpoons> "\<Union>x \<in> CONST UNIV. B"
   3.113 -  "\<Union>x\<in>A. B"   \<rightleftharpoons> "CONST UNION A (\<lambda>x. B)"
   3.114 +  "\<Union>x y. f"   \<rightleftharpoons> "\<Union>x. \<Union>y. f"
   3.115 +  "\<Union>x. f"     \<rightleftharpoons> "\<Union>CONST range (\<lambda>x. f)"
   3.116 +  "\<Union>x\<in>A. f"   \<rightleftharpoons> "CONST Union ((\<lambda>x. f) ` A)"
   3.117  
   3.118  text \<open>
   3.119    Note the difference between ordinary syntax of indexed
   3.120 @@ -1052,10 +1027,6 @@
   3.121    and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}.
   3.122  \<close>
   3.123  
   3.124 -print_translation \<open>
   3.125 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
   3.126 -\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
   3.127 -
   3.128  lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))"
   3.129    by (auto simp: disjnt_def)
   3.130  
     4.1 --- a/src/HOL/GCD.thy	Thu Aug 23 17:09:37 2018 +0000
     4.2 +++ b/src/HOL/GCD.thy	Thu Aug 23 17:09:39 2018 +0000
     4.3 @@ -146,15 +146,6 @@
     4.4  class Gcd = gcd +
     4.5    fixes Gcd :: "'a set \<Rightarrow> 'a"
     4.6      and Lcm :: "'a set \<Rightarrow> 'a"
     4.7 -begin
     4.8 -
     4.9 -abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    4.10 -  where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
    4.11 -
    4.12 -abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    4.13 -  where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
    4.14 -
    4.15 -end
    4.16  
    4.17  syntax
    4.18    "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
    4.19 @@ -163,17 +154,12 @@
    4.20    "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
    4.21  
    4.22  translations
    4.23 -  "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
    4.24 -  "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
    4.25 -  "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
    4.26 -  "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
    4.27 -  "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
    4.28 -  "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
    4.29 -
    4.30 -print_translation \<open>
    4.31 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"},
    4.32 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}]
    4.33 -\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    4.34 +  "GCD x y. f"   \<rightleftharpoons> "GCD x. GCD y. f"
    4.35 +  "GCD x. f"     \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))"
    4.36 +  "GCD x\<in>A. f"   \<rightleftharpoons> "CONST Gcd ((\<lambda>x. f) ` A)"
    4.37 +  "LCM x y. f"   \<rightleftharpoons> "LCM x. LCM y. f"
    4.38 +  "LCM x. f"     \<rightleftharpoons> "CONST Lcm (CONST range (\<lambda>x. f))"
    4.39 +  "LCM x\<in>A. f"   \<rightleftharpoons> "CONST Lcm ((\<lambda>x. f) ` A)"
    4.40  
    4.41  class semiring_gcd = normalization_semidom + gcd +
    4.42    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
     5.1 --- a/src/HOL/Lattices_Big.thy	Thu Aug 23 17:09:37 2018 +0000
     5.2 +++ b/src/HOL/Lattices_Big.thy	Thu Aug 23 17:09:39 2018 +0000
     5.3 @@ -462,14 +462,8 @@
     5.4  defines
     5.5    Min = Min.F and Max = Max.F ..
     5.6  
     5.7 -abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     5.8 -  where "MINIMUM A f \<equiv> Min(f ` A)"
     5.9 -abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    5.10 -  where "MAXIMUM A f \<equiv> Max(f ` A)"
    5.11 -
    5.12  end
    5.13  
    5.14 -
    5.15  syntax (ASCII)
    5.16    "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
    5.17    "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
    5.18 @@ -489,17 +483,12 @@
    5.19    "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
    5.20  
    5.21  translations
    5.22 -  "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
    5.23 -  "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
    5.24 -  "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
    5.25 -  "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
    5.26 -  "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
    5.27 -  "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
    5.28 -
    5.29 -print_translation \<open>
    5.30 -  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MINIMUM} @{syntax_const "_MIN"},
    5.31 -    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MAXIMUM} @{syntax_const "_MAX"}]
    5.32 -\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    5.33 +  "MIN x y. f"   \<rightleftharpoons> "MIN x. MIN y. f"
    5.34 +  "MIN x. f"     \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
    5.35 +  "MIN x\<in>A. f"   \<rightleftharpoons> "CONST Min ((\<lambda>x. f) ` A)"
    5.36 +  "MAX x y. f"   \<rightleftharpoons> "MAX x. MAX y. f"
    5.37 +  "MAX x. f"     \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))"
    5.38 +  "MAX x\<in>A. f"   \<rightleftharpoons> "CONST Max ((\<lambda>x. f) ` A)"
    5.39  
    5.40  text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>
    5.41