0
|
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 |
(*Could be generated automatically; requires use of fsplitD*)
|
|
24 |
val listn_induct = standard
|
|
25 |
(fsplitI RSN
|
|
26 |
(2, fsplitI RSN
|
|
27 |
(3, (read_instantiate [("P", "fsplit(R)")] ListN.induct) RS fsplitD)));
|
|
28 |
|
|
29 |
val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)";
|
|
30 |
by (rtac (major RS List.induct) 1);
|
|
31 |
by (ALLGOALS (ASM_SIMP_TAC list_ss));
|
|
32 |
by (REPEAT (ares_tac ListN.intrs 1));
|
|
33 |
val list_into_listn = result();
|
|
34 |
|
|
35 |
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
|
|
36 |
by (rtac iffI 1);
|
|
37 |
by (etac listn_induct 1);
|
|
38 |
by (dtac fsplitD 2);
|
|
39 |
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [Pair_iff])));
|
|
40 |
by (fast_tac (ZF_cs addSIs [list_into_listn]) 1);
|
|
41 |
val listn_iff = result();
|
|
42 |
|
|
43 |
goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
|
|
44 |
by (rtac equality_iffI 1);
|
|
45 |
by (SIMP_TAC (list_ss addrews [listn_iff,separation,image_singleton_iff]) 1);
|
|
46 |
val listn_image_eq = result();
|
|
47 |
|