src/HOL/Inductive.ML
author paulson
Tue Jan 02 10:46:50 1996 +0100 (1996-01-02)
changeset 1430 439e1476a7f8
parent 923 ff1574a81019
child 1465 5d7a7e439cec
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.
clasohm@923
     1
(*  Title: 	HOL/inductive.ML
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
(Co)Inductive Definitions for HOL
clasohm@923
     7
clasohm@923
     8
Inductive definitions use least fixedpoints with standard products and sums
clasohm@923
     9
Coinductive definitions use greatest fixedpoints with Quine products and sums
clasohm@923
    10
clasohm@923
    11
Sums are used only for mutual recursion;
clasohm@923
    12
Products are used only to derive "streamlined" induction rules for relations
clasohm@923
    13
*)
clasohm@923
    14
clasohm@923
    15
fun gen_fp_oper a (X,T,t) = 
paulson@1430
    16
    let val setT = Ind_Syntax.mk_setT T
clasohm@923
    17
    in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
clasohm@923
    18
clasohm@923
    19
structure Lfp_items =
clasohm@923
    20
  struct
clasohm@923
    21
  val oper	= gen_fp_oper "lfp"
clasohm@923
    22
  val Tarski	= def_lfp_Tarski
clasohm@923
    23
  val induct	= def_induct
clasohm@923
    24
  end;
clasohm@923
    25
clasohm@923
    26
structure Gfp_items =
clasohm@923
    27
  struct
clasohm@923
    28
  val oper	= gen_fp_oper "gfp"
clasohm@923
    29
  val Tarski	= def_gfp_Tarski
clasohm@923
    30
  val induct	= def_Collect_coinduct
clasohm@923
    31
  end;
clasohm@923
    32
clasohm@923
    33
clasohm@923
    34
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
clasohm@923
    35
  : sig include INTR_ELIM INDRULE end =
paulson@1430
    36
let
paulson@1430
    37
  structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
paulson@1430
    38
					  Fp=Lfp_items);
clasohm@923
    39
paulson@1430
    40
  structure Indrule = Indrule_Fun
paulson@1430
    41
      (structure Inductive=Inductive and Intr_elim=Intr_elim);
paulson@1430
    42
in 
paulson@1430
    43
   struct 
paulson@1430
    44
   val thy	= Intr_elim.thy
paulson@1430
    45
   val defs	= Intr_elim.defs
paulson@1430
    46
   val mono	= Intr_elim.mono
paulson@1430
    47
   val intrs	= Intr_elim.intrs
paulson@1430
    48
   val elim	= Intr_elim.elim
paulson@1430
    49
   val mk_cases	= Intr_elim.mk_cases
paulson@1430
    50
   open Indrule 
paulson@1430
    51
   end
clasohm@923
    52
end;
clasohm@923
    53
clasohm@923
    54
clasohm@923
    55
structure Ind = Add_inductive_def_Fun (Lfp_items);
clasohm@923
    56
clasohm@923
    57
clasohm@923
    58
signature INDUCTIVE_STRING =
clasohm@923
    59
  sig
clasohm@923
    60
  val thy_name   : string 		(*name of the new theory*)
clasohm@923
    61
  val srec_tms   : string list		(*recursion terms*)
clasohm@923
    62
  val sintrs     : string list		(*desired introduction rules*)
clasohm@923
    63
  end;
clasohm@923
    64
clasohm@923
    65
clasohm@923
    66
(*For upwards compatibility: can be called directly from ML*)
clasohm@923
    67
functor Inductive_Fun
clasohm@923
    68
 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
clasohm@923
    69
   : sig include INTR_ELIM INDRULE end =
clasohm@923
    70
Ind_section_Fun
clasohm@923
    71
   (open Inductive Ind_Syntax
clasohm@923
    72
    val sign = sign_of thy;
clasohm@923
    73
    val rec_tms = map (readtm sign termTVar) srec_tms
clasohm@923
    74
    and intr_tms = map (readtm sign propT) sintrs;
clasohm@923
    75
    val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
clasohm@923
    76
                  |> add_thyname thy_name);
clasohm@923
    77
clasohm@923
    78
clasohm@923
    79
clasohm@923
    80
signature COINDRULE =
clasohm@923
    81
  sig
clasohm@923
    82
  val coinduct : thm
clasohm@923
    83
  end;
clasohm@923
    84
clasohm@923
    85
clasohm@923
    86
functor CoInd_section_Fun
clasohm@923
    87
 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
clasohm@923
    88
    : sig include INTR_ELIM COINDRULE end =
clasohm@923
    89
struct
clasohm@923
    90
structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp_items);
clasohm@923
    91
clasohm@923
    92
open Intr_elim 
clasohm@923
    93
val coinduct = raw_induct
clasohm@923
    94
end;
clasohm@923
    95
clasohm@923
    96
clasohm@923
    97
structure CoInd = Add_inductive_def_Fun(Gfp_items);