src/HOL/Inductive.ML
author wenzelm
Wed Oct 01 18:13:41 1997 +0200 (1997-10-01)
changeset 3768 67f4ac759100
parent 2855 36f75c4a0047
child 4872 33e7cdc20681
permissions -rw-r--r--
fully qualified names: Theory.add_XXX;
     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 checkThy	= (fn thy => require_thy thy "Lfp" "inductive definitions")
    22   val oper      = gen_fp_oper "lfp"
    23   val Tarski    = def_lfp_Tarski
    24   val induct    = def_induct
    25   end;
    26 
    27 structure Gfp_items =
    28   struct
    29   val checkThy	= (fn thy => require_thy thy "Gfp" "coinductive definitions")
    30   val oper      = gen_fp_oper "gfp"
    31   val Tarski    = def_gfp_Tarski
    32   val induct    = def_Collect_coinduct
    33   end;
    34 
    35 
    36 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    37   : sig include INTR_ELIM INDRULE end =
    38 let
    39   structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
    40                                           Fp=Lfp_items);
    41 
    42   structure Indrule = Indrule_Fun
    43       (structure Inductive=Inductive and Intr_elim=Intr_elim);
    44 in 
    45    struct 
    46    val thy      = Intr_elim.thy
    47    val defs     = Intr_elim.defs
    48    val mono     = Intr_elim.mono
    49    val intrs    = Intr_elim.intrs
    50    val elim     = Intr_elim.elim
    51    val mk_cases = Intr_elim.mk_cases
    52    open Indrule 
    53    end
    54 end;
    55 
    56 
    57 structure Ind = Add_inductive_def_Fun (Lfp_items);
    58 
    59 
    60 signature INDUCTIVE_STRING =
    61   sig
    62   val thy_name   : string               (*name of the new theory*)
    63   val srec_tms   : string list          (*recursion terms*)
    64   val sintrs     : string list          (*desired introduction rules*)
    65   end;
    66 
    67 
    68 (*Called by the theory sections or directly from ML*)
    69 functor Inductive_Fun
    70  (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
    71    : sig include INTR_ELIM INDRULE end =
    72 Ind_section_Fun
    73    (open Inductive Ind_Syntax
    74     val sign = sign_of thy;
    75     val rec_tms = map (readtm sign termTVar) srec_tms
    76     and intr_tms = map (readtm sign propT) sintrs;
    77     val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
    78                   |> Theory.add_name thy_name);
    79 
    80 
    81 
    82 signature COINDRULE =
    83   sig
    84   val coinduct : thm
    85   end;
    86 
    87 
    88 functor CoInd_section_Fun
    89  (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    90     : sig include INTR_ELIM COINDRULE end =
    91 struct
    92 structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp_items);
    93 
    94 open Intr_elim 
    95 val coinduct = raw_induct
    96 end;
    97 
    98 
    99 structure CoInd = Add_inductive_def_Fun(Gfp_items);