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