# HG changeset patch
# User haftmann
# Date 1535044179 0
# Node ID 9ca183045102454c1a239e2dbf9cf8978d5be6a0
# Parent  210b687cdbbe2e6248aea542dad1ddf9a5c9bb25
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility

diff -r 210b687cdbbe -r 9ca183045102 NEWS
--- a/NEWS	Thu Aug 23 17:09:37 2018 +0000
+++ b/NEWS	Thu Aug 23 17:09:39 2018 +0000
@@ -14,6 +14,15 @@
 specified in seconds; a negative value means it is disabled (default).
 
 
+*** HOL ***
+
+* Simplified syntax setup for big operators under image. In rare
+situations, type conversions are not inserted implicitly any longer
+and need to be given explicitly. Auxiliary abbreviations INFIMUM,
+SUPREMUM, UNION, INTER should now rarely occur in output and are just
+retained as migration auxiliary. INCOMPATIBILITY.
+
+
 New in Isabelle2018 (August 2018)
 ---------------------------------
 
diff -r 210b687cdbbe -r 9ca183045102 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -1355,7 +1355,7 @@
     proof safe
       fix i :: 'a
       assume i: "i \<in> Basis"
-      have "norm (x - y) < MINIMUM Basis ((\<bullet>) x)"
+      have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
         using y by (auto simp: dist_norm less_eq_real_def)
       also have "... \<le> x\<bullet>i"
         using i by auto
diff -r 210b687cdbbe -r 9ca183045102 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -18,7 +18,7 @@
   fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>_" [900] 900)
 begin
 
-abbreviation INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
   where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
 
 lemma INF_image [simp]: "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
@@ -43,7 +43,7 @@
   fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>_" [900] 900)
 begin
 
-abbreviation SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
   where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
 
 lemma SUP_image [simp]: "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
@@ -64,12 +64,6 @@
 
 end
 
-text \<open>
-  Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of
-  \<open>INF\<close> and \<open>SUP\<close> to allow the following syntax coexist
-  with the plain constant names.
-\<close>
-
 syntax (ASCII)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
@@ -89,17 +83,12 @@
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "\<Sqinter>x y. B"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. B"
-  "\<Sqinter>x. B"     \<rightleftharpoons> "\<Sqinter>x \<in> CONST UNIV. B"
-  "\<Sqinter>x\<in>A. B"   \<rightleftharpoons> "CONST INFIMUM A (\<lambda>x. B)"
-  "\<Squnion>x y. B"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. B"
-  "\<Squnion>x. B"     \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
-  "\<Squnion>x\<in>A. B"   \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
-
-print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
-\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+  "\<Sqinter>x y. f"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
+  "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
+  "\<Sqinter>x\<in>A. f"   \<rightleftharpoons> "CONST Inf ((\<lambda>x. f) ` A)"
+  "\<Squnion>x y. f"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. f"
+  "\<Squnion>x. f"     \<rightleftharpoons> "\<Squnion>CONST range (\<lambda>x. f)"
+  "\<Squnion>x\<in>A. f"   \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) `  A)"
 
 
 subsection \<open>Abstract complete lattices\<close>
@@ -852,14 +841,9 @@
 
 subsubsection \<open>Intersections of families\<close>
 
-abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
   where "INTER \<equiv> INFIMUM"
 
-text \<open>
-  Note: must use name @{const INTER} here instead of \<open>INT\<close>
-  to allow the following syntax coexist with the plain constant name.
-\<close>
-
 syntax (ASCII)
   "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3INT _./ _)" [0, 10] 10)
   "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
@@ -873,13 +857,9 @@
   "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "\<Inter>x y. B"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. B"
-  "\<Inter>x. B"    \<rightleftharpoons> "\<Inter>x \<in> CONST UNIV. B"
-  "\<Inter>x\<in>A. B"  \<rightleftharpoons> "CONST INTER A (\<lambda>x. B)"
-
-print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
-\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+  "\<Inter>x y. f"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
+  "\<Inter>x. f"    \<rightleftharpoons> "\<Inter>CONST range (\<lambda>x. f)"
+  "\<Inter>x\<in>A. f"  \<rightleftharpoons> "CONST Inter ((\<lambda>x. f) ` A)"
 
 lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
   by (auto intro!: INF_eqI)
@@ -1021,14 +1001,9 @@
 
 subsubsection \<open>Unions of families\<close>
 
-abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
   where "UNION \<equiv> SUPREMUM"
 
-text \<open>
-  Note: must use name @{const UNION} here instead of \<open>UN\<close>
-  to allow the following syntax coexist with the plain constant name.
-\<close>
-
 syntax (ASCII)
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
@@ -1042,9 +1017,9 @@
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "\<Union>x y. B"   \<rightleftharpoons> "\<Union>x. \<Union>y. B"
-  "\<Union>x. B"     \<rightleftharpoons> "\<Union>x \<in> CONST UNIV. B"
-  "\<Union>x\<in>A. B"   \<rightleftharpoons> "CONST UNION A (\<lambda>x. B)"
+  "\<Union>x y. f"   \<rightleftharpoons> "\<Union>x. \<Union>y. f"
+  "\<Union>x. f"     \<rightleftharpoons> "\<Union>CONST range (\<lambda>x. f)"
+  "\<Union>x\<in>A. f"   \<rightleftharpoons> "CONST Union ((\<lambda>x. f) ` A)"
 
 text \<open>
   Note the difference between ordinary syntax of indexed
@@ -1052,10 +1027,6 @@
   and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}.
 \<close>
 
-print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
-\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
-
 lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))"
   by (auto simp: disjnt_def)
 
diff -r 210b687cdbbe -r 9ca183045102 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/GCD.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -146,15 +146,6 @@
 class Gcd = gcd +
   fixes Gcd :: "'a set \<Rightarrow> 'a"
     and Lcm :: "'a set \<Rightarrow> 'a"
-begin
-
-abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
-
-abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
-
-end
 
 syntax
   "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
@@ -163,17 +154,12 @@
   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
-  "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
-  "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
-  "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
-  "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
-  "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
-
-print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}]
-\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+  "GCD x y. f"   \<rightleftharpoons> "GCD x. GCD y. f"
+  "GCD x. f"     \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))"
+  "GCD x\<in>A. f"   \<rightleftharpoons> "CONST Gcd ((\<lambda>x. f) ` A)"
+  "LCM x y. f"   \<rightleftharpoons> "LCM x. LCM y. f"
+  "LCM x. f"     \<rightleftharpoons> "CONST Lcm (CONST range (\<lambda>x. f))"
+  "LCM x\<in>A. f"   \<rightleftharpoons> "CONST Lcm ((\<lambda>x. f) ` A)"
 
 class semiring_gcd = normalization_semidom + gcd +
   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
diff -r 210b687cdbbe -r 9ca183045102 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Thu Aug 23 17:09:37 2018 +0000
+++ b/src/HOL/Lattices_Big.thy	Thu Aug 23 17:09:39 2018 +0000
@@ -462,14 +462,8 @@
 defines
   Min = Min.F and Max = Max.F ..
 
-abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "MINIMUM A f \<equiv> Min(f ` A)"
-abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
-  where "MAXIMUM A f \<equiv> Max(f ` A)"
-
 end
 
-
 syntax (ASCII)
   "_MIN1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3MIN _./ _)" [0, 10] 10)
   "_MIN"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MIN _:_./ _)" [0, 0, 10] 10)
@@ -489,17 +483,12 @@
   "_MAX"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "MIN x y. B"   \<rightleftharpoons> "MIN x. MIN y. B"
-  "MIN x. B"     \<rightleftharpoons> "MIN x \<in> CONST UNIV. B"
-  "MIN x\<in>A. B"   \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)"
-  "MAX x y. B"   \<rightleftharpoons> "MAX x. MAX y. B"
-  "MAX x. B"     \<rightleftharpoons> "MAX x \<in> CONST UNIV. B"
-  "MAX x\<in>A. B"   \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)"
-
-print_translation \<open>
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MINIMUM} @{syntax_const "_MIN"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax MAXIMUM} @{syntax_const "_MAX"}]
-\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+  "MIN x y. f"   \<rightleftharpoons> "MIN x. MIN y. f"
+  "MIN x. f"     \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
+  "MIN x\<in>A. f"   \<rightleftharpoons> "CONST Min ((\<lambda>x. f) ` A)"
+  "MAX x y. f"   \<rightleftharpoons> "MAX x. MAX y. f"
+  "MAX x. f"     \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))"
+  "MAX x\<in>A. f"   \<rightleftharpoons> "CONST Max ((\<lambda>x. f) ` A)"
 
 text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close>