src/ZF/Inductive.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 22814 4cd25f1706bb
child 24826 78e6a3cea367
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/Inductive.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Inductive definitions use least fixedpoints with standard products and sums
     7 Coinductive definitions use greatest fixedpoints with Quine products and sums
     8 
     9 Sums are used only for mutual recursion;
    10 Products are used only to derive "streamlined" induction rules for relations
    11 *)
    12 
    13 header{*Inductive and Coinductive Definitions*}
    14 
    15 theory Inductive imports Fixedpt QPair
    16   uses
    17     "ind_syntax.ML"
    18     "Tools/cartprod.ML"
    19     "Tools/ind_cases.ML"
    20     "Tools/inductive_package.ML"
    21     "Tools/induct_tacs.ML"
    22     "Tools/primrec_package.ML" begin
    23 
    24 setup IndCases.setup
    25 setup DatatypeTactics.setup
    26 
    27 ML_setup {*
    28 val iT = Ind_Syntax.iT
    29 and oT = FOLogic.oT;
    30 
    31 structure Lfp =
    32   struct
    33   val oper      = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
    34   val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    35   val bnd_monoI = bnd_monoI
    36   val subs      = def_lfp_subset
    37   val Tarski    = def_lfp_unfold
    38   val induct    = def_induct
    39   end;
    40 
    41 structure Standard_Prod =
    42   struct
    43   val sigma     = Const("Sigma", [iT, iT-->iT]--->iT)
    44   val pair      = Const("Pair", [iT,iT]--->iT)
    45   val split_name = "split"
    46   val pair_iff  = Pair_iff
    47   val split_eq  = split
    48   val fsplitI   = splitI
    49   val fsplitD   = splitD
    50   val fsplitE   = splitE
    51   end;
    52 
    53 structure Standard_CP = CartProd_Fun (Standard_Prod);
    54 
    55 structure Standard_Sum =
    56   struct
    57   val sum       = Const("op +", [iT,iT]--->iT)
    58   val inl       = Const("Inl", iT-->iT)
    59   val inr       = Const("Inr", iT-->iT)
    60   val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
    61   val case_inl  = case_Inl
    62   val case_inr  = case_Inr
    63   val inl_iff   = Inl_iff
    64   val inr_iff   = Inr_iff
    65   val distinct  = Inl_Inr_iff
    66   val distinct' = Inr_Inl_iff
    67   val free_SEs  = Ind_Syntax.mk_free_SEs
    68             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
    69   end;
    70 
    71 
    72 structure Ind_Package =
    73     Add_inductive_def_Fun
    74       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    75        and Su=Standard_Sum val coind = false);
    76 
    77 
    78 structure Gfp =
    79   struct
    80   val oper      = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
    81   val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    82   val bnd_monoI = bnd_monoI
    83   val subs      = def_gfp_subset
    84   val Tarski    = def_gfp_unfold
    85   val induct    = def_Collect_coinduct
    86   end;
    87 
    88 structure Quine_Prod =
    89   struct
    90   val sigma     = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
    91   val pair      = Const("QPair.QPair", [iT,iT]--->iT)
    92   val split_name = "QPair.qsplit"
    93   val pair_iff  = QPair_iff
    94   val split_eq  = qsplit
    95   val fsplitI   = qsplitI
    96   val fsplitD   = qsplitD
    97   val fsplitE   = qsplitE
    98   end;
    99 
   100 structure Quine_CP = CartProd_Fun (Quine_Prod);
   101 
   102 structure Quine_Sum =
   103   struct
   104   val sum       = Const("QPair.op <+>", [iT,iT]--->iT)
   105   val inl       = Const("QPair.QInl", iT-->iT)
   106   val inr       = Const("QPair.QInr", iT-->iT)
   107   val elim      = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
   108   val case_inl  = qcase_QInl
   109   val case_inr  = qcase_QInr
   110   val inl_iff   = QInl_iff
   111   val inr_iff   = QInr_iff
   112   val distinct  = QInl_QInr_iff
   113   val distinct' = QInr_QInl_iff
   114   val free_SEs  = Ind_Syntax.mk_free_SEs
   115             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
   116   end;
   117 
   118 
   119 structure CoInd_Package =
   120   Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
   121     and Su=Quine_Sum val coind = true);
   122 
   123 *}
   124 
   125 end