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