src/ZF/InfDatatype.ML
changeset 801 316121afb5b5
parent 768 59c0a821e468
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
800:23f55b829ccb 801:316121afb5b5
     1 (*  Title: 	ZF/InfDatatype.ML
     1 (*  Title: 	ZF/InfDatatype.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Datatype Definitions involving function space and/or infinite-branching
     6 Infinite-branching datatype definitions
     7 *)
     7 *)
     8 
     8 
     9 (*** FINITE BRANCHING ***)
     9 val fun_Limit_VfromE =
    10 
    10    [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE 
    11 (** Closure under finite powerset **)
    11    |> standard;
    12 
       
    13 val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
       
    14 
       
    15 goal Fin_Univ_thy
       
    16    "!!i. [| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
       
    17 by (eresolve_tac [Fin_induct] 1);
       
    18 by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
       
    19 by (safe_tac ZF_cs);
       
    20 by (eresolve_tac [Limit_VfromE] 1);
       
    21 by (assume_tac 1);
       
    22 by (res_inst_tac [("x", "xa Un j")] exI 1);
       
    23 by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, 
       
    24 			   Un_least_lt]) 1);
       
    25 val Fin_Vfrom_lemma = result();
       
    26 
       
    27 goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
       
    28 by (rtac subsetI 1);
       
    29 by (dresolve_tac [Fin_Vfrom_lemma] 1);
       
    30 by (safe_tac ZF_cs);
       
    31 by (resolve_tac [Vfrom RS ssubst] 1);
       
    32 by (fast_tac (ZF_cs addSDs [ltD]) 1);
       
    33 val Fin_VLimit = result();
       
    34 
       
    35 val Fin_subset_VLimit = 
       
    36     [Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
       
    37 
       
    38 goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
       
    39 by (rtac (Limit_nat RS Fin_VLimit) 1);
       
    40 val Fin_univ = result();
       
    41 
       
    42 (** Closure under finite powers (functions from a fixed natural number) **)
       
    43 
       
    44 goal Fin_Univ_thy
       
    45     "!!i. [| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
       
    46 by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
       
    47 by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
       
    48 		      nat_subset_VLimit, subset_refl] 1));
       
    49 val nat_fun_VLimit = result();
       
    50 
       
    51 val nat_fun_subset_VLimit = 
       
    52     [Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
       
    53 
       
    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);
       
    56 val nat_fun_univ = result();
       
    57 
       
    58 
       
    59 (** Closure under finite function space **)
       
    60 
       
    61 (*General but seldom-used version; normally the domain is fixed*)
       
    62 goal Fin_Univ_thy
       
    63     "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)";
       
    64 by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1);
       
    65 by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1));
       
    66 val FiniteFun_VLimit1 = result();
       
    67 
       
    68 goalw Fin_Univ_thy [univ_def] "univ(A) -||> univ(A) <= univ(A)";
       
    69 by (rtac (Limit_nat RS FiniteFun_VLimit1) 1);
       
    70 val FiniteFun_univ1 = result();
       
    71 
       
    72 (*Version for a fixed domain*)
       
    73 goal Fin_Univ_thy
       
    74    "!!i.  [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)";
       
    75 by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1);
       
    76 by (eresolve_tac [FiniteFun_VLimit1] 1);
       
    77 val FiniteFun_VLimit = result();
       
    78 
       
    79 goalw Fin_Univ_thy [univ_def]
       
    80     "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)";
       
    81 by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1);
       
    82 val FiniteFun_univ = result();
       
    83 
       
    84 goal Fin_Univ_thy
       
    85     "!!W. [| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)";
       
    86 by (eresolve_tac [FiniteFun_univ RS subsetD] 1);
       
    87 by (assume_tac 1);
       
    88 val FiniteFun_in_univ = result();
       
    89 
       
    90 (*Remove <= from the rule above*)
       
    91 val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ);
       
    92 
       
    93 
       
    94 (*** INFINITE BRANCHING ***)
       
    95 
       
    96 val fun_Limit_VfromE = 
       
    97     [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
       
    98 	|> standard;
       
    99 
    12 
   100 goal InfDatatype.thy
    13 goal InfDatatype.thy
   101     "!!K. [| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
    14     "!!K. [| f: W -> Vfrom(A,csucc(K));  |W| le K;  InfCard(K)	\
   102 \         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
    15 \         |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
   103 by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
    16 by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
   160     "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
    73     "!!K. [| f: K -> Vfrom(A, csucc(K));  InfCard(K) \
   161 \         |] ==> f: Vfrom(A,csucc(K))";
    74 \         |] ==> f: Vfrom(A,csucc(K))";
   162 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
    75 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
   163 qed "Card_fun_in_Vcsucc";
    76 qed "Card_fun_in_Vcsucc";
   164 
    77 
   165 val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
    78 (*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*)
   166 val Inl_in_Vcsucc  = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
    79 qed_goal "Limit_csucc" InfDatatype.thy
   167 val Inr_in_Vcsucc  = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
    80     "!!K. InfCard(K) ==> Limit(csucc(K))"
   168 val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
    81   (fn _ => [etac (InfCard_csucc RS InfCard_is_Limit) 1]);
   169 val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
    82 
       
    83 bind_thm ("Pair_in_Vcsucc",  Limit_csucc RSN (3, Pair_in_VLimit));
       
    84 bind_thm ("Inl_in_Vcsucc",   Limit_csucc RSN (2, Inl_in_VLimit));
       
    85 bind_thm ("Inr_in_Vcsucc",   Limit_csucc RSN (2, Inr_in_VLimit));
       
    86 bind_thm ("zero_in_Vcsucc",  Limit_csucc RS zero_in_VLimit);
       
    87 bind_thm ("nat_into_Vcsucc", Limit_csucc RSN (2, nat_into_VLimit));
   170 
    88 
   171 (*For handling Cardinals of the form  (nat Un |X|) *)
    89 (*For handling Cardinals of the form  (nat Un |X|) *)
   172 
    90 
   173 val InfCard_nat_Un_cardinal = [InfCard_nat, Card_cardinal] MRS InfCard_Un
    91 bind_thm ("InfCard_nat_Un_cardinal",
   174                               |> standard;
    92 	  [InfCard_nat, Card_cardinal] MRS InfCard_Un);
   175 
    93 
   176 val le_nat_Un_cardinal = 
    94 bind_thm ("le_nat_Un_cardinal",
   177     [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le  |> standard;
    95 	  [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le);
   178 
    96 
   179 val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le 
    97 bind_thm ("UN_upper_cardinal",
   180                         |> standard;
    98 	  UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le);
   181 
    99 
   182 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   100 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   183 val inf_datatype_intrs =  
   101 val inf_datatype_intrs =  
   184     [InfCard_nat, InfCard_nat_Un_cardinal,
   102     [InfCard_nat, InfCard_nat_Un_cardinal,
   185      Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, 
   103      Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc,