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