src/HOL/Inductive.ML
 author nipkow Tue Apr 08 10:48:42 1997 +0200 (1997-04-08) changeset 2919 953a47dc0519 parent 2855 36f75c4a0047 child 3768 67f4ac759100 permissions -rw-r--r--
Dep. on Provers/nat_transitive
```     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                   |> add_thyname 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);
```