src/ZF/Zorn.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
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:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
     1
(*  Title:      ZF/Zorn.ML
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
485
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
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     6
Proofs from the paper
485
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
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    12
open Zorn;
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    13
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    14
(*** Section 1.  Mathematical Preamble ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    15
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    16
goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    17
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    18
qed "Union_lemma0";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    19
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    20
goal ZF.thy
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    21
    "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    22
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    23
qed "Inter_lemma0";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    24
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    25
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    26
(*** Section 2.  The Transfinite Construction ***)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    27
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    28
goalw Zorn.thy [increasing_def]
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    29
    "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    30
by (etac CollectD1 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    31
qed "increasingD1";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    32
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    33
goalw Zorn.thy [increasing_def]
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    34
    "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    35
by (eresolve_tac [CollectD2 RS spec RS mp] 1);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    36
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    37
qed "increasingD2";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    38
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    39
(*Introduction rules*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    40
val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    41
val TFin_UnionI = PowI RS Pow_TFin_UnionI;
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    42
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    43
val TFin_is_subset = TFin.dom_subset RS subsetD RS PowD;
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    44
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    45
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    46
(** Structural induction on TFin(S,next) **)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    47
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    48
val major::prems = goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    49
  "[| n: TFin(S,next);  \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    50
\     !!x. [| x : TFin(S,next);  P(x);  next: increasing(S) |] ==> P(next`x); \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    51
\     !!Y. [| Y <= TFin(S,next);  ALL y:Y. P(y) |] ==> P(Union(Y)) \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    52
\  |] ==> P(n)";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    53
by (rtac (major RS TFin.induct) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    54
by (ALLGOALS (fast_tac (ZF_cs addIs prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    55
qed "TFin_induct";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    56
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    57
(*Perform induction on n, then prove the major premise using prems. *)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    58
fun TFin_ind_tac a prems i = 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    59
    EVERY [res_inst_tac [("n",a)] TFin_induct i,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
    60
           rename_last_tac a ["1"] (i+1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
    61
           rename_last_tac a ["2"] (i+2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
    62
           ares_tac prems i];
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    63
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    64
(*** Section 3.  Some Properties of the Transfinite Construction ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    65
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 760
diff changeset
    66
bind_thm ("increasing_trans", 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
    67
          TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)));
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    68
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    69
(*Lemma 1 of section 3.1*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    70
val major::prems = goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    71
    "[| n: TFin(S,next);  m: TFin(S,next);  \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    72
\       ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    73
\    |] ==> n<=m | next`m<=n";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    74
by (cut_facts_tac prems 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    75
by (rtac (major RS TFin_induct) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
    76
by (etac Union_lemma0 2);               (*or just fast_tac ZF_cs*)
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    77
by (fast_tac (subset_cs addIs [increasing_trans]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
    78
qed "TFin_linear_lemma1";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    79
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    80
(*Lemma 2 of section 3.2.  Interesting in its own right!
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    81
  Requires next: increasing(S) in the second induction step. *)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    82
val [major,ninc] = goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    83
    "[| m: TFin(S,next);  next: increasing(S) \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    84
\    |] ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    85
by (rtac (major RS TFin_induct) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    86
by (rtac (impI RS ballI) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    87
(*case split using TFin_linear_lemma1*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    88
by (res_inst_tac [("n1","n"), ("m1","x")] 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    89
    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    90
by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    91
by (fast_tac (subset_cs addIs [increasing_trans]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    92
by (REPEAT (ares_tac [disjI1,equalityI] 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    93
(*second induction step*)
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    94
by (rtac (impI RS ballI) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    95
by (rtac (Union_lemma0 RS disjE) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    96
by (etac disjI2 3);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    97
by (REPEAT (ares_tac [disjI1,equalityI] 2));
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
    98
by (rtac ballI 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    99
by (ball_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   100
by (set_mp_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   101
by (res_inst_tac [("n1","n"), ("m1","x")] 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   102
    (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   103
by (fast_tac subset_cs 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   104
by (rtac (ninc RS increasingD2 RS subset_trans RS disjI1) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   105
by (REPEAT (ares_tac [TFin_is_subset] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   106
qed "TFin_linear_lemma2";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   107
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   108
(*a more convenient form for Lemma 2*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   109
goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   110
    "!!m n. [| n<=m;  m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   111
\           |] ==> n=m | next`n<=m";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   112
by (rtac (TFin_linear_lemma2 RS bspec RS mp) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   113
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   114
qed "TFin_subsetD";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   115
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   116
(*Consequences from section 3.3 -- Property 3.2, the ordering is total*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   117
goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   118
    "!!m n. [| m: TFin(S,next);  n: TFin(S,next);  next: increasing(S) \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   119
\           |] ==> n<=m | m<=n";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   120
by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   121
by (REPEAT (assume_tac 1) THEN etac disjI2 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   122
by (fast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   123
                               TFin_is_subset]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   124
qed "TFin_subset_linear";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   125
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   126
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   127
(*Lemma 3 of section 3.3*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   128
val major::prems = goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   129
    "[| n: TFin(S,next);  m: TFin(S,next);  m = next`m |] ==> n<=m";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   130
by (cut_facts_tac prems 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   131
by (rtac (major RS TFin_induct) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   132
by (dtac TFin_subsetD 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   133
by (REPEAT (assume_tac 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   134
by (fast_tac (ZF_cs addEs [ssubst]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   135
by (fast_tac (subset_cs addIs [TFin_is_subset]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   136
qed "equal_next_upper";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   137
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   138
(*Property 3.3 of section 3.3*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   139
goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   140
    "!!m. [| m: TFin(S,next);  next: increasing(S) \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   141
\         |] ==> m = next`m <-> m = Union(TFin(S,next))";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   142
by (rtac iffI 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   143
by (rtac (Union_upper RS equalityI) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   144
by (rtac (equal_next_upper RS Union_least) 2);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   145
by (REPEAT (assume_tac 1));
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   146
by (etac ssubst 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   147
by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   148
by (ALLGOALS
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   149
    (fast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   150
qed "equal_next_Union";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   151
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   152
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   153
(*** Section 4.  Hausdorff's Theorem: every set contains a maximal chain ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   154
(*** NB: We assume the partial ordering is <=, the subset relation! **)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   155
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   156
(** Defining the "next" operation for Hausdorff's Theorem **)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   157
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   158
goalw Zorn.thy [chain_def] "chain(A) <= Pow(A)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   159
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   160
qed "chain_subset_Pow";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   161
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   162
goalw Zorn.thy [super_def] "super(A,c) <= chain(A)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   163
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   164
qed "super_subset_chain";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   165
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   166
goalw Zorn.thy [maxchain_def] "maxchain(A) <= chain(A)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   167
by (rtac Collect_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   168
qed "maxchain_subset_chain";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   169
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   170
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   171
    "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X);      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   172
\            X : chain(S);  X ~: maxchain(S)            \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   173
\         |] ==> ch ` super(S,X) : super(S,X)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   174
by (etac apply_type 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   175
by (rewrite_goals_tac [super_def, maxchain_def]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   176
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   177
qed "choice_super";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   178
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   179
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   180
    "!!S. [| ch : (PROD X:Pow(chain(S)) - {0}. X);      \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   181
\            X : chain(S);  X ~: maxchain(S)            \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   182
\         |] ==> ch ` super(S,X) ~= X";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   183
by (rtac notI 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   184
by (dtac choice_super 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   185
by (assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   186
by (assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   187
by (asm_full_simp_tac (ZF_ss addsimps [super_def]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   188
qed "choice_not_equals";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   189
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   190
(*This justifies Definition 4.4*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   191
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   192
    "!!S. ch: (PROD X: Pow(chain(S))-{0}. X) ==>        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   193
\          EX next: increasing(S). ALL X: Pow(S).       \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   194
\                     next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   195
by (rtac bexI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   196
by (rtac ballI 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   197
by (rtac beta 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   198
by (assume_tac 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   199
by (rewtac increasing_def);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   200
by (rtac CollectI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   201
by (rtac lam_type 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   202
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   203
by (fast_tac (ZF_cs addSIs [super_subset_chain RS subsetD,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   204
                            chain_subset_Pow RS subsetD,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   205
                            choice_super]) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   206
(*Now, verify that it increases*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   207
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   208
                        setloop split_tac [expand_if]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   209
by (safe_tac ZF_cs);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   210
by (dtac choice_super 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   211
by (REPEAT (assume_tac 1));
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   212
by (rewtac super_def);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   213
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   214
qed "Hausdorff_next_exists";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   215
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   216
(*Lemma 4*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   217
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   218
 "!!S. [| c: TFin(S,next);                              \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   219
\         ch: (PROD X: Pow(chain(S))-{0}. X);           \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   220
\         next: increasing(S);                          \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   221
\         ALL X: Pow(S). next`X =       \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   222
\                         if(X: chain(S)-maxchain(S), ch`super(S,X), X) \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   223
\      |] ==> c: chain(S)";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   224
by (etac TFin_induct 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   225
by (asm_simp_tac 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   226
    (ZF_ss addsimps [chain_subset_Pow RS subsetD, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   227
                     choice_super RS (super_subset_chain RS subsetD)]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   228
           setloop split_tac [expand_if]) 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   229
by (rewtac chain_def);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   230
by (rtac CollectI 1 THEN fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   231
(*Cannot use safe_tac: the disjunction must be left alone*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   232
by (REPEAT (rtac ballI 1 ORELSE etac UnionE 1));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   233
by (res_inst_tac  [("m1","B"), ("n1","Ba")] (TFin_subset_linear RS disjE) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   234
(*fast_tac is just too slow here!*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   235
by (DEPTH_SOLVE (eresolve_tac [asm_rl, subsetD] 1
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   236
       ORELSE ball_tac 1 THEN etac (CollectD2 RS bspec RS bspec) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   237
qed "TFin_chain_lemma4";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   238
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   239
goal Zorn.thy "EX c. c : maxchain(S)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   240
by (rtac (AC_Pi_Pow RS exE) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   241
by (rtac (Hausdorff_next_exists RS bexE) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   242
by (assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   243
by (rename_tac "ch next" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   244
by (subgoal_tac "Union(TFin(S,next)) : chain(S)" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   245
by (REPEAT (ares_tac [TFin_chain_lemma4, subset_refl RS TFin_UnionI] 2));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   246
by (res_inst_tac [("x", "Union(TFin(S,next))")] exI 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   247
by (rtac classical 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   248
by (subgoal_tac "next ` Union(TFin(S,next)) = Union(TFin(S,next))" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   249
by (resolve_tac [equal_next_Union RS iffD2 RS sym] 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   250
by (resolve_tac [subset_refl RS TFin_UnionI] 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   251
by (assume_tac 2);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   252
by (rtac refl 2);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   253
by (asm_full_simp_tac 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   254
    (ZF_ss addsimps [subset_refl RS TFin_UnionI RS
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   255
                     (TFin.dom_subset RS subsetD)]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   256
           setloop split_tac [expand_if]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   257
by (eresolve_tac [choice_not_equals RS notE] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   258
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   259
qed "Hausdorff";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   260
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   261
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   262
(*** Section 5.  Zorn's Lemma: if all chains in S have upper bounds in S 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   263
                               then S contains a maximal element ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   264
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   265
(*Used in the proof of Zorn's Lemma*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   266
goalw Zorn.thy [chain_def]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   267
    "!!c. [| c: chain(A);  z: A;  ALL x:c. x<=z |] ==> cons(z,c) : chain(A)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   268
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   269
qed "chain_extend";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   270
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   271
goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   272
    "!!S. ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   273
by (resolve_tac [Hausdorff RS exE] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   274
by (asm_full_simp_tac (ZF_ss addsimps [maxchain_def]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   275
by (rename_tac "c" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   276
by (res_inst_tac [("x", "Union(c)")] bexI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   277
by (fast_tac ZF_cs 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   278
by (safe_tac ZF_cs);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   279
by (rename_tac "z" 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   280
by (rtac classical 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   281
by (subgoal_tac "cons(z,c): super(S,c)" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   282
by (fast_tac (ZF_cs addEs [equalityE]) 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   283
by (rewtac super_def);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   284
by (safe_tac eq_cs);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   285
by (fast_tac (ZF_cs addEs [chain_extend]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   286
by (best_tac (ZF_cs addEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   287
qed "Zorn";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   288
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   289
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   290
(*** Section 6.  Zermelo's Theorem: every set can be well-ordered ***)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   291
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   292
(*Lemma 5*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   293
val major::prems = goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   294
    "[| n: TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) : Z      \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   295
\    |] ==> ALL m:Z. n<=m";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   296
by (cut_facts_tac prems 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   297
by (rtac (major RS TFin_induct) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   298
by (fast_tac ZF_cs 2);                  (*second induction step is easy*)
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   299
by (rtac ballI 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   300
by (rtac (bspec RS TFin_subsetD RS disjE) 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   301
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   302
by (subgoal_tac "x = Inter(Z)" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   303
by (fast_tac ZF_cs 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   304
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   305
qed "TFin_well_lemma5";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   306
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   307
(*Well-ordering of TFin(S,next)*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   308
goal Zorn.thy "!!Z. [| Z <= TFin(S,next);  z:Z |] ==> Inter(Z) : Z";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   309
by (rtac classical 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   310
by (subgoal_tac "Z = {Union(TFin(S,next))}" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   311
by (asm_simp_tac (ZF_ss addsimps [Inter_singleton]) 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   312
by (etac equal_singleton 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   313
by (rtac (Union_upper RS equalityI) 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   314
by (rtac (subset_refl RS TFin_UnionI RS TFin_well_lemma5 RS bspec) 2);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   315
by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   316
qed "well_ord_TFin_lemma";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   317
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   318
(*This theorem just packages the previous result*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   319
goal Zorn.thy
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   320
    "!!S. next: increasing(S) ==> \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   321
\         well_ord(TFin(S,next), Subset_rel(TFin(S,next)))";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   322
by (rtac well_ordI 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   323
by (rewrite_goals_tac [Subset_rel_def, linear_def]);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   324
(*Prove the linearity goal first*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   325
by (REPEAT (rtac ballI 2));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   326
by (excluded_middle_tac "x=y" 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   327
by (fast_tac ZF_cs 3);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   328
(*The x~=y case remains*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   329
by (res_inst_tac [("n1","x"), ("m1","y")] 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   330
    (TFin_subset_linear RS disjE) 2  THEN  REPEAT (assume_tac 2));
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   331
by (fast_tac ZF_cs 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   332
by (fast_tac ZF_cs 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   333
(*Now prove the well_foundedness goal*)
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   334
by (rtac wf_onI 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   335
by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   336
by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   337
by (fast_tac eq_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   338
qed "well_ord_TFin";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   339
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   340
(** Defining the "next" operation for Zermelo's Theorem **)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   341
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   342
goal AC.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   343
    "!!S. [| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S        \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   344
\         |] ==> ch ` (S-X) : S-X";
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   345
by (etac apply_type 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   346
by (fast_tac (eq_cs addEs [equalityE]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   347
qed "choice_Diff";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   348
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   349
(*This justifies Definition 6.1*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   350
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   351
    "!!S. ch: (PROD X: Pow(S)-{0}. X) ==>               \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   352
\          EX next: increasing(S). ALL X: Pow(S).       \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   353
\                     next`X = if(X=S, S, cons(ch`(S-X), X))";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   354
by (rtac bexI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   355
by (rtac ballI 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   356
by (rtac beta 1);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   357
by (assume_tac 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   358
by (rewtac increasing_def);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   359
by (rtac CollectI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   360
by (rtac lam_type 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   361
(*Verify that it increases*)
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   362
by (rtac allI 2);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   363
by (rtac impI 2);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   364
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_consI, subset_refl]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   365
                        setloop split_tac [expand_if]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   366
(*Type checking is surprisingly hard!*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   367
by (asm_simp_tac (ZF_ss addsimps [Pow_iff, cons_subset_iff, subset_refl]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   368
                        setloop split_tac [expand_if]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   369
by (fast_tac (ZF_cs addSIs [choice_Diff RS DiffD1]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   370
qed "Zermelo_next_exists";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   371
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   372
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   373
(*The construction of the injection*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   374
goal Zorn.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   375
  "!!S. [| ch: (PROD X: Pow(S)-{0}. X);                 \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   376
\          next: increasing(S);                         \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   377
\          ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X))        \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   378
\       |] ==> (lam x:S. Union({y: TFin(S,next). x~: y}))       \
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   379
\              : inj(S, TFin(S,next) - {S})";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   380
by (res_inst_tac [("d", "%y. ch`(S-y)")] lam_injective 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   381
by (rtac DiffI 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   382
by (resolve_tac [Collect_subset RS TFin_UnionI] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   383
by (fast_tac (ZF_cs addSIs [Collect_subset RS TFin_UnionI]
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   384
                    addEs [equalityE]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   385
by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   386
by (fast_tac (ZF_cs addEs [equalityE]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   387
by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   388
by (fast_tac (ZF_cs addEs [equalityE]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   389
(*For proving x : next`Union(...);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   390
  Abrial & Laffitte's justification appears to be faulty.*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   391
by (subgoal_tac "~ next ` Union({y: TFin(S,next). x~: y}) <= \
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   392
\                  Union({y: TFin(S,next). x~: y})" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   393
by (asm_simp_tac 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   394
    (ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   395
                     Pow_iff, cons_subset_iff, subset_refl,
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   396
                     choice_Diff RS DiffD2]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   397
           setloop split_tac [expand_if]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   398
by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   399
by (fast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   400
(*End of the lemmas!*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   401
by (asm_full_simp_tac 
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   402
    (ZF_ss addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1079
diff changeset
   403
                     Pow_iff, cons_subset_iff, subset_refl]
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   404
           setloop split_tac [expand_if]) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   405
by (REPEAT (eresolve_tac [asm_rl, consE, sym, notE] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   406
qed "choice_imp_injection";
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   407
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   408
(*The wellordering theorem*)
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   409
goal Zorn.thy "EX r. well_ord(S,r)";
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   410
by (rtac (AC_Pi_Pow RS exE) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   411
by (rtac (Zermelo_next_exists RS bexE) 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   412
by (assume_tac 1);
804
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   413
by (rtac exI 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   414
by (rtac well_ord_rvimage 1);
02430d273ebf ran expandshort script
lcp
parents: 803
diff changeset
   415
by (etac well_ord_TFin 2);
485
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   416
by (resolve_tac [choice_imp_injection RS inj_weaken_type] 1);
5e00a676a211 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   417
by (REPEAT (ares_tac [Diff_subset] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 593
diff changeset
   418
qed "AC_well_ord";