author | clasohm |
Wed, 06 Mar 1996 14:19:39 +0100 | |
changeset 1557 | fe30812f5b5e |
parent 1465 | 5d7a7e439cec |
child 2855 | 36f75c4a0047 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/inductive.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 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) = |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
16 |
let val setT = Ind_Syntax.mk_setT T |
923 | 17 |
in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t) end; |
18 |
||
19 |
structure Lfp_items = |
|
20 |
struct |
|
1465 | 21 |
val oper = gen_fp_oper "lfp" |
22 |
val Tarski = def_lfp_Tarski |
|
23 |
val induct = def_induct |
|
923 | 24 |
end; |
25 |
||
26 |
structure Gfp_items = |
|
27 |
struct |
|
1465 | 28 |
val oper = gen_fp_oper "gfp" |
29 |
val Tarski = def_gfp_Tarski |
|
30 |
val induct = def_Collect_coinduct |
|
923 | 31 |
end; |
32 |
||
33 |
||
34 |
functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
35 |
: sig include INTR_ELIM INDRULE end = |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
36 |
let |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
37 |
structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and |
1465 | 38 |
Fp=Lfp_items); |
923 | 39 |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
40 |
structure Indrule = Indrule_Fun |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
41 |
(structure Inductive=Inductive and Intr_elim=Intr_elim); |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
42 |
in |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
43 |
struct |
1465 | 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 |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
50 |
open Indrule |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
923
diff
changeset
|
51 |
end |
923 | 52 |
end; |
53 |
||
54 |
||
55 |
structure Ind = Add_inductive_def_Fun (Lfp_items); |
|
56 |
||
57 |
||
58 |
signature INDUCTIVE_STRING = |
|
59 |
sig |
|
1465 | 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*) |
|
923 | 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); |