src/ZF/Inductive.ML
author paulson
Fri, 22 Dec 1995 11:09:28 +0100
changeset 1418 f5f97ee67cbb
parent 1093 c2b3b7b7a69f
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Inductive.ML
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     2
    ID:         $Id$
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     5
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     6
(Co)Inductive Definitions for Zermelo-Fraenkel Set Theory
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     7
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     8
Inductive definitions use least fixedpoints with standard products and sums
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
     9
Coinductive definitions use greatest fixedpoints with Quine products and sums
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    10
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    11
Sums are used only for mutual recursion;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    12
Products are used only to derive "streamlined" induction rules for relations
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    13
*)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    14
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    15
val iT = Ind_Syntax.iT
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    16
and oT = Ind_Syntax.oT;
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    17
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    18
structure Lfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    19
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    20
  val oper	= Const("lfp",      [iT,iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    21
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    22
  val bnd_monoI	= bnd_monoI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    23
  val subs	= def_lfp_subset
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    24
  val Tarski	= def_lfp_Tarski
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    25
  val induct	= def_induct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    26
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    27
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    28
structure Standard_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    29
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    30
  val sigma	= Const("Sigma", [iT, iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    31
  val pair	= Const("Pair", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    32
  val split_const	= Const("split", [[iT,iT]--->iT, iT]--->iT)
1093
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
    33
  val fsplit_const	= Const("split", [[iT,iT]--->oT, iT]--->oT)
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    34
  val pair_iff	= Pair_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    35
  val split_eq	= split
1093
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
    36
  val fsplitI	= splitI
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
    37
  val fsplitD	= splitD
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
    38
  val fsplitE	= splitE
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    39
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    40
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    41
structure Standard_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    42
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    43
  val sum	= Const("op +", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    44
  val inl	= Const("Inl", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    45
  val inr	= Const("Inr", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    46
  val elim	= Const("case", [iT-->iT, iT-->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    47
  val case_inl	= case_Inl
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    48
  val case_inr	= case_Inr
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    49
  val inl_iff	= Inl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    50
  val inr_iff	= Inr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    51
  val distinct	= Inl_Inr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    52
  val distinct' = Inr_Inl_iff
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    53
  val free_SEs  = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    54
            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    55
  end;
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    56
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    57
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    58
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    59
  : sig include INTR_ELIM INDRULE end =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    60
let
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    61
  structure Intr_elim = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    62
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    63
		    Pr=Standard_Prod and Su=Standard_Sum);
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    64
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    65
  structure Indrule = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    66
      Indrule_Fun (structure Inductive=Inductive and 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    67
		   Pr=Standard_Prod and Su=Standard_Sum and 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    68
		       Intr_elim=Intr_elim)
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    69
in 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    70
   struct 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    71
   val thy	= Intr_elim.thy
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    72
   val defs	= Intr_elim.defs
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    73
   val bnd_mono	= Intr_elim.bnd_mono
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    74
   val dom_subset = Intr_elim.dom_subset
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    75
   val intrs	= Intr_elim.intrs
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    76
   val elim	= Intr_elim.elim
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    77
   val mk_cases	= Intr_elim.mk_cases
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    78
   open Indrule 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
    79
   end
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    80
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    81
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    82
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    83
structure Ind = Add_inductive_def_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    84
    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    85
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    86
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    87
structure Gfp =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    88
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    89
  val oper	= Const("gfp",      [iT,iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    90
  val bnd_mono	= Const("bnd_mono", [iT,iT-->iT]--->oT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    91
  val bnd_monoI	= bnd_monoI
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    92
  val subs	= def_gfp_subset
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    93
  val Tarski	= def_gfp_Tarski
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    94
  val induct	= def_Collect_coinduct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    95
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    96
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    97
structure Quine_Prod =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    98
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
    99
  val sigma	= Const("QSigma", [iT, iT-->iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   100
  val pair	= Const("QPair", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   101
  val split_const	= Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
1093
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
   102
  val fsplit_const	= Const("qsplit", [[iT,iT]--->oT, iT]--->oT)
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   103
  val pair_iff	= QPair_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   104
  val split_eq	= qsplit
1093
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
   105
  val fsplitI	= qsplitI
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
   106
  val fsplitD	= qsplitD
c2b3b7b7a69f Changed to use split instead of fsplit. The weakening of fsplitE appears not
lcp
parents: 802
diff changeset
   107
  val fsplitE	= qsplitE
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   108
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   109
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   110
structure Quine_Sum =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   111
  struct
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   112
  val sum	= Const("op <+>", [iT,iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   113
  val inl	= Const("QInl", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   114
  val inr	= Const("QInr", iT-->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   115
  val elim	= Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   116
  val case_inl	= qcase_QInl
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   117
  val case_inr	= qcase_QInr
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   118
  val inl_iff	= QInl_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   119
  val inr_iff	= QInr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   120
  val distinct	= QInl_QInr_iff
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   121
  val distinct' = QInr_QInl_iff
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   122
  val free_SEs  = Ind_Syntax.mk_free_SEs 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   123
            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   124
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   125
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   126
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   127
signature COINDRULE =
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   128
  sig
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   129
  val coinduct : thm
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   130
  end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   131
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   132
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   133
functor CoInd_section_Fun
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   134
 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   135
    : sig include INTR_ELIM COINDRULE end =
1418
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   136
let
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   137
  structure Intr_elim = 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   138
      Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   139
		    Pr=Quine_Prod and Su=Quine_Sum);
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   140
in
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   141
   struct
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   142
   val thy	= Intr_elim.thy
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   143
   val defs	= Intr_elim.defs
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   144
   val bnd_mono	= Intr_elim.bnd_mono
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   145
   val dom_subset = Intr_elim.dom_subset
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   146
   val intrs	= Intr_elim.intrs
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   147
   val elim	= Intr_elim.elim
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   148
   val mk_cases	= Intr_elim.mk_cases
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   149
   val coinduct = Intr_elim.raw_induct
f5f97ee67cbb Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1093
diff changeset
   150
   end
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   151
end;
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   152
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   153
structure CoInd = 
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   154
    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff changeset
   155