# HG changeset patch
# User wenzelm
# Date 1724447679 -7200
# Node ID 701912f5645a025519be6735fb1970437ed364c5
# Parent  66893c47500db4d4158f213b88726424f4984beb
more markup for syntax consts;

diff -r 66893c47500d -r 701912f5645a src/CCL/Set.thy
--- 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)"
diff -r 66893c47500d -r 701912f5645a src/CCL/Term.thy
--- 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)"
diff -r 66893c47500d -r 701912f5645a src/CCL/Type.thy
--- 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)"
diff -r 66893c47500d -r 701912f5645a src/CTT/CTT.thy
--- 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"
diff -r 66893c47500d -r 701912f5645a src/Cube/Cube.thy
--- 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
diff -r 66893c47500d -r 701912f5645a src/FOL/IFOL.thy
--- 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>
diff -r 66893c47500d -r 701912f5645a src/ZF/Bin.thy
--- 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]
 
diff -r 66893c47500d -r 701912f5645a src/ZF/Induct/Multiset.thy
--- 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 *)
 
diff -r 66893c47500d -r 701912f5645a src/ZF/List.thy
--- 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"
diff -r 66893c47500d -r 701912f5645a src/ZF/OrdQuant.thy
--- 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>
diff -r 66893c47500d -r 701912f5645a src/ZF/QPair.thy
--- 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
diff -r 66893c47500d -r 701912f5645a src/ZF/UNITY/Union.thy
--- 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>
diff -r 66893c47500d -r 701912f5645a src/ZF/ZF_Base.thy
--- 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>
diff -r 66893c47500d -r 701912f5645a src/ZF/func.thy
--- 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)