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