src/ZF/AC/AC7_AC9.ML
changeset 9683 f87c8c449018
parent 5470 855654b691db
child 11151 4042eb2fde2f
equal deleted inserted replaced
9682:00f8be1b7209 9683:f87c8c449018
     7 *)
     7 *)
     8 
     8 
     9 (* ********************************************************************** *)
     9 (* ********************************************************************** *)
    10 (* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1                  *)
    10 (* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1                  *)
    11 (*  - Sigma_fun_space_not0                                                *)
    11 (*  - Sigma_fun_space_not0                                                *)
    12 (*  - all_eqpoll_imp_pair_eqpoll                                          *)
       
    13 (*  - Sigma_fun_space_eqpoll                                              *)
    12 (*  - Sigma_fun_space_eqpoll                                              *)
    14 (* ********************************************************************** *)
    13 (* ********************************************************************** *)
    15 
    14 
    16 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
    15 Goal "[| 0~:A; B:A |] ==> (nat->Union(A)) * B ~= 0";
    17 by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, 
    16 by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, 
    18 				Union_empty_iff RS iffD1]
    17 				Union_empty_iff RS iffD1]) 1);
    19                         addDs [fun_space_emptyD]) 1);
       
    20 qed "Sigma_fun_space_not0";
    18 qed "Sigma_fun_space_not0";
    21 
       
    22 Goal "(ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
       
    23 by (REPEAT (rtac ballI 1));
       
    24 by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
       
    25         THEN REPEAT (assume_tac 1));
       
    26 qed "all_eqpoll_imp_pair_eqpoll";
       
    27 
       
    28 Goal "[| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A |]  \
       
    29 \     ==> P(b)=R(b)";
       
    30 by Auto_tac;
       
    31 qed "if_eqE1";
       
    32 
       
    33 Goal "ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a))  \
       
    34 \       ==> ALL a:A. a~=b --> Q(a)=S(a)";
       
    35 by Auto_tac;
       
    36 qed "if_eqE2";
       
    37 
       
    38 Goal "[| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
       
    39 by (fast_tac (claset() addSIs [lamI] addEs [equalityE, lamE]) 1);
       
    40 qed "lam_eqE";
       
    41 
    19 
    42 Goalw [inj_def]
    20 Goalw [inj_def]
    43         "C:A ==> (lam g:(nat->Union(A))*C.  \
    21         "C:A ==> (lam g:(nat->Union(A))*C.  \
    44 \               (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1))))  \
    22 \               (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1))))  \
    45 \               : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
    23 \               : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
    99 val lemma2 = result();
    77 val lemma2 = result();
   100 
    78 
   101 Goalw AC_defs "AC7 ==> AC6";
    79 Goalw AC_defs "AC7 ==> AC6";
   102 by (rtac allI 1);
    80 by (rtac allI 1);
   103 by (rtac impI 1);
    81 by (rtac impI 1);
   104 by (excluded_middle_tac "A=0" 1);
    82 by (case_tac "A=0" 1);
   105 by (fast_tac (claset() addSIs [not_emptyI, empty_fun]) 2);
    83 by (Asm_simp_tac 1);
   106 by (rtac lemma1 1);
    84 by (rtac lemma1 1);
   107 by (etac allE 1);
    85 by (etac allE 1);
   108 by (etac impE 1 THEN (assume_tac 2));
    86 by (etac impE 1 THEN (assume_tac 2));
   109 by (fast_tac (claset() addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
    87 by (blast_tac (claset() addSIs [lemma2] 
   110 			       Sigma_fun_space_eqpoll]) 1);
    88                 addIs [eqpoll_sym, eqpoll_trans, Sigma_fun_space_eqpoll]) 1); 
   111 qed "AC7_AC6";
    89 qed "AC7_AC6";
   112 
    90 
   113 
    91 
   114 (* ********************************************************************** *)
    92 (* ********************************************************************** *)
   115 (* AC1 ==> AC8                                                            *)
    93 (* AC1 ==> AC8                                                            *)
   169 (* Rules nedded to prove lemma1 *)
   147 (* Rules nedded to prove lemma1 *)
   170 val snd_lepoll_SigmaI = prod_lepoll_self RS 
   148 val snd_lepoll_SigmaI = prod_lepoll_self RS 
   171         ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
   149         ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
   172 
   150 
   173 
   151 
   174 Goal "[| 0~:A; A~=0 |]  \
   152 Goal "[| 0~:A;  A~=0;  \
   175 \       ==> ALL B1: ({((nat->Union(A))*B)*nat. B:A}  \
   153 \        C = {((nat->Union(A))*B)*nat. B:A}  Un \
   176 \               Un {cons(0,((nat->Union(A))*B)*nat). B:A}).  \
   154 \            {cons(0,((nat->Union(A))*B)*nat). B:A}; \
   177 \       ALL B2: ({((nat->Union(A))*B)*nat. B:A}  \
   155 \        B1: C;  B2: C |]  \
   178 \               Un {cons(0,((nat->Union(A))*B)*nat). B:A}).  \
   156 \     ==> B1 eqpoll B2";
   179 \       B1 eqpoll B2";
   157 by (blast_tac (claset() addSIs [nat_cons_eqpoll RS eqpoll_trans]
   180 by (fast_tac (claset() addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
   158                 addDs [Sigma_fun_space_not0]
   181                         nat_cons_eqpoll RS eqpoll_trans]
   159                 addIs [eqpoll_trans, eqpoll_sym, snd_lepoll_SigmaI, 
   182                 addEs [Sigma_fun_space_not0 RS not_emptyE]
   160                        eqpoll_refl RSN (2, prod_eqpoll_cong), 
   183                 addIs [snd_lepoll_SigmaI, eqpoll_refl RSN 
   161                        Sigma_fun_space_eqpoll]) 1);
   184                         (2, prod_eqpoll_cong), Sigma_fun_space_eqpoll]) 1);
       
   185 val lemma1 = result();
   162 val lemma1 = result();
   186 
   163 
   187 Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}.  \
   164 Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}.  \
   188 \       ALL B2:{(F*B)*N. B:A}  \
   165 \       ALL B2:{(F*B)*N. B:A}  \
   189 \       Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2)  \
   166 \       Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2)  \
   198 
   175 
   199 Goalw AC_defs "AC9 ==> AC1";
   176 Goalw AC_defs "AC9 ==> AC1";
   200 by (rtac allI 1);
   177 by (rtac allI 1);
   201 by (rtac impI 1);
   178 by (rtac impI 1);
   202 by (etac allE 1);
   179 by (etac allE 1);
   203 by (excluded_middle_tac "A=0" 1);
   180 by (case_tac "A=0" 1);
   204 by (etac impE 1);
   181 by (blast_tac (claset() addDs [lemma1,lemma2]) 2); 
   205 by (rtac lemma1 1 THEN (REPEAT (assume_tac 1)));
   182 by Auto_tac;  
   206 by (fast_tac (claset() addSEs [lemma2]) 1);
       
   207 by (fast_tac (claset() addSIs [empty_fun]) 1);
       
   208 qed "AC9_AC1";
   183 qed "AC9_AC1";