src/ZF/OrdQuant.thy
author wenzelm
Fri Oct 17 17:40:02 1997 +0200 (1997-10-17)
changeset 3923 c257b82a1200
parent 2540 ba8311047f18
child 3940 1d5bee4d047f
permissions -rw-r--r--
global;
     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 global
    11 
    12 consts
    13   
    14   (* Ordinal Quantifiers *)
    15   oall, oex   :: [i, i => o] => o
    16 
    17   (* Ordinal Union *)
    18   OUnion      :: [i, i => i] => i
    19   
    20 syntax
    21   "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
    22   "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    23   "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    24 
    25 translations
    26   "ALL x<a. P"  == "oall(a, %x. P)"
    27   "EX x<a. P"   == "oex(a, %x. P)"
    28   "UN x<a. B"   == "OUnion(a, %x. B)"
    29 
    30 syntax (symbols)
    31   "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
    32   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    33   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    34 
    35 path OrdQuant
    36 
    37 defs
    38   
    39   (* Ordinal Quantifiers *)
    40   oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
    41   oex_def       "oex(A, P) == EX x. x<A & P(x)"
    42 
    43   OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    44   
    45 end