src/ZF/co-inductive.ML
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 0 a5a9c433f639
permissions -rw-r--r--
plain ASCII;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/co-inductive.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Co-inductive Definitions for Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Uses greatest fixedpoints with Quine-inspired products and sums
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
Sums are used only for mutual recursion;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
Products are used only to derive "streamlined" induction rules for relations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
structure Gfp =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val bnd_monoI	= bnd_monoI
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val subs	= def_gfp_subset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val Tarski	= def_gfp_Tarski
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val induct	= def_Collect_coinduct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
structure Quine_Prod =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val pair	= Const("QPair", [iT,iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val fsplit_const	= Const("qfsplit", [[iT,iT]--->oT, iT]--->oT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val pair_iff	= QPair_iff
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val split_eq	= qsplit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val fsplitI	= qfsplitI
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val fsplitD	= qfsplitD
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val fsplitE	= qfsplitE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
structure Quine_Sum =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  val sum	= Const("op <+>", [iT,iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  val inl	= Const("QInl", iT-->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val inr	= Const("QInr", iT-->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val case_inl	= qcase_QInl
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  val case_inr	= qcase_QInr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val inl_iff	= QInl_iff
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val inr_iff	= QInr_iff
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  val distinct	= QInl_QInr_iff
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
  val distinct' = QInr_QInl_iff
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
signature CO_INDRULE =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  val co_induct : thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
functor Co_Inductive_Fun (Ind: INDUCTIVE) 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
          : sig include INTR_ELIM CO_INDRULE end =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
structure Intr_elim = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    Intr_elim_Fun(structure Ind=Ind and Fp=Gfp and 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
		  Pr=Quine_Prod and Su=Quine_Sum);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
open Intr_elim 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val co_induct = raw_induct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67