src/ZF/AC/HH.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:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/AC/HH.thy
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Krzysztof Grabczewski
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     3
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
     4
Some properties of the recursive definition of HH used in the proofs of
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     5
  AC17 ==> AC1
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     6
  AC1 ==> WO2
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     7
  AC15 ==> WO6
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     8
*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     9
27678
85ea2be46c71 dropped locale (open)
haftmann
parents: 24894
diff changeset
    10
theory HH
85ea2be46c71 dropped locale (open)
haftmann
parents: 24894
diff changeset
    11
imports AC_Equiv Hartog
85ea2be46c71 dropped locale (open)
haftmann
parents: 24894
diff changeset
    12
begin
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    13
24894
163c82d039cf modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition
163c82d039cf modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
  HH :: "[i, i, i] => i"  where
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    16
    "HH(f,x,a) == transrec(a, %b r. let z = x - (\<Union>c \<in> b. r`c)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    17
                                    in  if f`z \<in> Pow(z)-{0} then f`z else {x})"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    18
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
    19
subsection\<open>Lemmas useful in each of the three proofs\<close>
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    20
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    21
lemma HH_def_satisfies_eq:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    22
     "HH(f,x,a) = (let z = x - (\<Union>b \<in> a. HH(f,x,b))   
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    23
                   in  if f`z \<in> Pow(z)-{0} then f`z else {x})"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    24
by (rule HH_def [THEN def_transrec, THEN trans], simp)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    25
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    26
lemma HH_values: "HH(f,x,a) \<in> Pow(x)-{0} | HH(f,x,a)={x}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    27
apply (rule HH_def_satisfies_eq [THEN ssubst])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    28
apply (simp add: Let_def Diff_subset [THEN PowI], fast)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    29
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    30
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    31
lemma subset_imp_Diff_eq:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    32
     "B \<subseteq> A ==> X-(\<Union>a \<in> A. P(a)) = X-(\<Union>a \<in> A-B. P(a))-(\<Union>b \<in> B. P(b))"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    33
by fast
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    34
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    35
lemma Ord_DiffE: "[| c \<in> a-b; b<a |] ==> c=b | b<c & c<a"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    36
apply (erule ltE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    37
apply (drule Ord_linear [of _ c])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    38
apply (fast elim: Ord_in_Ord)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    39
apply (fast intro!: ltI intro: Ord_in_Ord)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    40
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    41
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14171
diff changeset
    42
lemma Diff_UN_eq_self: "(!!y. y\<in>A ==> P(y) = {x}) ==> x - (\<Union>y \<in> A. P(y)) = x" 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14171
diff changeset
    43
by (simp, fast elim!: mem_irrefl)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    44
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    45
lemma HH_eq: "x - (\<Union>b \<in> a. HH(f,x,b)) = x - (\<Union>b \<in> a1. HH(f,x,b))   
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    46
              ==> HH(f,x,a) = HH(f,x,a1)"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14171
diff changeset
    47
apply (subst HH_def_satisfies_eq [of _ _ a1]) 
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    48
apply (rule HH_def_satisfies_eq [THEN trans], simp) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    49
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    50
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    51
lemma HH_is_x_gt_too: "[| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    52
apply (rule_tac P = "b<a" in impE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    53
prefer 2 apply assumption+
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    54
apply (erule lt_Ord2 [THEN trans_induct])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    55
apply (rule impI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    56
apply (rule HH_eq [THEN trans])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    57
prefer 2 apply assumption+
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    58
apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst], 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    59
       assumption)
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 46954
diff changeset
    60
apply (rule_tac t = "%z. z-X" for X in subst_context)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    61
apply (rule Diff_UN_eq_self)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    62
apply (drule Ord_DiffE, assumption) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    63
apply (fast elim: ltE, auto) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    64
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    65
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    66
lemma HH_subset_x_lt_too:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    67
     "[| HH(f,x,a) \<in> Pow(x)-{0}; b<a |] ==> HH(f,x,b) \<in> Pow(x)-{0}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    68
apply (rule HH_values [THEN disjE], assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    69
apply (drule HH_is_x_gt_too, assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    70
apply (drule subst, assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    71
apply (fast elim!: mem_irrefl)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    72
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    73
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    74
lemma HH_subset_x_imp_subset_Diff_UN:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    75
    "HH(f,x,a) \<in> Pow(x)-{0} ==> HH(f,x,a) \<in> Pow(x - (\<Union>b \<in> a. HH(f,x,b)))-{0}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    76
apply (drule HH_def_satisfies_eq [THEN subst])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    77
apply (rule HH_def_satisfies_eq [THEN ssubst])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    78
apply (simp add: Let_def Diff_subset [THEN PowI])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    79
apply (drule split_if [THEN iffD1])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    80
apply (fast elim!: mem_irrefl)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    81
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    82
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    83
lemma HH_eq_arg_lt:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    84
     "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v) \<in> Pow(x)-{0}; v \<in> w |] ==> P"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    85
apply (frule_tac P = "%y. y \<in> Pow (x) -{0}" in subst, assumption)
13339
0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents: 12820
diff changeset
    86
apply (drule_tac a = w in HH_subset_x_imp_subset_Diff_UN)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    87
apply (drule subst_elem, assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    88
apply (fast intro!: singleton_iff [THEN iffD2] equals0I)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    89
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    90
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    91
lemma HH_eq_imp_arg_eq:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    92
  "[| HH(f,x,v)=HH(f,x,w); HH(f,x,w) \<in> Pow(x)-{0}; Ord(v); Ord(w) |] ==> v=w"
13339
0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents: 12820
diff changeset
    93
apply (rule_tac j = w in Ord_linear_lt)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    94
apply (simp_all (no_asm_simp))
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    95
 apply (drule subst_elem, assumption) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    96
 apply (blast dest: ltD HH_eq_arg_lt)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    97
apply (blast dest: HH_eq_arg_lt [OF sym] ltD) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    98
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    99
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   100
lemma HH_subset_x_imp_lepoll: 
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 45602
diff changeset
   101
     "[| HH(f, x, i) \<in> Pow(x)-{0}; Ord(i) |] ==> i \<lesssim> Pow(x)-{0}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   102
apply (unfold lepoll_def inj_def)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   103
apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   104
apply (simp (no_asm_simp))
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   105
apply (fast del: DiffE
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
   106
            elim!: HH_eq_imp_arg_eq Ord_in_Ord HH_subset_x_lt_too 
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   107
            intro!: lam_type ballI ltI intro: bexI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   108
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   109
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   110
lemma HH_Hartog_is_x: "HH(f, x, Hartog(Pow(x)-{0})) = {x}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   111
apply (rule HH_values [THEN disjE])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   112
prefer 2 apply assumption 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   113
apply (fast del: DiffE
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   114
            intro!: Ord_Hartog 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
   115
            dest!: HH_subset_x_imp_lepoll 
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   116
            elim!: Hartog_lepoll_selfE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   117
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   118
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   119
lemma HH_Least_eq_x: "HH(f, x, \<mu> i. HH(f, x, i) = {x}) = {x}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   120
by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   121
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   122
lemma less_Least_subset_x:
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   123
     "a \<in> (\<mu> i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> Pow(x)-{0}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   124
apply (rule HH_values [THEN disjE], assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   125
apply (rule less_LeastE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   126
apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   127
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   128
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   129
subsection\<open>Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\<close>
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   130
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   131
lemma lam_Least_HH_inj_Pow: 
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   132
        "(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   133
         \<in> inj(\<mu> i. HH(f,x,i)={x}, Pow(x)-{0})"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   134
apply (unfold inj_def, simp)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   135
apply (fast intro!: lam_type dest: less_Least_subset_x 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   136
            elim!: HH_eq_imp_arg_eq Ord_Least [THEN Ord_in_Ord])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   137
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   138
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   139
lemma lam_Least_HH_inj:
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   140
     "\<forall>a \<in> (\<mu> i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z}   
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   141
      ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   142
          \<in> inj(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   143
by (rule lam_Least_HH_inj_Pow [THEN inj_strengthen_type], simp)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   144
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   145
lemma lam_surj_sing: 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   146
        "[| x - (\<Union>a \<in> A. F(a)) = 0;  \<forall>a \<in> A. \<exists>z \<in> x. F(a) = {z} |]   
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   147
         ==> (\<lambda>a \<in> A. F(a)) \<in> surj(A, {{y}. y \<in> x})"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   148
apply (simp add: surj_def lam_type Diff_eq_0_iff)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   149
apply (blast elim: equalityE) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   150
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   151
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   152
lemma not_emptyI2: "y \<in> Pow(x)-{0} ==> x \<noteq> 0"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   153
by auto
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   154
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   155
lemma f_subset_imp_HH_subset:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   156
     "f`(x - (\<Union>j \<in> i. HH(f,x,j))) \<in> Pow(x - (\<Union>j \<in> i. HH(f,x,j)))-{0}   
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   157
      ==> HH(f, x, i) \<in> Pow(x) - {0}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   158
apply (rule HH_def_satisfies_eq [THEN ssubst])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   159
apply (simp add: Let_def Diff_subset [THEN PowI] not_emptyI2 [THEN if_P], fast)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   160
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   161
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   162
lemma f_subsets_imp_UN_HH_eq_x:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   163
     "\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   164
      ==> x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
59788
6f7b6adac439 prefer local fixes;
wenzelm
parents: 46954
diff changeset
   165
apply (case_tac "P \<in> {0}" for P, fast)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   166
apply (drule Diff_subset [THEN PowI, THEN DiffI])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   167
apply (drule bspec, assumption) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   168
apply (drule f_subset_imp_HH_subset) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   169
apply (blast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]] 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   170
             elim!: mem_irrefl)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   171
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   172
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   173
lemma HH_values2: "HH(f,x,i) = f`(x - (\<Union>j \<in> i. HH(f,x,j))) | HH(f,x,i)={x}"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   174
apply (rule HH_def_satisfies_eq [THEN ssubst])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   175
apply (simp add: Let_def Diff_subset [THEN PowI])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   176
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   177
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   178
lemma HH_subset_imp_eq:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   179
     "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (\<Union>j \<in> i. HH(f,x,j)))"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   180
apply (rule HH_values2 [THEN disjE], assumption)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   181
apply (fast elim!: equalityE mem_irrefl dest!: singleton_subsetD)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   182
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   183
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   184
lemma f_sing_imp_HH_sing:
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   185
     "[| f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x};   
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   186
         a \<in> (\<mu> i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> x. HH(f,x,a) = {z}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   187
apply (drule less_Least_subset_x)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   188
apply (frule HH_subset_imp_eq)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   189
apply (drule apply_type)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   190
apply (rule Diff_subset [THEN PowI, THEN DiffI])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   191
apply (fast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2], force) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   192
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   193
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   194
lemma f_sing_lam_bij: 
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   195
     "[| x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0;   
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   196
         f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x} |]   
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   197
      ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   198
          \<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   199
apply (unfold bij_def)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   200
apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   201
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   202
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   203
lemma lam_singI:
61980
6b780867d426 clarified syntax;
wenzelm
parents: 61394
diff changeset
   204
     "f \<in> (\<Prod>X \<in> Pow(x)-{0}. F(X))   
6b780867d426 clarified syntax;
wenzelm
parents: 61394
diff changeset
   205
      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Prod>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   206
by (fast del: DiffI DiffE
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 27678
diff changeset
   207
            intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   208
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   209
(*FIXME: both uses have the form ...[THEN bij_converse_bij], so 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   210
  simplification is needed!*)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   211
lemmas bij_Least_HH_x =  
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   212
    comp_bij [OF f_sing_lam_bij [OF _ lam_singI] 
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   213
              lam_sing_bij [THEN bij_converse_bij]]
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   214
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   215
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59788
diff changeset
   216
subsection\<open>The proof of AC1 ==> WO2\<close>
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   217
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   218
(*Establishing the existence of a bijection, namely
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   219
converse
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   220
 (converse(\<lambda>x\<in>x. {x}) O
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   221
  Lambda
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   222
   (\<mu> i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x},
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   223
    HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x)))
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   224
Perhaps it could be simplified. *)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   225
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   226
lemma bijection:
61980
6b780867d426 clarified syntax;
wenzelm
parents: 61394
diff changeset
   227
     "f \<in> (\<Prod>X \<in> Pow(x) - {0}. X) 
61394
6142b282b164 tuned syntax -- more symbols;
wenzelm
parents: 60770
diff changeset
   228
      ==> \<exists>g. g \<in> bij(x, \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   229
apply (rule exI) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   230
apply (rule bij_Least_HH_x [THEN bij_converse_bij])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   231
apply (rule f_subsets_imp_UN_HH_eq_x)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   232
apply (intro ballI apply_type) 
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12776
diff changeset
   233
apply (fast intro: lam_type apply_type del: DiffE, assumption) 
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   234
apply (fast intro: Pi_weaken_type)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   235
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   236
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   237
lemma AC1_WO2: "AC1 ==> WO2"
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   238
apply (unfold AC1_def WO2_def eqpoll_def)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   239
apply (intro allI) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   240
apply (drule_tac x = "Pow(A) - {0}" in spec) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   241
apply (blast dest: bijection)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   242
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   243
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   244
end
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   245