|
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 local open Ind_Syntax |
|
16 in |
|
17 |
|
18 fun gen_fp_oper a (X,T,t) = |
|
19 let val setT = mk_setT T |
|
20 in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t) end; |
|
21 |
|
22 structure Lfp_items = |
|
23 struct |
|
24 val oper = gen_fp_oper "lfp" |
|
25 val Tarski = def_lfp_Tarski |
|
26 val induct = def_induct |
|
27 end; |
|
28 |
|
29 structure Gfp_items = |
|
30 struct |
|
31 val oper = gen_fp_oper "gfp" |
|
32 val Tarski = def_gfp_Tarski |
|
33 val induct = def_Collect_coinduct |
|
34 end; |
|
35 |
|
36 end; |
|
37 |
|
38 |
|
39 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
40 : sig include INTR_ELIM INDRULE end = |
|
41 struct |
|
42 structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and |
|
43 Fp=Lfp_items); |
|
44 |
|
45 structure Indrule = Indrule_Fun |
|
46 (structure Inductive=Inductive and Intr_elim=Intr_elim); |
|
47 |
|
48 open Intr_elim Indrule |
|
49 end; |
|
50 |
|
51 |
|
52 structure Ind = Add_inductive_def_Fun (Lfp_items); |
|
53 |
|
54 |
|
55 signature INDUCTIVE_STRING = |
|
56 sig |
|
57 val thy_name : string (*name of the new theory*) |
|
58 val srec_tms : string list (*recursion terms*) |
|
59 val sintrs : string list (*desired introduction rules*) |
|
60 end; |
|
61 |
|
62 |
|
63 (*For upwards compatibility: can be called directly from ML*) |
|
64 functor Inductive_Fun |
|
65 (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end) |
|
66 : sig include INTR_ELIM INDRULE end = |
|
67 Ind_section_Fun |
|
68 (open Inductive Ind_Syntax |
|
69 val sign = sign_of thy; |
|
70 val rec_tms = map (readtm sign termTVar) srec_tms |
|
71 and intr_tms = map (readtm sign propT) sintrs; |
|
72 val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) |
|
73 |> add_thyname thy_name); |
|
74 |
|
75 |
|
76 |
|
77 signature COINDRULE = |
|
78 sig |
|
79 val coinduct : thm |
|
80 end; |
|
81 |
|
82 |
|
83 functor CoInd_section_Fun |
|
84 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
85 : sig include INTR_ELIM COINDRULE end = |
|
86 struct |
|
87 structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp_items); |
|
88 |
|
89 open Intr_elim |
|
90 val coinduct = raw_induct |
|
91 end; |
|
92 |
|
93 |
|
94 structure CoInd = Add_inductive_def_Fun(Gfp_items); |