author | paulson |
Mon, 28 Dec 1998 16:54:01 +0100 | |
changeset 6046 | 2c8a8be36c94 |
parent 5618 | 721671c68324 |
child 6141 | a6922171b396 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/listn |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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 |
||
515 | 12 |
open ListN; |
0 | 13 |
|
5137 | 14 |
Goal "l:list(A) ==> <length(l),l> : listn(A)"; |
515 | 15 |
by (etac list.induct 1); |
2469 | 16 |
by (ALLGOALS Asm_simp_tac); |
515 | 17 |
by (REPEAT (ares_tac listn.intrs 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
515
diff
changeset
|
18 |
qed "list_into_listn"; |
0 | 19 |
|
5068 | 20 |
Goal "<n,l> : listn(A) <-> l:list(A) & length(l)=n"; |
0 | 21 |
by (rtac iffI 1); |
6046 | 22 |
by (blast_tac (claset() addIs [list_into_listn]) 2); |
1732 | 23 |
by (etac listn.induct 1); |
6046 | 24 |
by (ALLGOALS Asm_simp_tac); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
515
diff
changeset
|
25 |
qed "listn_iff"; |
0 | 26 |
|
5068 | 27 |
Goal "listn(A)``{n} = {l:list(A). length(l)=n}"; |
0 | 28 |
by (rtac equality_iffI 1); |
4091 | 29 |
by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
515
diff
changeset
|
30 |
qed "listn_image_eq"; |
0 | 31 |
|
5137 | 32 |
Goalw listn.defs "A<=B ==> listn(A) <= listn(B)"; |
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
33 |
by (rtac lfp_mono 1); |
515 | 34 |
by (REPEAT (rtac listn.bnd_mono 1)); |
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
35 |
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
515
diff
changeset
|
36 |
qed "listn_mono"; |
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
37 |
|
5268 | 38 |
Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)"; |
1732 | 39 |
by (etac listn.induct 1); |
4091 | 40 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs))); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
515
diff
changeset
|
41 |
qed "listn_append"; |
71
729fe026c5f3
sample datatype defs now use datatype_intrs, datatype_elims
lcp
parents:
56
diff
changeset
|
42 |
|
515 | 43 |
val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)" |
44 |
and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)"; |
|
85 | 45 |
|
515 | 46 |
val zero_listn_case = listn.mk_cases list.con_defs "<0,l> : listn(A)" |
47 |
and succ_listn_case = listn.mk_cases list.con_defs "<succ(i),l> : listn(A)"; |