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