author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 13615 | 449a70d88b38 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
13134 | 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 |
||
13356 | 8 |
header{*Infinite-Branching Datatype Definitions*} |
9 |
||
13134 | 10 |
theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC: |
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)" |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13356
diff
changeset
|
18 |
apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d : Vfrom (A,i) " in exI) |
13134 | 19 |
apply (rule conjI) |
20 |
apply (rule_tac [2] le_UN_Ord_lt_csucc) |
|
13269 | 21 |
apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) |
13134 | 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 |
|
13269 | 47 |
Un_least_lt) |
13134 | 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 |