src/ZF/co-inductive.ML
 author paulson Fri, 16 Feb 1996 18:00:47 +0100 changeset 1512 ce37c64244c0 parent 0 a5a9c433f639 permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
```
(*  Title: 	ZF/co-inductive.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Co-inductive Definitions for Zermelo-Fraenkel Set Theory

Uses greatest fixedpoints with Quine-inspired products and sums

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

structure Gfp =
struct
val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
val bnd_monoI	= bnd_monoI
val subs	= def_gfp_subset
val Tarski	= def_gfp_Tarski
val induct	= def_Collect_coinduct
end;

structure Quine_Prod =
struct
val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
val pair	= Const("QPair", [iT,iT]--->iT)
val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
val pair_iff	= QPair_iff
val split_eq	= qsplit
val fsplitI	= qfsplitI
val fsplitD	= qfsplitD
val fsplitE	= qfsplitE
end;

structure Quine_Sum =
struct
val sum	= Const("op <+>", [iT,iT]--->iT)
val inl	= Const("QInl", iT-->iT)
val inr	= Const("QInr", iT-->iT)
val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
val case_inl	= qcase_QInl
val case_inr	= qcase_QInr
val inl_iff	= QInl_iff
val inr_iff	= QInr_iff
val distinct	= QInl_QInr_iff
val distinct' = QInr_QInl_iff
end;

signature CO_INDRULE =
sig
val co_induct : thm
end;

functor Co_Inductive_Fun (Ind: INDUCTIVE)
: sig include INTR_ELIM CO_INDRULE 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
end;

```