485

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
