equal
deleted
inserted
replaced
1 (* Title: ZF/list.ML |
1 (* Title: ZF/List.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Datatype definition of Lists |
6 Datatype definition of Lists |
34 fun list_ind_tac a prems i = |
34 fun list_ind_tac a prems i = |
35 EVERY [res_inst_tac [("x",a)] List.induct i, |
35 EVERY [res_inst_tac [("x",a)] List.induct i, |
36 rename_last_tac a ["1"] (i+2), |
36 rename_last_tac a ["1"] (i+2), |
37 ares_tac prems i]; |
37 ares_tac prems i]; |
38 |
38 |
|
39 goal List.thy "list(A) = {0} + (A * list(A))"; |
|
40 by (rtac (List.unfold RS trans) 1); |
|
41 bws List.con_defs; |
|
42 by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs) |
|
43 addDs [List.dom_subset RS subsetD] |
|
44 addEs [A_into_univ]) 1); |
|
45 val list_unfold = result(); |
|
46 |
39 (** Lemmas to justify using "list" in other recursive type definitions **) |
47 (** Lemmas to justify using "list" in other recursive type definitions **) |
40 |
48 |
41 goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)"; |
49 goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)"; |
42 by (rtac lfp_mono 1); |
50 by (rtac lfp_mono 1); |
43 by (REPEAT (rtac List.bnd_mono 1)); |
51 by (REPEAT (rtac List.bnd_mono 1)); |
51 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
59 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, |
52 Pair_in_univ]) 1); |
60 Pair_in_univ]) 1); |
53 val list_univ = result(); |
61 val list_univ = result(); |
54 |
62 |
55 val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans); |
63 val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans); |
|
64 |
|
65 goal List.thy "!!l A B. [| l: list(A); A <= univ(B) |] ==> l: univ(B)"; |
|
66 by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1)); |
|
67 val list_into_univ = result(); |
56 |
68 |
57 val major::prems = goal List.thy |
69 val major::prems = goal List.thy |
58 "[| l: list(A); \ |
70 "[| l: list(A); \ |
59 \ c: C(Nil); \ |
71 \ c: C(Nil); \ |
60 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ |
72 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ |