src/ZF/ex/ListN.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
     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