author | nipkow |
Fri, 02 Dec 1994 11:43:20 +0100 | |
changeset 194 | b93cc55cb7ab |
parent 187 | fcf8024c920d |
permissions | -rw-r--r-- |
128 | 1 |
(* Title: HOL/add_ind_def.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Fixedpoint definition module -- for Inductive/Coinductive Definitions |
|
7 |
||
8 |
Features: |
|
9 |
* least or greatest fixedpoints |
|
10 |
* user-specified product and sum constructions |
|
11 |
* mutually recursive definitions |
|
12 |
* definitions involving arbitrary monotone operators |
|
13 |
* automatically proves introduction and elimination rules |
|
14 |
||
15 |
The recursive sets must *already* be declared as constants in parent theory! |
|
16 |
||
17 |
Introduction rules have the form |
|
18 |
[| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |] |
|
19 |
where M is some monotone operator (usually the identity) |
|
20 |
P(x) is any (non-conjunctive) side condition on the free variables |
|
21 |
ti, t are any terms |
|
22 |
Sj, Sk are two of the sets being defined in mutual recursion |
|
23 |
||
24 |
Sums are used only for mutual recursion; |
|
25 |
Products are used only to derive "streamlined" induction rules for relations |
|
26 |
||
27 |
Nestings of disjoint sum types: |
|
28 |
(a+(b+c)) for 3, ((a+b)+(c+d)) for 4, ((a+b)+(c+(d+e))) for 5, |
|
29 |
((a+(b+c))+(d+(e+f))) for 6 |
|
30 |
*) |
|
31 |
||
32 |
signature FP = (** Description of a fixed point operator **) |
|
33 |
sig |
|
34 |
val oper : string * typ * term -> term (*fixed point operator*) |
|
35 |
val Tarski : thm (*Tarski's fixed point theorem*) |
|
36 |
val induct : thm (*induction/coinduction rule*) |
|
37 |
end; |
|
38 |
||
39 |
||
40 |
signature ADD_INDUCTIVE_DEF = |
|
41 |
sig |
|
42 |
val add_fp_def_i : term list * term list -> theory -> theory |
|
43 |
end; |
|
44 |
||
45 |
||
46 |
||
47 |
(*Declares functions to add fixedpoint/constructor defs to a theory*) |
|
48 |
functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF = |
|
49 |
struct |
|
50 |
open Logic Ind_Syntax; |
|
51 |
||
52 |
(*internal version*) |
|
53 |
fun add_fp_def_i (rec_tms, intr_tms) thy = |
|
54 |
let |
|
55 |
val sign = sign_of thy; |
|
56 |
||
57 |
(*recT and rec_params should agree for all mutually recursive components*) |
|
181
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
58 |
val rec_hds = map head_of rec_tms; |
128 | 59 |
|
181
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
60 |
val _ = assert_all is_Const rec_hds |
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
61 |
(fn t => "Recursive set not previously declared as constant: " ^ |
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
62 |
Sign.string_of_term sign t); |
128 | 63 |
|
181
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
64 |
(*Now we know they are all Consts, so get their names, type and params*) |
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
65 |
val rec_names = map (#1 o dest_Const) rec_hds |
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
66 |
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
128 | 67 |
|
68 |
val _ = assert_all Syntax.is_identifier rec_names |
|
69 |
(fn a => "Name of recursive set not an identifier: " ^ a); |
|
70 |
||
71 |
local (*Checking the introduction rules*) |
|
72 |
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
|
73 |
fun intr_ok set = |
|
74 |
case head_of set of Const(a,_) => a mem rec_names | _ => false; |
|
75 |
in |
|
76 |
val _ = assert_all intr_ok intr_sets |
|
77 |
(fn t => "Conclusion of rule does not name a recursive set: " ^ |
|
78 |
Sign.string_of_term sign t); |
|
79 |
end; |
|
80 |
||
81 |
val _ = assert_all is_Free rec_params |
|
82 |
(fn t => "Param in recursion term not a free variable: " ^ |
|
83 |
Sign.string_of_term sign t); |
|
84 |
||
85 |
(*** Construct the lfp definition ***) |
|
86 |
val mk_variant = variant (foldr add_term_names (intr_tms,[])); |
|
87 |
||
88 |
val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w"; |
|
89 |
||
181
3f5136a61a72
checks that the recursive sets are Consts before taking
lcp
parents:
142
diff
changeset
|
90 |
(*Probably INCORRECT for mutual recursion!*) |
187 | 91 |
val domTs = summands(dest_setT (body_type recT)); |
128 | 92 |
val dom_sumT = fold_bal mk_sum domTs; |
187 | 93 |
val dom_set = mk_setT dom_sumT; |
128 | 94 |
|
95 |
val freez = Free(z, dom_sumT) |
|
96 |
and freeX = Free(X, dom_set); |
|
97 |
(*type of w may be any of the domTs*) |
|
98 |
||
99 |
fun dest_tprop (Const("Trueprop",_) $ P) = P |
|
100 |
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |
|
101 |
Sign.string_of_term sign Q); |
|
102 |
||
103 |
(*Makes a disjunct from an introduction rule*) |
|
104 |
fun lfp_part intr = (*quantify over rule's free vars except parameters*) |
|
105 |
let val prems = map dest_tprop (strip_imp_prems intr) |
|
106 |
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds |
|
107 |
val exfrees = term_frees intr \\ rec_params |
|
108 |
val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr)) |
|
109 |
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; |
|
110 |
||
111 |
(*The Part(A,h) terms -- compose injections to make h*) |
|
112 |
fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*) |
|
113 |
| mk_Part (h, domT) = |
|
114 |
let val goodh = mend_sum_types (h, dom_sumT) |
|
115 |
and Part_const = |
|
116 |
Const("Part", [dom_set, domT-->dom_sumT]---> dom_set) |
|
117 |
in Part_const $ freeX $ Abs(w,domT,goodh) end; |
|
118 |
||
119 |
(*Access to balanced disjoint sums via injections*) |
|
120 |
val parts = map mk_Part |
|
121 |
(accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~ |
|
122 |
domTs); |
|
123 |
||
124 |
(*replace each set by the corresponding Part(A,h)*) |
|
125 |
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; |
|
126 |
||
127 |
val lfp_rhs = Fp.oper(X, dom_sumT, |
|
128 |
mk_Collect(z, dom_sumT, |
|
129 |
fold_bal (app disj) part_intrs)) |
|
130 |
||
131 |
val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) |
|
132 |
"Illegal occurrence of recursion operator") |
|
133 |
rec_hds; |
|
134 |
||
135 |
(*** Make the new theory ***) |
|
136 |
||
137 |
(*A key definition: |
|
138 |
If no mutual recursion then it equals the one recursive set. |
|
139 |
If mutual recursion then it differs from all the recursive sets. *) |
|
140 |
val big_rec_name = space_implode "_" rec_names; |
|
141 |
||
142 |
(*Big_rec... is the union of the mutually recursive sets*) |
|
143 |
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); |
|
144 |
||
145 |
(*The individual sets must already be declared*) |
|
146 |
val axpairs = map mk_defpair |
|
147 |
((big_rec_tm, lfp_rhs) :: |
|
148 |
(case parts of |
|
149 |
[_] => [] (*no mutual recursion*) |
|
150 |
| _ => rec_tms ~~ (*define the sets as Parts*) |
|
151 |
map (subst_atomic [(freeX, big_rec_tm)]) parts)); |
|
152 |
||
153 |
val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs |
|
154 |
||
155 |
in thy |> add_defs_i axpairs end |
|
156 |
||
157 |
||
158 |
(****************************************************************OMITTED |
|
159 |
||
160 |
(*Expects the recursive sets to have been defined already. |
|
161 |
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) |
|
162 |
fun add_constructs_def (rec_names, con_ty_lists) thy = |
|
163 |
* let |
|
164 |
* val _ = writeln" Defining the constructor functions..."; |
|
165 |
* val case_name = "f"; (*name for case variables*) |
|
166 |
||
167 |
* (** Define the constructors **) |
|
168 |
||
169 |
* (*The empty tuple is 0*) |
|
170 |
* fun mk_tuple [] = Const("0",iT) |
|
171 |
* | mk_tuple args = foldr1 mk_Pair args; |
|
172 |
||
173 |
* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k; |
|
174 |
||
175 |
* val npart = length rec_names; (*total # of mutually recursive parts*) |
|
176 |
||
177 |
* (*Make constructor definition; kpart is # of this mutually recursive part*) |
|
178 |
* fun mk_con_defs (kpart, con_ty_list) = |
|
179 |
* let val ncon = length con_ty_list (*number of constructors*) |
|
180 |
fun mk_def (((id,T,syn), name, args, prems), kcon) = |
|
181 |
(*kcon is index of constructor*) |
|
182 |
mk_defpair (list_comb (Const(name,T), args), |
|
183 |
mk_inject npart kpart |
|
184 |
(mk_inject ncon kcon (mk_tuple args))) |
|
185 |
* in map mk_def (con_ty_list ~~ (1 upto ncon)) end; |
|
186 |
||
187 |
* (** Define the case operator **) |
|
188 |
||
189 |
* (*Combine split terms using case; yields the case operator for one part*) |
|
190 |
* fun call_case case_list = |
|
191 |
* let fun call_f (free,args) = |
|
192 |
ap_split T free (map (#2 o dest_Free) args) |
|
193 |
* in fold_bal (app sum_case) (map call_f case_list) end; |
|
194 |
||
195 |
* (** Generating function variables for the case definition |
|
196 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
|
197 |
||
198 |
* (*Treatment of a single constructor*) |
|
199 |
* fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = |
|
200 |
if Syntax.is_identifier id |
|
201 |
then (opno, |
|
202 |
(Free(case_name ^ "_" ^ id, T), args) :: cases) |
|
203 |
else (opno+1, |
|
204 |
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: |
|
205 |
cases) |
|
206 |
||
207 |
* (*Treatment of a list of constructors, for one part*) |
|
208 |
* fun add_case_list (con_ty_list, (opno,case_lists)) = |
|
209 |
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) |
|
210 |
in (opno', case_list :: case_lists) end; |
|
211 |
||
212 |
* (*Treatment of all parts*) |
|
213 |
* val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); |
|
214 |
||
215 |
* val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT); |
|
216 |
||
217 |
* val big_rec_name = space_implode "_" rec_names; |
|
218 |
||
219 |
* val big_case_name = big_rec_name ^ "_case"; |
|
220 |
||
221 |
* (*The list of all the function variables*) |
|
222 |
* val big_case_args = flat (map (map #1) case_lists); |
|
223 |
||
224 |
* val big_case_tm = |
|
225 |
list_comb (Const(big_case_name, big_case_typ), big_case_args); |
|
226 |
||
227 |
* val big_case_def = mk_defpair |
|
228 |
(big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); |
|
229 |
||
230 |
* (** Build the new theory **) |
|
231 |
||
232 |
* val const_decs = |
|
233 |
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); |
|
234 |
||
235 |
* val axpairs = |
|
236 |
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)) |
|
237 |
||
238 |
* in thy |> add_consts_i const_decs |> add_defs_i axpairs end; |
|
239 |
****************************************************************) |
|
240 |
end; |
|
241 |
||
242 |
||
243 |
||
244 |