src/ZF/ex/LList.ML

-(*  Title: 	ZF/ex/LList.ML
+(*  Title:      ZF/ex/LList.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Codatatype definition of Lazy Lists
 *)
 

 qed "llist_mono";
 
 (** Closure of quniv(A) under llist -- why so complex?  Its a gfp... **)
 
 val quniv_cs = subset_cs addSIs [QPair_Int_Vset_subset_UN RS subset_trans, 
-				 QPair_subset_univ,
-				 empty_subsetI, one_in_quniv RS qunivD]
+                                 QPair_subset_univ,
+                                 empty_subsetI, one_in_quniv RS qunivD]
                  addIs  [Int_lower1 RS subset_trans]
-		 addSDs [qunivD]
+                 addSDs [qunivD]
                  addSEs [Ord_in_Ord];
 
 goal LList.thy
    "!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
 by (etac trans_induct 1);

 
 
 (*** Lazy List Equality: lleq ***)
 
 val lleq_cs = subset_cs
-	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+        addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
         addSEs [Ord_in_Ord, Pair_inject];
 
 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
 goal LList.thy
    "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";

 by (safe_tac lleq_cs);
 by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
 qed "lleq_Int_Vset_subset_lemma";
 
 bind_thm ("lleq_Int_Vset_subset",
-	(lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
+        (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp));
 
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
 val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
 by (rtac (prem RS converseI RS lleq.coinduct) 1);

 
 goalw LList.thy llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
 by (rtac bnd_monoI 1);
 by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
 by (REPEAT (ares_tac [subset_refl, A_subset_univ, 
-		      QInr_subset_univ, QPair_subset_univ] 1));
+                      QInr_subset_univ, QPair_subset_univ] 1));
 qed "lconst_fun_bnd_mono";
 
 (* lconst(a) = LCons(a,lconst(a)) *)
 bind_thm ("lconst",
     ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski));