src/ZF/Zorn0.ML
 author paulson Fri, 16 Feb 1996 18:00:47 +0100 changeset 1512 ce37c64244c0 parent 485 5e00a676a211 permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
```
(*  Title: 	ZF/Zorn0.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

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.
**)

```