12088
|
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 |
Goal "l \\<in> list(A) ==> <length(l),l> \\<in> listn(A)";
|
|
13 |
by (etac list.induct 1);
|
|
14 |
by (ALLGOALS Asm_simp_tac);
|
|
15 |
by (REPEAT (ares_tac listn.intrs 1));
|
|
16 |
qed "list_into_listn";
|
|
17 |
|
|
18 |
Goal "<n,l> \\<in> listn(A) <-> l \\<in> list(A) & length(l)=n";
|
|
19 |
by (rtac iffI 1);
|
|
20 |
by (blast_tac (claset() addIs [list_into_listn]) 2);
|
|
21 |
by (etac listn.induct 1);
|
|
22 |
by Auto_tac;
|
|
23 |
qed "listn_iff";
|
|
24 |
|
|
25 |
Goal "listn(A)``{n} = {l \\<in> list(A). length(l)=n}";
|
|
26 |
by (rtac equality_iffI 1);
|
|
27 |
by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1);
|
|
28 |
qed "listn_image_eq";
|
|
29 |
|
|
30 |
Goalw listn.defs "A \\<subseteq> B ==> listn(A) \\<subseteq> listn(B)";
|
|
31 |
by (rtac lfp_mono 1);
|
|
32 |
by (REPEAT (rtac listn.bnd_mono 1));
|
|
33 |
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
|
|
34 |
qed "listn_mono";
|
|
35 |
|
|
36 |
Goal "[| <n,l> \\<in> listn(A); <n',l'> \\<in> listn(A) |] ==> <n#+n', l@l'> \\<in> listn(A)";
|
|
37 |
by (etac listn.induct 1);
|
|
38 |
by (ftac (impOfSubs listn.dom_subset) 1);
|
|
39 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
|
|
40 |
qed "listn_append";
|
|
41 |
|
|
42 |
val Nil_listn_case = listn.mk_cases "<i,Nil> \\<in> listn(A)"
|
|
43 |
and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> \\<in> listn(A)";
|
|
44 |
|
|
45 |
val zero_listn_case = listn.mk_cases "<0,l> \\<in> listn(A)"
|
|
46 |
and succ_listn_case = listn.mk_cases "<succ(i),l> \\<in> listn(A)";
|