src/ZF/ex/LList.ML
author lcp
Tue Nov 30 11:08:18 1993 +0100 (1993-11-30)
changeset 173 85071e6ad295
parent 120 09287f26bfb8
child 279 7738aed3f84d
permissions -rw-r--r--
ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma,
ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN

ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and
QPair_Int_Vset_subset_UN

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