src/ZF/AC/OrdQuant.thy

updated version

(*  Title: 	ZF/AC/OrdQuant.thy
    ID:         $Id$
    Authors: 	Krzysztof Gr`abczewski and L C Paulson

Quantifiers and union operator for ordinals. 
*)

OrdQuant = Ordinal +

consts
  
  (* Ordinal Quantifiers *)
  oall, oex   :: "[i, i => o] => o"

  (* Ordinal Union *)
  OUnion      :: "[i, i => i] => i"
  
syntax
  
  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)

translations
  
  "ALL x<a. P"  == "oall(a, %x. P)"
  "EX x<a. P"   == "oex(a, %x. P)"
  "UN x<a. B"   == "OUnion(a, %x. B)"

defs
  
  (* Ordinal Quantifiers *)
  oall_def      "oall(A, P) == ALL x. x<A --> P(x)"
  oex_def       "oex(A, P) == EX x. x<A & P(x)"

  OUnion_def     "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
  
end