src/ZF/Inductive.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 4352 7ac9f3e8a97d
child 6093 87bf8c03b169
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
     1 (*  Title:      ZF/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 Inductive definitions use least fixedpoints with standard products and sums
     9 Coinductive definitions use greatest fixedpoints with Quine products and sums
    10 
    11 Sums are used only for mutual recursion;
    12 Products are used only to derive "streamlined" induction rules for relations
    13 *)
    14 
    15 val iT = Ind_Syntax.iT
    16 and oT = FOLogic.oT;
    17 
    18 structure Lfp =
    19   struct
    20   val oper      = Const("lfp",      [iT,iT-->iT]--->iT)
    21   val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
    22   val bnd_monoI = bnd_monoI
    23   val subs      = def_lfp_subset
    24   val Tarski    = def_lfp_Tarski
    25   val induct    = def_induct
    26   end;
    27 
    28 structure Standard_Prod =
    29   struct
    30   val sigma     = Const("Sigma", [iT, iT-->iT]--->iT)
    31   val pair      = Const("Pair", [iT,iT]--->iT)
    32   val split_name = "split"
    33   val pair_iff  = Pair_iff
    34   val split_eq  = split
    35   val fsplitI   = splitI
    36   val fsplitD   = splitD
    37   val fsplitE   = splitE
    38   end;
    39 
    40 structure Standard_CP = CartProd_Fun (Standard_Prod);
    41 
    42 structure Standard_Sum =
    43   struct
    44   val sum       = Const("op +", [iT,iT]--->iT)
    45   val inl       = Const("Inl", iT-->iT)
    46   val inr       = Const("Inr", iT-->iT)
    47   val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
    48   val case_inl  = case_Inl
    49   val case_inr  = case_Inr
    50   val inl_iff   = Inl_iff
    51   val inr_iff   = Inr_iff
    52   val distinct  = Inl_Inr_iff
    53   val distinct' = Inr_Inl_iff
    54   val free_SEs  = Ind_Syntax.mk_free_SEs 
    55             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
    56   end;
    57 
    58 
    59 structure Ind_Package = 
    60     Add_inductive_def_Fun
    61       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    62        and Su=Standard_Sum);
    63 
    64 
    65 structure Gfp =
    66   struct
    67   val oper      = Const("gfp",      [iT,iT-->iT]--->iT)
    68   val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
    69   val bnd_monoI = bnd_monoI
    70   val subs      = def_gfp_subset
    71   val Tarski    = def_gfp_Tarski
    72   val induct    = def_Collect_coinduct
    73   end;
    74 
    75 structure Quine_Prod =
    76   struct
    77   val sigma     = Const("QSigma", [iT, iT-->iT]--->iT)
    78   val pair      = Const("QPair", [iT,iT]--->iT)
    79   val split_name = "qsplit"
    80   val pair_iff  = QPair_iff
    81   val split_eq  = qsplit
    82   val fsplitI   = qsplitI
    83   val fsplitD   = qsplitD
    84   val fsplitE   = qsplitE
    85   end;
    86 
    87 structure Quine_CP = CartProd_Fun (Quine_Prod);
    88 
    89 structure Quine_Sum =
    90   struct
    91   val sum       = Const("op <+>", [iT,iT]--->iT)
    92   val inl       = Const("QInl", iT-->iT)
    93   val inr       = Const("QInr", iT-->iT)
    94   val elim      = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
    95   val case_inl  = qcase_QInl
    96   val case_inr  = qcase_QInr
    97   val inl_iff   = QInl_iff
    98   val inr_iff   = QInr_iff
    99   val distinct  = QInl_QInr_iff
   100   val distinct' = QInr_QInl_iff
   101   val free_SEs  = Ind_Syntax.mk_free_SEs 
   102             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
   103   end;
   104 
   105 
   106 structure CoInd_Package = 
   107     Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
   108                           and Su=Quine_Sum);
   109