src/ZF/InfDatatype.thy
author wenzelm
Tue Sep 01 22:32:58 2015 +0200 (2015-09-01)
changeset 61076 bdc1e2f0a86a
parent 60770 240563fbf41d
child 61798 27f3c10b0b50
permissions -rw-r--r--
eliminated \<Colon>;
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
wenzelm@60770
     6
section\<open>Infinite-Branching Datatype Definitions\<close>
paulson@13356
     7
krauss@26056
     8
theory InfDatatype imports Datatype_ZF Univ Finite Cardinal_AC begin
paulson@13134
     9
paulson@46820
    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@47071
    14
  assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)"
paulson@47071
    15
  shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)"
paulson@47071
    16
proof (rule exI, rule conjI)
paulson@47071
    17
  show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))"
paulson@47071
    18
    proof (rule Pi_type [OF f])
paulson@47071
    19
      fix d
paulson@47071
    20
      assume d: "d \<in> D"
paulson@47071
    21
      show "f ` d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))"
paulson@47071
    22
        proof (rule fun_Limit_VfromE [OF f d ICK]) 
paulson@47071
    23
          fix x
paulson@47071
    24
          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
paulson@47071
    25
          hence "f`d \<in> Vfrom(A, \<mu> i. f`d \<in> Vfrom (A,i))" using d
paulson@47071
    26
            by (fast elim: LeastI ltE)
paulson@47071
    27
          also have "... \<subseteq> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" 
paulson@47071
    28
            by (rule Vfrom_mono) (auto intro: d) 
paulson@47071
    29
          finally show "f`d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" .
paulson@47071
    30
        qed
paulson@47071
    31
    qed
paulson@47071
    32
next
paulson@47071
    33
  show "(\<Union>d\<in>D. \<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
paulson@47071
    34
    proof (rule le_UN_Ord_lt_csucc [OF ICK DK])
paulson@47071
    35
      fix d
paulson@47071
    36
      assume d: "d \<in> D"
paulson@47071
    37
      show "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
paulson@47071
    38
        proof (rule fun_Limit_VfromE [OF f d ICK]) 
paulson@47071
    39
          fix x
paulson@47071
    40
          assume "x < csucc(K)"  "f ` d \<in> Vfrom(A, x)"
paulson@47071
    41
          thus "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)"
paulson@47071
    42
            by (blast intro: Least_le lt_trans1 lt_Ord) 
paulson@47071
    43
        qed
paulson@47071
    44
    qed
paulson@47071
    45
qed
paulson@13134
    46
paulson@13134
    47
lemma subset_Vcsucc:
paulson@46820
    48
     "[| D \<subseteq> Vfrom(A,csucc(K));  |D| \<le> K;  InfCard(K) |]
paulson@46820
    49
      ==> \<exists>j. D \<subseteq> Vfrom(A,j) & j < csucc(K)"
paulson@13134
    50
by (simp add: subset_iff_id fun_Vcsucc_lemma)
paulson@13134
    51
paulson@13134
    52
(*Version for arbitrary index sets*)
paulson@13134
    53
lemma fun_Vcsucc:
paulson@46820
    54
     "[| |D| \<le> K;  InfCard(K);  D \<subseteq> Vfrom(A,csucc(K)) |] ==>
paulson@46820
    55
          D -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))"
paulson@13134
    56
apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc)
paulson@13134
    57
apply (rule Vfrom [THEN ssubst])
paulson@13134
    58
apply (drule fun_is_rel)
paulson@13134
    59
(*This level includes the function, and is below csucc(K)*)
paulson@46820
    60
apply (rule_tac a1 = "succ (succ (j \<union> ja))" in UN_I [THEN UnI2])
paulson@13134
    61
apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
paulson@46820
    62
                    Un_least_lt)
paulson@13134
    63
apply (erule subset_trans [THEN PowI])
paulson@13134
    64
apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
paulson@13134
    65
done
paulson@13134
    66
paulson@13134
    67
lemma fun_in_Vcsucc:
paulson@46820
    68
     "[| f: D -> Vfrom(A, csucc(K));  |D| \<le> K;  InfCard(K);
paulson@46820
    69
         D \<subseteq> Vfrom(A,csucc(K)) |]
paulson@13134
    70
       ==> f: Vfrom(A,csucc(K))"
paulson@13134
    71
by (blast intro: fun_Vcsucc [THEN subsetD])
paulson@13134
    72
wenzelm@60770
    73
text\<open>Remove @{text "\<subseteq>"} from the rule above\<close>
paulson@13134
    74
lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]
paulson@13134
    75
paulson@13134
    76
(** Version where K itself is the index set **)
paulson@13134
    77
paulson@13134
    78
lemma Card_fun_Vcsucc:
paulson@46820
    79
     "InfCard(K) ==> K -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))"
paulson@13134
    80
apply (frule InfCard_is_Card [THEN Card_is_Ord])
paulson@13134
    81
apply (blast del: subsetI
paulson@46820
    82
             intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom
paulson@46820
    83
                   lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans])
paulson@13134
    84
done
paulson@13134
    85
paulson@13134
    86
lemma Card_fun_in_Vcsucc:
paulson@13134
    87
     "[| f: K -> Vfrom(A, csucc(K));  InfCard(K) |] ==> f: Vfrom(A,csucc(K))"
paulson@46820
    88
by (blast intro: Card_fun_Vcsucc [THEN subsetD])
paulson@13134
    89
paulson@13134
    90
lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))"
paulson@13134
    91
by (erule InfCard_csucc [THEN InfCard_is_Limit])
paulson@13134
    92
paulson@13134
    93
lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc]
paulson@13134
    94
lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc]
paulson@13134
    95
lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc]
paulson@13134
    96
lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit]
paulson@13134
    97
lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc]
paulson@13134
    98
paulson@46820
    99
(*For handling Cardinals of the form  @{term"nat \<union> |X|"} *)
paulson@13134
   100
paulson@13134
   101
lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal]
paulson@13134
   102
paulson@13134
   103
lemmas le_nat_Un_cardinal =
paulson@13134
   104
     Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
paulson@13134
   105
paulson@13134
   106
lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
paulson@13134
   107
paulson@13134
   108
(*The new version of Data_Arg.intrs, declared in Datatype.ML*)
paulson@13134
   109
lemmas Data_Arg_intros =
paulson@13134
   110
       SigmaI InlI InrI
paulson@46820
   111
       Pair_in_univ Inl_in_univ Inr_in_univ
paulson@13134
   112
       zero_in_univ A_into_univ nat_into_univ UnCI
paulson@13134
   113
paulson@13134
   114
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
paulson@13134
   115
lemmas inf_datatype_intros =
paulson@13134
   116
     InfCard_nat InfCard_nat_Un_cardinal
paulson@46820
   117
     Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc
paulson@13134
   118
     zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc
paulson@46820
   119
     Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I
paulson@13134
   120
paulson@13134
   121
end
paulson@13134
   122