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