equal
deleted
inserted
replaced
1 (* Title: ZF/Zorn0.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Based upon the article |
|
7 Abrial & Laffitte, |
|
8 Towards the Mechanization of the Proofs of Some |
|
9 Classical Theorems of Set Theory. |
|
10 *) |
|
11 |
|
12 Zorn0 = OrderArith + AC + "inductive" + |
|
13 |
|
14 consts |
|
15 Subset_rel :: "i=>i" |
|
16 increasing :: "i=>i" |
|
17 chain, maxchain :: "i=>i" |
|
18 super :: "[i,i]=>i" |
|
19 |
|
20 rules |
|
21 Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}" |
|
22 increasing_def "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}" |
|
23 |
|
24 chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}" |
|
25 super_def "super(A,c) == {d: chain(A). c<=d & c~=d}" |
|
26 maxchain_def "maxchain(A) == {c: chain(A). super(A,c)=0}" |
|
27 |
|
28 end |
|