src/ZF/InfDatatype.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 26056 6a0801279f4c
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/InfDatatype.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Infinite-Branching Datatype Definitions*}
     9 
    10 theory InfDatatype imports Datatype Univ Finite Cardinal_AC begin
    11 
    12 lemmas fun_Limit_VfromE = 
    13     Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]
    14 
    15 lemma fun_Vcsucc_lemma:
    16      "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]   
    17       ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"
    18 apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d : Vfrom (A,i) " in exI)
    19 apply (rule conjI)
    20 apply (rule_tac [2] le_UN_Ord_lt_csucc) 
    21 apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) 
    22  prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
    23 apply (rule Pi_type)
    24 apply (rename_tac [2] d)
    25 apply (erule_tac [2] fun_Limit_VfromE, simp_all)
    26 apply (subgoal_tac "f`d : Vfrom (A, LEAST i. f`d : Vfrom (A,i))")
    27  apply (erule Vfrom_mono [OF subset_refl UN_upper, THEN subsetD])
    28  apply assumption
    29 apply (fast elim: LeastI ltE)
    30 done
    31 
    32 lemma subset_Vcsucc:
    33      "[| D <= Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]     
    34       ==> EX j. D <= Vfrom(A,j) & j < csucc(K)"
    35 by (simp add: subset_iff_id fun_Vcsucc_lemma)
    36 
    37 (*Version for arbitrary index sets*)
    38 lemma fun_Vcsucc:
    39      "[| |D| le K;  InfCard(K);  D <= Vfrom(A,csucc(K)) |] ==>  
    40           D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
    41 apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc)
    42 apply (rule Vfrom [THEN ssubst])
    43 apply (drule fun_is_rel)
    44 (*This level includes the function, and is below csucc(K)*)
    45 apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
    46 apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
    47                     Un_least_lt) 
    48 apply (erule subset_trans [THEN PowI])
    49 apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
    50 done
    51 
    52 lemma fun_in_Vcsucc:
    53      "[| f: D -> Vfrom(A, csucc(K));  |D| le K;  InfCard(K);         
    54          D <= Vfrom(A,csucc(K)) |]                                   
    55        ==> f: Vfrom(A,csucc(K))"
    56 by (blast intro: fun_Vcsucc [THEN subsetD])
    57 
    58 (*Remove <= from the rule above*)
    59 lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
    60 
    61 (** Version where K itself is the index set **)
    62 
    63 lemma Card_fun_Vcsucc:
    64      "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
    65 apply (frule InfCard_is_Card [THEN Card_is_Ord])
    66 apply (blast del: subsetI
    67 	     intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom 
    68                    lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans]) 
    69 done
    70 
    71 lemma Card_fun_in_Vcsucc:
    72      "[| f: K -> Vfrom(A, csucc(K));  InfCard(K) |] ==> f: Vfrom(A,csucc(K))"
    73 by (blast intro: Card_fun_Vcsucc [THEN subsetD]) 
    74 
    75 lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))"
    76 by (erule InfCard_csucc [THEN InfCard_is_Limit])
    77 
    78 lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc]
    79 lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc]
    80 lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc]
    81 lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit]
    82 lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc]
    83 
    84 (*For handling Cardinals of the form  (nat Un |X|) *)
    85 
    86 lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal]
    87 
    88 lemmas le_nat_Un_cardinal =
    89      Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
    90 
    91 lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
    92 
    93 (*The new version of Data_Arg.intrs, declared in Datatype.ML*)
    94 lemmas Data_Arg_intros =
    95        SigmaI InlI InrI
    96        Pair_in_univ Inl_in_univ Inr_in_univ 
    97        zero_in_univ A_into_univ nat_into_univ UnCI
    98 
    99 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
   100 lemmas inf_datatype_intros =
   101      InfCard_nat InfCard_nat_Un_cardinal
   102      Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc 
   103      zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc
   104      Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I 
   105 
   106 end
   107