src/CCL/Set.thy
changeset 17456 bcf7544875b2
parent 3935 52c14fe8f16b
child 20140 98acc6d0fab6
equal deleted inserted replaced
17455:151e76f0e3c7 17456:bcf7544875b2
     1 (*  Title:      CCL/set.thy
     1 (*  Title:      CCL/Set.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3 
       
     4 Modified version of HOL/set.thy that extends FOL
       
     5 
       
     6 *)
     3 *)
     7 
     4 
     8 Set = FOL +
     5 header {* Extending FOL by a modified version of HOL set theory *}
       
     6 
       
     7 theory Set
       
     8 imports FOL
       
     9 begin
     9 
    10 
    10 global
    11 global
    11 
    12 
    12 types
    13 typedecl 'a set
    13   'a set
    14 arities set :: ("term") "term"
    14 
       
    15 arities
       
    16   set :: (term) term
       
    17 
    15 
    18 consts
    16 consts
    19   Collect       :: "['a => o] => 'a set"                    (*comprehension*)
    17   Collect       :: "['a => o] => 'a set"                    (*comprehension*)
    20   Compl         :: "('a set) => 'a set"                     (*complement*)
    18   Compl         :: "('a set) => 'a set"                     (*complement*)
    21   Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
    19   Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
    22   Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
    20   Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
    23   Union, Inter  :: "(('a set)set) => 'a set"                (*...of a set*)
    21   Union         :: "(('a set)set) => 'a set"                (*...of a set*)
    24   UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"       (*general*)
    22   Inter         :: "(('a set)set) => 'a set"                (*...of a set*)
    25   Ball, Bex     :: "['a set, 'a => o] => o"                 (*bounded quants*)
    23   UNION         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
       
    24   INTER         :: "['a set, 'a => 'b set] => 'b set"       (*general*)
       
    25   Ball          :: "['a set, 'a => o] => o"                 (*bounded quants*)
       
    26   Bex           :: "['a set, 'a => o] => o"                 (*bounded quants*)
    26   mono          :: "['a set => 'b set] => o"                (*monotonicity*)
    27   mono          :: "['a set => 'b set] => o"                (*monotonicity*)
    27   ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
    28   ":"           :: "['a, 'a set] => o"                  (infixl 50) (*membership*)
    28   "<="          :: "['a set, 'a set] => o"              (infixl 50)
    29   "<="          :: "['a set, 'a set] => o"              (infixl 50)
    29   singleton     :: "'a => 'a set"                       ("{_}")
    30   singleton     :: "'a => 'a set"                       ("{_}")
    30   empty         :: "'a set"                             ("{}")
    31   empty         :: "'a set"                             ("{}")
    41   (* Bounded Quantifiers *)
    42   (* Bounded Quantifiers *)
    42 
    43 
    43   "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    44   "@Ball"       :: "[idt, 'a set, o] => o"              ("(ALL _:_./ _)" [0, 0, 0] 10)
    44   "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    45   "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
    45 
    46 
    46 
       
    47 translations
    47 translations
    48   "{x. P}"      == "Collect(%x. P)"
    48   "{x. P}"      == "Collect(%x. P)"
    49   "INT x:A. B"  == "INTER(A, %x. B)"
    49   "INT x:A. B"  == "INTER(A, %x. B)"
    50   "UN x:A. B"   == "UNION(A, %x. B)"
    50   "UN x:A. B"   == "UNION(A, %x. B)"
    51   "ALL x:A. P"  == "Ball(A, %x. P)"
    51   "ALL x:A. P"  == "Ball(A, %x. P)"
    52   "EX x:A. P"   == "Bex(A, %x. P)"
    52   "EX x:A. P"   == "Bex(A, %x. P)"
    53 
    53 
    54 local
    54 local
    55 
    55 
    56 rules
    56 axioms
    57   mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
    57   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
    58   set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
    58   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
    59 
    59 
    60   Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
    60 defs
    61   Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
    61   Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"
    62   mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
    62   Bex_def:       "Bex(A, P)   == EX x. x:A & P(x)"
    63   subset_def    "A <= B      == ALL x:A. x:B"
    63   mono_def:      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
    64   singleton_def "{a}         == {x. x=a}"
    64   subset_def:    "A <= B      == ALL x:A. x:B"
    65   empty_def     "{}          == {x. False}"
    65   singleton_def: "{a}         == {x. x=a}"
    66   Un_def        "A Un B      == {x. x:A | x:B}"
    66   empty_def:     "{}          == {x. False}"
    67   Int_def       "A Int B     == {x. x:A & x:B}"
    67   Un_def:        "A Un B      == {x. x:A | x:B}"
    68   Compl_def     "Compl(A)    == {x. ~x:A}"
    68   Int_def:       "A Int B     == {x. x:A & x:B}"
    69   INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
    69   Compl_def:     "Compl(A)    == {x. ~x:A}"
    70   UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
    70   INTER_def:     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
    71   Inter_def     "Inter(S)    == (INT x:S. x)"
    71   UNION_def:     "UNION(A, B) == {y. EX x:A. y: B(x)}"
    72   Union_def     "Union(S)    == (UN x:S. x)"
    72   Inter_def:     "Inter(S)    == (INT x:S. x)"
       
    73   Union_def:     "Union(S)    == (UN x:S. x)"
       
    74 
       
    75 ML {* use_legacy_bindings (the_context ()) *}
    73 
    76 
    74 end
    77 end
    75 
    78