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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Zorn0.ML
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     2
    ID:         $Id$
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     5
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     6
Preamble to proofs from the paper
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     7
    Abrial & Laffitte, 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     8
    Towards the Mechanization of the Proofs of Some 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     9
    Classical Theorems of Set Theory. 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    10
*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    11
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    12
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    13
(*** Section 1.  Mathematical Preamble ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    14
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    15
goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    16
by (fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    17
val Union_lemma0 = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    18
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    19
goal ZF.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    20
    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    21
by (fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    22
val Inter_lemma0 = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    23
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    24
open Zorn0;
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    25
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    26
(*** Section 2.  The Transfinite Construction ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    27
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    28
goalw Zorn0.thy [increasing_def]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    29
    "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    30
by (eresolve_tac [CollectD1] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    31
val increasingD1 = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    32
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    33
goalw Zorn0.thy [increasing_def]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    34
    "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    35
by (eresolve_tac [CollectD2 RS spec RS mp] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    36
by (assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    37
val increasingD2 = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    38
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    39
goal Zorn0.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    40
    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    41
by (eresolve_tac [increasingD1 RS apply_type] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    42
by (assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    43
val next_bounded = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    44
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    45
(*Trivial to prove here; hard to prove within Inductive_Fun*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    46
goal ZF.thy "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    47
by (fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    48
val Union_in_Pow = result();
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    49
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    50
(** We could make the inductive definition conditional on next: increasing(S)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    51
    but instead we make this a side-condition of an introduction rule.  Thus
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    52
    the induction rule lets us assume that condition!  Many inductive proofs
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    53
    are therefore unconditional.
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    54
**)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    55
    
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    56