changed all co- and co_ to co
authorlcp
Mon Nov 15 14:41:25 1993 +0100 (1993-11-15)
changeset 12009287f26bfb8
parent 119 0e58da397b1d
child 121 d392174734e9
changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs
src/ZF/Datatype.ML
src/ZF/Nat.ML
src/ZF/QPair.thy
src/ZF/QUniv.ML
src/ZF/ROOT.ML
src/ZF/ZF.ML
src/ZF/coinductive.ML
src/ZF/datatype.ML
src/ZF/ex/BinFn.ML
src/ZF/ex/LList.ML
src/ZF/ex/LListFn.ML
src/ZF/ex/LListFn.thy
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ROOT.ML
src/ZF/ex/binfn.ML
src/ZF/ex/counit.ML
src/ZF/ex/llist.ML
src/ZF/ex/llist_eq.ML
src/ZF/ex/llistfn.ML
src/ZF/ex/llistfn.thy
src/ZF/nat.ML
src/ZF/qpair.thy
src/ZF/quniv.ML
src/ZF/zf.ML
     1.1 --- a/src/ZF/Datatype.ML	Mon Nov 15 14:33:40 1993 +0100
     1.2 +++ b/src/ZF/Datatype.ML	Mon Nov 15 14:41:25 1993 +0100
     1.3 @@ -3,8 +3,7 @@
     1.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
     1.8 -
     1.9 +(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
    1.10  *)
    1.11  
    1.12  
    1.13 @@ -29,15 +28,15 @@
    1.14  end;
    1.15  
    1.16  
    1.17 -(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
    1.18 -functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
    1.19 -         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
    1.20 +(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
    1.21 +functor CoDatatype_Fun (Const: CONSTRUCTOR) 
    1.22 +         : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    1.23  struct
    1.24  structure Constructor = Constructor_Fun (structure Const=Const and 
    1.25    		                      Pr=Quine_Prod and Su=Quine_Sum);
    1.26  open Const Constructor;
    1.27  
    1.28 -structure Co_Inductive = Co_Inductive_Fun
    1.29 +structure CoInductive = CoInductive_Fun
    1.30          (val thy = con_thy;
    1.31  	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    1.32  	 val sintrs = sintrs;
    1.33 @@ -46,7 +45,7 @@
    1.34  	 val type_intrs = type_intrs;
    1.35  	 val type_elims = type_elims);
    1.36  
    1.37 -open Co_Inductive
    1.38 +open CoInductive
    1.39  end;
    1.40  
    1.41  
    1.42 @@ -60,11 +59,11 @@
    1.43  (*Needed for mutual recursion*)
    1.44  val datatype_elims = [make_elim InlD, make_elim InrD];
    1.45  
    1.46 -(*For most co-datatypes involving quniv*)
    1.47 -val co_datatype_intrs = 
    1.48 +(*For most codatatypes involving quniv*)
    1.49 +val codatatype_intrs = 
    1.50      [QSigmaI, QInlI, QInrI,
    1.51       QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    1.52       zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    1.53  
    1.54 -val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
    1.55 +val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    1.56  
     2.1 --- a/src/ZF/Nat.ML	Mon Nov 15 14:33:40 1993 +0100
     2.2 +++ b/src/ZF/Nat.ML	Mon Nov 15 14:41:25 1993 +0100
     2.3 @@ -36,7 +36,8 @@
     2.4  val nat_1I = result();
     2.5  
     2.6  goal Nat.thy "bool <= nat";
     2.7 -by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
     2.8 +by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
     2.9 +	    ORELSE eresolve_tac [boolE,ssubst] 1));
    2.10  val bool_subset_nat = result();
    2.11  
    2.12  val bool_into_nat = bool_subset_nat RS subsetD;
     3.1 --- a/src/ZF/QPair.thy	Mon Nov 15 14:33:40 1993 +0100
     3.2 +++ b/src/ZF/QPair.thy	Mon Nov 15 14:41:25 1993 +0100
     3.3 @@ -31,12 +31,12 @@
     3.4  
     3.5  rules
     3.6    QPair_def       "<a;b> == a+b"
     3.7 -  qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
     3.8 +  qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
     3.9    qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
    3.10    qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
    3.11    QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
    3.12  
    3.13 -  qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
    3.14 +  qsum_def        "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
    3.15    QInl_def        "QInl(a)      == <0;a>"
    3.16    QInr_def        "QInr(b)      == <1;b>"
    3.17    qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
     4.1 --- a/src/ZF/QUniv.ML	Mon Nov 15 14:33:40 1993 +0100
     4.2 +++ b/src/ZF/QUniv.ML	Mon Nov 15 14:41:25 1993 +0100
     4.3 @@ -290,7 +290,7 @@
     4.4  val QPair_Int_Vfrom_in_quniv = result();
     4.5  
     4.6  
     4.7 -(**** "Take-lemma" rules for proving a=b by co-induction ****)
     4.8 +(**** "Take-lemma" rules for proving a=b by coinduction ****)
     4.9  
    4.10  (** Unfortunately, the technique used above does not apply here, since
    4.11      the base case appears impossible to prove: it involves an intersection
     5.1 --- a/src/ZF/ROOT.ML	Mon Nov 15 14:33:40 1993 +0100
     5.2 +++ b/src/ZF/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
     5.3 @@ -46,7 +46,7 @@
     5.4  use     "mono.ML";
     5.5  use_thy "fixedpt";
     5.6  
     5.7 -(*Inductive/co-inductive definitions*)
     5.8 +(*Inductive/coinductive definitions*)
     5.9  use     "ind_syntax.ML";
    5.10  use     "intr_elim.ML";
    5.11  use     "indrule.ML";
    5.12 @@ -61,7 +61,7 @@
    5.13  use_thy "epsilon";
    5.14  use_thy "arith";
    5.15  
    5.16 -(*Datatype/co-datatype definitions*)
    5.17 +(*Datatype/codatatype definitions*)
    5.18  use_thy "univ";
    5.19  use_thy "quniv";
    5.20  use     "constructor.ML";
     6.1 --- a/src/ZF/ZF.ML	Mon Nov 15 14:33:40 1993 +0100
     6.2 +++ b/src/ZF/ZF.ML	Mon Nov 15 14:41:25 1993 +0100
     6.3 @@ -270,7 +270,7 @@
     6.4      "!!a A. a : A ==> f(a) : {f(x). x:A}"
     6.5   (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
     6.6  
     6.7 -(*Useful for co-induction proofs*)
     6.8 +(*Useful for coinduction proofs*)
     6.9  val RepFun_eqI = prove_goal ZF.thy
    6.10      "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
    6.11   (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
     7.1 --- a/src/ZF/coinductive.ML	Mon Nov 15 14:33:40 1993 +0100
     7.2 +++ b/src/ZF/coinductive.ML	Mon Nov 15 14:41:25 1993 +0100
     7.3 @@ -1,9 +1,9 @@
     7.4 -(*  Title: 	ZF/co-inductive.ML
     7.5 +(*  Title: 	ZF/coinductive.ML
     7.6      ID:         $Id$
     7.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     7.8      Copyright   1993  University of Cambridge
     7.9  
    7.10 -Co-inductive Definitions for Zermelo-Fraenkel Set Theory
    7.11 +Coinductive Definitions for Zermelo-Fraenkel Set Theory
    7.12  
    7.13  Uses greatest fixedpoints with Quine-inspired products and sums
    7.14  
    7.15 @@ -48,20 +48,20 @@
    7.16    val distinct' = QInr_QInl_iff
    7.17    end;
    7.18  
    7.19 -signature CO_INDRULE =
    7.20 +signature COINDRULE =
    7.21    sig
    7.22 -  val co_induct : thm
    7.23 +  val coinduct : thm
    7.24    end;
    7.25  
    7.26  
    7.27 -functor Co_Inductive_Fun (Ind: INDUCTIVE) 
    7.28 -          : sig include INTR_ELIM CO_INDRULE end =
    7.29 +functor CoInductive_Fun (Ind: INDUCTIVE) 
    7.30 +          : sig include INTR_ELIM COINDRULE end =
    7.31  struct
    7.32  structure Intr_elim = 
    7.33      Intr_elim_Fun(structure Ind=Ind and Fp=Gfp and 
    7.34  		  Pr=Quine_Prod and Su=Quine_Sum);
    7.35  
    7.36  open Intr_elim 
    7.37 -val co_induct = raw_induct
    7.38 +val coinduct = raw_induct
    7.39  end;
    7.40  
     8.1 --- a/src/ZF/datatype.ML	Mon Nov 15 14:33:40 1993 +0100
     8.2 +++ b/src/ZF/datatype.ML	Mon Nov 15 14:41:25 1993 +0100
     8.3 @@ -3,8 +3,7 @@
     8.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1993  University of Cambridge
     8.6  
     8.7 -(Co-) Datatype Definitions for Zermelo-Fraenkel Set Theory
     8.8 -
     8.9 +(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory
    8.10  *)
    8.11  
    8.12  
    8.13 @@ -29,15 +28,15 @@
    8.14  end;
    8.15  
    8.16  
    8.17 -(*Co-datatype definitions use greatest fixedpoints, Quine products and sums*)
    8.18 -functor Co_Datatype_Fun (Const: CONSTRUCTOR) 
    8.19 -         : sig include CONSTRUCTOR_RESULT INTR_ELIM CO_INDRULE end =
    8.20 +(*Codatatype definitions use greatest fixedpoints, Quine products and sums*)
    8.21 +functor CoDatatype_Fun (Const: CONSTRUCTOR) 
    8.22 +         : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
    8.23  struct
    8.24  structure Constructor = Constructor_Fun (structure Const=Const and 
    8.25    		                      Pr=Quine_Prod and Su=Quine_Sum);
    8.26  open Const Constructor;
    8.27  
    8.28 -structure Co_Inductive = Co_Inductive_Fun
    8.29 +structure CoInductive = CoInductive_Fun
    8.30          (val thy = con_thy;
    8.31  	 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
    8.32  	 val sintrs = sintrs;
    8.33 @@ -46,7 +45,7 @@
    8.34  	 val type_intrs = type_intrs;
    8.35  	 val type_elims = type_elims);
    8.36  
    8.37 -open Co_Inductive
    8.38 +open CoInductive
    8.39  end;
    8.40  
    8.41  
    8.42 @@ -60,11 +59,11 @@
    8.43  (*Needed for mutual recursion*)
    8.44  val datatype_elims = [make_elim InlD, make_elim InrD];
    8.45  
    8.46 -(*For most co-datatypes involving quniv*)
    8.47 -val co_datatype_intrs = 
    8.48 +(*For most codatatypes involving quniv*)
    8.49 +val codatatype_intrs = 
    8.50      [QSigmaI, QInlI, QInrI,
    8.51       QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
    8.52       zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    8.53  
    8.54 -val co_datatype_elims = [make_elim QInlD, make_elim QInrD];
    8.55 +val codatatype_elims = [make_elim QInlD, make_elim QInrD];
    8.56  
     9.1 --- a/src/ZF/ex/BinFn.ML	Mon Nov 15 14:33:40 1993 +0100
     9.2 +++ b/src/ZF/ex/BinFn.ML	Mon Nov 15 14:41:25 1993 +0100
     9.3 @@ -108,7 +108,7 @@
     9.4  val bin_ss = integ_ss 
     9.5      addsimps([bool_1I, bool_0I,
     9.6  	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
     9.7 -	     bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
     9.8 +	     bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
     9.9  
    9.10  val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
    9.11                   [bool_subset_nat RS subsetD];
    10.1 --- a/src/ZF/ex/LList.ML	Mon Nov 15 14:33:40 1993 +0100
    10.2 +++ b/src/ZF/ex/LList.ML	Mon Nov 15 14:41:25 1993 +0100
    10.3 @@ -3,10 +3,10 @@
    10.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    10.5      Copyright   1993  University of Cambridge
    10.6  
    10.7 -Co-Datatype definition of Lazy Lists
    10.8 +CoDatatype definition of Lazy Lists
    10.9  *)
   10.10  
   10.11 -structure LList = Co_Datatype_Fun
   10.12 +structure LList = CoDatatype_Fun
   10.13   (val thy = QUniv.thy;
   10.14    val rec_specs = 
   10.15        [("llist", "quniv(A)",
   10.16 @@ -18,8 +18,8 @@
   10.17        ["LNil : llist(A)",
   10.18         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   10.19    val monos = [];
   10.20 -  val type_intrs = co_datatype_intrs
   10.21 -  val type_elims = co_datatype_elims);
   10.22 +  val type_intrs = codatatype_intrs
   10.23 +  val type_elims = codatatype_elims);
   10.24    
   10.25  val [LNilI, LConsI] = LList.intrs;
   10.26  
   10.27 @@ -46,7 +46,7 @@
   10.28    QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
   10.29  
   10.30  val quniv_cs = ZF_cs addSIs in_quniv_rls 
   10.31 -                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
   10.32 +                     addIs (Int_quniv_in_quniv::codatatype_intrs);
   10.33  
   10.34  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   10.35  goal LList.thy
    11.1 --- a/src/ZF/ex/LListFn.ML	Mon Nov 15 14:33:40 1993 +0100
    11.2 +++ b/src/ZF/ex/LListFn.ML	Mon Nov 15 14:41:25 1993 +0100
    11.3 @@ -4,6 +4,8 @@
    11.4      Copyright   1993  University of Cambridge
    11.5  
    11.6  Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
    11.7 +
    11.8 +Examples of coinduction for type-checking and to prove llist equations
    11.9  *)
   11.10  
   11.11  open LListFn;
   11.12 @@ -31,7 +33,84 @@
   11.13  val lconst_in_quniv = result();
   11.14  
   11.15  goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
   11.16 -by (rtac (singletonI RS LList.co_induct) 1);
   11.17 +by (rtac (singletonI RS LList.coinduct) 1);
   11.18  by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
   11.19  by (fast_tac (ZF_cs addSIs [lconst]) 1);
   11.20  val lconst_type = result();
   11.21 +
   11.22 +(*** flip --- equations merely assumed; certain consequences proved ***)
   11.23 +
   11.24 +val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
   11.25 +
   11.26 +goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
   11.27 +be boolE 1;
   11.28 +by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
   11.29 +     ORELSE etac ssubst 1));
   11.30 +val bool_Int_into_quniv = result();
   11.31 +
   11.32 +(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
   11.33 +val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
   11.34 +
   11.35 +val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
   11.36 +
   11.37 +val flip_cs = 
   11.38 +  ZF_cs addSIs [not_type,
   11.39 +		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
   11.40 +		zero_in_quniv, Int_Vset_0_subset RS qunivI,
   11.41 +		Transset_0,
   11.42 +		zero_Int_in_quniv, one_Int_in_quniv,
   11.43 +		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
   11.44 +        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
   11.45 +
   11.46 +(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
   11.47 +  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
   11.48 +goal LListFn.thy
   11.49 +   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
   11.50 +by (etac trans_induct 1);
   11.51 +by (safe_tac ZF_cs);
   11.52 +by (etac LList.elim 1);
   11.53 +by (asm_simp_tac flip_ss 1);
   11.54 +by (asm_simp_tac flip_ss 2);
   11.55 +by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
   11.56 +by (fast_tac flip_cs 1);
   11.57 +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   11.58 +(*0 case*)
   11.59 +by (fast_tac flip_cs 1);
   11.60 +(*succ(j) case*)
   11.61 +by (fast_tac flip_cs 1);
   11.62 +(*Limit(i) case*)
   11.63 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
   11.64 +by (rtac (Int_UN_distrib RS ssubst) 1);
   11.65 +by (rtac UN_in_quniv 1);
   11.66 +by (fast_tac flip_cs 1);
   11.67 +val flip_llist_quniv_lemma = result();
   11.68 +
   11.69 +goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
   11.70 +br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
   11.71 +by (REPEAT (assume_tac 1));
   11.72 +val flip_in_quniv = result();
   11.73 +
   11.74 +val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
   11.75 +by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
   11.76 +       LList.coinduct 1);
   11.77 +br (prem RS RepFunI) 1;
   11.78 +by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
   11.79 +be RepFunE 1;
   11.80 +by (etac LList.elim 1);
   11.81 +by (asm_simp_tac flip_ss 1);
   11.82 +by (asm_simp_tac flip_ss 1);
   11.83 +by (fast_tac (ZF_cs addSIs [not_type]) 1);
   11.84 +val flip_type = result();
   11.85 +
   11.86 +val [prem] = goal LListFn.thy
   11.87 +    "l : llist(bool) ==> flip(flip(l)) = l";
   11.88 +by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
   11.89 +       (LList_Eq.coinduct RS lleq_implies_equal) 1);
   11.90 +br (prem RS RepFunI) 1;
   11.91 +by (fast_tac (ZF_cs addSIs [flip_type]) 1);
   11.92 +be RepFunE 1;
   11.93 +by (etac LList.elim 1);
   11.94 +by (asm_simp_tac flip_ss 1);
   11.95 +by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
   11.96 +by (fast_tac (ZF_cs addSIs [not_type]) 1);
   11.97 +val flip_flip = result();
    12.1 --- a/src/ZF/ex/LListFn.thy	Mon Nov 15 14:33:40 1993 +0100
    12.2 +++ b/src/ZF/ex/LListFn.thy	Mon Nov 15 14:41:25 1993 +0100
    12.3 @@ -4,13 +4,23 @@
    12.4      Copyright   1993  University of Cambridge
    12.5  
    12.6  Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
    12.7 +
    12.8 +STILL NEEDS:
    12.9 +co_recursion for defining lconst, flip, etc.
   12.10 +a typing rule for it, based on some notion of "productivity..."
   12.11  *)
   12.12  
   12.13 -LListFn = LList +
   12.14 +LListFn = LList + LList_Eq +
   12.15  consts
   12.16    lconst   :: "i => i"
   12.17 +  flip     :: "i => i"
   12.18  
   12.19  rules
   12.20    lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
   12.21  
   12.22 +  flip_LNil   "flip(LNil) = LNil"
   12.23 +
   12.24 +  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
   12.25 +\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
   12.26 +
   12.27  end
    13.1 --- a/src/ZF/ex/LList_Eq.ML	Mon Nov 15 14:33:40 1993 +0100
    13.2 +++ b/src/ZF/ex/LList_Eq.ML	Mon Nov 15 14:41:25 1993 +0100
    13.3 @@ -3,25 +3,27 @@
    13.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    13.5      Copyright   1993  University of Cambridge
    13.6  
    13.7 -Former part of llist.ML, contains definition and use of LList_Eq
    13.8 -*)
    13.9 +Equality for llist(A) as a greatest fixed point
   13.10 +***)
   13.11  
   13.12 -(*** Equality for llist(A) as a greatest fixed point ***)
   13.13 +(*Previously used <*> in the domain and variant pairs as elements.  But
   13.14 +  standard pairs work just as well.  To use variant pairs, must change prefix
   13.15 +  a q/Q to the Sigma, Pair and converse rules.*)
   13.16  
   13.17 -structure LList_Eq = Co_Inductive_Fun
   13.18 +structure LList_Eq = CoInductive_Fun
   13.19   (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
   13.20 -  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
   13.21 +  val rec_doms = [("lleq", "llist(A) * llist(A)")];
   13.22    val sintrs = 
   13.23 -      ["<LNil; LNil> : lleq(A)",
   13.24 -       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
   13.25 +      ["<LNil, LNil> : lleq(A)",
   13.26 +       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
   13.27    val monos = [];
   13.28    val con_defs = [];
   13.29 -  val type_intrs = LList.intrs@[QSigmaI];
   13.30 -  val type_elims = [QSigmaE2]);
   13.31 +  val type_intrs = LList.intrs@[SigmaI];
   13.32 +  val type_elims = [SigmaE2]);
   13.33  
   13.34  (** Alternatives for above:
   13.35    val con_defs = LList.con_defs
   13.36 -  val type_intrs = co_datatype_intrs
   13.37 +  val type_intrs = codatatype_intrs
   13.38    val type_elims = [quniv_QPair_E]
   13.39  **)
   13.40  
   13.41 @@ -34,11 +36,11 @@
   13.42  
   13.43  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   13.44  goal LList_Eq.thy
   13.45 -   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
   13.46 +   "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
   13.47  by (etac trans_induct 1);
   13.48  by (safe_tac subset_cs);
   13.49  by (etac LList_Eq.elim 1);
   13.50 -by (safe_tac (subset_cs addSEs [QPair_inject]));
   13.51 +by (safe_tac (subset_cs addSEs [Pair_inject]));
   13.52  by (rewrite_goals_tac LList.con_defs);
   13.53  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   13.54  (*0 case*)
   13.55 @@ -57,27 +59,26 @@
   13.56  
   13.57  
   13.58  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
   13.59 -val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
   13.60 -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
   13.61 -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
   13.62 -by (safe_tac qconverse_cs);
   13.63 +val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
   13.64 +by (rtac (prem RS converseI RS LList_Eq.coinduct) 1);
   13.65 +by (rtac (LList_Eq.dom_subset RS converse_type) 1);
   13.66 +by (safe_tac converse_cs);
   13.67  by (etac LList_Eq.elim 1);
   13.68  by (ALLGOALS (fast_tac qconverse_cs));
   13.69  val lleq_symmetric = result();
   13.70  
   13.71 -goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
   13.72 +goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
   13.73  by (rtac equalityI 1);
   13.74  by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
   13.75       ORELSE etac lleq_symmetric 1));
   13.76  val lleq_implies_equal = result();
   13.77  
   13.78  val [eqprem,lprem] = goal LList_Eq.thy
   13.79 -    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
   13.80 -by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
   13.81 +    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
   13.82 +by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1);
   13.83  by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
   13.84  by (safe_tac qpair_cs);
   13.85  by (etac LList.elim 1);
   13.86 -by (ALLGOALS (fast_tac qpair_cs));
   13.87 +by (ALLGOALS (fast_tac pair_cs));
   13.88  val equal_llist_implies_leq = result();
   13.89  
   13.90 -
    14.1 --- a/src/ZF/ex/ROOT.ML	Mon Nov 15 14:33:40 1993 +0100
    14.2 +++ b/src/ZF/ex/ROOT.ML	Mon Nov 15 14:41:25 1993 +0100
    14.3 @@ -51,7 +51,7 @@
    14.4  time_use     "ex/parcontract.ML";
    14.5  time_use_thy "ex/primrec0";
    14.6  
    14.7 -(** Co-Datatypes **)
    14.8 +(** CoDatatypes **)
    14.9  time_use_thy "ex/LList";
   14.10  time_use     "ex/llist_eq.ML";
   14.11  time_use_thy "ex/llistfn";
    15.1 --- a/src/ZF/ex/binfn.ML	Mon Nov 15 14:33:40 1993 +0100
    15.2 +++ b/src/ZF/ex/binfn.ML	Mon Nov 15 14:41:25 1993 +0100
    15.3 @@ -108,7 +108,7 @@
    15.4  val bin_ss = integ_ss 
    15.5      addsimps([bool_1I, bool_0I,
    15.6  	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
    15.7 -	     bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
    15.8 +	     bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
    15.9  
   15.10  val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
   15.11                   [bool_subset_nat RS subsetD];
    16.1 --- a/src/ZF/ex/counit.ML	Mon Nov 15 14:33:40 1993 +0100
    16.2 +++ b/src/ZF/ex/counit.ML	Mon Nov 15 14:41:25 1993 +0100
    16.3 @@ -3,15 +3,15 @@
    16.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    16.5      Copyright   1993  University of Cambridge
    16.6  
    16.7 -Trivial co-datatype definitions, one of which goes wrong!
    16.8 +Trivial codatatype definitions, one of which goes wrong!
    16.9  
   16.10 -Need to find sufficient conditions for co-datatypes to work correctly!
   16.11 +Need to find sufficient conditions for codatatypes to work correctly!
   16.12  *)
   16.13  
   16.14  (*This degenerate definition does not work well because the one constructor's
   16.15    definition is trivial!
   16.16  *)
   16.17 -structure CoUnit = Co_Datatype_Fun
   16.18 +structure CoUnit = CoDatatype_Fun
   16.19   (val thy = QUniv.thy;
   16.20    val rec_specs = 
   16.21        [("counit", "quniv(0)",
   16.22 @@ -20,8 +20,8 @@
   16.23    val ext = None
   16.24    val sintrs = ["x: counit ==> Con(x) : counit"];
   16.25    val monos = [];
   16.26 -  val type_intrs = co_datatype_intrs
   16.27 -  val type_elims = co_datatype_elims);
   16.28 +  val type_intrs = codatatype_intrs
   16.29 +  val type_elims = codatatype_elims);
   16.30    
   16.31  val [ConI] = CoUnit.intrs;
   16.32  
   16.33 @@ -35,7 +35,7 @@
   16.34  goal CoUnit.thy "counit = quniv(0)";
   16.35  by (rtac (CoUnit.dom_subset RS equalityI) 1);
   16.36  by (rtac subsetI 1);
   16.37 -by (etac CoUnit.co_induct 1);
   16.38 +by (etac CoUnit.coinduct 1);
   16.39  by (rtac subset_refl 1);
   16.40  by (rewrite_goals_tac CoUnit.con_defs);
   16.41  by (fast_tac ZF_cs 1);
   16.42 @@ -48,7 +48,7 @@
   16.43    The resulting set is a singleton.
   16.44  *)
   16.45  
   16.46 -structure CoUnit2 = Co_Datatype_Fun
   16.47 +structure CoUnit2 = CoDatatype_Fun
   16.48   (val thy = QUniv.thy;
   16.49    val rec_specs = 
   16.50        [("counit2", "quniv(0)",
   16.51 @@ -57,8 +57,8 @@
   16.52    val ext = None
   16.53    val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];
   16.54    val monos = [];
   16.55 -  val type_intrs = co_datatype_intrs
   16.56 -  val type_elims = co_datatype_elims);
   16.57 +  val type_intrs = codatatype_intrs
   16.58 +  val type_elims = codatatype_elims);
   16.59  
   16.60  val [Con2I] = CoUnit2.intrs;
   16.61  
   16.62 @@ -73,7 +73,7 @@
   16.63  val Con2_bnd_mono = result();
   16.64  
   16.65  goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
   16.66 -by (rtac (singletonI RS CoUnit2.co_induct) 1);
   16.67 +by (rtac (singletonI RS CoUnit2.coinduct) 1);
   16.68  by (rtac (qunivI RS singleton_subsetI) 1);
   16.69  by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
   16.70  by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
    17.1 --- a/src/ZF/ex/llist.ML	Mon Nov 15 14:33:40 1993 +0100
    17.2 +++ b/src/ZF/ex/llist.ML	Mon Nov 15 14:41:25 1993 +0100
    17.3 @@ -3,10 +3,10 @@
    17.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    17.5      Copyright   1993  University of Cambridge
    17.6  
    17.7 -Co-Datatype definition of Lazy Lists
    17.8 +CoDatatype definition of Lazy Lists
    17.9  *)
   17.10  
   17.11 -structure LList = Co_Datatype_Fun
   17.12 +structure LList = CoDatatype_Fun
   17.13   (val thy = QUniv.thy;
   17.14    val rec_specs = 
   17.15        [("llist", "quniv(A)",
   17.16 @@ -18,8 +18,8 @@
   17.17        ["LNil : llist(A)",
   17.18         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   17.19    val monos = [];
   17.20 -  val type_intrs = co_datatype_intrs
   17.21 -  val type_elims = co_datatype_elims);
   17.22 +  val type_intrs = codatatype_intrs
   17.23 +  val type_elims = codatatype_elims);
   17.24    
   17.25  val [LNilI, LConsI] = LList.intrs;
   17.26  
   17.27 @@ -46,7 +46,7 @@
   17.28    QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
   17.29  
   17.30  val quniv_cs = ZF_cs addSIs in_quniv_rls 
   17.31 -                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
   17.32 +                     addIs (Int_quniv_in_quniv::codatatype_intrs);
   17.33  
   17.34  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   17.35  goal LList.thy
    18.1 --- a/src/ZF/ex/llist_eq.ML	Mon Nov 15 14:33:40 1993 +0100
    18.2 +++ b/src/ZF/ex/llist_eq.ML	Mon Nov 15 14:41:25 1993 +0100
    18.3 @@ -3,25 +3,27 @@
    18.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    18.5      Copyright   1993  University of Cambridge
    18.6  
    18.7 -Former part of llist.ML, contains definition and use of LList_Eq
    18.8 -*)
    18.9 +Equality for llist(A) as a greatest fixed point
   18.10 +***)
   18.11  
   18.12 -(*** Equality for llist(A) as a greatest fixed point ***)
   18.13 +(*Previously used <*> in the domain and variant pairs as elements.  But
   18.14 +  standard pairs work just as well.  To use variant pairs, must change prefix
   18.15 +  a q/Q to the Sigma, Pair and converse rules.*)
   18.16  
   18.17 -structure LList_Eq = Co_Inductive_Fun
   18.18 +structure LList_Eq = CoInductive_Fun
   18.19   (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
   18.20 -  val rec_doms = [("lleq", "llist(A) <*> llist(A)")];
   18.21 +  val rec_doms = [("lleq", "llist(A) * llist(A)")];
   18.22    val sintrs = 
   18.23 -      ["<LNil; LNil> : lleq(A)",
   18.24 -       "[| a:A;  <l; l'>: lleq(A) |] ==> <LCons(a,l); LCons(a,l')> : lleq(A)"];
   18.25 +      ["<LNil, LNil> : lleq(A)",
   18.26 +       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
   18.27    val monos = [];
   18.28    val con_defs = [];
   18.29 -  val type_intrs = LList.intrs@[QSigmaI];
   18.30 -  val type_elims = [QSigmaE2]);
   18.31 +  val type_intrs = LList.intrs@[SigmaI];
   18.32 +  val type_elims = [SigmaE2]);
   18.33  
   18.34  (** Alternatives for above:
   18.35    val con_defs = LList.con_defs
   18.36 -  val type_intrs = co_datatype_intrs
   18.37 +  val type_intrs = codatatype_intrs
   18.38    val type_elims = [quniv_QPair_E]
   18.39  **)
   18.40  
   18.41 @@ -34,11 +36,11 @@
   18.42  
   18.43  (*Keep unfolding the lazy list until the induction hypothesis applies*)
   18.44  goal LList_Eq.thy
   18.45 -   "!!i. Ord(i) ==> ALL l l'. <l;l'> : lleq(A) --> l Int Vset(i) <= l'";
   18.46 +   "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
   18.47  by (etac trans_induct 1);
   18.48  by (safe_tac subset_cs);
   18.49  by (etac LList_Eq.elim 1);
   18.50 -by (safe_tac (subset_cs addSEs [QPair_inject]));
   18.51 +by (safe_tac (subset_cs addSEs [Pair_inject]));
   18.52  by (rewrite_goals_tac LList.con_defs);
   18.53  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   18.54  (*0 case*)
   18.55 @@ -57,27 +59,26 @@
   18.56  
   18.57  
   18.58  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
   18.59 -val [prem] = goal LList_Eq.thy "<l;l'> : lleq(A) ==> <l';l> : lleq(A)";
   18.60 -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1);
   18.61 -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1);
   18.62 -by (safe_tac qconverse_cs);
   18.63 +val [prem] = goal LList_Eq.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
   18.64 +by (rtac (prem RS converseI RS LList_Eq.coinduct) 1);
   18.65 +by (rtac (LList_Eq.dom_subset RS converse_type) 1);
   18.66 +by (safe_tac converse_cs);
   18.67  by (etac LList_Eq.elim 1);
   18.68  by (ALLGOALS (fast_tac qconverse_cs));
   18.69  val lleq_symmetric = result();
   18.70  
   18.71 -goal LList_Eq.thy "!!l l'. <l;l'> : lleq(A) ==> l=l'";
   18.72 +goal LList_Eq.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
   18.73  by (rtac equalityI 1);
   18.74  by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
   18.75       ORELSE etac lleq_symmetric 1));
   18.76  val lleq_implies_equal = result();
   18.77  
   18.78  val [eqprem,lprem] = goal LList_Eq.thy
   18.79 -    "[| l=l';  l: llist(A) |] ==> <l;l'> : lleq(A)";
   18.80 -by (res_inst_tac [("X", "{<l;l>. l: llist(A)}")] LList_Eq.co_induct 1);
   18.81 +    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
   18.82 +by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] LList_Eq.coinduct 1);
   18.83  by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
   18.84  by (safe_tac qpair_cs);
   18.85  by (etac LList.elim 1);
   18.86 -by (ALLGOALS (fast_tac qpair_cs));
   18.87 +by (ALLGOALS (fast_tac pair_cs));
   18.88  val equal_llist_implies_leq = result();
   18.89  
   18.90 -
    19.1 --- a/src/ZF/ex/llistfn.ML	Mon Nov 15 14:33:40 1993 +0100
    19.2 +++ b/src/ZF/ex/llistfn.ML	Mon Nov 15 14:41:25 1993 +0100
    19.3 @@ -4,6 +4,8 @@
    19.4      Copyright   1993  University of Cambridge
    19.5  
    19.6  Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
    19.7 +
    19.8 +Examples of coinduction for type-checking and to prove llist equations
    19.9  *)
   19.10  
   19.11  open LListFn;
   19.12 @@ -31,7 +33,84 @@
   19.13  val lconst_in_quniv = result();
   19.14  
   19.15  goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)";
   19.16 -by (rtac (singletonI RS LList.co_induct) 1);
   19.17 +by (rtac (singletonI RS LList.coinduct) 1);
   19.18  by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
   19.19  by (fast_tac (ZF_cs addSIs [lconst]) 1);
   19.20  val lconst_type = result();
   19.21 +
   19.22 +(*** flip --- equations merely assumed; certain consequences proved ***)
   19.23 +
   19.24 +val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
   19.25 +
   19.26 +goal QUniv.thy "!!b. b:bool ==> b Int X : quniv(A)";
   19.27 +be boolE 1;
   19.28 +by (REPEAT (resolve_tac [one_Int_in_quniv, zero_Int_in_quniv] 1
   19.29 +     ORELSE etac ssubst 1));
   19.30 +val bool_Int_into_quniv = result();
   19.31 +
   19.32 +(* (!!x. x : A ==> B(x) : quniv(C)) ==> (UN x:A. B(x)) : quniv(C) *)
   19.33 +val UN_in_quniv = standard (qunivD RS UN_least RS qunivI);
   19.34 +
   19.35 +val Int_Vset_in_quniv = qunivD RS Int_Vset_subset RS qunivI;
   19.36 +
   19.37 +val flip_cs = 
   19.38 +  ZF_cs addSIs [not_type,
   19.39 +		QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
   19.40 +		zero_in_quniv, Int_Vset_0_subset RS qunivI,
   19.41 +		Transset_0,
   19.42 +		zero_Int_in_quniv, one_Int_in_quniv,
   19.43 +		QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]
   19.44 +        addIs  [bool_Int_into_quniv, Int_quniv_in_quniv];
   19.45 +
   19.46 +(*Reasoning borrowed from llist_eq.ML; a similar proof works for all
   19.47 +  "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
   19.48 +goal LListFn.thy
   19.49 +   "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) : quniv(bool)";
   19.50 +by (etac trans_induct 1);
   19.51 +by (safe_tac ZF_cs);
   19.52 +by (etac LList.elim 1);
   19.53 +by (asm_simp_tac flip_ss 1);
   19.54 +by (asm_simp_tac flip_ss 2);
   19.55 +by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
   19.56 +by (fast_tac flip_cs 1);
   19.57 +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   19.58 +(*0 case*)
   19.59 +by (fast_tac flip_cs 1);
   19.60 +(*succ(j) case*)
   19.61 +by (fast_tac flip_cs 1);
   19.62 +(*Limit(i) case*)
   19.63 +by (etac (Limit_Vfrom_eq RS ssubst) 1);
   19.64 +by (rtac (Int_UN_distrib RS ssubst) 1);
   19.65 +by (rtac UN_in_quniv 1);
   19.66 +by (fast_tac flip_cs 1);
   19.67 +val flip_llist_quniv_lemma = result();
   19.68 +
   19.69 +goal LListFn.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
   19.70 +br (flip_llist_quniv_lemma RS bspec RS Int_Vset_in_quniv) 1;
   19.71 +by (REPEAT (assume_tac 1));
   19.72 +val flip_in_quniv = result();
   19.73 +
   19.74 +val [prem] = goal LListFn.thy "l : llist(bool) ==> flip(l): llist(bool)";
   19.75 +by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
   19.76 +       LList.coinduct 1);
   19.77 +br (prem RS RepFunI) 1;
   19.78 +by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
   19.79 +be RepFunE 1;
   19.80 +by (etac LList.elim 1);
   19.81 +by (asm_simp_tac flip_ss 1);
   19.82 +by (asm_simp_tac flip_ss 1);
   19.83 +by (fast_tac (ZF_cs addSIs [not_type]) 1);
   19.84 +val flip_type = result();
   19.85 +
   19.86 +val [prem] = goal LListFn.thy
   19.87 +    "l : llist(bool) ==> flip(flip(l)) = l";
   19.88 +by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
   19.89 +       (LList_Eq.coinduct RS lleq_implies_equal) 1);
   19.90 +br (prem RS RepFunI) 1;
   19.91 +by (fast_tac (ZF_cs addSIs [flip_type]) 1);
   19.92 +be RepFunE 1;
   19.93 +by (etac LList.elim 1);
   19.94 +by (asm_simp_tac flip_ss 1);
   19.95 +by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
   19.96 +by (fast_tac (ZF_cs addSIs [not_type]) 1);
   19.97 +val flip_flip = result();
    20.1 --- a/src/ZF/ex/llistfn.thy	Mon Nov 15 14:33:40 1993 +0100
    20.2 +++ b/src/ZF/ex/llistfn.thy	Mon Nov 15 14:41:25 1993 +0100
    20.3 @@ -4,13 +4,23 @@
    20.4      Copyright   1993  University of Cambridge
    20.5  
    20.6  Functions for Lazy Lists in Zermelo-Fraenkel Set Theory 
    20.7 +
    20.8 +STILL NEEDS:
    20.9 +co_recursion for defining lconst, flip, etc.
   20.10 +a typing rule for it, based on some notion of "productivity..."
   20.11  *)
   20.12  
   20.13 -LListFn = LList +
   20.14 +LListFn = LList + LList_Eq +
   20.15  consts
   20.16    lconst   :: "i => i"
   20.17 +  flip     :: "i => i"
   20.18  
   20.19  rules
   20.20    lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
   20.21  
   20.22 +  flip_LNil   "flip(LNil) = LNil"
   20.23 +
   20.24 +  flip_LCons  "[| x:bool; l: llist(bool) |] ==> \
   20.25 +\              flip(LCons(x,l)) = LCons(not(x), flip(l))"
   20.26 +
   20.27  end
    21.1 --- a/src/ZF/nat.ML	Mon Nov 15 14:33:40 1993 +0100
    21.2 +++ b/src/ZF/nat.ML	Mon Nov 15 14:41:25 1993 +0100
    21.3 @@ -36,7 +36,8 @@
    21.4  val nat_1I = result();
    21.5  
    21.6  goal Nat.thy "bool <= nat";
    21.7 -by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 ORELSE etac boolE 1));
    21.8 +by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
    21.9 +	    ORELSE eresolve_tac [boolE,ssubst] 1));
   21.10  val bool_subset_nat = result();
   21.11  
   21.12  val bool_into_nat = bool_subset_nat RS subsetD;
    22.1 --- a/src/ZF/qpair.thy	Mon Nov 15 14:33:40 1993 +0100
    22.2 +++ b/src/ZF/qpair.thy	Mon Nov 15 14:41:25 1993 +0100
    22.3 @@ -31,12 +31,12 @@
    22.4  
    22.5  rules
    22.6    QPair_def       "<a;b> == a+b"
    22.7 -  qsplit_def      "qsplit(c,p)  ==  THE y. EX a b. p=<a;b> & y=c(a,b)"
    22.8 +  qsplit_def      "qsplit(c,p)  == THE y. EX a b. p=<a;b> & y=c(a,b)"
    22.9    qfsplit_def     "qfsplit(R,z) == EX x y. z=<x;y> & R(x,y)"
   22.10    qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
   22.11    QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
   22.12  
   22.13 -  qsum_def        "A <+> B      == QSigma({0}, %x.A) Un QSigma({1}, %x.B)"
   22.14 +  qsum_def        "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
   22.15    QInl_def        "QInl(a)      == <0;a>"
   22.16    QInr_def        "QInr(b)      == <1;b>"
   22.17    qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
    23.1 --- a/src/ZF/quniv.ML	Mon Nov 15 14:33:40 1993 +0100
    23.2 +++ b/src/ZF/quniv.ML	Mon Nov 15 14:41:25 1993 +0100
    23.3 @@ -290,7 +290,7 @@
    23.4  val QPair_Int_Vfrom_in_quniv = result();
    23.5  
    23.6  
    23.7 -(**** "Take-lemma" rules for proving a=b by co-induction ****)
    23.8 +(**** "Take-lemma" rules for proving a=b by coinduction ****)
    23.9  
   23.10  (** Unfortunately, the technique used above does not apply here, since
   23.11      the base case appears impossible to prove: it involves an intersection
    24.1 --- a/src/ZF/zf.ML	Mon Nov 15 14:33:40 1993 +0100
    24.2 +++ b/src/ZF/zf.ML	Mon Nov 15 14:41:25 1993 +0100
    24.3 @@ -270,7 +270,7 @@
    24.4      "!!a A. a : A ==> f(a) : {f(x). x:A}"
    24.5   (fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
    24.6  
    24.7 -(*Useful for co-induction proofs*)
    24.8 +(*Useful for coinduction proofs*)
    24.9  val RepFun_eqI = prove_goal ZF.thy
   24.10      "!!b a f. [| b=f(a);  a : A |] ==> b : {f(x). x:A}"
   24.11   (fn _ => [ etac ssubst 1, etac RepFunI 1 ]);