src/ZF/AC/AC18_AC19.thy
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 76216 9fc34f76b4e8
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/AC/AC18_AC19.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
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
     4
The proof of AC1 \<Longrightarrow> AC18 \<Longrightarrow> AC19 \<Longrightarrow> AC1
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     5
*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     6
27678
85ea2be46c71 dropped locale (open)
haftmann
parents: 24893
diff changeset
     7
theory AC18_AC19
85ea2be46c71 dropped locale (open)
haftmann
parents: 24893
diff changeset
     8
imports AC_Equiv
85ea2be46c71 dropped locale (open)
haftmann
parents: 24893
diff changeset
     9
begin
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    10
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    11
definition
76215
a642599ffdea More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents: 76214
diff changeset
    12
  uu    :: "i \<Rightarrow> i" where
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    13
    "uu(a) \<equiv> {c \<union> {0}. c \<in> a}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    14
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    15
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    16
(* ********************************************************************** *)
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    17
(* AC1 \<Longrightarrow> AC18                                                           *)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    18
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    19
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    20
lemma PROD_subsets:
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    21
     "\<lbrakk>f \<in> (\<Prod>b \<in> {P(a). a \<in> A}. b);  \<forall>a \<in> A. P(a)<=Q(a)\<rbrakk>   
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    22
      \<Longrightarrow> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Prod>a \<in> A. Q(a))"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    23
by (rule lam_type, drule apply_type, auto)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    24
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    25
lemma lemma_AC18:
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    26
     "\<lbrakk>\<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X)); A \<noteq> 0\<rbrakk> 
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    27
      \<Longrightarrow> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> 
61980
6b780867d426 clarified syntax;
wenzelm
parents: 46822
diff changeset
    28
          (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    29
apply (rule subsetI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    30
apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    31
apply (erule impE, fast)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    32
apply (erule exE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    33
apply (rule UN_I)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    34
 apply (fast elim!: PROD_subsets)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    35
apply (simp, fast elim!: not_emptyE dest: apply_type [OF _ RepFunI])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    36
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    37
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    38
lemma AC1_AC18: "AC1 \<Longrightarrow> PROP AC18"
76216
9fc34f76b4e8 getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents: 76215
diff changeset
    39
  unfolding AC1_def
13421
8fcdf4a26468 simplified locale predicates;
wenzelm
parents: 13416
diff changeset
    40
apply (rule AC18.intro)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    41
apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    42
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    43
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    44
(* ********************************************************************** *)
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    45
(* AC18 \<Longrightarrow> AC19                                                          *)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    46
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    47
13416
5851987ab2e8 AC18: meta-level predicate via locale;
wenzelm
parents: 13339
diff changeset
    48
theorem (in AC18) AC19
76216
9fc34f76b4e8 getting rid of apply (unfold ...)
paulson <lp15@cam.ac.uk>
parents: 76215
diff changeset
    49
  unfolding AC19_def
13416
5851987ab2e8 AC18: meta-level predicate via locale;
wenzelm
parents: 13339
diff changeset
    50
apply (intro allI impI)
76215
a642599ffdea More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents: 76214
diff changeset
    51
apply (rule AC18 [of _ "\<lambda>x. x", THEN mp], blast)
13416
5851987ab2e8 AC18: meta-level predicate via locale;
wenzelm
parents: 13339
diff changeset
    52
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    53
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    54
(* ********************************************************************** *)
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    55
(* AC19 \<Longrightarrow> AC1                                                           *)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    56
(* ********************************************************************** *)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    57
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    58
lemma RepRep_conj: 
76214
0c18df79b1c8 more modernisation of syntax
paulson <lp15@cam.ac.uk>
parents: 76213
diff changeset
    59
        "\<lbrakk>A \<noteq> 0; 0 \<notin> A\<rbrakk> \<Longrightarrow> {uu(a). a \<in> A} \<noteq> 0 \<and> 0 \<notin> {uu(a). a \<in> A}"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    60
apply (unfold uu_def, auto) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    61
apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]])
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    62
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    63
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    64
lemma lemma1_1: "\<lbrakk>c \<in> a; x = c \<union> {0}; x \<notin> a\<rbrakk> \<Longrightarrow> x - {0} \<in> a"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    65
apply clarify 
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12776
diff changeset
    66
apply (rule subst_elem, assumption)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    67
apply (fast elim: notE subst_elem)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    68
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    69
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    70
lemma lemma1_2: 
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    71
        "\<lbrakk>f`(uu(a)) \<notin> a; f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B); a \<in> A\<rbrakk>   
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    72
                \<Longrightarrow> f`(uu(a))-{0} \<in> a"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    73
apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    74
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    75
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    76
lemma lemma1: "\<exists>f. f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B) \<Longrightarrow> \<exists>f. f \<in> (\<Prod>B \<in> A. B)"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    77
apply (erule exE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    78
apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})" 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    79
       in exI)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    80
apply (rule lam_type) 
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    81
apply (simp add: lemma1_2)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    82
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    83
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    84
lemma lemma2_1: "a\<noteq>0 \<Longrightarrow> 0 \<in> (\<Union>b \<in> uu(a). b)"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    85
by (unfold uu_def, auto)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    86
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    87
lemma lemma2: "\<lbrakk>A\<noteq>0; 0\<notin>A\<rbrakk> \<Longrightarrow> (\<Inter>x \<in> {uu(a). a \<in> A}. \<Union>b \<in> x. b) \<noteq> 0"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    88
apply (erule not_emptyE) 
13339
0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents: 12820
diff changeset
    89
apply (rule_tac a = 0 in not_emptyI)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    90
apply (fast intro!: lemma2_1)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    91
done
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    92
76213
e44d86131648 Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents: 61980
diff changeset
    93
lemma AC19_AC1: "AC19 \<Longrightarrow> AC1"
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    94
apply (unfold AC19_def AC1_def, clarify)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    95
apply (case_tac "A=0", force)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    96
apply (erule_tac x = "{uu (a) . a \<in> A}" in allE)
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    97
apply (erule impE)
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12776
diff changeset
    98
apply (erule RepRep_conj, assumption)
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
    99
apply (rule lemma1)
12820
02e2ff3e4d37 lexical tidying
paulson
parents: 12776
diff changeset
   100
apply (drule lemma2, assumption, auto) 
12776
249600a63ba9 Isar version of AC
paulson
parents: 11317
diff changeset
   101
done
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
   102
1203
a39bec971684 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1123
diff changeset
   103
end