src/ZF/OrdQuant.thy
author paulson
Fri Jan 03 15:01:55 1997 +0100 (1997-01-03)
changeset 2469 b50b8c0eec01
child 2540 ba8311047f18
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
     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   
    20   "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
    21   "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    22   "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    23 
    24 translations
    25   
    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 defs
    31   
    32   (* Ordinal Quantifiers *)
    33   oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
    34   oex_def       "oex(A, P) == EX x. x<A & P(x)"
    35 
    36   OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    37   
    38 end