src/ZF/OrdQuant.thy
author paulson
Wed Dec 19 11:13:27 2001 +0100 (2001-12-19)
changeset 12552 d2d2ab3f1f37
parent 12114 a8e860c86252
child 12620 4e6626725e21
permissions -rw-r--r--
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
     1 (*  Title:      ZF/AC/OrdQuant.thy
     2     ID:         $Id$
     3     Authors:    Krzysztof Grabczewski and L C Paulson
     4 
     5 Quantifiers and union operator for ordinals. 
     6 *)
     7 
     8 OrdQuant = Ordinal +
     9 
    10 consts
    11   
    12   (* Ordinal Quantifiers *)
    13   oall, oex   :: [i, i => o] => o
    14 
    15   (* Ordinal Union *)
    16   OUnion      :: [i, i => i] => i
    17   
    18 syntax
    19   "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
    20   "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    21   "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    22 
    23 translations
    24   "ALL x<a. P"  == "oall(a, %x. P)"
    25   "EX x<a. P"   == "oex(a, %x. P)"
    26   "UN x<a. B"   == "OUnion(a, %x. B)"
    27 
    28 syntax (xsymbols)
    29   "@oall"     :: [idt, i, o] => o        ("(3\\<forall>_<_./ _)" 10)
    30   "@oex"      :: [idt, i, o] => o        ("(3\\<exists>_<_./ _)" 10)
    31   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union>_<_./ _)" 10)
    32 
    33 defs
    34   
    35   (* Ordinal Quantifiers *)
    36   oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
    37   oex_def       "oex(A, P) == EX x. x<A & P(x)"
    38 
    39   OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    40   
    41 end