--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sun Aug 25 21:27:25 2024 +0100
@@ -28,6 +28,8 @@
syntax
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/CCL/Set.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/CCL/Set.thy Sun Aug 25 21:27:25 2024 +0100
@@ -19,10 +19,10 @@
syntax
"_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})")
+syntax_consts
+ "_Coll" == Collect
translations
"{x. P}" == "CONST Collect(\<lambda>x. P)"
-syntax_consts
- "_Coll" == Collect
lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
apply (rule mem_Collect_iff [THEN iffD2])
@@ -52,12 +52,12 @@
syntax
"_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" ("(ALL _:_./ _)" [0, 0, 0] 10)
"_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" ("(EX _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+ "_Ball" == Ball and
+ "_Bex" == Bex
translations
"ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)"
"EX x:A. P" == "CONST Bex(A, \<lambda>x. P)"
-syntax_consts
- "_Ball" == Ball and
- "_Bex" == Bex
lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
by (simp add: Ball_def)
@@ -129,12 +129,12 @@
syntax
"_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
"_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
+syntax_consts
+ "_INTER" == INTER and
+ "_UNION" == UNION
translations
"INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
"UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
-syntax_consts
- "_INTER" == INTER and
- "_UNION" == UNION
definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
where "Inter(S) == (INT x:S. x)"
--- a/src/CCL/Term.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/CCL/Term.thy Sun Aug 25 21:27:25 2024 +0100
@@ -49,8 +49,8 @@
where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
+syntax_consts "_let1" == let1
translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
-syntax_consts "_let1" == let1
definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -68,6 +68,10 @@
"_letrec" :: "[idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
"_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
"_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+syntax_consts
+ "_letrec" == letrec and
+ "_letrec2" == letrec2 and
+ "_letrec3" == letrec3
parse_translation \<open>
let
fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
@@ -123,10 +127,6 @@
(\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
end
\<close>
-syntax_consts
- "_letrec" == letrec and
- "_letrec2" == letrec2 and
- "_letrec3" == letrec3
definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
--- a/src/CCL/Type.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/CCL/Type.thy Sun Aug 25 21:27:25 2024 +0100
@@ -14,10 +14,10 @@
syntax
"_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})")
+syntax_consts
+ "_Subtype" == Subtype
translations
"{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
-syntax_consts
- "_Subtype" == Subtype
definition Unit :: "i set"
where "Unit == {x. x=one}"
@@ -39,6 +39,9 @@
"_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3SUM _:_./ _)" [0,0,60] 60)
"_arrow" :: "[i set, i set] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53)
"_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55)
+syntax_consts
+ "_Pi" "_arrow" \<rightleftharpoons> Pi and
+ "_Sigma" "_star" \<rightleftharpoons> Sigma
translations
"PROD x:A. B" \<rightharpoonup> "CONST Pi(A, \<lambda>x. B)"
"A -> B" \<rightharpoonup> "CONST Pi(A, \<lambda>_. B)"
@@ -50,9 +53,6 @@
(\<^const_syntax>\<open>Sigma\<close>,
fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Sigma\<close>, \<^syntax_const>\<open>_star\<close>))]
\<close>
-syntax_consts
- "_Pi" "_arrow" \<rightleftharpoons> Pi and
- "_Sigma" "_star" \<rightleftharpoons> Sigma
definition Nat :: "i set"
where "Nat == lfp(\<lambda>X. Unit + X)"
--- a/src/CTT/CTT.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/CTT/CTT.thy Sun Aug 25 21:27:25 2024 +0100
@@ -58,12 +58,12 @@
syntax
"_PROD" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Prod>_:_./ _)" 10)
"_SUM" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Sum>_:_./ _)" 10)
+syntax_consts
+ "_PROD" \<rightleftharpoons> Prod and
+ "_SUM" \<rightleftharpoons> Sum
translations
"\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
"\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
-syntax_consts
- "_PROD" \<rightleftharpoons> Prod and
- "_SUM" \<rightleftharpoons> Sum
abbreviation Arrow :: "[t,t]\<Rightarrow>t" (infixr "\<longrightarrow>" 30)
where "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"
--- a/src/Cube/Cube.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Cube/Cube.thy Sun Aug 25 21:27:25 2024 +0100
@@ -39,6 +39,13 @@
"_Lam" :: "[idt, term, term] \<Rightarrow> term" ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10)
"_Pi" :: "[idt, term, term] \<Rightarrow> term" ("(3\<Prod>_:_./ _)" [0, 0] 10)
"_arrow" :: "[term, term] \<Rightarrow> term" (infixr "\<rightarrow>" 10)
+syntax_consts
+ "_Trueprop" \<rightleftharpoons> Trueprop and
+ "_MT_context" \<rightleftharpoons> MT_context and
+ "_Context" \<rightleftharpoons> Context and
+ "_Has_type" \<rightleftharpoons> Has_type and
+ "_Lam" \<rightleftharpoons> Abs and
+ "_Pi" "_arrow" \<rightleftharpoons> Prod
translations
"_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X"
@@ -52,13 +59,6 @@
[(\<^const_syntax>\<open>Prod\<close>,
fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Pi\<close>, \<^syntax_const>\<open>_arrow\<close>))]
\<close>
-syntax_consts
- "_Trueprop" \<rightleftharpoons> Trueprop and
- "_MT_context" \<rightleftharpoons> MT_context and
- "_Context" \<rightleftharpoons> Context and
- "_Has_type" \<rightleftharpoons> Has_type and
- "_Lam" \<rightleftharpoons> Abs and
- "_Pi" "_arrow" \<rightleftharpoons> Prod
axiomatization where
s_b: "*: \<box>" and
--- a/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sun Aug 25 21:27:25 2024 +0100
@@ -81,6 +81,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/FOL/IFOL.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/FOL/IFOL.thy Sun Aug 25 21:27:25 2024 +0100
@@ -102,8 +102,8 @@
where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
-syntax_consts "_Uniq" \<rightleftharpoons> Uniq
print_translation \<open>
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
@@ -747,10 +747,10 @@
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
"_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(let (_)/ in (_))\<close> 10)
+syntax_consts "_Let" \<rightleftharpoons> Let
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "CONST Let(a, \<lambda>x. e)"
-syntax_consts "_Let" \<rightleftharpoons> Let
lemma LetI:
assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>
--- a/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Sun Aug 25 21:27:25 2024 +0100
@@ -308,6 +308,8 @@
syntax
"_finprod" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
+syntax_consts
+ "_finprod" \<rightleftharpoons> finprod
translations
"\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A"
\<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/Algebra/Lattice.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Algebra/Lattice.thy Sun Aug 25 21:27:25 2024 +0100
@@ -36,6 +36,10 @@
"_sup1" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrns \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _./ _)" [0, 10] 10)
"_sup" :: "('a, 'b) gorder_scheme \<Rightarrow> pttrn \<Rightarrow> 'c set \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SSUP\<index> _:_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_inf1" "_inf" == infi and
+ "_sup1" "_sup" == supr
+
translations
"IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)"
"IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)"
--- a/src/HOL/Algebra/Ring.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Algebra/Ring.thy Sun Aug 25 21:27:25 2024 +0100
@@ -46,6 +46,8 @@
syntax
"_finsum" :: "index \<Rightarrow> idt \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"
("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
+syntax_consts
+ "_finsum" \<rightleftharpoons> finsum
translations
"\<Oplus>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finsum G (\<lambda>i. b) A"
\<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy Sun Aug 25 21:27:25 2024 +0100
@@ -1588,7 +1588,7 @@
by (force simp: Cauchy_def Met_TC.MCauchy_def)
lemma mcomplete_iff_complete [iff]:
- "Met_TC.mcomplete (Pure.type ::'a::metric_space itself) \<longleftrightarrow> complete (UNIV::'a set)"
+ "Met_TC.mcomplete TYPE('a::metric_space) \<longleftrightarrow> complete (UNIV::'a set)"
by (auto simp: Met_TC.mcomplete_def complete_def)
context Submetric
--- a/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Sun Aug 25 21:27:25 2024 +0100
@@ -892,12 +892,18 @@
syntax
"_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" ("\<integral>((2 _./ _)/ \<partial>_)" [60,61] 110)
+syntax_consts
+ "_lebesgue_integral" == lebesgue_integral
+
translations
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
syntax
"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
+syntax_consts
+ "_ascii_lebesgue_integral" == lebesgue_integral
+
translations
"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
--- a/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Sun Aug 25 21:27:25 2024 +0100
@@ -34,6 +34,7 @@
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
syntax "_type_dimension" :: "type \<Rightarrow> nat" ("(1DIM/(1'(_')))")
+syntax_consts "_type_dimension" \<rightleftharpoons> card
translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
typed_print_translation \<open>
[(\<^const_syntax>\<open>card\<close>,
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Aug 25 21:27:25 2024 +0100
@@ -40,6 +40,7 @@
\<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
\<close>
syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
+syntax_types "_vec_type" \<rightleftharpoons> vec
parse_translation \<open>
let
fun vec t u = Syntax.const \<^type_syntax>\<open>vec\<close> $ t $ u;
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 25 21:27:25 2024 +0100
@@ -170,6 +170,8 @@
syntax
"_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
+syntax_consts
+ "_PiM" == PiM
translations
"\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Sun Aug 25 21:27:25 2024 +0100
@@ -100,6 +100,8 @@
syntax
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
+syntax_consts
+ "_infsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
@@ -109,6 +111,8 @@
syntax
"_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
+syntax_consts
+ "_uinfsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
@@ -118,6 +122,8 @@
syntax
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qinfsetsum" \<rightleftharpoons> infsetsum
translations
"\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Sun Aug 25 21:27:25 2024 +0100
@@ -50,6 +50,8 @@
"_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(3INFSUM (_/:_)./ _)" [0, 51, 10] 10)
syntax
"_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" ("(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)" [0, 51, 10] 10)
+syntax_consts
+ "_infsum" \<rightleftharpoons> infsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
@@ -57,6 +59,8 @@
"_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _./ _)" [0, 10] 10)
syntax
"_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_./ _)" [0, 10] 10)
+syntax_consts
+ "_univinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
@@ -64,6 +68,8 @@
"_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3INFSUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
"_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
--- a/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Sun Aug 25 21:27:25 2024 +0100
@@ -148,6 +148,9 @@
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
+
translations
"LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
@@ -159,6 +162,9 @@
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
("(4LBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
+
translations
"LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
@@ -1045,11 +1051,17 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
("(2CLBINT _. _)" [0,60] 60)
+syntax_consts
+ "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
+
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
("(3CLBINT _:_. _)" [0,60,61] 60)
+syntax_consts
+ "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
+
translations
"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
@@ -1065,6 +1077,9 @@
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
+syntax_consts
+ "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
+
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
--- a/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 21:27:25 2024 +0100
@@ -1006,6 +1006,9 @@
syntax
"_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
+syntax_consts
+ "_almost_everywhere" \<rightleftharpoons> almost_everywhere
+
translations
"AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
@@ -1016,6 +1019,9 @@
"_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+syntax_consts
+ "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
+
translations
"AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Aug 25 21:27:25 2024 +0100
@@ -586,6 +586,9 @@
syntax
"_simple_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>S _. _ \<partial>_" [60,61] 110)
+syntax_consts
+ "_simple_integral" == simple_integral
+
translations
"\<integral>\<^sup>S x. f \<partial>M" == "CONST simple_integral M (%x. f)"
@@ -819,6 +822,9 @@
syntax
"_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
+syntax_consts
+ "_nn_integral" == nn_integral
+
translations
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
--- a/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Sun Aug 25 21:27:25 2024 +0100
@@ -26,6 +26,9 @@
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10)
+syntax_consts
+ "_ascii_set_lebesgue_integral" == set_lebesgue_integral
+
translations
"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -576,6 +579,9 @@
"_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
("\<integral>\<^sup>C _. _ \<partial>_" [0,0] 110)
+syntax_consts
+ "_complex_lebesgue_integral" == complex_lebesgue_integral
+
translations
"\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -583,6 +589,9 @@
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(3CLINT _|_. _)" [0,0,10] 10)
+syntax_consts
+ "_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
+
translations
"CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -617,6 +626,9 @@
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
("(4CLINT _:_|_. _)" [0,0,0,10] 10)
+syntax_consts
+ "_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
+
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
@@ -640,6 +652,10 @@
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,0,0,110] 10)
+syntax_consts
+"_set_nn_integral" == set_nn_integral and
+"_set_lebesgue_integral" == set_lebesgue_integral
+
translations
"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
--- a/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 21:27:25 2024 +0100
@@ -166,11 +166,15 @@
syntax
"_eventually_cosparse" :: "pttrn => 'a set => bool => bool" ("(3\<forall>\<^sub>\<approx>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_eventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
syntax
"_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<forall>\<^sub>\<approx>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qeventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"
--- a/src/HOL/Auth/Message.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Auth/Message.thy Sun Aug 25 21:27:25 2024 +0100
@@ -51,6 +51,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" \<rightleftharpoons> MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Sun Aug 25 21:27:25 2024 +0100
@@ -275,6 +275,9 @@
"pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
("(3CSUM _:_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_Csum" == Csum
+
translations
"CSUM i:r. rs" == "CONST Csum r (%i. rs)"
--- a/src/HOL/Bali/AxSem.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Bali/AxSem.thy Sun Aug 25 21:27:25 2024 +0100
@@ -205,6 +205,8 @@
syntax
"_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)
+syntax_consts
+ "_peek_res" == peek_res
translations
"\<lambda>w:. P" == "CONST peek_res (\<lambda>w. P)"
@@ -266,6 +268,8 @@
syntax
"_peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)
+syntax_consts
+ "_peek_st" == peek_st
translations
"\<lambda>s.. P" == "CONST peek_st (\<lambda>s. P)"
--- a/src/HOL/Bali/Basis.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Aug 25 21:27:25 2024 +0100
@@ -195,6 +195,10 @@
"_Oall" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
"_Oex" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
+syntax_consts
+ "_Oall" \<rightleftharpoons> Ball and
+ "_Oex" \<rightleftharpoons> Bex
+
translations
"\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST set_option A. P"
"\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
@@ -257,6 +261,8 @@
text \<open>list patterns -- extends pre-defined type "pttrn" used in abstractions\<close>
syntax
"_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn" ("_#/_" [901,900] 900)
+syntax_consts
+ "_lpttrn" \<rightleftharpoons> lsplit
translations
"\<lambda>y # x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>y x # xs. b)"
"\<lambda>x # xs. b" \<rightleftharpoons> "CONST lsplit (\<lambda>x xs. b)"
--- a/src/HOL/Bali/State.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Bali/State.thy Sun Aug 25 21:27:25 2024 +0100
@@ -135,6 +135,10 @@
Heap :: "loc \<Rightarrow> oref"
Stat :: "qtname \<Rightarrow> oref"
+syntax_consts
+ Heap == Inl and
+ Stat == Inr
+
translations
"Heap" => "CONST Inl"
"Stat" => "CONST Inr"
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 21:27:25 2024 +0100
@@ -24,6 +24,7 @@
no_notation lazy_llist ("_")
syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]")
+syntax_consts "_llist" == lazy_llist
translations
"\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
"\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
--- a/src/HOL/Complete_Lattices.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Aug 25 21:27:25 2024 +0100
@@ -32,6 +32,10 @@
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_INF1" "_INF" \<rightleftharpoons> Inf and
+ "_SUP1" "_SUP" \<rightleftharpoons> Sup
+
translations
"\<Sqinter>x y. f" \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
"\<Sqinter>x. f" \<rightleftharpoons> "\<Sqinter>(CONST range (\<lambda>x. f))"
@@ -850,6 +854,9 @@
"_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
"_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+syntax_consts
+ "_INTER1" "_INTER" \<rightleftharpoons> Inter
+
translations
"\<Inter>x y. f" \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
"\<Inter>x. f" \<rightleftharpoons> "\<Inter>(CONST range (\<lambda>x. f))"
@@ -1013,6 +1020,9 @@
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+syntax_consts
+ "_UNION1" "_UNION" \<rightleftharpoons> Union
+
translations
"\<Union>x y. f" \<rightleftharpoons> "\<Union>x. \<Union>y. f"
"\<Union>x. f" \<rightleftharpoons> "\<Union>(CONST range (\<lambda>x. f))"
--- a/src/HOL/Filter.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Filter.thy Sun Aug 25 21:27:25 2024 +0100
@@ -41,6 +41,8 @@
syntax
"_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_eventually" == eventually
translations
"\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
@@ -159,6 +161,8 @@
syntax
"_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_frequently" == frequently
translations
"\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
@@ -1305,6 +1309,9 @@
syntax
"_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
+syntax_consts
+ "_LIM" == filterlim
+
translations
"LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
--- a/src/HOL/Fun.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Fun.thy Sun Aug 25 21:27:25 2024 +0100
@@ -846,6 +846,9 @@
"_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
"_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" ("_/'((_)')" [1000, 0] 900)
+syntax_consts
+ "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
+
translations
"_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
"f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
--- a/src/HOL/GCD.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/GCD.thy Sun Aug 25 21:27:25 2024 +0100
@@ -153,6 +153,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)
+syntax_consts
+ "_GCD1" "_GCD" \<rightleftharpoons> Gcd and
+ "_LCM1" "_LCM" \<rightleftharpoons> Lcm
+
translations
"GCD x y. f" \<rightleftharpoons> "GCD x. GCD y. f"
"GCD x. f" \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))"
@@ -2847,18 +2851,23 @@
definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat"
where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
+syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
+syntax_consts "_type_char" \<rightleftharpoons> semiring_char
+translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
+print_translation \<open>
+ let
+ fun char_type_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
+ Syntax.const \<^syntax_const>\<open>_type_char\<close> $ Syntax_Phases.term_of_typ ctxt T
+ in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
+\<close>
+
context semiring_1
begin
-context
- fixes CHAR :: nat
- defines "CHAR \<equiv> semiring_char (Pure.type :: 'a itself)"
-begin
-
-lemma of_nat_CHAR [simp]: "of_nat CHAR = (0 :: 'a)"
+lemma of_nat_CHAR [simp]: "of_nat CHAR('a) = (0 :: 'a)"
proof -
- have "CHAR \<in> {n. of_nat n = (0::'a)}"
- unfolding CHAR_def semiring_char_def
+ have "CHAR('a) \<in> {n. of_nat n = (0::'a)}"
+ unfolding semiring_char_def
proof (rule Gcd_in, clarify)
fix a b :: nat
assume *: "of_nat a = (0 :: 'a)" "of_nat b = (0 :: 'a)"
@@ -2882,14 +2891,14 @@
by simp
qed
-lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \<longleftrightarrow> CHAR dvd n"
+lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \<longleftrightarrow> CHAR('a) dvd n"
proof
assume "of_nat n = (0 :: 'a)"
- thus "CHAR dvd n"
- unfolding CHAR_def semiring_char_def by (intro Gcd_dvd) auto
+ thus "CHAR('a) dvd n"
+ unfolding semiring_char_def by (intro Gcd_dvd) auto
next
- assume "CHAR dvd n"
- then obtain m where "n = CHAR * m"
+ assume "CHAR('a) dvd n"
+ then obtain m where "n = CHAR('a) * m"
by auto
thus "of_nat n = (0 :: 'a)"
by simp
@@ -2898,51 +2907,36 @@
lemma CHAR_eqI:
assumes "of_nat c = (0 :: 'a)"
assumes "\<And>x. of_nat x = (0 :: 'a) \<Longrightarrow> c dvd x"
- shows "CHAR = c"
+ shows "CHAR('a) = c"
using assms by (intro dvd_antisym) (auto simp: of_nat_eq_0_iff_char_dvd)
-lemma CHAR_eq0_iff: "CHAR = 0 \<longleftrightarrow> (\<forall>n>0. of_nat n \<noteq> (0::'a))"
+lemma CHAR_eq0_iff: "CHAR('a) = 0 \<longleftrightarrow> (\<forall>n>0. of_nat n \<noteq> (0::'a))"
by (auto simp: of_nat_eq_0_iff_char_dvd)
-lemma CHAR_pos_iff: "CHAR > 0 \<longleftrightarrow> (\<exists>n>0. of_nat n = (0::'a))"
+lemma CHAR_pos_iff: "CHAR('a) > 0 \<longleftrightarrow> (\<exists>n>0. of_nat n = (0::'a))"
using CHAR_eq0_iff neq0_conv by blast
lemma CHAR_eq_posI:
assumes "c > 0" "of_nat c = (0 :: 'a)" "\<And>x. x > 0 \<Longrightarrow> x < c \<Longrightarrow> of_nat x \<noteq> (0 :: 'a)"
- shows "CHAR = c"
+ shows "CHAR('a) = c"
proof (rule antisym)
- from assms have "CHAR > 0"
+ from assms have "CHAR('a) > 0"
by (auto simp: CHAR_pos_iff)
- from assms(3)[OF this] show "CHAR \<ge> c"
+ from assms(3)[OF this] show "CHAR('a) \<ge> c"
by force
next
- have "CHAR dvd c"
+ have "CHAR('a) dvd c"
using assms by (auto simp: of_nat_eq_0_iff_char_dvd)
- thus "CHAR \<le> c"
+ thus "CHAR('a) \<le> c"
using \<open>c > 0\<close> by (intro dvd_imp_le) auto
qed
end
-end
-
-lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char (Pure.type :: 'a itself) = 0"
+
+lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0"
by (simp add: CHAR_eq0_iff)
-(* nicer notation *)
-
-syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
-
-translations "CHAR('t)" => "CONST semiring_char (CONST Pure.type :: 't itself)"
-
-print_translation \<open>
- let
- fun char_type_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
- Syntax.const \<^syntax_const>\<open>_type_char\<close> $ Syntax_Phases.term_of_typ ctxt T
- in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
-\<close>
-
-
lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \<noteq> Suc 0"
by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one)
--- a/src/HOL/Groups_Big.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Groups_Big.thy Sun Aug 25 21:27:25 2024 +0100
@@ -654,32 +654,41 @@
"_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10)
syntax
"_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10)
+
+syntax_consts
+ "_sum" \<rightleftharpoons> sum
+
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A"
+
text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
syntax (ASCII)
"_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
syntax
"_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
+
+syntax_consts
+ "_qsum" == sum
+
translations
"\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
print_translation \<open>
-let
- fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
- if x <> y then raise Match
- else
- let
- val x' = Syntax_Trans.mark_bound_body (x, Tx);
- val t' = subst_bound (x', t);
- val P' = subst_bound (x', P);
- in
- Syntax.const \<^syntax_const>\<open>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
-in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end
+ let
+ fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
+ if x <> y then raise Match
+ else
+ let
+ val x' = Syntax_Trans.mark_bound_body (x, Tx);
+ val t' = subst_bound (x', t);
+ val P' = subst_bound (x', P);
+ in
+ Syntax.const \<^syntax_const>\<open>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+ end
+ | sum_tr' _ = raise Match;
+ in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end
\<close>
@@ -1415,18 +1424,43 @@
"_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10)
syntax
"_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10)
+
+syntax_consts
+ "_prod" == prod
+
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
+
text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
syntax (ASCII)
"_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
syntax
"_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
+
+syntax_consts
+ "_qprod" == prod
+
translations
"\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
+print_translation \<open>
+ let
+ fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] =
+ if x <> y then raise Match
+ else
+ let
+ val x' = Syntax_Trans.mark_bound_body (x, Tx);
+ val t' = subst_bound (x', t);
+ val P' = subst_bound (x', P);
+ in
+ Syntax.const \<^syntax_const>\<open>_qprod\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
+ end
+ | prod_tr' _ = raise Match;
+ in [(\<^const_syntax>\<open>prod\<close>, K prod_tr')] end
+\<close>
+
context comm_monoid_mult
begin
--- a/src/HOL/Groups_List.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Groups_List.thy Sun Aug 25 21:27:25 2024 +0100
@@ -101,6 +101,8 @@
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax
"_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_sum_list" == sum_list
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)"
@@ -598,6 +600,8 @@
"_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax
"_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_prod_list" \<rightleftharpoons> prod_list
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)"
--- a/src/HOL/HOL.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOL.thy Sun Aug 25 21:27:25 2024 +0100
@@ -129,6 +129,9 @@
syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(4?< _./ _)" [0, 10] 10)
syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
+
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
print_translation \<open>
@@ -141,6 +144,9 @@
syntax (input)
"_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3?! _./ _)" [0, 10] 10)
syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!_./ _)" [0, 10] 10)
+
+syntax_consts "_Ex1" \<rightleftharpoons> Ex1
+
translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
print_translation \<open>
@@ -151,6 +157,9 @@
syntax
"_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_./ _)" [0, 10] 10)
"_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_./ _)" [0, 10] 10)
+syntax_consts
+ "_Not_Ex" \<rightleftharpoons> Ex and
+ "_Not_Ex1" \<rightleftharpoons> Ex1
translations
"\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
"\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
@@ -171,6 +180,7 @@
where "A \<longleftrightarrow> B \<equiv> A = B"
syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" ("(3THE _./ _)" [0, 10] 10)
+syntax_consts "_The" \<rightleftharpoons> The
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
print_translation \<open>
[(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
@@ -178,13 +188,6 @@
in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
\<close> \<comment> \<open>To avoid eta-contraction of body\<close>
-nonterminal letbinds and letbind
-syntax
- "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10)
- "" :: "letbind \<Rightarrow> letbinds" ("_")
- "_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" ("(let (_)/ in (_))" [0, 10] 10)
-
nonterminal case_syn and cases_syn
syntax
"_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" ("(case _ of/ _)" 10)
@@ -227,6 +230,14 @@
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
where "Let s f \<equiv> f s"
+nonterminal letbinds and letbind
+syntax
+ "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10)
+ "" :: "letbind \<Rightarrow> letbinds" ("_")
+ "_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _")
+ "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" ("(let (_)/ in (_))" [0, 10] 10)
+syntax_consts
+ "_bind" "_binds" "_Let" \<rightleftharpoons> Let
translations
"_Let (_binds b bs) e" \<rightleftharpoons> "_Let b (_Let bs e)"
"let x = a in e" \<rightleftharpoons> "CONST Let a (\<lambda>x. e)"
--- a/src/HOL/HOLCF/Cfun.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Sun Aug 25 21:27:25 2024 +0100
@@ -52,6 +52,9 @@
syntax
"_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
+syntax_consts
+ "_Lambda" \<rightleftharpoons> Abs_cfun
+
parse_ast_translation \<open>
(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Sun Aug 25 21:27:25 2024 +0100
@@ -181,6 +181,9 @@
syntax
"_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
+syntax_consts
+ "_convex_pd" == convex_add
+
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
"{x}\<natural>" == "CONST convex_unit\<cdot>x"
@@ -348,6 +351,9 @@
"_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<natural>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_convex_bind" == convex_bind
+
translations
"\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Sun Aug 25 21:27:25 2024 +0100
@@ -72,6 +72,8 @@
syntax
"_totlist" :: "args \<Rightarrow> 'a Seq" ("[(_)!]")
"_partlist" :: "args \<Rightarrow> 'a Seq" ("[(_)?]")
+syntax_consts
+ "_totlist" "_partlist" \<rightleftharpoons> Consq
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"
--- a/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Sun Aug 25 21:27:25 2024 +0100
@@ -136,6 +136,9 @@
syntax
"_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
+syntax_consts
+ "_lower_pd" == lower_add
+
translations
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
"{x}\<flat>" == "CONST lower_unit\<cdot>x"
@@ -342,6 +345,9 @@
"_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<flat>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_lower_bind" == lower_bind
+
translations
"\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy Sun Aug 25 21:27:25 2024 +0100
@@ -153,6 +153,7 @@
text \<open>Old "UU" syntax:\<close>
syntax UU :: logic
+syntax_consts UU \<rightleftharpoons> bottom
translations "UU" \<rightharpoonup> "CONST bottom"
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
--- a/src/HOL/HOLCF/Porder.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/Porder.thy Sun Aug 25 21:27:25 2024 +0100
@@ -118,6 +118,9 @@
syntax
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
+syntax_consts
+ "_BLub" \<rightleftharpoons> lub
+
translations
"LUB x:A. t" \<rightleftharpoons> "CONST lub ((\<lambda>x. t) ` A)"
--- a/src/HOL/HOLCF/Representable.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/Representable.thy Sun Aug 25 21:27:25 2024 +0100
@@ -32,6 +32,7 @@
assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a)) = liftemb oo liftprj"
syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))")
+syntax_consts "_LIFTDEFL" \<rightleftharpoons> liftdefl
translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)"
definition liftdefl_of :: "udom defl \<rightarrow> udom u defl"
@@ -51,6 +52,7 @@
assumes liftdefl_eq: "liftdefl TYPE('a) = liftdefl_of\<cdot>(defl TYPE('a))"
syntax "_DEFL" :: "type \<Rightarrow> logic" ("(1DEFL/(1'(_')))")
+syntax_consts "_DEFL" \<rightleftharpoons> defl
translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)"
instance "domain" \<subseteq> predomain
--- a/src/HOL/HOLCF/Sprod.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/Sprod.thy Sun Aug 25 21:27:25 2024 +0100
@@ -41,6 +41,7 @@
where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+syntax_consts "_stuple" \<rightleftharpoons> spair
translations
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Sun Aug 25 21:27:25 2024 +0100
@@ -134,6 +134,9 @@
syntax
"_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
+syntax_consts
+ "_upper_pd" == upper_add
+
translations
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
"{x}\<sharp>" == "CONST upper_unit\<cdot>x"
@@ -335,6 +338,9 @@
"_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
("(3\<Union>\<sharp>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_upper_bind" == upper_bind
+
translations
"\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy Sun Aug 25 21:27:25 2024 +0100
@@ -22,6 +22,9 @@
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
+syntax_consts
+ "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec
+
translations
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)"
--- a/src/HOL/Hilbert_Choice.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sun Aug 25 21:27:25 2024 +0100
@@ -22,6 +22,9 @@
"_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3@ _./ _)" [0, 10] 10)
syntax
"_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+
+syntax_consts "_Eps" \<rightleftharpoons> Eps
+
translations
"SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
--- a/src/HOL/Lattices_Big.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Lattices_Big.thy Sun Aug 25 21:27:25 2024 +0100
@@ -470,6 +470,10 @@
"_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10)
"_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_MIN1" "_MIN" \<rightleftharpoons> Min and
+ "_MAX1" "_MAX" \<rightleftharpoons> Max
+
translations
"MIN x y. f" \<rightleftharpoons> "MIN x. MIN y. f"
"MIN x. f" \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
@@ -478,6 +482,7 @@
"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>\<open>Min\<close>/\<^const>\<open>Max\<close> on linear orders as special case of \<^const>\<open>Inf_fin\<close>/\<^const>\<open>Sup_fin\<close>\<close>
lemma Inf_fin_Min:
@@ -919,6 +924,8 @@
syntax
"_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
+syntax_consts
+ "_arg_min" \<rightleftharpoons> arg_min
translations
"ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
@@ -1028,6 +1035,8 @@
syntax
"_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
+syntax_consts
+ "_arg_max" \<rightleftharpoons> arg_max
translations
"ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
--- a/src/HOL/Library/Cardinality.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Cardinality.thy Sun Aug 25 21:27:25 2024 +0100
@@ -32,6 +32,8 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
+syntax_consts "_type_card" == card
+
translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)"
print_translation \<open>
--- a/src/HOL/Library/FSet.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/FSet.thy Sun Aug 25 21:27:25 2024 +0100
@@ -167,6 +167,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == finsert
+
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
@@ -200,6 +203,10 @@
"_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
"_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_fBall" \<rightleftharpoons> FSet.Ball and
+ "_fBex" \<rightleftharpoons> FSet.Bex
+
translations
"\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
"\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
--- a/src/HOL/Library/FuncSet.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/FuncSet.thy Sun Aug 25 21:27:25 2024 +0100
@@ -25,6 +25,9 @@
syntax
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi> _\<in>_./ _)" 10)
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
+syntax_consts
+ "_Pi" \<rightleftharpoons> Pi and
+ "_lam" \<rightleftharpoons> restrict
translations
"\<Pi> x\<in>A. B" \<rightleftharpoons> "CONST Pi A (\<lambda>x. B)"
"\<lambda>x\<in>A. f" \<rightleftharpoons> "CONST restrict (\<lambda>x. f) A"
@@ -350,6 +353,8 @@
syntax
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
+syntax_consts
+ "_PiE" \<rightleftharpoons> Pi\<^sub>E
translations
"\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Aug 25 21:27:25 2024 +0100
@@ -202,6 +202,8 @@
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _. _)" [0, 10] 10)
syntax
"_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_. _)" [0, 10] 10)
+syntax_consts
+ "_Sum_any" \<rightleftharpoons> Sum_any
translations
"\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
@@ -255,6 +257,8 @@
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _. _)" [0, 10] 10)
syntax
"_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_. _)" [0, 10] 10)
+syntax_consts
+ "_Prod_any" == Prod_any
translations
"\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
--- a/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Sun Aug 25 21:27:25 2024 +0100
@@ -46,6 +46,11 @@
"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
+syntax_consts
+ "_do_block" "_do_cons" \<rightleftharpoons> bind_do and
+ "_do_bind" "_thenM" \<rightleftharpoons> bind and
+ "_do_let" \<rightleftharpoons> Let
+
translations
"_do_block (_do_cons (_do_then t) (_do_final e))"
\<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
--- a/src/HOL/Library/Multiset.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Aug 25 21:27:25 2024 +0100
@@ -93,6 +93,8 @@
syntax
"_multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}")
+syntax_consts
+ "_multiset" == add_mset
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
@@ -169,6 +171,10 @@
"_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
"_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_MBall" \<rightleftharpoons> Multiset.Ball and
+ "_MBex" \<rightleftharpoons> Multiset.Bex
+
translations
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
@@ -1248,6 +1254,8 @@
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ :# _./ _#})")
syntax
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{#_ \<in># _./ _#})")
+syntax_consts
+ "_MCollect" == filter_mset
translations
"{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
@@ -1821,6 +1829,8 @@
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ :# _#})")
syntax
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ \<in># _#})")
+syntax_consts
+ "_comprehension_mset" \<rightleftharpoons> image_mset
translations
"{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
@@ -1828,6 +1838,8 @@
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/ | _ :# _./ _#})")
syntax
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/ | _ \<in># _./ _#})")
+syntax_consts
+ "_comprehension_mset'" \<rightleftharpoons> image_mset
translations
"{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
@@ -2675,6 +2687,8 @@
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_sum_mset_image" \<rightleftharpoons> sum_mset
translations
"\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
@@ -2854,6 +2868,8 @@
"_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10)
syntax
"_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
+syntax_consts
+ "_prod_mset_image" \<rightleftharpoons> prod_mset
translations
"\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
--- a/src/HOL/Library/Numeral_Type.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sun Aug 25 21:27:25 2024 +0100
@@ -540,6 +540,10 @@
"_NumeralType0" :: type ("0")
"_NumeralType1" :: type ("1")
+syntax_types
+ "_NumeralType0" == num0 and
+ "_NumeralType1" == num1
+
translations
(type) "1" == (type) "num1"
(type) "0" == (type) "num0"
--- a/src/HOL/Library/Phantom_Type.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Phantom_Type.thy Sun Aug 25 21:27:25 2024 +0100
@@ -18,6 +18,7 @@
by(simp_all add: o_def id_def)
syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))")
+syntax_consts "_Phantom" == phantom
translations
"Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
--- a/src/HOL/Library/Type_Length.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Library/Type_Length.thy Sun Aug 25 21:27:25 2024 +0100
@@ -19,6 +19,9 @@
syntax "_type_length" :: "type \<Rightarrow> nat" (\<open>(1LENGTH/(1'(_')))\<close>)
+syntax_consts
+ "_type_length" \<rightleftharpoons> len_of
+
translations "LENGTH('a)" \<rightharpoonup>
"CONST len_of (CONST Pure.type :: 'a itself)"
--- a/src/HOL/List.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/List.thy Sun Aug 25 21:27:25 2024 +0100
@@ -46,6 +46,9 @@
\<comment> \<open>list Enumeration\<close>
"_list" :: "args => 'a list" ("[(_)]")
+syntax_consts
+ "_list" == Cons
+
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
@@ -83,6 +86,8 @@
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
syntax
"_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_\<leftarrow>_ ./ _])")
+syntax_consts
+ "_filter" \<rightleftharpoons> filter
translations
"[x<-xs . P]" \<rightharpoonup> "CONST filter (\<lambda>x. P) xs"
@@ -132,6 +137,9 @@
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
"_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [1000,0] 900)
+syntax_consts
+ "_lupdbind" "_lupdbinds" "_LUpdate" == list_update
+
translations
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
"xs[i:=x]" == "CONST list_update xs i x"
--- a/src/HOL/Map.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Map.thy Sun Aug 25 21:27:25 2024 +0100
@@ -67,6 +67,9 @@
syntax (ASCII)
"_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _")
+syntax_consts
+ "_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd
+
translations
"_Update f (_maplet x y)" \<rightleftharpoons> "f(x := CONST Some y)"
"_Maplets m ms" \<rightharpoonup> "_updbinds m ms"
@@ -76,6 +79,7 @@
"_Map (_maplet x y)" \<leftharpoondown> "_Update (\<lambda>u. CONST None) (_maplet x y)"
"_Map (_updbinds m (_maplet x y))" \<leftharpoondown> "_Update (_Map m) (_maplet x y)"
+
text \<open>Updating with lists:\<close>
primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
@@ -98,6 +102,9 @@
syntax (ASCII)
"_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _")
+syntax_consts
+ "_maplets" \<rightleftharpoons> map_upds
+
translations
"_Update m (_maplets xs ys)" \<rightleftharpoons> "CONST map_upds m xs ys"
--- a/src/HOL/Metis_Examples/Message.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Sun Aug 25 21:27:25 2024 +0100
@@ -50,6 +50,8 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/Orderings.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Orderings.thy Sun Aug 25 21:27:25 2024 +0100
@@ -745,6 +745,10 @@
"_All_neq" :: "[idt, 'a, bool] => bool" ("(3! _~=_./ _)" [0, 0, 10] 10)
"_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3? _~=_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \<rightleftharpoons> All and
+ "_Ex_less" "_Ex_less_eq" "_Ex_greater" "_Ex_greater_eq" "_Ex_neq" \<rightleftharpoons> Ex
+
translations
"\<forall>x<y. P" \<rightharpoonup> "\<forall>x. x < y \<longrightarrow> P"
"\<exists>x<y. P" \<rightharpoonup> "\<exists>x. x < y \<and> P"
--- a/src/HOL/Probability/Fin_Map.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Sun Aug 25 21:27:25 2024 +0100
@@ -90,6 +90,8 @@
syntax
"_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>'' _\<in>_./ _)" 10)
+syntax_consts
+ "_Pi'" == Pi'
translations
"\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"
@@ -635,6 +637,8 @@
syntax
"_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>F _\<in>_./ _)" 10)
+syntax_consts
+ "_PiF" == PiF
translations
"\<Pi>\<^sub>F x\<in>I. M" == "CONST PiF I (%x. M)"
--- a/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Aug 25 21:27:25 2024 +0100
@@ -250,6 +250,9 @@
syntax
"_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>)
+syntax_consts
+ "_prob" == measure
+
translations
"\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
@@ -322,6 +325,9 @@
syntax
"_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>)
+syntax_consts
+ "_conditional_prob" == cond_prob
+
translations
"\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"
--- a/src/HOL/Product_Type.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Product_Type.thy Sun Aug 25 21:27:25 2024 +0100
@@ -293,6 +293,10 @@
"" :: "pttrn \<Rightarrow> patterns" ("_")
"_patterns" :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns" ("_,/ _")
"_unit" :: pttrn ("'(')")
+syntax_consts
+ "_tuple" "_tuple_arg" "_tuple_args" \<rightleftharpoons> Pair and
+ "_pattern" "_patterns" \<rightleftharpoons> case_prod and
+ "_unit" \<rightleftharpoons> case_unit
translations
"(x, y)" \<rightleftharpoons> "CONST Pair x y"
"_pattern x y" \<rightleftharpoons> "CONST Pair x y"
@@ -1010,6 +1014,8 @@
syntax
"_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_Sigma" \<rightleftharpoons> Sigma
translations
"SIGMA x:A. B" \<rightleftharpoons> "CONST Sigma A (\<lambda>x. B)"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Aug 25 21:27:25 2024 +0100
@@ -98,6 +98,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == fcons
+
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Sun Aug 25 21:27:25 2024 +0100
@@ -291,6 +291,9 @@
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
+syntax_consts
+ "_insert_fset" == insert_fset
+
translations
"{|x, xs|}" == "CONST insert_fset x {|xs|}"
"{|x|}" == "CONST insert_fset x {||}"
--- a/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Sun Aug 25 21:27:25 2024 +0100
@@ -70,6 +70,8 @@
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+syntax_consts
+ "_MTuple" == MPair
translations
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
--- a/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Sun Aug 25 21:27:25 2024 +0100
@@ -57,6 +57,9 @@
syntax
"_updsbind" :: "['a, 'a] => updbind" ("(2_ [:=]/ _)")
+syntax_consts
+ "_updsbind" == fun_upds
+
translations
"f(xs[:=]y)" == "CONST fun_upds f xs y"
--- a/src/HOL/Set.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Set.thy Sun Aug 25 21:27:25 2024 +0100
@@ -40,6 +40,8 @@
syntax
"_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_./ _})")
+syntax_consts
+ "_Coll" \<rightleftharpoons> Collect
translations
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
@@ -47,6 +49,8 @@
"_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/: _)./ _})")
syntax
"_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/ \<in> _)./ _})")
+syntax_consts
+ "_Collect" \<rightleftharpoons> Collect
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
@@ -141,6 +145,8 @@
syntax
"_Finset" :: "args \<Rightarrow> 'a set" ("{(_)}")
+syntax_consts
+ "_Finset" \<rightleftharpoons> insert
translations
"{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
"{x}" \<rightleftharpoons> "CONST insert x {}"
@@ -203,6 +209,12 @@
"_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
"_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_Ball" \<rightleftharpoons> Ball and
+ "_Bex" \<rightleftharpoons> Bex and
+ "_Bex1" \<rightleftharpoons> Ex1 and
+ "_Bleast" \<rightleftharpoons> Least
+
translations
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
@@ -223,12 +235,17 @@
"_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
"_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_setlessAll" "_setleAll" \<rightleftharpoons> All and
+ "_setlessEx" "_setleEx" \<rightleftharpoons> Ex and
+ "_setleEx1" \<rightleftharpoons> Ex1
+
translations
- "\<forall>A\<subset>B. P" \<rightharpoonup> "\<forall>A. A \<subset> B \<longrightarrow> P"
- "\<exists>A\<subset>B. P" \<rightharpoonup> "\<exists>A. A \<subset> B \<and> P"
- "\<forall>A\<subseteq>B. P" \<rightharpoonup> "\<forall>A. A \<subseteq> B \<longrightarrow> P"
- "\<exists>A\<subseteq>B. P" \<rightharpoonup> "\<exists>A. A \<subseteq> B \<and> P"
- "\<exists>!A\<subseteq>B. P" \<rightharpoonup> "\<exists>!A. A \<subseteq> B \<and> P"
+ "\<forall>A\<subset>B. P" \<rightharpoonup> "\<forall>A. A \<subset> B \<longrightarrow> P"
+ "\<exists>A\<subset>B. P" \<rightharpoonup> "\<exists>A. A \<subset> B \<and> P"
+ "\<forall>A\<subseteq>B. P" \<rightharpoonup> "\<forall>A. A \<subseteq> B \<longrightarrow> P"
+ "\<exists>A\<subseteq>B. P" \<rightharpoonup> "\<exists>A. A \<subseteq> B \<and> P"
+ "\<exists>!A\<subseteq>B. P" \<rightharpoonup> "\<exists>!A. A \<subseteq> B \<and> P"
print_translation \<open>
let
@@ -272,6 +289,8 @@
syntax
"_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_ |/_./ _})")
+syntax_consts
+ "_Setcompr" \<rightleftharpoons> Collect
parse_translation \<open>
let
--- a/src/HOL/Set_Interval.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Set_Interval.thy Sun Aug 25 21:27:25 2024 +0100
@@ -84,6 +84,10 @@
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
+ "_INTER_le" "_INTER_less" \<rightleftharpoons> Inter
+
translations
"\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A"
"\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A"
@@ -2005,6 +2009,9 @@
"_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
"_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
+syntax_consts
+ "_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
+
translations
"\<Sum>x=a..b. t" == "CONST sum (\<lambda>x. t) {a..b}"
"\<Sum>x=a..<b. t" == "CONST sum (\<lambda>x. t) {a..<b}"
@@ -2695,6 +2702,9 @@
"_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
"_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax_consts
+ "_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod
+
translations
"\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}"
"\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}"
--- a/src/HOL/String.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/String.thy Sun Aug 25 21:27:25 2024 +0100
@@ -218,6 +218,8 @@
syntax
"_Char" :: "str_position \<Rightarrow> char" ("CHR _")
"_Char_ord" :: "num_const \<Rightarrow> char" ("CHR _")
+syntax_consts
+ "_Char" "_Char_ord" \<rightleftharpoons> Char
type_synonym string = "char list"
@@ -522,6 +524,8 @@
syntax
"_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
"_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _")
+syntax_consts
+ "_Literal" "_Ascii" \<rightleftharpoons> String.Literal
ML_file \<open>Tools/literal.ML\<close>
--- a/src/HOL/Typerep.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/Typerep.thy Sun Aug 25 21:27:25 2024 +0100
@@ -19,6 +19,8 @@
syntax
"_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
+syntax_consts
+ "_TYPEREP" \<rightleftharpoons> typerep
parse_translation \<open>
let
--- a/src/HOL/UNITY/PPROD.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/UNITY/PPROD.thy Sun Aug 25 21:27:25 2024 +0100
@@ -16,6 +16,8 @@
syntax
"_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10)
+syntax_consts
+ "_PLam" == PLam
translations
"plam x : A. B" == "CONST PLam A (%x. B)"
--- a/src/HOL/UNITY/Union.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/UNITY/Union.thy Sun Aug 25 21:27:25 2024 +0100
@@ -41,6 +41,8 @@
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion>_./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion>_\<in>_./ _)" 10)
+syntax_consts
+ "_JOIN1" "_JOIN" == JOIN
translations
"\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)"
"\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
--- a/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Sun Aug 25 21:27:25 2024 +0100
@@ -40,6 +40,7 @@
| LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
syntax "_llist" :: "args => 'a list" ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+syntax_consts "_llist" == LCons
translations
"\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
"\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
--- a/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Pure/Examples/Higher_Order_Logic.thy Sun Aug 25 21:27:25 2024 +0100
@@ -402,6 +402,7 @@
where someI: "P x \<Longrightarrow> P (Eps P)"
syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+syntax_consts "_Eps" \<rightleftharpoons> Eps
translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
text \<open>
--- a/src/Pure/Isar/isar_cmd.ML Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Aug 25 21:27:25 2024 +0100
@@ -135,11 +135,11 @@
in Sign.syntax_deps (maps check args) thy end;
fun check_const ctxt (s, pos) =
- Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos])
+ Proof_Context.check_const {proper = true, strict = false} ctxt (s, [pos])
|>> (Term.dest_Const_name #> Lexicon.mark_const);
fun check_type_name ctxt arg =
- Proof_Context.check_type_name {proper = false, strict = true} ctxt arg
+ Proof_Context.check_type_name {proper = true, strict = false} ctxt arg
|>> (Term.dest_Type_name #> Lexicon.mark_type);
in
--- a/src/Pure/Syntax/syntax.ML Sun Aug 25 17:24:42 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Aug 25 21:27:25 2024 +0100
@@ -442,7 +442,9 @@
| NONE => Printer.get_binder prtabs c)
|> Option.map Prefix);
-fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts;
+fun is_const (Syntax ({consts, ...}, _)) c =
+ Graph.defined consts c andalso not (Lexicon.is_marked c);
+
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);
--- a/src/ZF/Bin.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/Bin.thy Sun Aug 25 21:27:25 2024 +0100
@@ -117,10 +117,11 @@
"_Int" :: "num_token \<Rightarrow> i" (\<open>#_\<close> 1000)
"_Neg_Int" :: "num_token \<Rightarrow> i" (\<open>#-_\<close> 1000)
+syntax_consts
+ "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
+
ML_file \<open>Tools/numeral_syntax.ML\<close>
-syntax_consts
- "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
declare bin.intros [simp,TC]
--- a/src/ZF/Induct/Multiset.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/Induct/Multiset.thy Sun Aug 25 21:27:25 2024 +0100
@@ -75,9 +75,9 @@
syntax
"_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+syntax_consts "_MColl" \<rightleftharpoons> MCollect
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
-syntax_consts "_MColl" \<rightleftharpoons> MCollect
(* multiset orderings *)
--- a/src/ZF/List.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/List.thy Sun Aug 25 21:27:25 2024 +0100
@@ -17,11 +17,11 @@
syntax
"_Nil" :: i (\<open>[]\<close>)
"_List" :: "is \<Rightarrow> i" (\<open>[(_)]\<close>)
+syntax_consts "_List" \<rightleftharpoons> Cons
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"
"[]" == "CONST Nil"
-syntax_consts "_List" \<rightleftharpoons> Cons
consts
length :: "i\<Rightarrow>i"
--- a/src/ZF/OrdQuant.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/OrdQuant.thy Sun Aug 25 21:27:25 2024 +0100
@@ -26,14 +26,14 @@
"_oall" :: "[idt, i, o] \<Rightarrow> o" (\<open>(3\<forall>_<_./ _)\<close> 10)
"_oex" :: "[idt, i, o] \<Rightarrow> o" (\<open>(3\<exists>_<_./ _)\<close> 10)
"_OUNION" :: "[idt, i, i] \<Rightarrow> i" (\<open>(3\<Union>_<_./ _)\<close> 10)
+syntax_consts
+ "_oall" \<rightleftharpoons> oall and
+ "_oex" \<rightleftharpoons> oex and
+ "_OUNION" \<rightleftharpoons> OUnion
translations
"\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
"\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
"\<Union>x<a. B" \<rightleftharpoons> "CONST OUnion(a, \<lambda>x. B)"
-syntax_consts
- "_oall" \<rightleftharpoons> oall and
- "_oex" \<rightleftharpoons> oex and
- "_OUNION" \<rightleftharpoons> OUnion
subsubsection \<open>simplification of the new quantifiers\<close>
@@ -198,12 +198,12 @@
syntax
"_rall" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(3\<forall>_[_]./ _)\<close> 10)
"_rex" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(3\<exists>_[_]./ _)\<close> 10)
+syntax_consts
+ "_rall" \<rightleftharpoons> rall and
+ "_rex" \<rightleftharpoons> rex
translations
"\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
"\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
-syntax_consts
- "_rall" \<rightleftharpoons> rall and
- "_rex" \<rightleftharpoons> rex
subsubsection\<open>Relativized universal quantifier\<close>
--- a/src/ZF/QPair.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/QPair.thy Sun Aug 25 21:27:25 2024 +0100
@@ -46,10 +46,10 @@
syntax
"_QSUM" :: "[idt, i, i] \<Rightarrow> i" (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
+syntax_consts
+ "_QSUM" \<rightleftharpoons> QSigma
translations
"QSUM x \<in> A. B" => "CONST QSigma(A, \<lambda>x. B)"
-syntax_consts
- "_QSUM" \<rightleftharpoons> QSigma
abbreviation
qprod (infixr \<open><*>\<close> 80) where
--- a/src/ZF/UNITY/Union.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/UNITY/Union.thy Sun Aug 25 21:27:25 2024 +0100
@@ -43,12 +43,12 @@
syntax
"_JOIN1" :: "[pttrns, i] \<Rightarrow> i" (\<open>(3\<Squnion>_./ _)\<close> 10)
"_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
+syntax_consts
+ "_JOIN1" "_JOIN" == JOIN
translations
"\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))"
"\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
"\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))"
-syntax_consts
- "_JOIN1" "_JOIN" == JOIN
subsection\<open>SKIP\<close>
--- a/src/ZF/ZF_Base.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/ZF_Base.thy Sun Aug 25 21:27:25 2024 +0100
@@ -38,12 +38,12 @@
syntax
"_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
"_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
+syntax_consts
+ "_Ball" \<rightleftharpoons> Ball and
+ "_Bex" \<rightleftharpoons> Bex
translations
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
-syntax_consts
- "_Ball" \<rightleftharpoons> Ball and
- "_Bex" \<rightleftharpoons> Bex
subsection \<open>Variations on Replacement\<close>
@@ -56,10 +56,10 @@
syntax
"_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+syntax_consts
+ "_Replace" \<rightleftharpoons> Replace
translations
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
-syntax_consts
- "_Replace" \<rightleftharpoons> Replace
(* Functional form of replacement -- analgous to ML's map functional *)
@@ -69,10 +69,10 @@
syntax
"_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
+syntax_consts
+ "_RepFun" \<rightleftharpoons> RepFun
translations
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
-syntax_consts
- "_RepFun" \<rightleftharpoons> RepFun
(* Separation and Pairing can be derived from the Replacement
and Powerset Axioms using the following definitions. *)
@@ -81,10 +81,10 @@
syntax
"_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>)
+syntax_consts
+ "_Collect" \<rightleftharpoons> Collect
translations
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
-syntax_consts
- "_Collect" \<rightleftharpoons> Collect
subsection \<open>General union and intersection\<close>
@@ -95,12 +95,12 @@
syntax
"_UNION" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
"_INTER" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
+syntax_consts
+ "_UNION" == Union and
+ "_INTER" == Inter
translations
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
-syntax_consts
- "_UNION" == Union and
- "_INTER" == Inter
subsection \<open>Finite sets and binary operations\<close>
@@ -134,11 +134,11 @@
"" :: "i \<Rightarrow> is" (\<open>_\<close>)
"_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>)
"_Finset" :: "is \<Rightarrow> i" (\<open>{(_)}\<close>)
+syntax_consts
+ "_Finset" == cons
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
-syntax_consts
- "_Finset" == cons
subsection \<open>Axioms\<close>
@@ -199,14 +199,14 @@
"" :: "pttrn \<Rightarrow> patterns" (\<open>_\<close>)
"_patterns" :: "[pttrn, patterns] \<Rightarrow> patterns" (\<open>_,/_\<close>)
"_Tuple" :: "[i, is] \<Rightarrow> i" (\<open>\<langle>(_,/ _)\<rangle>\<close>)
+syntax_consts
+ "_pattern" "_patterns" == split and
+ "_Tuple" == Pair
translations
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
"\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
"\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)"
-syntax_consts
- "_pattern" "_patterns" == split and
- "_Tuple" == Pair
definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where "Sigma(A,B) \<equiv> \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
@@ -268,14 +268,14 @@
"_PROD" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
"_SUM" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
"_lam" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
+syntax_consts
+ "_PROD" == Pi and
+ "_SUM" == Sigma and
+ "_lam" == Lambda
translations
"\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
"\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
"\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)"
-syntax_consts
- "_PROD" == Pi and
- "_SUM" == Sigma and
- "_lam" == Lambda
subsection \<open>ASCII syntax\<close>
--- a/src/ZF/func.thy Sun Aug 25 17:24:42 2024 +0100
+++ b/src/ZF/func.thy Sun Aug 25 21:27:25 2024 +0100
@@ -452,10 +452,10 @@
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
+syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
"f(x:=y)" == "CONST update(f,x,y)"
-syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
apply (simp add: update_def)