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