src/ZF/Zorn.thy
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 14653 0848ab6fe5fc
child 16417 9bc16273c2d4
permissions -rw-r--r--
fixed reference to renamed theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Zorn.thy
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     4
    Copyright   1994  University of Cambridge
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     5
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     6
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
     7
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     8
header{*Zorn's Lemma*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
     9
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    10
theory Zorn = OrderArith + AC + Inductive:
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    11
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    12
text{*Based upon the unpublished article ``Towards the Mechanization of the
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    13
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    14
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    15
constdefs
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    16
  Subset_rel :: "i=>i"
13558
paulson
parents: 13356
diff changeset
    17
   "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    18
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    19
  chain      :: "i=>i"
13558
paulson
parents: 13356
diff changeset
    20
   "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    21
14653
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14171
diff changeset
    22
  super      :: "[i,i]=>i"
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14171
diff changeset
    23
   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14171
diff changeset
    24
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    25
  maxchain   :: "i=>i"
13558
paulson
parents: 13356
diff changeset
    26
   "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
paulson
parents: 13356
diff changeset
    27
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    28
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    29
constdefs
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    30
  increasing :: "i=>i"
13558
paulson
parents: 13356
diff changeset
    31
    "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A --> x<=f`x}"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    32
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    33
13558
paulson
parents: 13356
diff changeset
    34
text{*Lemma for the inductive definition below*}
paulson
parents: 13356
diff changeset
    35
lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> Union(Y) \<in> Pow(A)"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    36
by blast
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    37
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    38
13558
paulson
parents: 13356
diff changeset
    39
text{*We could make the inductive definition conditional on
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    40
    @{term "next \<in> increasing(S)"}
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    41
    but instead we make this a side-condition of an introduction rule.  Thus
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    42
    the induction rule lets us assume that condition!  Many inductive proofs
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    43
    are therefore unconditional.*}
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    44
consts
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    45
  "TFin" :: "[i,i]=>i"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    46
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    47
inductive
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    48
  domains       "TFin(S,next)" <= "Pow(S)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    49
  intros
13558
paulson
parents: 13356
diff changeset
    50
    nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson
parents: 13356
diff changeset
    51
                  ==> next`x \<in> TFin(S,next)"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    52
13558
paulson
parents: 13356
diff changeset
    53
    Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> Union(Y) \<in> TFin(S,next)"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
    54
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 1478
diff changeset
    55
  monos         Pow_mono
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 1478
diff changeset
    56
  con_defs      increasing_def
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    57
  type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    58
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    59
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    60
subsection{*Mathematical Preamble *}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    61
13558
paulson
parents: 13356
diff changeset
    62
lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
    63
by blast
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    64
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    65
lemma Inter_lemma0:
13558
paulson
parents: 13356
diff changeset
    66
     "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A <= Inter(C) | Inter(C) <= B"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
    67
by blast
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    68
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    69
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    70
subsection{*The Transfinite Construction *}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    71
13558
paulson
parents: 13356
diff changeset
    72
lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    73
apply (unfold increasing_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    74
apply (erule CollectD1)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    75
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    76
13558
paulson
parents: 13356
diff changeset
    77
lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
    78
by (unfold increasing_def, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    79
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    80
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    81
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    82
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    83
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    84
13558
paulson
parents: 13356
diff changeset
    85
text{*Structural induction on @{term "TFin(S,next)"} *}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    86
lemma TFin_induct:
13558
paulson
parents: 13356
diff changeset
    87
  "[| n \<in> TFin(S,next);
paulson
parents: 13356
diff changeset
    88
      !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
paulson
parents: 13356
diff changeset
    89
      !!Y. [| Y <= TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(Union(Y))
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    90
   |] ==> P(n)"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    91
by (erule TFin.induct, blast+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    92
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    93
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
    94
subsection{*Some Properties of the Transfinite Construction *}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    95
13558
paulson
parents: 13356
diff changeset
    96
lemmas increasing_trans = subset_trans [OF _ increasingD2,
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    97
                                        OF _ _ TFin_is_subset]
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
    98
13558
paulson
parents: 13356
diff changeset
    99
text{*Lemma 1 of section 3.1*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   100
lemma TFin_linear_lemma1:
13558
paulson
parents: 13356
diff changeset
   101
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
paulson
parents: 13356
diff changeset
   102
         \<forall>x \<in> TFin(S,next) . x<=m --> x=m | next`x<=m |]
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   103
      ==> n<=m | next`m<=n"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   104
apply (erule TFin_induct)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   105
apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   106
(*downgrade subsetI from intro! to intro*)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   107
apply (blast dest: increasing_trans)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   108
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   109
13558
paulson
parents: 13356
diff changeset
   110
text{*Lemma 2 of section 3.2.  Interesting in its own right!
paulson
parents: 13356
diff changeset
   111
  Requires @{term "next \<in> increasing(S)"} in the second induction step.*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   112
lemma TFin_linear_lemma2:
13558
paulson
parents: 13356
diff changeset
   113
    "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson
parents: 13356
diff changeset
   114
     ==> \<forall>n \<in> TFin(S,next). n<=m --> n=m | next`n <= m"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   115
apply (erule TFin_induct)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   116
apply (rule impI [THEN ballI])
13558
paulson
parents: 13356
diff changeset
   117
txt{*case split using @{text TFin_linear_lemma1}*}
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13558
diff changeset
   118
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   119
       assumption+)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   120
apply (blast del: subsetI
13558
paulson
parents: 13356
diff changeset
   121
	     intro: increasing_trans subsetI, blast)
paulson
parents: 13356
diff changeset
   122
txt{*second induction step*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   123
apply (rule impI [THEN ballI])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   124
apply (rule Union_lemma0 [THEN disjE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   125
apply (erule_tac [3] disjI2)
13558
paulson
parents: 13356
diff changeset
   126
prefer 2 apply blast
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   127
apply (rule ballI)
13558
paulson
parents: 13356
diff changeset
   128
apply (drule bspec, assumption)
paulson
parents: 13356
diff changeset
   129
apply (drule subsetD, assumption)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13558
diff changeset
   130
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
13558
paulson
parents: 13356
diff changeset
   131
       assumption+, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   132
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   133
apply (blast dest: TFin_is_subset)+
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   134
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   135
13558
paulson
parents: 13356
diff changeset
   136
text{*a more convenient form for Lemma 2*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   137
lemma TFin_subsetD:
13558
paulson
parents: 13356
diff changeset
   138
     "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson
parents: 13356
diff changeset
   139
      ==> n=m | next`n <= m"
paulson
parents: 13356
diff changeset
   140
by (blast dest: TFin_linear_lemma2 [rule_format])
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   141
13558
paulson
parents: 13356
diff changeset
   142
text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   143
lemma TFin_subset_linear:
13558
paulson
parents: 13356
diff changeset
   144
     "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
paulson
parents: 13356
diff changeset
   145
      ==> n <= m | m<=n"
paulson
parents: 13356
diff changeset
   146
apply (rule disjE)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   147
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   148
apply (assumption+, erule disjI2)
13558
paulson
parents: 13356
diff changeset
   149
apply (blast del: subsetI
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   150
             intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   151
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   152
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   153
13558
paulson
parents: 13356
diff changeset
   154
text{*Lemma 3 of section 3.3*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   155
lemma equal_next_upper:
13558
paulson
parents: 13356
diff changeset
   156
     "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   157
apply (erule TFin_induct)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   158
apply (drule TFin_subsetD)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13558
diff changeset
   159
apply (assumption+, force, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   160
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   161
13558
paulson
parents: 13356
diff changeset
   162
text{*Property 3.3 of section 3.3*}
paulson
parents: 13356
diff changeset
   163
lemma equal_next_Union:
paulson
parents: 13356
diff changeset
   164
     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   165
      ==> m = next`m <-> m = Union(TFin(S,next))"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   166
apply (rule iffI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   167
apply (rule Union_upper [THEN equalityI])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   168
apply (rule_tac [2] equal_next_upper [THEN Union_least])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   169
apply (assumption+)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   170
apply (erule ssubst)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   171
apply (rule increasingD2 [THEN equalityI], assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   172
apply (blast del: subsetI
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   173
	     intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   174
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   175
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   176
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   177
subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   178
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   179
text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   180
relation!*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   181
13558
paulson
parents: 13356
diff changeset
   182
text{** Defining the "next" operation for Hausdorff's Theorem **}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   183
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   184
lemma chain_subset_Pow: "chain(A) <= Pow(A)"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   185
apply (unfold chain_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   186
apply (rule Collect_subset)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   187
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   188
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   189
lemma super_subset_chain: "super(A,c) <= chain(A)"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   190
apply (unfold super_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   191
apply (rule Collect_subset)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   192
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   193
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   194
lemma maxchain_subset_chain: "maxchain(A) <= chain(A)"
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   195
apply (unfold maxchain_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   196
apply (rule Collect_subset)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   197
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   198
13558
paulson
parents: 13356
diff changeset
   199
lemma choice_super:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   200
     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
13558
paulson
parents: 13356
diff changeset
   201
      ==> ch ` super(S,X) \<in> super(S,X)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   202
apply (erule apply_type)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   203
apply (unfold super_def maxchain_def, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   204
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   205
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   206
lemma choice_not_equals:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   207
     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
13558
paulson
parents: 13356
diff changeset
   208
      ==> ch ` super(S,X) \<noteq> X"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   209
apply (rule notI)
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13558
diff changeset
   210
apply (drule choice_super, assumption, assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   211
apply (simp add: super_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   212
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   213
13558
paulson
parents: 13356
diff changeset
   214
text{*This justifies Definition 4.4*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   215
lemma Hausdorff_next_exists:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   216
     "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
13558
paulson
parents: 13356
diff changeset
   217
      \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
paulson
parents: 13356
diff changeset
   218
                   next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
paulson
parents: 13356
diff changeset
   219
apply (rule_tac x="\<lambda>X\<in>Pow(S).
paulson
parents: 13356
diff changeset
   220
                   if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13134
diff changeset
   221
       in bexI)
13558
paulson
parents: 13356
diff changeset
   222
apply force
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   223
apply (unfold increasing_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   224
apply (rule CollectI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   225
apply (rule lam_type)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   226
apply (simp (no_asm_simp))
13558
paulson
parents: 13356
diff changeset
   227
apply (blast dest: super_subset_chain [THEN subsetD] 
paulson
parents: 13356
diff changeset
   228
                   chain_subset_Pow [THEN subsetD] choice_super)
paulson
parents: 13356
diff changeset
   229
txt{*Now, verify that it increases*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   230
apply (simp (no_asm_simp) add: Pow_iff subset_refl)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   231
apply safe
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   232
apply (drule choice_super)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   233
apply (assumption+)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   234
apply (simp add: super_def, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   235
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   236
13558
paulson
parents: 13356
diff changeset
   237
text{*Lemma 4*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   238
lemma TFin_chain_lemma4:
13558
paulson
parents: 13356
diff changeset
   239
     "[| c \<in> TFin(S,next);
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   240
         ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
13558
paulson
parents: 13356
diff changeset
   241
         next \<in> increasing(S);
paulson
parents: 13356
diff changeset
   242
         \<forall>X \<in> Pow(S). next`X =
paulson
parents: 13356
diff changeset
   243
                          if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
paulson
parents: 13356
diff changeset
   244
     ==> c \<in> chain(S)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   245
apply (erule TFin_induct)
13558
paulson
parents: 13356
diff changeset
   246
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   247
            choice_super [THEN super_subset_chain [THEN subsetD]])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   248
apply (unfold chain_def)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   249
apply (rule CollectI, blast, safe)
13558
paulson
parents: 13356
diff changeset
   250
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
paulson
parents: 13356
diff changeset
   251
      txt{*@{text "Blast_tac's"} slow*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   252
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   253
13558
paulson
parents: 13356
diff changeset
   254
theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   255
apply (rule AC_Pi_Pow [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   256
apply (rule Hausdorff_next_exists [THEN bexE], assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   257
apply (rename_tac ch "next")
13558
paulson
parents: 13356
diff changeset
   258
apply (subgoal_tac "Union (TFin (S,next)) \<in> chain (S) ")
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   259
prefer 2
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   260
 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   261
apply (rule_tac x = "Union (TFin (S,next))" in exI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   262
apply (rule classical)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   263
apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   264
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   265
apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   266
prefer 2 apply assumption
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   267
apply (rule_tac [2] refl)
13558
paulson
parents: 13356
diff changeset
   268
apply (simp add: subset_refl [THEN TFin_UnionI,
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   269
                              THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   270
apply (erule choice_not_equals [THEN notE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   271
apply (assumption+)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   272
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   273
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   274
13558
paulson
parents: 13356
diff changeset
   275
subsection{*Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
paulson
parents: 13356
diff changeset
   276
       then S contains a Maximal Element*}
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   277
13558
paulson
parents: 13356
diff changeset
   278
text{*Used in the proof of Zorn's Lemma*}
paulson
parents: 13356
diff changeset
   279
lemma chain_extend:
paulson
parents: 13356
diff changeset
   280
    "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   281
by (unfold chain_def, blast)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   282
13558
paulson
parents: 13356
diff changeset
   283
lemma Zorn: "\<forall>c \<in> chain(S). Union(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   284
apply (rule Hausdorff [THEN exE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   285
apply (simp add: maxchain_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   286
apply (rename_tac c)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   287
apply (rule_tac x = "Union (c)" in bexI)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   288
prefer 2 apply blast
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   289
apply safe
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   290
apply (rename_tac z)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   291
apply (rule classical)
13558
paulson
parents: 13356
diff changeset
   292
apply (subgoal_tac "cons (z,c) \<in> super (S,c) ")
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   293
apply (blast elim: equalityE)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   294
apply (unfold super_def, safe)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   295
apply (fast elim: chain_extend)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   296
apply (fast elim: equalityE)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   297
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   298
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   299
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13269
diff changeset
   300
subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   301
13558
paulson
parents: 13356
diff changeset
   302
text{*Lemma 5*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   303
lemma TFin_well_lemma5:
13558
paulson
parents: 13356
diff changeset
   304
     "[| n \<in> TFin(S,next);  Z <= TFin(S,next);  z:Z;  ~ Inter(Z) \<in> Z |]
paulson
parents: 13356
diff changeset
   305
      ==> \<forall>m \<in> Z. n <= m"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   306
apply (erule TFin_induct)
13558
paulson
parents: 13356
diff changeset
   307
prefer 2 apply blast txt{*second induction step is easy*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   308
apply (rule ballI)
13558
paulson
parents: 13356
diff changeset
   309
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   310
apply (subgoal_tac "m = Inter (Z) ")
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   311
apply blast+
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   312
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   313
13558
paulson
parents: 13356
diff changeset
   314
text{*Well-ordering of @{term "TFin(S,next)"} *}
paulson
parents: 13356
diff changeset
   315
lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next);  z \<in> Z |] ==> Inter(Z) \<in> Z"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   316
apply (rule classical)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   317
apply (subgoal_tac "Z = {Union (TFin (S,next))}")
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   318
apply (simp (no_asm_simp) add: Inter_singleton)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   319
apply (erule equal_singleton)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   320
apply (rule Union_upper [THEN equalityI])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   321
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   322
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   323
13558
paulson
parents: 13356
diff changeset
   324
text{*This theorem just packages the previous result*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   325
lemma well_ord_TFin:
13558
paulson
parents: 13356
diff changeset
   326
     "next \<in> increasing(S) 
paulson
parents: 13356
diff changeset
   327
      ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   328
apply (rule well_ordI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   329
apply (unfold Subset_rel_def linear_def)
13558
paulson
parents: 13356
diff changeset
   330
txt{*Prove the well-foundedness goal*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   331
apply (rule wf_onI)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   332
apply (frule well_ord_TFin_lemma, assumption)
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   333
apply (drule_tac x = "Inter (Z) " in bspec, assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   334
apply blast
13558
paulson
parents: 13356
diff changeset
   335
txt{*Now prove the linearity goal*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   336
apply (intro ballI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   337
apply (case_tac "x=y")
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   338
 apply blast
13558
paulson
parents: 13356
diff changeset
   339
txt{*The @{term "x\<noteq>y"} case remains*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   340
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   341
       assumption+, blast+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   342
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   343
13558
paulson
parents: 13356
diff changeset
   344
text{** Defining the "next" operation for Zermelo's Theorem **}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   345
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   346
lemma choice_Diff:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   347
     "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   348
apply (erule apply_type)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   349
apply (blast elim!: equalityE)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   350
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   351
13558
paulson
parents: 13356
diff changeset
   352
text{*This justifies Definition 6.1*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   353
lemma Zermelo_next_exists:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   354
     "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
13558
paulson
parents: 13356
diff changeset
   355
           \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13134
diff changeset
   356
                      next`X = (if X=S then S else cons(ch`(S-X), X))"
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13134
diff changeset
   357
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13134
diff changeset
   358
       in bexI)
13558
paulson
parents: 13356
diff changeset
   359
apply force
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   360
apply (unfold increasing_def)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   361
apply (rule CollectI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   362
apply (rule lam_type)
13558
paulson
parents: 13356
diff changeset
   363
txt{*Type checking is surprisingly hard!*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   364
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   365
apply (blast intro!: choice_Diff [THEN DiffD1])
13558
paulson
parents: 13356
diff changeset
   366
txt{*Verify that it increases*}
paulson
parents: 13356
diff changeset
   367
apply (intro allI impI)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   368
apply (simp add: Pow_iff subset_consI subset_refl)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   369
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   370
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   371
13558
paulson
parents: 13356
diff changeset
   372
text{*The construction of the injection*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   373
lemma choice_imp_injection:
14171
0cab06e3bbd0 Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents: 13784
diff changeset
   374
     "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
13558
paulson
parents: 13356
diff changeset
   375
         next \<in> increasing(S);
paulson
parents: 13356
diff changeset
   376
         \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
paulson
parents: 13356
diff changeset
   377
      ==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y}))
paulson
parents: 13356
diff changeset
   378
               \<in> inj(S, TFin(S,next) - {S})"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   379
apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   380
apply (rule DiffI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   381
apply (rule Collect_subset [THEN TFin_UnionI])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   382
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
13558
paulson
parents: 13356
diff changeset
   383
apply (subgoal_tac "x \<notin> Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   384
prefer 2 apply (blast elim: equalityE)
13558
paulson
parents: 13356
diff changeset
   385
apply (subgoal_tac "Union ({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   386
prefer 2 apply (blast elim: equalityE)
13558
paulson
parents: 13356
diff changeset
   387
txt{*For proving @{text "x \<in> next`Union(...)"}.
paulson
parents: 13356
diff changeset
   388
  Abrial and Laffitte's justification appears to be faulty.*}
paulson
parents: 13356
diff changeset
   389
apply (subgoal_tac "~ next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) 
paulson
parents: 13356
diff changeset
   390
                    <= Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson
parents: 13356
diff changeset
   391
 prefer 2
paulson
parents: 13356
diff changeset
   392
 apply (simp del: Union_iff
paulson
parents: 13356
diff changeset
   393
	     add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
paulson
parents: 13356
diff changeset
   394
	     Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
paulson
parents: 13356
diff changeset
   395
apply (subgoal_tac "x \<in> next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) ")
paulson
parents: 13356
diff changeset
   396
 prefer 2
paulson
parents: 13356
diff changeset
   397
 apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
paulson
parents: 13356
diff changeset
   398
txt{*End of the lemmas!*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   399
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   400
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   401
13558
paulson
parents: 13356
diff changeset
   402
text{*The wellordering theorem*}
paulson
parents: 13356
diff changeset
   403
theorem AC_well_ord: "\<exists>r. well_ord(S,r)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   404
apply (rule AC_Pi_Pow [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   405
apply (rule Zermelo_next_exists [THEN bexE], assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   406
apply (rule exI)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   407
apply (rule well_ord_rvimage)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   408
apply (erule_tac [2] well_ord_TFin)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13175
diff changeset
   409
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 6053
diff changeset
   410
done
13558
paulson
parents: 13356
diff changeset
   411
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 485
diff changeset
   412
end