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