--- a/src/CCL/Set.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Set.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/CCL/Term.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/CCL/Type.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/CTT/CTT.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/Cube/Cube.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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/FOL/IFOL.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/FOL/IFOL.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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/ZF/Bin.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/Bin.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/List.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/OrdQuant.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/QPair.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/UNITY/Union.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/ZF_Base.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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 15:02:19 2024 +0200
+++ b/src/ZF/func.thy Sun Aug 25 15:07:22 2024 +0200
@@ -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)