src/CCL/Set.thy
changeset 38499 8f0cd11238a7
parent 35113 1a0c129bb2e0
child 39128 93a7365fb4ee
equal deleted inserted replaced
38498:205e1d735bb1 38499:8f0cd11238a7
     1 header {* Extending FOL by a modified version of HOL set theory *}
     1 header {* Extending FOL by a modified version of HOL set theory *}
     2 
     2 
     3 theory Set
     3 theory Set
     4 imports FOL
     4 imports FOL
     5 begin
     5 begin
     6 
       
     7 global
       
     8 
     6 
     9 typedecl 'a set
     7 typedecl 'a set
    10 arities set :: ("term") "term"
     8 arities set :: ("term") "term"
    11 
     9 
    12 consts
    10 consts
    44   "INT x:A. B"  == "CONST INTER(A, %x. B)"
    42   "INT x:A. B"  == "CONST INTER(A, %x. B)"
    45   "UN x:A. B"   == "CONST UNION(A, %x. B)"
    43   "UN x:A. B"   == "CONST UNION(A, %x. B)"
    46   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
    44   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
    47   "EX x:A. P"   == "CONST Bex(A, %x. P)"
    45   "EX x:A. P"   == "CONST Bex(A, %x. P)"
    48 
    46 
    49 local
       
    50 
       
    51 axioms
    47 axioms
    52   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
    48   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
    53   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
    49   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
    54 
    50 
    55 defs
    51 defs