src/ZF/InfDatatype.ML
changeset 524 b1bf18e83302
parent 517 a9f93400f307
child 534 cd8bec47e175
equal deleted inserted replaced
523:972119df615e 524:b1bf18e83302
    53 
    53 
    54 goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
    54 goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)";
    55 by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
    55 by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1);
    56 val nat_fun_univ = result();
    56 val nat_fun_univ = result();
    57 
    57 
    58 val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
       
    59 
       
    60 goal Fin_Univ_thy
       
    61     "!!f. [| f: n -> B;  B <= univ(A);  n : nat |] ==> f : univ(A)";
       
    62 by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
       
    63 val nat_fun_into_univ = result();
       
    64 
       
    65 
    58 
    66 (*** Infinite branching ***)
    59 (*** Infinite branching ***)
    67 
    60 
    68 val fun_Limit_VfromE = 
    61 val fun_Limit_VfromE = 
    69     [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
    62     [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
   102 by (eresolve_tac [PiE] 1);
    95 by (eresolve_tac [PiE] 1);
   103 (*This level includes the function, and is below csucc(K)*)
    96 (*This level includes the function, and is below csucc(K)*)
   104 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
    97 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
   105 by (eresolve_tac [subset_trans RS PowI] 2);
    98 by (eresolve_tac [subset_trans RS PowI] 2);
   106 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2);
    99 by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2);
   107 
       
   108 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
   100 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, 
   109 		      Limit_has_succ, Un_least_lt] 1));
   101 		      Limit_has_succ, Un_least_lt] 1));
   110 val fun_Vcsucc = result();
   102 val fun_Vcsucc = result();
   111 
   103 
   112 goal InfDatatype.thy
   104 goal InfDatatype.thy
   114 \            W <= Vfrom(A,csucc(K)) 					\
   106 \            W <= Vfrom(A,csucc(K)) 					\
   115 \         |] ==> f: Vfrom(A,csucc(K))";
   107 \         |] ==> f: Vfrom(A,csucc(K))";
   116 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
   108 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
   117 val fun_in_Vcsucc = result();
   109 val fun_in_Vcsucc = result();
   118 
   110 
   119 goal InfDatatype.thy
   111 (*Remove <= from the rule above*)
   120     "!!K. [| W <= Vfrom(A,csucc(K));  B <= Vfrom(A,csucc(K));	\
   112 val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc);
   121 \            |W| le K;  InfCard(K)				\
       
   122 \         |] ==> W -> B <= Vfrom(A, csucc(K))";
       
   123 by (REPEAT (ares_tac [[Pi_mono, fun_Vcsucc] MRS subset_trans] 1));
       
   124 val fun_subset_Vcsucc = result();
       
   125 
   113 
   126 goal InfDatatype.thy
   114 (** Version where K itself is the index set **)
   127     "!!f. [| f: W -> B;  W <= Vfrom(A,csucc(K));  B <= Vfrom(A,csucc(K)); \
       
   128 \            |W| le K;  InfCard(K) 					  \
       
   129 \         |] ==> f: Vfrom(A,csucc(K))";
       
   130 by (DEPTH_SOLVE (ares_tac [fun_subset_Vcsucc RS subsetD] 1));
       
   131 val fun_into_Vcsucc = result();
       
   132 
   115 
   133 (*Version where K itself is the index set*)
       
   134 goal InfDatatype.thy
   116 goal InfDatatype.thy
   135     "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
   117     "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
   136 by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   118 by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
   137 by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
   119 by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
   138 		      i_subset_Vfrom,
   120 		      i_subset_Vfrom,
   143     "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
   125     "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
   144 \         |] ==> f: Vfrom(A,csucc(K))";
   126 \         |] ==> f: Vfrom(A,csucc(K))";
   145 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
   127 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
   146 val Card_fun_in_Vcsucc = result();
   128 val Card_fun_in_Vcsucc = result();
   147 
   129 
   148 val Card_fun_subset_Vcsucc = 
       
   149 	[Pi_mono, Card_fun_Vcsucc] MRS subset_trans |> standard;
       
   150 
       
   151 goal InfDatatype.thy
       
   152     "!!f. [| f: K -> B;  B <= Vfrom(A,csucc(K));  InfCard(K) \
       
   153 \         |] ==> f: Vfrom(A,csucc(K))";
       
   154 by (REPEAT (ares_tac [Card_fun_subset_Vcsucc RS subsetD] 1));
       
   155 val Card_fun_into_Vcsucc = result();
       
   156 
       
   157 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
   130 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
   158 val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
   131 val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
   159 val Inr_in_Vcsucc  = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
   132 val Inr_in_Vcsucc  = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
   160 val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
   133 val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
   161 val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
   134 val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
   162 
   135 
       
   136 (*For handling Cardinals of the form  (nat Un |X|) *)
       
   137 
       
   138 val InfCard_nat_Un_cardinal = [InfCard_nat, Card_cardinal] MRS InfCard_Un
       
   139                               |> standard;
       
   140 
       
   141 val le_nat_Un_cardinal = 
       
   142     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
       
   143 
       
   144 val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le 
       
   145                         |> standard;
       
   146 
   163 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   147 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   164 val inf_datatype_intrs =  
   148 val inf_datatype_intrs =  
   165     [Card_fun_in_Vcsucc, fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc, 
   149     [InfCard_nat, InfCard_nat_Un_cardinal,
   166      Inl_in_Vcsucc, Inr_in_Vcsucc, 
   150      Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
   167      zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs;
   151      zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc,
   168 
   152      Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs;