src/ZF/ZF_Base.thy

--- 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>