|
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 val fun_Limit_VfromE = |
|
10 [apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE |
|
11 |> standard; |
|
12 |
|
13 goal InfDatatype.thy |
|
14 "!!K. [| f: K -> Vfrom(A,csucc(K)); InfCard(K) \ |
|
15 \ |] ==> EX j. f: K -> Vfrom(A,j) & j < csucc(K)"; |
|
16 by (res_inst_tac [("x", "UN k:K. LEAST i. f`k : Vfrom(A,i)")] exI 1); |
|
17 by (resolve_tac [conjI] 1); |
|
18 by (resolve_tac [ballI RSN (2,cardinal_UN_Ord_lt_csucc)] 2); |
|
19 by (eresolve_tac [fun_Limit_VfromE] 3 THEN REPEAT_SOME assume_tac); |
|
20 by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); |
|
21 by (resolve_tac [Pi_type] 1); |
|
22 by (rename_tac "k" 2); |
|
23 by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); |
|
24 by (subgoal_tac "f`k : Vfrom(A, LEAST i. f`k : Vfrom(A,i))" 1); |
|
25 by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); |
|
26 by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
|
27 by (assume_tac 1); |
|
28 val fun_Vfrom_csucc_lemma = result(); |
|
29 |
|
30 goal InfDatatype.thy |
|
31 "!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
32 by (safe_tac (ZF_cs addSDs [fun_Vfrom_csucc_lemma])); |
|
33 by (resolve_tac [Vfrom RS ssubst] 1); |
|
34 by (eresolve_tac [PiE] 1); |
|
35 (*This level includes the function, and is below csucc(K)*) |
|
36 by (res_inst_tac [("a1", "succ(succ(K Un j))")] (UN_I RS UnI2) 1); |
|
37 by (eresolve_tac [subset_trans RS PowI] 2); |
|
38 by (safe_tac (ZF_cs addSIs [Pair_in_Vfrom])); |
|
39 by (fast_tac (ZF_cs addIs [i_subset_Vfrom RS subsetD]) 2); |
|
40 by (eresolve_tac [[subset_refl, Un_upper2] MRS Vfrom_mono RS subsetD] 2); |
|
41 by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
|
42 Limit_has_succ, Un_least_lt] 1)); |
|
43 by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS lt_csucc] 1); |
|
44 by (assume_tac 1); |
|
45 val fun_Vfrom_csucc = result(); |
|
46 |
|
47 goal InfDatatype.thy |
|
48 "!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ |
|
49 \ |] ==> f: Vfrom(A,csucc(K))"; |
|
50 by (REPEAT (ares_tac [fun_Vfrom_csucc RS subsetD] 1)); |
|
51 val fun_in_Vfrom_csucc = result(); |
|
52 |
|
53 val fun_subset_Vfrom_csucc = |
|
54 [Pi_mono, fun_Vfrom_csucc] MRS subset_trans |> standard; |
|
55 |
|
56 goal InfDatatype.thy |
|
57 "!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \ |
|
58 \ |] ==> f: Vfrom(A,csucc(K))"; |
|
59 by (REPEAT (ares_tac [fun_subset_Vfrom_csucc RS subsetD] 1)); |
|
60 val fun_into_Vfrom_csucc = result(); |
|
61 |
|
62 val Limit_csucc = InfCard_csucc RS InfCard_is_Limit |> standard; |
|
63 |
|
64 val Pair_in_Vfrom_csucc = Limit_csucc RSN (3, Pair_in_Vfrom_Limit) |> standard; |
|
65 val Inl_in_Vfrom_csucc = Limit_csucc RSN (2, Inl_in_Vfrom_Limit) |> standard; |
|
66 val Inr_in_Vfrom_csucc = Limit_csucc RSN (2, Inr_in_Vfrom_Limit) |> standard; |
|
67 val zero_in_Vfrom_csucc = Limit_csucc RS zero_in_Vfrom_Limit |> standard; |
|
68 val nat_into_Vfrom_csucc = Limit_csucc RSN (2, nat_into_Vfrom_Limit) |
|
69 |> standard; |
|
70 |
|
71 (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *) |
|
72 val inf_datatype_intrs = |
|
73 [fun_in_Vfrom_csucc, InfCard_nat, Pair_in_Vfrom_csucc, |
|
74 Inl_in_Vfrom_csucc, Inr_in_Vfrom_csucc, |
|
75 zero_in_Vfrom_csucc, A_into_Vfrom, nat_into_Vfrom_csucc] @ datatype_intrs; |
|
76 |