src/ZF/co-inductive.ML
changeset 0 a5a9c433f639
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     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