changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs
--- 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];
--- 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;
--- 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)))"
--- 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
--- 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";
--- 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 ]);
--- 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;
--- 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];
--- 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];
--- 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
--- 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();
--- 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
--- 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();
-
--- 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";
--- 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];
--- 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);
--- 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
--- 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();
-
--- 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();
--- 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
--- 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;
--- 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)))"
--- 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
--- 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 ]);