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