src/ZF/ex/listn.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 279 7738aed3f84d
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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)";