516

1 
(* Title: ZF/Zorn.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 
Union_in_Pow is proved in ZF.ML


12 
*)


13 

806

14 
Zorn = OrderArith + AC + Inductive +

516

15 


16 
consts

1401

17 
Subset_rel :: i=>i


18 
increasing :: i=>i


19 
chain, maxchain :: i=>i


20 
super :: [i,i]=>i

516

21 

753

22 
defs

516

23 
Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"


24 
increasing_def "increasing(A) == {f: Pow(A)>Pow(A). ALL x. x<=A > x<=f`x}"

485

25 

516

26 
chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y  Y<=X}"


27 
super_def "super(A,c) == {d: chain(A). c<=d & c~=d}"


28 
maxchain_def "maxchain(A) == {c: chain(A). super(A,c)=0}"


29 


30 


31 
(** We could make the inductive definition conditional on next: increasing(S)


32 
but instead we make this a sidecondition of an introduction rule. Thus


33 
the induction rule lets us assume that condition! Many inductive proofs


34 
are therefore unconditional.


35 
**)


36 
consts

1401

37 
"TFin" :: [i,i]=>i

516

38 


39 
inductive


40 
domains "TFin(S,next)" <= "Pow(S)"


41 
intrs

1155

42 
nextI "[ x : TFin(S,next); next: increasing(S)


43 
] ==> next`x : TFin(S,next)"

516

44 


45 
Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"


46 


47 
monos "[Pow_mono]"


48 
con_defs "[increasing_def]"


49 
type_intrs "[CollectD1 RS apply_funtype, Union_in_Pow]"


50 


51 
end
