author | blanchet |
Wed, 06 Nov 2013 22:50:12 +0100 | |
changeset 54284 | 0b53378080d9 |
parent 47071 | 2884ee1ffbf0 |
child 58871 | c399ae4b836f |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26056
diff
changeset
|
1 |
(* Title: ZF/InfDatatype.thy |
13134 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1994 University of Cambridge |
|
4 |
*) |
|
5 |
||
13356 | 6 |
header{*Infinite-Branching Datatype Definitions*} |
7 |
||
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
16417
diff
changeset
|
8 |
theory InfDatatype imports Datatype_ZF Univ Finite Cardinal_AC begin |
13134 | 9 |
|
46820 | 10 |
lemmas fun_Limit_VfromE = |
13134 | 11 |
Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]] |
12 |
||
13 |
lemma fun_Vcsucc_lemma: |
|
47071
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
14 |
assumes f: "f \<in> D -> Vfrom(A,csucc(K))" and DK: "|D| \<le> K" and ICK: "InfCard(K)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
15 |
shows "\<exists>j. f \<in> D -> Vfrom(A,j) & j < csucc(K)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
16 |
proof (rule exI, rule conjI) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
17 |
show "f \<in> D \<rightarrow> Vfrom(A, \<Union>z\<in>D. \<mu> i. f`z \<in> Vfrom (A,i))" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
18 |
proof (rule Pi_type [OF f]) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
19 |
fix d |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
20 |
assume d: "d \<in> D" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
21 |
show "f ` d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
22 |
proof (rule fun_Limit_VfromE [OF f d ICK]) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
23 |
fix x |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
24 |
assume "x < csucc(K)" "f ` d \<in> Vfrom(A, x)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
25 |
hence "f`d \<in> Vfrom(A, \<mu> i. f`d \<in> Vfrom (A,i))" using d |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
26 |
by (fast elim: LeastI ltE) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
27 |
also have "... \<subseteq> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
28 |
by (rule Vfrom_mono) (auto intro: d) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
29 |
finally show "f`d \<in> Vfrom(A, \<Union>z\<in>D. \<mu> i. f ` z \<in> Vfrom(A, i))" . |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
30 |
qed |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
31 |
qed |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
32 |
next |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
33 |
show "(\<Union>d\<in>D. \<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
34 |
proof (rule le_UN_Ord_lt_csucc [OF ICK DK]) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
35 |
fix d |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
36 |
assume d: "d \<in> D" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
37 |
show "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
38 |
proof (rule fun_Limit_VfromE [OF f d ICK]) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
39 |
fix x |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
40 |
assume "x < csucc(K)" "f ` d \<in> Vfrom(A, x)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
41 |
thus "(\<mu> i. f ` d \<in> Vfrom(A, i)) < csucc(K)" |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
42 |
by (blast intro: Least_le lt_trans1 lt_Ord) |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
43 |
qed |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
44 |
qed |
2884ee1ffbf0
More structured proofs for infinite cardinalities
paulson
parents:
46820
diff
changeset
|
45 |
qed |
13134 | 46 |
|
47 |
lemma subset_Vcsucc: |
|
46820 | 48 |
"[| D \<subseteq> Vfrom(A,csucc(K)); |D| \<le> K; InfCard(K) |] |
49 |
==> \<exists>j. D \<subseteq> Vfrom(A,j) & j < csucc(K)" |
|
13134 | 50 |
by (simp add: subset_iff_id fun_Vcsucc_lemma) |
51 |
||
52 |
(*Version for arbitrary index sets*) |
|
53 |
lemma fun_Vcsucc: |
|
46820 | 54 |
"[| |D| \<le> K; InfCard(K); D \<subseteq> Vfrom(A,csucc(K)) |] ==> |
55 |
D -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))" |
|
13134 | 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)*) |
|
46820 | 60 |
apply (rule_tac a1 = "succ (succ (j \<union> ja))" in UN_I [THEN UnI2]) |
13134 | 61 |
apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ |
46820 | 62 |
Un_least_lt) |
13134 | 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: |
|
46820 | 68 |
"[| f: D -> Vfrom(A, csucc(K)); |D| \<le> K; InfCard(K); |
69 |
D \<subseteq> Vfrom(A,csucc(K)) |] |
|
13134 | 70 |
==> f: Vfrom(A,csucc(K))" |
71 |
by (blast intro: fun_Vcsucc [THEN subsetD]) |
|
72 |
||
46820 | 73 |
text{*Remove @{text "\<subseteq>"} from the rule above*} |
13134 | 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: |
|
46820 | 79 |
"InfCard(K) ==> K -> Vfrom(A,csucc(K)) \<subseteq> Vfrom(A,csucc(K))" |
13134 | 80 |
apply (frule InfCard_is_Card [THEN Card_is_Ord]) |
81 |
apply (blast del: subsetI |
|
46820 | 82 |
intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom |
83 |
lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans]) |
|
13134 | 84 |
done |
85 |
||
86 |
lemma Card_fun_in_Vcsucc: |
|
87 |
"[| f: K -> Vfrom(A, csucc(K)); InfCard(K) |] ==> f: Vfrom(A,csucc(K))" |
|
46820 | 88 |
by (blast intro: Card_fun_Vcsucc [THEN subsetD]) |
13134 | 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 |
||
46820 | 99 |
(*For handling Cardinals of the form @{term"nat \<union> |X|"} *) |
13134 | 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 |
|
46820 | 111 |
Pair_in_univ Inl_in_univ Inr_in_univ |
13134 | 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 |
|
46820 | 117 |
Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc |
13134 | 118 |
zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc |
46820 | 119 |
Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I |
13134 | 120 |
|
121 |
end |
|
122 |