1 (* Title: ZF/ex/ListN |
1 (* Title: ZF/Induct/ListN |
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 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Inductive definition of lists of n elements |
6 Inductive definition of lists of n elements |
7 |
7 |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
10 *) |
10 *) |
11 |
11 |
12 ListN = Main + |
12 theory ListN = Main: |
13 |
13 |
14 consts listn ::i=>i |
14 consts listn :: "i=>i" |
15 inductive |
15 inductive |
16 domains "listn(A)" <= "nat*list(A)" |
16 domains "listn(A)" <= "nat*list(A)" |
17 intrs |
17 intros |
18 NilI "<0,Nil> \\<in> listn(A)" |
18 NilI: "<0,Nil> \<in> listn(A)" |
19 ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)" |
19 ConsI: "[| a \<in> A; <n,l> \<in> listn(A) |] ==> <succ(n), Cons(a,l)> \<in> listn(A)" |
20 type_intrs "nat_typechecks @ list.intrs" |
20 type_intros nat_typechecks list.intros |
|
21 |
|
22 |
|
23 lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)" |
|
24 by (erule list.induct, simp_all add: listn.intros) |
|
25 |
|
26 lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n" |
|
27 apply (rule iffI) |
|
28 apply (erule listn.induct) |
|
29 apply auto |
|
30 apply (blast intro: list_into_listn) |
|
31 done |
|
32 |
|
33 lemma listn_image_eq: "listn(A)``{n} = {l \<in> list(A). length(l)=n}" |
|
34 apply (rule equality_iffI) |
|
35 apply (simp (no_asm) add: listn_iff separation image_singleton_iff) |
|
36 done |
|
37 |
|
38 lemma listn_mono: "A \<subseteq> B ==> listn(A) \<subseteq> listn(B)" |
|
39 apply (unfold listn.defs ) |
|
40 apply (rule lfp_mono) |
|
41 apply (rule listn.bnd_mono)+ |
|
42 apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+ |
|
43 done |
|
44 |
|
45 lemma listn_append: |
|
46 "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)" |
|
47 apply (erule listn.induct) |
|
48 apply (frule listn.dom_subset [THEN subsetD]) |
|
49 apply (simp_all add: listn.intros) |
|
50 done |
|
51 |
|
52 inductive_cases Nil_listn_case: "<i,Nil> \<in> listn(A)" |
|
53 inductive_cases Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)" |
|
54 |
|
55 inductive_cases zero_listn_case: "<0,l> \<in> listn(A)" |
|
56 inductive_cases succ_listn_case: "<succ(i),l> \<in> listn(A)" |
21 |
57 |
22 end |
58 end |