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