src/ZF/OrdQuant.thy
author wenzelm
Mon Oct 20 10:53:42 1997 +0200 (1997-10-20)
changeset 3940 1d5bee4d047f
parent 3923 c257b82a1200
child 6093 87bf8c03b169
permissions -rw-r--r--
local;
paulson@2469
     1
(*  Title:      ZF/AC/OrdQuant.thy
paulson@2469
     2
    ID:         $Id$
paulson@2469
     3
    Authors:    Krzysztof Grabczewski and L C Paulson
paulson@2469
     4
paulson@2469
     5
Quantifiers and union operator for ordinals. 
paulson@2469
     6
*)
paulson@2469
     7
paulson@2469
     8
OrdQuant = Ordinal +
paulson@2469
     9
wenzelm@3923
    10
global
wenzelm@3923
    11
paulson@2469
    12
consts
paulson@2469
    13
  
paulson@2469
    14
  (* Ordinal Quantifiers *)
paulson@2469
    15
  oall, oex   :: [i, i => o] => o
paulson@2469
    16
paulson@2469
    17
  (* Ordinal Union *)
paulson@2469
    18
  OUnion      :: [i, i => i] => i
paulson@2469
    19
  
paulson@2469
    20
syntax
paulson@2469
    21
  "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
paulson@2469
    22
  "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
paulson@2469
    23
  "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
paulson@2469
    24
paulson@2469
    25
translations
paulson@2469
    26
  "ALL x<a. P"  == "oall(a, %x. P)"
paulson@2469
    27
  "EX x<a. P"   == "oex(a, %x. P)"
paulson@2469
    28
  "UN x<a. B"   == "OUnion(a, %x. B)"
paulson@2469
    29
wenzelm@2540
    30
syntax (symbols)
wenzelm@2540
    31
  "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
wenzelm@2540
    32
  "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
wenzelm@2540
    33
  "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
wenzelm@2540
    34
wenzelm@3940
    35
local
wenzelm@2540
    36
paulson@2469
    37
defs
paulson@2469
    38
  
paulson@2469
    39
  (* Ordinal Quantifiers *)
paulson@2469
    40
  oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
paulson@2469
    41
  oex_def       "oex(A, P) == EX x. x<A & P(x)"
paulson@2469
    42
paulson@2469
    43
  OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
paulson@2469
    44
  
paulson@2469
    45
end