src/ZF/ex/LList.ML
changeset 173 85071e6ad295
parent 120 09287f26bfb8
child 279 7738aed3f84d
     1.1 --- a/src/ZF/ex/LList.ML	Tue Nov 30 11:07:57 1993 +0100
     1.2 +++ b/src/ZF/ex/LList.ML	Tue Nov 30 11:08:18 1993 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -CoDatatype definition of Lazy Lists
     1.8 +Codatatype definition of Lazy Lists
     1.9  *)
    1.10  
    1.11  structure LList = CoDatatype_Fun
    1.12 @@ -40,32 +40,29 @@
    1.13  
    1.14  (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
    1.15  
    1.16 -val in_quniv_rls =
    1.17 - [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv, 
    1.18 -  zero_Int_in_quniv, one_Int_in_quniv,
    1.19 -  QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
    1.20 +val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
    1.21 +				 QPair_subset_univ,
    1.22 +				 empty_subsetI, one_in_quniv RS qunivD]
    1.23 +                 addIs  [Int_lower1 RS subset_trans]
    1.24 +		 addSDs [qunivD]
    1.25 +                 addSEs [Ord_in_Ord];
    1.26  
    1.27 -val quniv_cs = ZF_cs addSIs in_quniv_rls 
    1.28 -                     addIs (Int_quniv_in_quniv::codatatype_intrs);
    1.29 -
    1.30 -(*Keep unfolding the lazy list until the induction hypothesis applies*)
    1.31  goal LList.thy
    1.32 -   "!!i. i : nat ==> 	\
    1.33 -\        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";
    1.34 -by (etac complete_induct 1);
    1.35 +   "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
    1.36 +by (etac trans_induct 1);
    1.37  by (rtac ballI 1);
    1.38  by (etac LList.elim 1);
    1.39  by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
    1.40 +(*LNil case*)
    1.41  by (fast_tac quniv_cs 1);
    1.42 -by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac);
    1.43 -by (fast_tac quniv_cs 1);
    1.44 -by (fast_tac quniv_cs 1);
    1.45 +(*LCons case*)
    1.46 +by (safe_tac quniv_cs);
    1.47 +by (ALLGOALS (fast_tac (quniv_cs addSEs [Ord_trans, make_elim bspec])));
    1.48  val llist_quniv_lemma = result();
    1.49  
    1.50  goal LList.thy "llist(quniv(A)) <= quniv(A)";
    1.51 -by (rtac subsetI 1);
    1.52 -by (rtac quniv_Int_Vfrom 1);
    1.53 -by (etac (LList.dom_subset RS subsetD) 1);
    1.54 +by (rtac (qunivI RS subsetI) 1);
    1.55 +by (rtac Int_Vset_subset 1);
    1.56  by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
    1.57  val llist_quniv = result();
    1.58