--- a/src/CCL/Set.thy Fri Aug 23 22:47:51 2024 +0200
+++ b/src/CCL/Set.thy Fri Aug 23 23:14:39 2024 +0200
@@ -21,6 +21,8 @@
"_Coll" :: "[idt, o] \<Rightarrow> 'a set" ("(1{_./ _})")
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])
@@ -53,6 +55,9 @@
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)
@@ -127,6 +132,9 @@
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/CCL/Term.thy Fri Aug 23 23:14:39 2024 +0200
@@ -50,6 +50,7 @@
syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
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)"
@@ -122,6 +123,10 @@
(\<^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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/CCL/Type.thy Fri Aug 23 23:14:39 2024 +0200
@@ -16,6 +16,8 @@
"_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})")
translations
"{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
+syntax_consts
+ "_Subtype" == Subtype
definition Unit :: "i set"
where "Unit == {x. x=one}"
@@ -48,6 +50,9 @@
(\<^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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/CTT/CTT.thy Fri Aug 23 23:14:39 2024 +0200
@@ -61,6 +61,9 @@
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/Cube/Cube.thy Fri Aug 23 23:14:39 2024 +0200
@@ -52,6 +52,13 @@
[(\<^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/FOL/IFOL.thy Fri Aug 23 22:47:51 2024 +0200
+++ b/src/FOL/IFOL.thy Fri Aug 23 23:14:39 2024 +0200
@@ -103,6 +103,7 @@
syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
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>]
@@ -746,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)
-
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/ZF/Bin.thy Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/Bin.thy Fri Aug 23 23:14:39 2024 +0200
@@ -119,6 +119,8 @@
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Fri Aug 23 23:14:39 2024 +0200
@@ -77,6 +77,7 @@
"_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
+syntax_consts "_MColl" \<rightleftharpoons> MCollect
(* multiset orderings *)
--- a/src/ZF/List.thy Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/List.thy Fri Aug 23 23:14:39 2024 +0200
@@ -17,12 +17,11 @@
syntax
"_Nil" :: i (\<open>[]\<close>)
"_List" :: "is \<Rightarrow> i" (\<open>[(_)]\<close>)
-
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/OrdQuant.thy Fri Aug 23 23:14:39 2024 +0200
@@ -30,6 +30,10 @@
"\<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>
@@ -197,6 +201,9 @@
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/QPair.thy Fri Aug 23 23:14:39 2024 +0200
@@ -48,6 +48,8 @@
"_QSUM" :: "[idt, i, i] \<Rightarrow> i" (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/UNITY/Union.thy Fri Aug 23 23:14:39 2024 +0200
@@ -43,11 +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)
-
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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/ZF_Base.thy Fri Aug 23 23:14:39 2024 +0200
@@ -41,6 +41,9 @@
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>
@@ -52,9 +55,11 @@
where "Replace(A,P) \<equiv> PrimReplace(A, \<lambda>x y. (\<exists>!z. P(x,z)) \<and> P(x,y))"
syntax
- "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+ "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
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 *)
@@ -66,7 +71,8 @@
"_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
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. *)
@@ -77,6 +83,8 @@
"_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>)
translations
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
+syntax_consts
+ "_Collect" \<rightleftharpoons> Collect
subsection \<open>General union and intersection\<close>
@@ -90,6 +98,9 @@
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>
@@ -126,6 +137,8 @@
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
+syntax_consts
+ "_Finset" == cons
subsection \<open>Axioms\<close>
@@ -191,6 +204,9 @@
"\<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>}"
@@ -256,6 +272,10 @@
"\<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 Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/func.thy Fri Aug 23 23:14:39 2024 +0200
@@ -448,18 +448,14 @@
nonterminal updbinds and updbind
syntax
-
- (* Let expressions *)
-
"_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
-
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)