--- a/src/CCL/Set.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Set.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,28 +1,29 @@
-(* Title: CCL/set.thy
+(* Title: CCL/Set.thy
ID: $Id$
-
-Modified version of HOL/set.thy that extends FOL
-
*)
-Set = FOL +
+header {* Extending FOL by a modified version of HOL set theory *}
+
+theory Set
+imports FOL
+begin
global
-types
- 'a set
-
-arities
- set :: (term) term
+typedecl 'a set
+arities set :: ("term") "term"
consts
Collect :: "['a => o] => 'a set" (*comprehension*)
Compl :: "('a set) => 'a set" (*complement*)
Int :: "['a set, 'a set] => 'a set" (infixl 70)
Un :: "['a set, 'a set] => 'a set" (infixl 65)
- Union, Inter :: "(('a set)set) => 'a set" (*...of a set*)
- UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
- Ball, Bex :: "['a set, 'a => o] => o" (*bounded quants*)
+ Union :: "(('a set)set) => 'a set" (*...of a set*)
+ Inter :: "(('a set)set) => 'a set" (*...of a set*)
+ UNION :: "['a set, 'a => 'b set] => 'b set" (*general*)
+ INTER :: "['a set, 'a => 'b set] => 'b set" (*general*)
+ Ball :: "['a set, 'a => o] => o" (*bounded quants*)
+ Bex :: "['a set, 'a => o] => o" (*bounded quants*)
mono :: "['a set => 'b set] => o" (*monotonicity*)
":" :: "['a, 'a set] => o" (infixl 50) (*membership*)
"<=" :: "['a set, 'a set] => o" (infixl 50)
@@ -43,7 +44,6 @@
"@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10)
"@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)
-
translations
"{x. P}" == "Collect(%x. P)"
"INT x:A. B" == "INTER(A, %x. B)"
@@ -53,23 +53,26 @@
local
-rules
- mem_Collect_iff "(a : {x. P(x)}) <-> P(a)"
- set_extension "A=B <-> (ALL x. x:A <-> x:B)"
+axioms
+ mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)"
+ set_extension: "A=B <-> (ALL x. x:A <-> x:B)"
- Ball_def "Ball(A, P) == ALL x. x:A --> P(x)"
- Bex_def "Bex(A, P) == EX x. x:A & P(x)"
- mono_def "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))"
- subset_def "A <= B == ALL x:A. x:B"
- singleton_def "{a} == {x. x=a}"
- empty_def "{} == {x. False}"
- Un_def "A Un B == {x. x:A | x:B}"
- Int_def "A Int B == {x. x:A & x:B}"
- Compl_def "Compl(A) == {x. ~x:A}"
- INTER_def "INTER(A, B) == {y. ALL x:A. y: B(x)}"
- UNION_def "UNION(A, B) == {y. EX x:A. y: B(x)}"
- Inter_def "Inter(S) == (INT x:S. x)"
- Union_def "Union(S) == (UN x:S. x)"
+defs
+ Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)"
+ Bex_def: "Bex(A, P) == EX x. x:A & P(x)"
+ mono_def: "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))"
+ subset_def: "A <= B == ALL x:A. x:B"
+ singleton_def: "{a} == {x. x=a}"
+ empty_def: "{} == {x. False}"
+ Un_def: "A Un B == {x. x:A | x:B}"
+ Int_def: "A Int B == {x. x:A & x:B}"
+ Compl_def: "Compl(A) == {x. ~x:A}"
+ INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}"
+ UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}"
+ Inter_def: "Inter(S) == (INT x:S. x)"
+ Union_def: "Union(S) == (UN x:S. x)"
+
+ML {* use_legacy_bindings (the_context ()) *}
end