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
clasohm@0
     1
(*  Title: 	ZF/ex/listn
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Inductive definition of lists of n elements
clasohm@0
     7
clasohm@0
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
clasohm@0
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
structure ListN = Inductive_Fun
lcp@279
    13
 (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
lcp@279
    14
  val rec_doms   = [("listn", "nat*list(A)")]
lcp@279
    15
  val sintrs     = 
lcp@279
    16
          ["<0,Nil> : listn(A)",
lcp@279
    17
           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
lcp@279
    18
  val monos      = []
lcp@279
    19
  val con_defs   = []
lcp@279
    20
  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
clasohm@0
    21
  val type_elims = [SigmaE2]);
clasohm@0
    22
lcp@7
    23
val listn_induct = standard 
lcp@7
    24
    (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
clasohm@0
    25
lcp@71
    26
goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
lcp@71
    27
by (etac List.induct 1);
lcp@7
    28
by (ALLGOALS (asm_simp_tac list_ss));
clasohm@0
    29
by (REPEAT (ares_tac ListN.intrs 1));
clasohm@0
    30
val list_into_listn = result();
clasohm@0
    31
clasohm@0
    32
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
clasohm@0
    33
by (rtac iffI 1);
clasohm@0
    34
by (etac listn_induct 1);
lcp@7
    35
by (safe_tac (ZF_cs addSIs (list_typechecks @
lcp@7
    36
			    [length_Nil, length_Cons, list_into_listn])));
clasohm@0
    37
val listn_iff = result();
clasohm@0
    38
clasohm@0
    39
goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}";
clasohm@0
    40
by (rtac equality_iffI 1);
lcp@7
    41
by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
clasohm@0
    42
val listn_image_eq = result();
clasohm@0
    43
lcp@16
    44
goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
lcp@16
    45
by (rtac lfp_mono 1);
lcp@16
    46
by (REPEAT (rtac ListN.bnd_mono 1));
lcp@16
    47
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
lcp@16
    48
val listn_mono = result();
lcp@16
    49
lcp@71
    50
goal ListN.thy
lcp@71
    51
    "!!n l. [| <n,l> : listn(A);  <n',l'> : listn(A) |] ==> \
lcp@71
    52
\           <n#+n', l@l'> : listn(A)";
lcp@71
    53
by (etac listn_induct 1);
lcp@71
    54
by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs)));
lcp@71
    55
val listn_append = result();
lcp@71
    56
lcp@56
    57
val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
lcp@85
    58
and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
lcp@85
    59
lcp@85
    60
val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
lcp@85
    61
and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";