src/ZF/AC/AC15_WO6.thy
author nipkow
Sat, 08 Aug 2020 18:20:09 +0200
changeset 72122 2dcb6523f6af
parent 61980 6b780867d426
child 76213 e44d86131648
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     1
(*  Title:      ZF/AC/AC15_WO6.thy
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     2
    Author:     Krzysztof Grabczewski
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     3
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     4
The proofs needed to state that AC10, ..., AC15 are equivalent to the rest.
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     5
We need the following:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     6
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     7
WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     8
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
     9
In order to add the formulations AC13 and AC14 we need:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    10
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    11
AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    12
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    13
or
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    14
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    15
AC1 ==> AC13(1);  AC13(m) ==> AC13(n) ==> AC14 ==> AC15    (m\<le>n)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    16
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    17
So we don't have to prove all implications of both cases.
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    18
Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    19
Rubin & Rubin do.
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    20
*)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    21
27678
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
    22
theory AC15_WO6
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
    23
imports HH Cardinal_aux
85ea2be46c71 dropped locale (open)
haftmann
parents: 16417
diff changeset
    24
begin
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    25
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    26
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    27
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    28
(* Lemmas used in the proofs in which the conclusion is AC13, AC14        *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    29
(* or AC15                                                                *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    30
(*  - cons_times_nat_not_Finite                                           *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    31
(*  - ex_fun_AC13_AC15                                                    *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    32
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    33
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    34
lemma lepoll_Sigma: "A\<noteq>0 ==> B \<lesssim> A*B"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    35
apply (unfold lepoll_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    36
apply (erule not_emptyE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    37
apply (rule_tac x = "\<lambda>z \<in> B. <x,z>" in exI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    38
apply (fast intro!: snd_conv lam_injective)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    39
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    40
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    41
lemma cons_times_nat_not_Finite:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    42
     "0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    43
apply clarify 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    44
apply (rule nat_not_Finite [THEN notE] )
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    45
apply (subgoal_tac "x \<noteq> 0")
13245
714f7a423a15 development and tweaks
paulson
parents: 13175
diff changeset
    46
 apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    47
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    48
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    49
lemma lemma1: "[| \<Union>(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    50
by fast
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    51
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    52
lemma lemma2: 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    53
        "[| pairwise_disjoint(A); B \<in> A; C \<in> A; a \<in> B; a \<in> C |] ==> B=C"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    54
by (unfold pairwise_disjoint_def, blast) 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    55
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    56
lemma lemma3: 
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
    57
     "\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &   
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
    58
             sets_of_size_between(f`B, 2, n) & \<Union>(f`B)=B   
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
    59
     ==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &   
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
    60
             0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    61
apply (unfold sets_of_size_between_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    62
apply (rule ballI)
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
    63
apply (erule_tac x="cons(0, B*nat)" in ballE)
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12814
diff changeset
    64
 apply (blast dest: lemma1 intro!: lemma2, blast)
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    65
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    66
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    67
lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    68
apply (unfold lepoll_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    69
apply (erule exE)
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 46822
diff changeset
    70
apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) & f`a=j" 
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    71
       in exI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    72
apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    73
apply (erule RepFunE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    74
apply (frule inj_is_fun [THEN apply_type], assumption)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    75
apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    76
apply (erule RepFunE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    77
apply (rule LeastI2)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    78
  apply fast
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    79
 apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    80
apply (fast elim: sym left_inverse [THEN ssubst])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    81
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    82
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    83
lemma lemma5_1:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    84
     "[| B \<in> A; 2 \<lesssim> u(B) |] ==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<noteq> 0"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    85
apply simp
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    86
apply (fast dest: lepoll_Diff_sing 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    87
            elim: lepoll_trans [THEN succ_lepoll_natE] ssubst
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    88
            intro!: lepoll_refl)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    89
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    90
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    91
lemma lemma5_2:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    92
     "[|  B \<in> A; u(B) \<subseteq> cons(0, B*nat) |]   
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    93
      ==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<subseteq> B"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    94
apply auto 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    95
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    96
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    97
lemma lemma5_3:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    98
     "[| n \<in> nat; B \<in> A; 0 \<in> u(B); u(B) \<lesssim> succ(n) |]   
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
    99
      ==> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<lesssim> n"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   100
apply simp
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   101
apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   102
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   103
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   104
lemma ex_fun_AC13_AC15:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   105
     "[| \<forall>B \<in> {cons(0, x*nat). x \<in> A}.   
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   106
                pairwise_disjoint(f`B) &   
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 32960
diff changeset
   107
                sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B; 
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   108
         n \<in> nat |]   
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   109
      ==> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 & f`B \<subseteq> B & f`B \<lesssim> n"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   110
by (fast del: subsetI notI
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
   111
         dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3)
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   112
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   113
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   114
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   115
(* The target proofs                                                      *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   116
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   117
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   118
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   119
(* AC10(n) ==> AC11                                                       *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   120
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   121
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   122
theorem AC10_AC11: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC11"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   123
by (unfold AC10_def AC11_def, blast)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   124
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   125
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   126
(* AC11 ==> AC12                                                          *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   127
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   128
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   129
theorem AC11_AC12: "AC11 ==> AC12"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   130
by (unfold AC10_def AC11_def AC11_def AC12_def, blast)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   131
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   132
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   133
(* AC12 ==> AC15                                                          *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   134
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   135
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   136
theorem AC12_AC15: "AC12 ==> AC15"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   137
apply (unfold AC12_def AC15_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   138
apply (blast del: ballI 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   139
             intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   140
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   141
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   142
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   143
(* AC15 ==> WO6                                                           *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   144
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   145
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   146
lemma OUN_eq_UN: "Ord(x) ==> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   147
by (fast intro!: ltI dest!: ltD)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   148
13535
007559e981c7 *** empty log message ***
wenzelm
parents: 13245
diff changeset
   149
lemma AC15_WO6_aux1:
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   150
     "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 46822
diff changeset
   151
      ==> (\<Union>i<\<mu> x. HH(f,A,x)={A}. HH(f,A,i)) = A"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   152
apply (simp add: Ord_Least [THEN OUN_eq_UN])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   153
apply (rule equalityI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   154
apply (fast dest!: less_Least_subset_x)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   155
apply (blast del: subsetI 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   156
           intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   157
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   158
13535
007559e981c7 *** empty log message ***
wenzelm
parents: 13245
diff changeset
   159
lemma AC15_WO6_aux2:
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   160
     "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 46822
diff changeset
   161
      ==> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   162
apply (rule oallI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   163
apply (drule ltD [THEN less_Least_subset_x])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   164
apply (frule HH_subset_imp_eq)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   165
apply (erule ssubst)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   166
apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
   167
        (*but can't use del: DiffE despite the obvious conflict*)
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   168
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   169
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   170
theorem AC15_WO6: "AC15 ==> WO6"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   171
apply (unfold AC15_def WO6_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   172
apply (rule allI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   173
apply (erule_tac x = "Pow (A) -{0}" in allE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   174
apply (erule impE, fast)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   175
apply (elim bexE conjE exE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   176
apply (rule bexI)
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 12820
diff changeset
   177
 apply (rule conjI, assumption)
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 46822
diff changeset
   178
 apply (rule_tac x = "\<mu> i. HH (f,A,i) ={A}" in exI)
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 46822
diff changeset
   179
 apply (rule_tac x = "\<lambda>j \<in> (\<mu> i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 12820
diff changeset
   180
 apply (simp_all add: ltD)
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   181
apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
13535
007559e981c7 *** empty log message ***
wenzelm
parents: 13245
diff changeset
   182
            elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) 
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   183
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   184
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   185
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   186
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   187
(* The proof needed in the first case, not in the second                  *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   188
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   189
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   190
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   191
(* AC10(n) ==> AC13(n-1)  if 2\<le>n                                       *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   192
(*                                                                        *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   193
(* Because of the change to the formal definition of AC10(n) we prove     *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   194
(* the following obviously equivalent theorem \<in>                           *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   195
(* AC10(n) implies AC13(n) for (1\<le>n)                                   *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   196
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   197
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   198
theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   199
apply (unfold AC10_def AC13_def, safe)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   200
apply (erule allE) 
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12814
diff changeset
   201
apply (erule impE [OF _ cons_times_nat_not_Finite], assumption) 
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   202
apply (fast elim!: impE [OF _ cons_times_nat_not_Finite] 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   203
            dest!: ex_fun_AC13_AC15)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   204
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   205
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   206
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   207
(* The proofs needed in the second case, not in the first                 *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   208
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   209
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   210
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   211
(* AC1 ==> AC13(1)                                                        *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   212
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   213
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   214
lemma AC1_AC13: "AC1 ==> AC13(1)"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   215
apply (unfold AC1_def AC13_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   216
apply (rule allI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   217
apply (erule allE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   218
apply (rule impI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   219
apply (drule mp, assumption) 
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   220
apply (elim exE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   221
apply (rule_tac x = "\<lambda>x \<in> A. {f`x}" in exI)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   222
apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll])
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   223
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   224
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   225
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   226
(* AC13(m) ==> AC13(n) for m \<subseteq> n                                         *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   227
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   228
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   229
lemma AC13_mono: "[| m\<le>n; AC13(m) |] ==> AC13(n)"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   230
apply (unfold AC13_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   231
apply (drule le_imp_lepoll)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   232
apply (fast elim!: lepoll_trans)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   233
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   234
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   235
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   236
(* The proofs necessary for both cases                                    *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   237
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   238
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   239
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   240
(* AC13(n) ==> AC14  if 1 \<subseteq> n                                            *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   241
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   242
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   243
theorem AC13_AC14: "[| n \<in> nat; 1\<le>n; AC13(n) |] ==> AC14"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   244
by (unfold AC13_def AC14_def, auto)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   245
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   246
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   247
(* AC14 ==> AC15                                                          *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   248
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   249
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   250
theorem AC14_AC15: "AC14 ==> AC15"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   251
by (unfold AC13_def AC14_def AC15_def, fast)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   252
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   253
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   254
(* The redundant proofs; however cited by Rubin & Rubin                   *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   255
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   256
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   257
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   258
(* AC13(1) ==> AC1                                                        *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   259
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   260
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   261
lemma lemma_aux: "[| A\<noteq>0; A \<lesssim> 1 |] ==> \<exists>a. A={a}"
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   262
by (fast elim!: not_emptyE lepoll_1_is_sing)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   263
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   264
lemma AC13_AC1_lemma:
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   265
     "\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1   
61980
6b780867d426 clarified syntax;
wenzelm
parents: 61394
diff changeset
   266
      ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   267
apply (rule lam_type)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   268
apply (drule bspec, assumption)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   269
apply (elim conjE)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   270
apply (erule lemma_aux [THEN exE], assumption)
12814
paulson
parents: 12788
diff changeset
   271
apply (simp add: the_equality)
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   272
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   273
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   274
theorem AC13_AC1: "AC13(1) ==> AC1"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   275
apply (unfold AC13_def AC1_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   276
apply (fast elim!: AC13_AC1_lemma)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   277
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   278
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   279
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   280
(* AC11 ==> AC14                                                          *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   281
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   282
12788
6842f90972da made proofs more robust
paulson
parents: 12776
diff changeset
   283
theorem AC11_AC14: "AC11 ==> AC14"
12776
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   284
apply (unfold AC11_def AC14_def)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   285
apply (fast intro!: AC10_AC13)
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   286
done
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   287
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   288
end
249600a63ba9 Isar version of AC
paulson
parents: 1155
diff changeset
   289