|
992
|
1 |
(* Title: ZF/AC/OrdQuant.thy
|
|
|
2 |
ID: $Id$
|
|
1039
|
3 |
Authors: Krzysztof Gr`abczewski and L C Paulson
|
|
992
|
4 |
|
|
|
5 |
Quantifiers and union operator for ordinals.
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
OrdQuant = Ordinal +
|
|
|
9 |
|
|
|
10 |
consts
|
|
|
11 |
|
|
|
12 |
(* Ordinal Quantifiers *)
|
|
1039
|
13 |
oall, oex :: "[i, i => o] => o"
|
|
|
14 |
|
|
|
15 |
(* Ordinal Union *)
|
|
992
|
16 |
OUnion :: "[i, i => i] => i"
|
|
|
17 |
|
|
|
18 |
syntax
|
|
|
19 |
|
|
1039
|
20 |
"@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
|
|
|
21 |
"@oex" :: "[idt, i, o] => o" ("(3EX _<_./ _)" 10)
|
|
992
|
22 |
"@OUNION" :: "[idt, i, i] => i" ("(3UN _<_./ _)" 10)
|
|
|
23 |
|
|
|
24 |
translations
|
|
|
25 |
|
|
1039
|
26 |
"ALL x<a. P" == "oall(a, %x. P)"
|
|
|
27 |
"EX x<a. P" == "oex(a, %x. P)"
|
|
992
|
28 |
"UN x<a. B" == "OUnion(a, %x. B)"
|
|
|
29 |
|
|
|
30 |
defs
|
|
|
31 |
|
|
|
32 |
(* Ordinal Quantifiers *)
|
|
1039
|
33 |
oall_def "oall(A, P) == ALL x. x<A --> P(x)"
|
|
|
34 |
oex_def "oex(A, P) == EX x. x<A & P(x)"
|
|
992
|
35 |
|
|
1039
|
36 |
OUnion_def "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
|
|
|
37 |
|
|
992
|
38 |
end
|