485

1 
(* Title: ZF/Zorn0.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Preamble to proofs from the paper


7 
Abrial & Laffitte,


8 
Towards the Mechanization of the Proofs of Some


9 
Classical Theorems of Set Theory.


10 
*)


11 


12 


13 
(*** Section 1. Mathematical Preamble ***)


14 


15 
goal ZF.thy "!!A B C. (ALL x:C. x<=A  B<=x) ==> Union(C)<=A  B<=Union(C)";


16 
by (fast_tac ZF_cs 1);


17 
val Union_lemma0 = result();


18 


19 
goal ZF.thy


20 
"!!A B C. [ c:C; ALL x:C. A<=x  x<=B ] ==> A<=Inter(C)  Inter(C)<=B";


21 
by (fast_tac ZF_cs 1);


22 
val Inter_lemma0 = result();


23 


24 
open Zorn0;


25 


26 
(*** Section 2. The Transfinite Construction ***)


27 


28 
goalw Zorn0.thy [increasing_def]


29 
"!!f A. f: increasing(A) ==> f: Pow(A)>Pow(A)";


30 
by (eresolve_tac [CollectD1] 1);


31 
val increasingD1 = result();


32 


33 
goalw Zorn0.thy [increasing_def]


34 
"!!f A. [ f: increasing(A); x<=A ] ==> x <= f`x";


35 
by (eresolve_tac [CollectD2 RS spec RS mp] 1);


36 
by (assume_tac 1);


37 
val increasingD2 = result();


38 


39 
goal Zorn0.thy


40 
"!!next S. [ X : Pow(S); next: increasing(S) ] ==> next`X : Pow(S)";


41 
by (eresolve_tac [increasingD1 RS apply_type] 1);


42 
by (assume_tac 1);


43 
val next_bounded = result();


44 


45 
(*Trivial to prove here; hard to prove within Inductive_Fun*)


46 
goal ZF.thy "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";


47 
by (fast_tac ZF_cs 1);


48 
val Union_in_Pow = result();


49 


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


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


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


53 
are therefore unconditional.


54 
**)


55 


56 
