src/ZF/ex/llist.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/llist.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Codatatype definition of Lazy Lists
     7 *)
     8 
     9 structure LList = CoDatatype_Fun
    10  (val thy        = QUniv.thy
    11   val rec_specs  = [("llist", "quniv(A)",
    12                       [(["LNil"],   "i"), 
    13                        (["LCons"],  "[i,i]=>i")])]
    14   val rec_styp   = "i=>i"
    15   val ext        = None
    16   val sintrs     = ["LNil : llist(A)",
    17                     "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
    18   val monos      = []
    19   val type_intrs = codatatype_intrs
    20   val type_elims = codatatype_elims);
    21 
    22 val [LNilI, LConsI] = LList.intrs;
    23 
    24 (*An elimination rule, for type-checking*)
    25 val LConsE = LList.mk_cases LList.con_defs "LCons(a,l) : llist(A)";
    26 
    27 (*Proving freeness results*)
    28 val LCons_iff      = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
    29 val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)";
    30 
    31 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
    32 
    33 goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
    34 by (rtac gfp_mono 1);
    35 by (REPEAT (rtac LList.bnd_mono 1));
    36 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
    37 val llist_mono = result();
    38 
    39 (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
    40 
    41 val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
    42 				 QPair_subset_univ,
    43 				 empty_subsetI, one_in_quniv RS qunivD]
    44                  addIs  [Int_lower1 RS subset_trans]
    45 		 addSDs [qunivD]
    46                  addSEs [Ord_in_Ord];
    47 
    48 goal LList.thy
    49    "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    50 by (etac trans_induct 1);
    51 by (rtac ballI 1);
    52 by (etac LList.elim 1);
    53 by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    54 (*LNil case*)
    55 by (fast_tac quniv_cs 1);
    56 (*LCons case*)
    57 by (safe_tac quniv_cs);
    58 by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
    59 val llist_quniv_lemma = result();
    60 
    61 goal LList.thy "llist(quniv(A)) <= quniv(A)";
    62 by (rtac (qunivI RS subsetI) 1);
    63 by (rtac Int_Vset_subset 1);
    64 by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    65 val llist_quniv = result();
    66 
    67 val llist_subset_quniv = standard
    68     (llist_mono RS (llist_quniv RSN (2,subset_trans)));
    69 
    70 (* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
    71    automatic association between theory name and filename. *)