--- a/NEWS Fri Aug 24 13:08:53 2018 +0200
+++ b/NEWS Fri Aug 24 13:09:35 2018 +0200
@@ -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 Fri Aug 24 13:08:53 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Fri Aug 24 13:09:35 2018 +0200
@@ -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 Fri Aug 24 13:08:53 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Aug 24 13:09:35 2018 +0200
@@ -18,58 +18,20 @@
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)"
- by (simp add: image_comp)
-
-lemma INF_identity_eq [simp]: "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
- by simp
-
-lemma INF_id_eq [simp]: "INFIMUM A id = \<Sqinter>A"
- by simp
-
-lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
- by (simp add: image_def)
-
-lemma strong_INF_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
- unfolding simp_implies_def by (fact INF_cong)
-
end
class Sup =
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)"
- by (simp add: image_comp)
-
-lemma SUP_identity_eq [simp]: "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
- by simp
-
-lemma SUP_id_eq [simp]: "SUPREMUM A id = \<Squnion>A"
- by (simp add: id_def)
-
-lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
- by (simp add: image_def)
-
-lemma strong_SUP_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
- unfolding simp_implies_def by (fact SUP_cong)
-
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,19 +51,54 @@
"_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> "CONST INFIMUM CONST UNIV (\<lambda>x. 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> "CONST SUPREMUM CONST UNIV (\<lambda>x. B)"
- "\<Squnion>x. B" \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
- "\<Squnion>x\<in>A. B" \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
+ "\<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)"
+
+context Inf
+begin
+
+lemma INF_image [simp]: " \<Sqinter>(g ` f ` A) = \<Sqinter>((g \<circ> f) ` A)"
+ by (simp add: image_comp)
+
+lemma INF_identity_eq [simp]: "(\<Sqinter>x\<in>A. x) = \<Sqinter>A"
+ by simp
+
+lemma INF_id_eq [simp]: "\<Sqinter>(id ` A) = \<Sqinter>A"
+ by simp
+
+lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
+ by (simp add: image_def)
-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>
+lemma strong_INF_cong [cong]:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
+ unfolding simp_implies_def by (fact INF_cong)
+
+end
+
+context Sup
+begin
+
+lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
+ by (simp add: image_comp)
+
+lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
+ by simp
+
+lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A"
+ by (simp add: id_def)
+
+lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
+ by (simp add: image_def)
+
+lemma strong_SUP_cong [cong]:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
+ unfolding simp_implies_def by (fact SUP_cong)
+
+end
subsection \<open>Abstract complete lattices\<close>
@@ -193,13 +190,13 @@
lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
-lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
+lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
by (simp cong del: strong_INF_cong)
lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
-lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
+lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
by (simp cong del: strong_SUP_cong)
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
@@ -282,13 +279,13 @@
lemma INF_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
- shows "INFIMUM A f = INFIMUM B g"
+ shows "\<Sqinter>(f ` A) = \<Sqinter>(g ` B)"
by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
lemma SUP_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
- shows "SUPREMUM A f = SUPREMUM B g"
+ shows "\<Squnion>(f ` A) = \<Squnion>(g ` B)"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
@@ -435,20 +432,20 @@
lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
-lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
+lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> \<Sqinter>(f ` A) \<le> \<Squnion>(f ` A)"
using Inf_le_Sup [of "f ` A"] by simp
-lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
+lemma INF_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Sqinter>(f ` I) = x"
by (auto intro: INF_eqI)
-lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
+lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Squnion>(f ` I) = x"
by (auto intro: SUP_eqI)
-lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> INFIMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
using INF_eq_const [of I f c] INF_lower [of _ I f]
by (auto intro: antisym cong del: strong_INF_cong)
-lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> SUPREMUM I f = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
using SUP_eq_const [of I f c] SUP_upper [of _ I f]
by (auto intro: antisym cong del: strong_SUP_cong)
@@ -480,7 +477,8 @@
by (rule le_infI1, simp)
have [simp]: "b \<sqinter> a \<le> a \<squnion> b \<sqinter> c"
by (rule le_infI2, simp)
- have " INFIMUM {{a, b}, {a, c}} Sup = SUPREMUM {f ` {{a, b}, {a, c}} |f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y} Inf"
+ have "\<Sqinter>(Sup ` {{a, b}, {a, c}}) =
+ \<Squnion>(Inf ` {f ` {{a, b}, {a, c}} | f. \<forall>Y\<in>{{a, b}, {a, c}}. f Y \<in> Y})"
by (rule Inf_Sup)
from this show "(a \<squnion> b) \<sqinter> (a \<squnion> c) \<le> a \<squnion> b \<sqinter> c"
apply simp
@@ -854,14 +852,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)
@@ -875,14 +868,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> "CONST INTER CONST UNIV (\<lambda>x. 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)
@@ -1024,14 +1012,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)
@@ -1045,10 +1028,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> "CONST UNION CONST UNIV (\<lambda>x. 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
@@ -1056,10 +1038,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 Fri Aug 24 13:08:53 2018 +0200
+++ b/src/HOL/GCD.thy Fri Aug 24 13:09:35 2018 +0200
@@ -146,35 +146,20 @@
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)
"_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
"_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _./ _)" [0, 10] 10)
"_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> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. 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> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. 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 Fri Aug 24 13:08:53 2018 +0200
+++ b/src/HOL/Lattices_Big.thy Fri Aug 24 13:09:35 2018 +0200
@@ -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,19 +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> "CONST MINIMUM CONST UNIV (\<lambda>x. 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> "CONST MAXIMUM CONST UNIV (\<lambda>x. 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>