author | wenzelm |
Tue, 06 May 1997 15:27:35 +0200 | |
changeset 3118 | 24dae6222579 |
parent 2995 | 84df3b150b67 |
child 3768 | 67f4ac759100 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/add_ind_def.ML |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 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 |
||
1465 | 32 |
signature FP = (** Description of a fixed point operator **) |
923 | 33 |
sig |
2859 | 34 |
val checkThy : theory -> unit (*signals error if Lfp/Gfp is missing*) |
1465 | 35 |
val oper : string * typ * term -> term (*fixed point operator*) |
2859 | 36 |
val Tarski : thm (*Tarski's fixed point theorem*) |
37 |
val induct : thm (*induction/coinduction rule*) |
|
923 | 38 |
end; |
39 |
||
40 |
||
41 |
signature ADD_INDUCTIVE_DEF = |
|
42 |
sig |
|
43 |
val add_fp_def_i : term list * term list -> theory -> theory |
|
44 |
end; |
|
45 |
||
46 |
||
47 |
||
48 |
(*Declares functions to add fixedpoint/constructor defs to a theory*) |
|
49 |
functor Add_inductive_def_Fun (Fp: FP) : ADD_INDUCTIVE_DEF = |
|
50 |
struct |
|
1397 | 51 |
open Ind_Syntax; |
923 | 52 |
|
53 |
(*internal version*) |
|
54 |
fun add_fp_def_i (rec_tms, intr_tms) thy = |
|
55 |
let |
|
2859 | 56 |
val dummy = Fp.checkThy thy (*has essential ancestors?*) |
57 |
||
923 | 58 |
val sign = sign_of thy; |
59 |
||
1189 | 60 |
(*rec_params should agree for all mutually recursive components*) |
923 | 61 |
val rec_hds = map head_of rec_tms; |
62 |
||
63 |
val _ = assert_all is_Const rec_hds |
|
1465 | 64 |
(fn t => "Recursive set not previously declared as constant: " ^ |
65 |
Sign.string_of_term sign t); |
|
923 | 66 |
|
67 |
(*Now we know they are all Consts, so get their names, type and params*) |
|
68 |
val rec_names = map (#1 o dest_Const) rec_hds |
|
69 |
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
|
70 |
||
71 |
val _ = assert_all Syntax.is_identifier rec_names |
|
72 |
(fn a => "Name of recursive set not an identifier: " ^ a); |
|
73 |
||
74 |
local (*Checking the introduction rules*) |
|
75 |
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
|
76 |
fun intr_ok set = |
|
1465 | 77 |
case head_of set of Const(a,_) => a mem rec_names | _ => false; |
923 | 78 |
in |
79 |
val _ = assert_all intr_ok intr_sets |
|
1465 | 80 |
(fn t => "Conclusion of rule does not name a recursive set: " ^ |
81 |
Sign.string_of_term sign t); |
|
923 | 82 |
end; |
83 |
||
84 |
val _ = assert_all is_Free rec_params |
|
1465 | 85 |
(fn t => "Param in recursion term not a free variable: " ^ |
86 |
Sign.string_of_term sign t); |
|
923 | 87 |
|
88 |
(*** Construct the lfp definition ***) |
|
89 |
val mk_variant = variant (foldr add_term_names (intr_tms,[])); |
|
90 |
||
91 |
val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w"; |
|
92 |
||
1189 | 93 |
(*Mutual recursion ?? *) |
2995
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
94 |
val dom_set = body_type recT |
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
95 |
val dom_sumT = dest_setT dom_set |
923 | 96 |
|
97 |
val freez = Free(z, dom_sumT) |
|
98 |
and freeX = Free(X, dom_set); |
|
99 |
||
100 |
fun dest_tprop (Const("Trueprop",_) $ P) = P |
|
101 |
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |
|
1465 | 102 |
Sign.string_of_term sign Q); |
923 | 103 |
|
104 |
(*Makes a disjunct from an introduction rule*) |
|
105 |
fun lfp_part intr = (*quantify over rule's free vars except parameters*) |
|
1397 | 106 |
let val prems = map dest_tprop (Logic.strip_imp_prems intr) |
1465 | 107 |
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds |
108 |
val exfrees = term_frees intr \\ rec_params |
|
109 |
val zeq = eq_const dom_sumT $ freez $ (#1 (rule_concl intr)) |
|
923 | 110 |
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end; |
111 |
||
112 |
(*The Part(A,h) terms -- compose injections to make h*) |
|
1465 | 113 |
fun mk_Part (Bound 0, _) = freeX (*no mutual rec, no Part needed*) |
923 | 114 |
| mk_Part (h, domT) = |
1465 | 115 |
let val goodh = mend_sum_types (h, dom_sumT) |
923 | 116 |
and Part_const = |
1465 | 117 |
Const("Part", [dom_set, domT-->dom_sumT]---> dom_set) |
923 | 118 |
in Part_const $ freeX $ Abs(w,domT,goodh) end; |
119 |
||
2995
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
120 |
(*Access to balanced disjoint sums via injections?? |
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
121 |
Mutual recursion is NOT supported*) |
2270 | 122 |
val parts = ListPair.map mk_Part |
2995
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
123 |
(accesses_bal (ap Inl, ap Inr, Bound 0) 1, |
84df3b150b67
Disabled the attempts for mutual induction to work so that single induction
paulson
parents:
2859
diff
changeset
|
124 |
[dom_set]); |
923 | 125 |
|
126 |
(*replace each set by the corresponding Part(A,h)*) |
|
127 |
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; |
|
128 |
||
129 |
val lfp_rhs = Fp.oper(X, dom_sumT, |
|
1465 | 130 |
mk_Collect(z, dom_sumT, |
131 |
fold_bal (app disj) part_intrs)) |
|
923 | 132 |
|
133 |
||
134 |
(*** Make the new theory ***) |
|
135 |
||
136 |
(*A key definition: |
|
137 |
If no mutual recursion then it equals the one recursive set. |
|
138 |
If mutual recursion then it differs from all the recursive sets. *) |
|
139 |
val big_rec_name = space_implode "_" rec_names; |
|
140 |
||
141 |
(*Big_rec... is the union of the mutually recursive sets*) |
|
142 |
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); |
|
143 |
||
144 |
(*The individual sets must already be declared*) |
|
145 |
val axpairs = map mk_defpair |
|
1465 | 146 |
((big_rec_tm, lfp_rhs) :: |
147 |
(case parts of |
|
148 |
[_] => [] (*no mutual recursion*) |
|
149 |
| _ => rec_tms ~~ (*define the sets as Parts*) |
|
150 |
map (subst_atomic [(freeX, big_rec_tm)]) parts)); |
|
923 | 151 |
|
152 |
val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs |
|
153 |
||
1397 | 154 |
(*Detect occurrences of operator, even with other types!*) |
155 |
val _ = (case rec_names inter (add_term_names (lfp_rhs,[])) of |
|
1465 | 156 |
[] => () |
157 |
| x::_ => error ("Illegal occurrence of recursion op: " ^ x ^ |
|
1397 | 158 |
"\n\t*Consider adding type constraints*")) |
159 |
||
923 | 160 |
in thy |> add_defs_i axpairs end |
161 |
||
162 |
||
163 |
(****************************************************************OMITTED |
|
164 |
||
165 |
(*Expects the recursive sets to have been defined already. |
|
166 |
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) |
|
167 |
fun add_constructs_def (rec_names, con_ty_lists) thy = |
|
168 |
* let |
|
169 |
* val _ = writeln" Defining the constructor functions..."; |
|
1465 | 170 |
* val case_name = "f"; (*name for case variables*) |
923 | 171 |
|
172 |
* (** Define the constructors **) |
|
173 |
||
174 |
* (*The empty tuple is 0*) |
|
175 |
* fun mk_tuple [] = Const("0",iT) |
|
176 |
* | mk_tuple args = foldr1 mk_Pair args; |
|
177 |
||
178 |
* fun mk_inject n k u = access_bal(ap Inl, ap Inr, u) n k; |
|
179 |
||
1465 | 180 |
* val npart = length rec_names; (*total # of mutually recursive parts*) |
923 | 181 |
|
182 |
* (*Make constructor definition; kpart is # of this mutually recursive part*) |
|
183 |
* fun mk_con_defs (kpart, con_ty_list) = |
|
1465 | 184 |
* let val ncon = length con_ty_list (*number of constructors*) |
185 |
fun mk_def (((id,T,syn), name, args, prems), kcon) = |
|
186 |
(*kcon is index of constructor*) |
|
187 |
mk_defpair (list_comb (Const(name,T), args), |
|
188 |
mk_inject npart kpart |
|
189 |
(mk_inject ncon kcon (mk_tuple args))) |
|
2270 | 190 |
* in ListPair.map mk_def (con_ty_list, (1 upto ncon)) end; |
923 | 191 |
|
192 |
* (** Define the case operator **) |
|
193 |
||
194 |
* (*Combine split terms using case; yields the case operator for one part*) |
|
195 |
* fun call_case case_list = |
|
196 |
* let fun call_f (free,args) = |
|
1465 | 197 |
ap_split T free (map (#2 o dest_Free) args) |
923 | 198 |
* in fold_bal (app sum_case) (map call_f case_list) end; |
199 |
||
200 |
* (** Generating function variables for the case definition |
|
1465 | 201 |
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) |
923 | 202 |
|
203 |
* (*Treatment of a single constructor*) |
|
204 |
* fun add_case (((id,T,syn), name, args, prems), (opno,cases)) = |
|
1465 | 205 |
if Syntax.is_identifier id |
206 |
then (opno, |
|
207 |
(Free(case_name ^ "_" ^ id, T), args) :: cases) |
|
208 |
else (opno+1, |
|
209 |
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: |
|
210 |
cases) |
|
923 | 211 |
|
212 |
* (*Treatment of a list of constructors, for one part*) |
|
213 |
* fun add_case_list (con_ty_list, (opno,case_lists)) = |
|
1465 | 214 |
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[])) |
215 |
in (opno', case_list :: case_lists) end; |
|
923 | 216 |
|
217 |
* (*Treatment of all parts*) |
|
218 |
* val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); |
|
219 |
||
220 |
* val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT); |
|
221 |
||
222 |
* val big_rec_name = space_implode "_" rec_names; |
|
223 |
||
224 |
* val big_case_name = big_rec_name ^ "_case"; |
|
225 |
||
226 |
* (*The list of all the function variables*) |
|
227 |
* val big_case_args = flat (map (map #1) case_lists); |
|
228 |
||
229 |
* val big_case_tm = |
|
1465 | 230 |
list_comb (Const(big_case_name, big_case_typ), big_case_args); |
923 | 231 |
|
232 |
* val big_case_def = mk_defpair |
|
1465 | 233 |
(big_case_tm, fold_bal (app sum_case) (map call_case case_lists)); |
923 | 234 |
|
235 |
* (** Build the new theory **) |
|
236 |
||
237 |
* val const_decs = |
|
1465 | 238 |
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); |
923 | 239 |
|
240 |
* val axpairs = |
|
2270 | 241 |
big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists)) |
923 | 242 |
|
243 |
* in thy |> add_consts_i const_decs |> add_defs_i axpairs end; |
|
244 |
****************************************************************) |
|
245 |
end; |
|
246 |
||
247 |
||
248 |
||
249 |