src/ZF/Zorn0.ML
changeset 485 5e00a676a211
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Zorn0.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -0,0 +1,56 @@
+(*  Title: 	ZF/Zorn0.ML
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Preamble to proofs from the paper
+    Abrial & Laffitte, 
+    Towards the Mechanization of the Proofs of Some 
+    Classical Theorems of Set Theory. 
+*)
+
+
+(*** Section 1.  Mathematical Preamble ***)
+
+goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
+by (fast_tac ZF_cs 1);
+val Union_lemma0 = result();
+
+goal ZF.thy
+    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
+by (fast_tac ZF_cs 1);
+val Inter_lemma0 = result();
+
+open Zorn0;
+
+(*** Section 2.  The Transfinite Construction ***)
+
+goalw Zorn0.thy [increasing_def]
+    "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
+by (eresolve_tac [CollectD1] 1);
+val increasingD1 = result();
+
+goalw Zorn0.thy [increasing_def]
+    "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
+by (eresolve_tac [CollectD2 RS spec RS mp] 1);
+by (assume_tac 1);
+val increasingD2 = result();
+
+goal Zorn0.thy
+    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
+by (eresolve_tac [increasingD1 RS apply_type] 1);
+by (assume_tac 1);
+val next_bounded = result();
+
+(*Trivial to prove here; hard to prove within Inductive_Fun*)
+goal ZF.thy "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
+by (fast_tac ZF_cs 1);
+val Union_in_Pow = result();
+
+(** We could make the inductive definition conditional on next: increasing(S)
+    but instead we make this a side-condition of an introduction rule.  Thus
+    the induction rule lets us assume that condition!  Many inductive proofs
+    are therefore unconditional.
+**)
+    
+