1 (* Title: ZF/ex/listn |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Inductive definition of lists of n elements |
|
7 |
|
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
|
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
|
10 *) |
|
11 |
|
12 structure ListN = Inductive_Fun |
|
13 (val thy = ListFn.thy addconsts [(["listn"],"i=>i")] |
|
14 val rec_doms = [("listn", "nat*list(A)")] |
|
15 val sintrs = |
|
16 ["<0,Nil> : listn(A)", |
|
17 "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"] |
|
18 val monos = [] |
|
19 val con_defs = [] |
|
20 val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] |
|
21 val type_elims = [SigmaE2]); |
|
22 |
|
23 val listn_induct = standard |
|
24 (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp)); |
|
25 |
|
26 goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)"; |
|
27 by (etac List.induct 1); |
|
28 by (ALLGOALS (asm_simp_tac list_ss)); |
|
29 by (REPEAT (ares_tac ListN.intrs 1)); |
|
30 val list_into_listn = result(); |
|
31 |
|
32 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n"; |
|
33 by (rtac iffI 1); |
|
34 by (etac listn_induct 1); |
|
35 by (safe_tac (ZF_cs addSIs (list_typechecks @ |
|
36 [length_Nil, length_Cons, list_into_listn]))); |
|
37 val listn_iff = result(); |
|
38 |
|
39 goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}"; |
|
40 by (rtac equality_iffI 1); |
|
41 by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1); |
|
42 val listn_image_eq = result(); |
|
43 |
|
44 goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)"; |
|
45 by (rtac lfp_mono 1); |
|
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
|
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
|
48 val listn_mono = result(); |
|
49 |
|
50 goal ListN.thy |
|
51 "!!n l. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \ |
|
52 \ <n#+n', l@l'> : listn(A)"; |
|
53 by (etac listn_induct 1); |
|
54 by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs))); |
|
55 val listn_append = result(); |
|
56 |
|
57 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)" |
|
58 and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)"; |
|
59 |
|
60 val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)" |
|
61 and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)"; |
|