# HG changeset patch
# User lcp
# Date 753370885 -3600
# Node ID 09287f26bfb8bc5105ef0e52475a10082b7436b5
# Parent  0e58da397b1d3a76119e10341b09cb9727b8b3b1
changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs

diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/Datatype.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,8 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
-
+(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
 *)
 
 
@@ -29,15 +28,15 @@
 end;
 
 
-(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
-functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
-         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
+(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
+functor CoDatatype_Fun (Const: CONSTRUCTOR) 
+         : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
 struct
 structure Constructor = Constructor_Fun (structure Const=Const and 
   		                      Pr=Quine_Prod and Su=Quine_Sum);
 open Const Constructor;
 
-structure Co_Inductive = Co_Inductive_Fun
+structure CoInductive = CoInductive_Fun
         (val thy = con_thy;
 	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
 	 val sintrs = sintrs;
@@ -46,7 +45,7 @@
 	 val type_intrs = type_intrs;
 	 val type_elims = type_elims);
 
-open Co_Inductive
+open CoInductive
 end;
 
 
@@ -60,11 +59,11 @@
 (*Needed for mutual recursion*)
 val datatype_elims = [make_elim InlD, make_elim InrD];
 
-(*For most co-datatypes involving quniv*)
-val co_datatype_intrs = 
+(*For most codatatypes involving quniv*)
+val codatatype_intrs = 
     [QSigmaI, QInlI, QInrI,
      QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
      zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
+val codatatype_elims = [make_elim QInlD, make_elim QInrD];
 
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/Nat.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -36,7 +36,8 @@
 val nat_1I = result();
 
 goal Nat.thy "bool <= nat";
-by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
+by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
+	    ORELSE eresolve_tac [boolE,ssubst] 1));
 val bool_subset_nat = result();
 
 val bool_into_nat = bool_subset_nat RS subsetD;
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/QPair.thy	Mon Nov 15 14:41:25 1993 +0100
@@ -31,12 +31,12 @@
 
 rules
   QPair_def       "<a;b> == a+b"
-  qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
+  qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
   qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
   qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
   QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
 
-  qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
+  qsum_def        "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
   QInl_def        "QInl(a)      == <0;a>"
   QInr_def        "QInr(b)      == <1;b>"
   qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/QUniv.ML
--- a/src/ZF/QUniv.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/QUniv.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -290,7 +290,7 @@
 val QPair_Int_Vfrom_in_quniv = result();
 
 
-(**** "Take-lemma" rules for proving a=b by co-induction ****)
+(**** "Take-lemma" rules for proving a=b by coinduction ****)
 
 (** Unfortunately, the technique used above does not apply here, since
     the base case appears impossible to prove: it involves an intersection
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -46,7 +46,7 @@
 use     "mono.ML";
 use_thy "fixedpt";
 
-(*Inductive/co-inductive definitions*)
+(*Inductive/coinductive definitions*)
 use     "ind_syntax.ML";
 use     "intr_elim.ML";
 use     "indrule.ML";
@@ -61,7 +61,7 @@
 use_thy "epsilon";
 use_thy "arith";
 
-(*Datatype/co-datatype definitions*)
+(*Datatype/codatatype definitions*)
 use_thy "univ";
 use_thy "quniv";
 use     "constructor.ML";
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ZF.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -270,7 +270,7 @@
     "!!a A. a : A ==> f(a) : {f(x). x:A}"
  (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
 
-(*Useful for co-induction proofs*)
+(*Useful for coinduction proofs*)
 val RepFun_eqI = prove_goal ZF.thy
     "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
  (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/coinductive.ML
--- a/src/ZF/coinductive.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/coinductive.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -1,9 +1,9 @@
-(*  Title: 	ZF/co-inductive.ML
+(*  Title: 	ZF/coinductive.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Co-inductive Definitions for Zermelo-Fraenkel Set Theory
+Coinductive Definitions for Zermelo-Fraenkel Set Theory
 
 Uses greatest fixedpoints with Quine-inspired products and sums
 
@@ -48,20 +48,20 @@
   val distinct' = QInr_QInl_iff
   end;
 
-signature CO_INDRULE =
+signature COINDRULE =
   sig
-  val co_induct : thm
+  val coinduct : thm
   end;
 
 
-functor Co_Inductive_Fun (Ind: INDUCTIVE) 
-          : sig include INTR_ELIM CO_INDRULE end =
+functor CoInductive_Fun (Ind: INDUCTIVE) 
+          : sig include INTR_ELIM COINDRULE end =
 struct
 structure Intr_elim = 
     Intr_elim_Fun(structure Ind=Ind and Fp=Gfp and 
 		  Pr=Quine_Prod and Su=Quine_Sum);
 
 open Intr_elim 
-val co_induct = raw_induct
+val coinduct = raw_induct
 end;
 
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/datatype.ML
--- a/src/ZF/datatype.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/datatype.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,8 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
-
+(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
 *)
 
 
@@ -29,15 +28,15 @@
 end;
 
 
-(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
-functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
-         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
+(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
+functor CoDatatype_Fun (Const: CONSTRUCTOR) 
+         : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
 struct
 structure Constructor = Constructor_Fun (structure Const=Const and 
   		                      Pr=Quine_Prod and Su=Quine_Sum);
 open Const Constructor;
 
-structure Co_Inductive = Co_Inductive_Fun
+structure CoInductive = CoInductive_Fun
         (val thy = con_thy;
 	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
 	 val sintrs = sintrs;
@@ -46,7 +45,7 @@
 	 val type_intrs = type_intrs;
 	 val type_elims = type_elims);
 
-open Co_Inductive
+open CoInductive
 end;
 
 
@@ -60,11 +59,11 @@
 (*Needed for mutual recursion*)
 val datatype_elims = [make_elim InlD, make_elim InrD];
 
-(*For most co-datatypes involving quniv*)
-val co_datatype_intrs = 
+(*For most codatatypes involving quniv*)
+val codatatype_intrs = 
     [QSigmaI, QInlI, QInrI,
      QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
      zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
+val codatatype_elims = [make_elim QInlD, make_elim QInrD];
 
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/BinFn.ML
--- a/src/ZF/ex/BinFn.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/BinFn.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -108,7 +108,7 @@
 val bin_ss = integ_ss 
     addsimps([bool_1I, bool_0I,
 	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
-	     bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
+	     bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
 
 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
                  [bool_subset_nat RS subsetD];
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/LList.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,10 +3,10 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Co-Datatype definition of Lazy Lists
+CoDatatype definition of Lazy Lists
 *)
 
-structure LList = Co_Datatype_Fun
+structure LList = CoDatatype_Fun
  (val thy = QUniv.thy;
   val rec_specs = 
       [("llist", "quniv(A)",
@@ -18,8 +18,8 @@
       ["LNil : llist(A)",
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
-  val type_intrs = co_datatype_intrs
-  val type_elims = co_datatype_elims);
+  val type_intrs = codatatype_intrs
+  val type_elims = codatatype_elims);
   
 val [LNilI, LConsI] = LList.intrs;
 
@@ -46,7 +46,7 @@
   QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
 
 val quniv_cs = ZF_cs addSIs in_quniv_rls 
-                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
+                     addIs (Int_quniv_in_quniv::codatatype_intrs);
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList.thy
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/LListFn.ML
--- a/src/ZF/ex/LListFn.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/LListFn.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -4,6 +4,8 @@
     Copyright   1993  University of Cambridge
 
 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
+
+Examples of coinduction for type-checking and to prove llist equations
 *)
 
 open LListFn;
@@ -31,7 +33,84 @@
 val lconst_in_quniv = result();
 
 goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
-by (rtac (singletonI RS LList.co_induct) 1);
+by (rtac (singletonI RS LList.coinduct) 1);
 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
 by (fast_tac (ZF_cs addSIs [lconst]) 1);
 val lconst_type = result();
+
+(*** flip --- equations merely assumed; certain consequences proved ***)
+
+val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
+
+goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
+be boolE 1;
+by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
+     ORELSE etac ssubst 1));
+val bool_Int_into_quniv = result();
+
+(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
+val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
+
+val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
+
+val flip_cs = 
+  ZF_cs addSIs [not_type,
+		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
+		zero_in_quniv, Int_Vset_0_subset RS qunivI,
+		Transset_0,
+		zero_Int_in_quniv, one_Int_in_quniv,
+		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
+        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
+
+(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
+  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
+goal LListFn.thy
+   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
+by (etac trans_induct 1);
+by (safe_tac ZF_cs);
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 2);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+by (fast_tac flip_cs 1);
+by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
+(*0 case*)
+by (fast_tac flip_cs 1);
+(*succ(j) case*)
+by (fast_tac flip_cs 1);
+(*Limit(i) case*)
+by (etac (Limit_Vfrom_eq RS ssubst) 1);
+by (rtac (Int_UN_distrib RS ssubst) 1);
+by (rtac UN_in_quniv 1);
+by (fast_tac flip_cs 1);
+val flip_llist_quniv_lemma = result();
+
+goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
+br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
+by (REPEAT (assume_tac 1));
+val flip_in_quniv = result();
+
+val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
+by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
+       LList.coinduct 1);
+br (prem RS RepFunI) 1;
+by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
+be RepFunE 1;
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_type = result();
+
+val [prem] = goal LListFn.thy
+    "l : llist(bool) ==> flip(flip(l)) = l";
+by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
+       (LList_Eq.coinduct RS lleq_implies_equal) 1);
+br (prem RS RepFunI) 1;
+by (fast_tac (ZF_cs addSIs [flip_type]) 1);
+be RepFunE 1;
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_flip = result();
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/LListFn.thy
--- a/src/ZF/ex/LListFn.thy	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/LListFn.thy	Mon Nov 15 14:41:25 1993 +0100
@@ -4,13 +4,23 @@
     Copyright   1993  University of Cambridge
 
 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
+
+STILL NEEDS:
+co_recursion for defining lconst, flip, etc.
+a typing rule for it, based on some notion of "productivity..."
 *)
 
-LListFn = LList +
+LListFn = LList + LList_Eq +
 consts
   lconst   :: "i => i"
+  flip     :: "i => i"
 
 rules
   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
+  flip_LNil   "flip(LNil) = LNil"
+
+  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
+\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
+
 end
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/LList_Eq.ML
--- a/src/ZF/ex/LList_Eq.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/LList_Eq.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,25 +3,27 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Former part of llist.ML, contains definition and use of LList_Eq
-*)
+Equality for llist(A) as a greatest fixed point
+***)
 
-(*** Equality for llist(A) as a greatest fixed point ***)
+(*Previously used <*> in the domain and variant pairs as elements.  But
+  standard pairs work just as well.  To use variant pairs, must change prefix
+  a q/Q to the Sigma, Pair and converse rules.*)
 
-structure LList_Eq = Co_Inductive_Fun
+structure LList_Eq = CoInductive_Fun
  (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
+  val rec_doms = [("lleq", "llist(A) * llist(A)")];
   val sintrs = 
-      ["<LNil; LNil> : lleq(A)",
-       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
+      ["<LNil, LNil> : lleq(A)",
+       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
   val monos = [];
   val con_defs = [];
-  val type_intrs = LList.intrs@[QSigmaI];
-  val type_elims = [QSigmaE2]);
+  val type_intrs = LList.intrs@[SigmaI];
+  val type_elims = [SigmaE2]);
 
 (** Alternatives for above:
   val con_defs = LList.con_defs
-  val type_intrs = co_datatype_intrs
+  val type_intrs = codatatype_intrs
   val type_elims = [quniv_QPair_E]
 **)
 
@@ -34,11 +36,11 @@
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList_Eq.thy
-   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
+   "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
 by (etac trans_induct 1);
 by (safe_tac subset_cs);
 by (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [QPair_inject]));
+by (safe_tac (subset_cs addSEs [Pair_inject]));
 by (rewrite_goals_tac LList.con_defs);
 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
 (*0 case*)
@@ -57,27 +59,26 @@
 
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
-by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
-by (safe_tac qconverse_cs);
+val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
+by (rtac (prem RS converseI RS LList_Eq.coinduct) 1);
+by (rtac (LList_Eq.dom_subset RS converse_type) 1);
+by (safe_tac converse_cs);
 by (etac LList_Eq.elim 1);
 by (ALLGOALS (fast_tac qconverse_cs));
 val lleq_symmetric = result();
 
-goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
+goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
      ORELSE etac lleq_symmetric 1));
 val lleq_implies_equal = result();
 
 val [eqprem,lprem] = goal LList_Eq.thy
-    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
-by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
+    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1);
 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
 by (safe_tac qpair_cs);
 by (etac LList.elim 1);
-by (ALLGOALS (fast_tac qpair_cs));
+by (ALLGOALS (fast_tac pair_cs));
 val equal_llist_implies_leq = result();
 
-
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -51,7 +51,7 @@
 time_use     "ex/parcontract.ML";
 time_use_thy "ex/primrec0";
 
-(** Co-Datatypes **)
+(** CoDatatypes **)
 time_use_thy "ex/LList";
 time_use     "ex/llist_eq.ML";
 time_use_thy "ex/llistfn";
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/binfn.ML
--- a/src/ZF/ex/binfn.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/binfn.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -108,7 +108,7 @@
 val bin_ss = integ_ss 
     addsimps([bool_1I, bool_0I,
 	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
-	     bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
+	     bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
 
 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
                  [bool_subset_nat RS subsetD];
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/counit.ML
--- a/src/ZF/ex/counit.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/counit.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,15 +3,15 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Trivial co-datatype definitions, one of which goes wrong!
+Trivial codatatype definitions, one of which goes wrong!
 
-Need to find sufficient conditions for co-datatypes to work correctly!
+Need to find sufficient conditions for codatatypes to work correctly!
 *)
 
 (*This degenerate definition does not work well because the one constructor's
   definition is trivial!
 *)
-structure CoUnit = Co_Datatype_Fun
+structure CoUnit = CoDatatype_Fun
  (val thy = QUniv.thy;
   val rec_specs = 
       [("counit", "quniv(0)",
@@ -20,8 +20,8 @@
   val ext = None
   val sintrs = ["x: counit ==> Con(x) : counit"];
   val monos = [];
-  val type_intrs = co_datatype_intrs
-  val type_elims = co_datatype_elims);
+  val type_intrs = codatatype_intrs
+  val type_elims = codatatype_elims);
   
 val [ConI] = CoUnit.intrs;
 
@@ -35,7 +35,7 @@
 goal CoUnit.thy "counit = quniv(0)";
 by (rtac (CoUnit.dom_subset RS equalityI) 1);
 by (rtac subsetI 1);
-by (etac CoUnit.co_induct 1);
+by (etac CoUnit.coinduct 1);
 by (rtac subset_refl 1);
 by (rewrite_goals_tac CoUnit.con_defs);
 by (fast_tac ZF_cs 1);
@@ -48,7 +48,7 @@
   The resulting set is a singleton.
 *)
 
-structure CoUnit2 = Co_Datatype_Fun
+structure CoUnit2 = CoDatatype_Fun
  (val thy = QUniv.thy;
   val rec_specs = 
       [("counit2", "quniv(0)",
@@ -57,8 +57,8 @@
   val ext = None
   val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];
   val monos = [];
-  val type_intrs = co_datatype_intrs
-  val type_elims = co_datatype_elims);
+  val type_intrs = codatatype_intrs
+  val type_elims = codatatype_elims);
 
 val [Con2I] = CoUnit2.intrs;
 
@@ -73,7 +73,7 @@
 val Con2_bnd_mono = result();
 
 goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
-by (rtac (singletonI RS CoUnit2.co_induct) 1);
+by (rtac (singletonI RS CoUnit2.coinduct) 1);
 by (rtac (qunivI RS singleton_subsetI) 1);
 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
 by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/llist.ML
--- a/src/ZF/ex/llist.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/llist.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,10 +3,10 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Co-Datatype definition of Lazy Lists
+CoDatatype definition of Lazy Lists
 *)
 
-structure LList = Co_Datatype_Fun
+structure LList = CoDatatype_Fun
  (val thy = QUniv.thy;
   val rec_specs = 
       [("llist", "quniv(A)",
@@ -18,8 +18,8 @@
       ["LNil : llist(A)",
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
-  val type_intrs = co_datatype_intrs
-  val type_elims = co_datatype_elims);
+  val type_intrs = codatatype_intrs
+  val type_elims = codatatype_elims);
   
 val [LNilI, LConsI] = LList.intrs;
 
@@ -46,7 +46,7 @@
   QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
 
 val quniv_cs = ZF_cs addSIs in_quniv_rls 
-                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
+                     addIs (Int_quniv_in_quniv::codatatype_intrs);
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList.thy
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/llist_eq.ML
--- a/src/ZF/ex/llist_eq.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/llist_eq.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -3,25 +3,27 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Former part of llist.ML, contains definition and use of LList_Eq
-*)
+Equality for llist(A) as a greatest fixed point
+***)
 
-(*** Equality for llist(A) as a greatest fixed point ***)
+(*Previously used <*> in the domain and variant pairs as elements.  But
+  standard pairs work just as well.  To use variant pairs, must change prefix
+  a q/Q to the Sigma, Pair and converse rules.*)
 
-structure LList_Eq = Co_Inductive_Fun
+structure LList_Eq = CoInductive_Fun
  (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
-  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
+  val rec_doms = [("lleq", "llist(A) * llist(A)")];
   val sintrs = 
-      ["<LNil; LNil> : lleq(A)",
-       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
+      ["<LNil, LNil> : lleq(A)",
+       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
   val monos = [];
   val con_defs = [];
-  val type_intrs = LList.intrs@[QSigmaI];
-  val type_elims = [QSigmaE2]);
+  val type_intrs = LList.intrs@[SigmaI];
+  val type_elims = [SigmaE2]);
 
 (** Alternatives for above:
   val con_defs = LList.con_defs
-  val type_intrs = co_datatype_intrs
+  val type_intrs = codatatype_intrs
   val type_elims = [quniv_QPair_E]
 **)
 
@@ -34,11 +36,11 @@
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList_Eq.thy
-   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
+   "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
 by (etac trans_induct 1);
 by (safe_tac subset_cs);
 by (etac LList_Eq.elim 1);
-by (safe_tac (subset_cs addSEs [QPair_inject]));
+by (safe_tac (subset_cs addSEs [Pair_inject]));
 by (rewrite_goals_tac LList.con_defs);
 by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
 (*0 case*)
@@ -57,27 +59,26 @@
 
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
-by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
-by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
-by (safe_tac qconverse_cs);
+val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
+by (rtac (prem RS converseI RS LList_Eq.coinduct) 1);
+by (rtac (LList_Eq.dom_subset RS converse_type) 1);
+by (safe_tac converse_cs);
 by (etac LList_Eq.elim 1);
 by (ALLGOALS (fast_tac qconverse_cs));
 val lleq_symmetric = result();
 
-goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
+goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
      ORELSE etac lleq_symmetric 1));
 val lleq_implies_equal = result();
 
 val [eqprem,lprem] = goal LList_Eq.thy
-    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
-by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
+    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1);
 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
 by (safe_tac qpair_cs);
 by (etac LList.elim 1);
-by (ALLGOALS (fast_tac qpair_cs));
+by (ALLGOALS (fast_tac pair_cs));
 val equal_llist_implies_leq = result();
 
-
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/llistfn.ML
--- a/src/ZF/ex/llistfn.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/llistfn.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -4,6 +4,8 @@
     Copyright   1993  University of Cambridge
 
 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
+
+Examples of coinduction for type-checking and to prove llist equations
 *)
 
 open LListFn;
@@ -31,7 +33,84 @@
 val lconst_in_quniv = result();
 
 goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
-by (rtac (singletonI RS LList.co_induct) 1);
+by (rtac (singletonI RS LList.coinduct) 1);
 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
 by (fast_tac (ZF_cs addSIs [lconst]) 1);
 val lconst_type = result();
+
+(*** flip --- equations merely assumed; certain consequences proved ***)
+
+val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
+
+goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
+be boolE 1;
+by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
+     ORELSE etac ssubst 1));
+val bool_Int_into_quniv = result();
+
+(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
+val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
+
+val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
+
+val flip_cs = 
+  ZF_cs addSIs [not_type,
+		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
+		zero_in_quniv, Int_Vset_0_subset RS qunivI,
+		Transset_0,
+		zero_Int_in_quniv, one_Int_in_quniv,
+		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
+        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
+
+(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
+  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
+goal LListFn.thy
+   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
+by (etac trans_induct 1);
+by (safe_tac ZF_cs);
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 2);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+by (fast_tac flip_cs 1);
+by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
+(*0 case*)
+by (fast_tac flip_cs 1);
+(*succ(j) case*)
+by (fast_tac flip_cs 1);
+(*Limit(i) case*)
+by (etac (Limit_Vfrom_eq RS ssubst) 1);
+by (rtac (Int_UN_distrib RS ssubst) 1);
+by (rtac UN_in_quniv 1);
+by (fast_tac flip_cs 1);
+val flip_llist_quniv_lemma = result();
+
+goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
+br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
+by (REPEAT (assume_tac 1));
+val flip_in_quniv = result();
+
+val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
+by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
+       LList.coinduct 1);
+br (prem RS RepFunI) 1;
+by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
+be RepFunE 1;
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_type = result();
+
+val [prem] = goal LListFn.thy
+    "l : llist(bool) ==> flip(flip(l)) = l";
+by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
+       (LList_Eq.coinduct RS lleq_implies_equal) 1);
+br (prem RS RepFunI) 1;
+by (fast_tac (ZF_cs addSIs [flip_type]) 1);
+be RepFunE 1;
+by (etac LList.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_flip = result();
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/ex/llistfn.thy
--- a/src/ZF/ex/llistfn.thy	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/ex/llistfn.thy	Mon Nov 15 14:41:25 1993 +0100
@@ -4,13 +4,23 @@
     Copyright   1993  University of Cambridge
 
 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
+
+STILL NEEDS:
+co_recursion for defining lconst, flip, etc.
+a typing rule for it, based on some notion of "productivity..."
 *)
 
-LListFn = LList +
+LListFn = LList + LList_Eq +
 consts
   lconst   :: "i => i"
+  flip     :: "i => i"
 
 rules
   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
 
+  flip_LNil   "flip(LNil) = LNil"
+
+  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
+\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
+
 end
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/nat.ML
--- a/src/ZF/nat.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/nat.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -36,7 +36,8 @@
 val nat_1I = result();
 
 goal Nat.thy "bool <= nat";
-by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
+by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
+	    ORELSE eresolve_tac [boolE,ssubst] 1));
 val bool_subset_nat = result();
 
 val bool_into_nat = bool_subset_nat RS subsetD;
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/qpair.thy
--- a/src/ZF/qpair.thy	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/qpair.thy	Mon Nov 15 14:41:25 1993 +0100
@@ -31,12 +31,12 @@
 
 rules
   QPair_def       "<a;b> == a+b"
-  qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
+  qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
   qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
   qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
   QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
 
-  qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
+  qsum_def        "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
   QInl_def        "QInl(a)      == <0;a>"
   QInr_def        "QInr(b)      == <1;b>"
   qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/quniv.ML
--- a/src/ZF/quniv.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/quniv.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -290,7 +290,7 @@
 val QPair_Int_Vfrom_in_quniv = result();
 
 
-(**** "Take-lemma" rules for proving a=b by co-induction ****)
+(**** "Take-lemma" rules for proving a=b by coinduction ****)
 
 (** Unfortunately, the technique used above does not apply here, since
     the base case appears impossible to prove: it involves an intersection
diff -r 0e58da397b1d -r 09287f26bfb8 src/ZF/zf.ML
--- a/src/ZF/zf.ML	Mon Nov 15 14:33:40 1993 +0100
+++ b/src/ZF/zf.ML	Mon Nov 15 14:41:25 1993 +0100
@@ -270,7 +270,7 @@
     "!!a A. a : A ==> f(a) : {f(x). x:A}"
  (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
 
-(*Useful for co-induction proofs*)
+(*Useful for coinduction proofs*)
 val RepFun_eqI = prove_goal ZF.thy
     "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
  (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);