simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
--- 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)
---------------------------------
--- 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
--- 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)
--- 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"
--- 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>