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 Infinite-branching datatype definitions |
|
7 *) |
|
8 |
|
9 bind_thm ("fun_Limit_VfromE", |
|
10 [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS |
|
11 transfer (the_context ()) Limit_VfromE |
|
12 |> standard); |
|
13 |
|
14 Goal "[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] \ |
|
15 \ ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"; |
|
16 by (res_inst_tac [("x", "UN d:D. LEAST i. f`d : Vfrom(A,i)")] exI 1); |
|
17 by (rtac conjI 1); |
|
18 by (rtac le_UN_Ord_lt_csucc 2); |
|
19 by (rtac ballI 4 THEN |
|
20 etac fun_Limit_VfromE 4 THEN REPEAT_SOME assume_tac); |
|
21 by (fast_tac (claset() addEs [Least_le RS lt_trans1, ltE]) 2); |
|
22 by (rtac Pi_type 1); |
|
23 by (rename_tac "d" 2); |
|
24 by (etac fun_Limit_VfromE 2 THEN REPEAT_SOME assume_tac); |
|
25 by (subgoal_tac "f`d : Vfrom(A, LEAST i. f`d : Vfrom(A,i))" 1); |
|
26 by (fast_tac (claset() addEs [LeastI, ltE]) 2); |
|
27 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
|
28 by (assume_tac 1); |
|
29 qed "fun_Vcsucc_lemma"; |
|
30 |
|
31 Goal "[| D <= Vfrom(A,csucc(K)); |D| le K; InfCard(K) |] \ |
|
32 \ ==> EX j. D <= Vfrom(A,j) & j < csucc(K)"; |
|
33 by (asm_full_simp_tac (simpset() addsimps [subset_iff_id,fun_Vcsucc_lemma]) 1); |
|
34 qed "subset_Vcsucc"; |
|
35 |
|
36 (*Version for arbitrary index sets*) |
|
37 Goal "[| |D| le K; InfCard(K); D <= Vfrom(A,csucc(K)) |] ==> \ |
|
38 \ D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
39 by (safe_tac (claset() addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); |
|
40 by (resolve_tac [Vfrom RS ssubst] 1); |
|
41 by (dtac fun_is_rel 1); |
|
42 (*This level includes the function, and is below csucc(K)*) |
|
43 by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); |
|
44 by (eresolve_tac [subset_trans RS PowI] 2); |
|
45 by (fast_tac (claset() addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); |
|
46 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
|
47 Limit_has_succ, Un_least_lt] 1)); |
|
48 qed "fun_Vcsucc"; |
|
49 |
|
50 Goal "[| f: D -> Vfrom(A, csucc(K)); |D| le K; InfCard(K); \ |
|
51 \ D <= Vfrom(A,csucc(K)) |] \ |
|
52 \ ==> f: Vfrom(A,csucc(K))"; |
|
53 by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); |
|
54 qed "fun_in_Vcsucc"; |
|
55 |
|
56 (*Remove <= from the rule above*) |
|
57 bind_thm ("fun_in_Vcsucc'", subsetI RSN (4, fun_in_Vcsucc)); |
|
58 |
|
59 (** Version where K itself is the index set **) |
|
60 |
|
61 Goal "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
62 by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); |
|
63 by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, |
|
64 i_subset_Vfrom, |
|
65 lt_csucc RS leI RS le_imp_subset RS subset_trans] 1)); |
|
66 qed "Card_fun_Vcsucc"; |
|
67 |
|
68 Goal "[| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ |
|
69 \ |] ==> f: Vfrom(A,csucc(K))"; |
|
70 by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); |
|
71 qed "Card_fun_in_Vcsucc"; |
|
72 |
|
73 (*Proved explicitly, in theory InfDatatype, to allow the bind_thm calls below*) |
|
74 Goal "InfCard(K) ==> Limit(csucc(K))"; |
|
75 by (etac (InfCard_csucc RS InfCard_is_Limit) 1); |
|
76 qed "Limit_csucc"; |
|
77 |
|
78 bind_thm ("Pair_in_Vcsucc", Limit_csucc RSN (3, Pair_in_VLimit)); |
|
79 bind_thm ("Inl_in_Vcsucc", Limit_csucc RSN (2, Inl_in_VLimit)); |
|
80 bind_thm ("Inr_in_Vcsucc", Limit_csucc RSN (2, Inr_in_VLimit)); |
|
81 bind_thm ("zero_in_Vcsucc", Limit_csucc RS zero_in_VLimit); |
|
82 bind_thm ("nat_into_Vcsucc", Limit_csucc RSN (2, nat_into_VLimit)); |
|
83 |
|
84 (*For handling Cardinals of the form (nat Un |X|) *) |
|
85 |
|
86 bind_thm ("InfCard_nat_Un_cardinal", |
|
87 [InfCard_nat, Card_cardinal] MRS InfCard_Un); |
|
88 |
|
89 bind_thm ("le_nat_Un_cardinal", |
|
90 [Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le); |
|
91 |
|
92 bind_thm ("UN_upper_cardinal", |
|
93 UN_upper RS subset_imp_lepoll RS lepoll_imp_Card_le); |
|
94 |
|
95 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *) |
|
96 bind_thms ("inf_datatype_intrs", |
|
97 [InfCard_nat, InfCard_nat_Un_cardinal, |
|
98 Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, |
|
99 zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc, |
|
100 Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ Data_Arg.intrs); |
|