src/HOL/Inductive.ML
 author wenzelm Thu Jan 23 14:19:16 1997 +0100 (1997-01-23) changeset 2545 d10abc8c11fb parent 1465 5d7a7e439cec child 2855 36f75c4a0047 permissions -rw-r--r--
```     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);
```