wenzelm@23152
|
1 |
(* Title: HOLCF/Tools/fixrec_package.ML
|
wenzelm@23152
|
2 |
Author: Amber Telfer and Brian Huffman
|
wenzelm@23152
|
3 |
|
wenzelm@23152
|
4 |
Recursive function definition package for HOLCF.
|
wenzelm@23152
|
5 |
*)
|
wenzelm@23152
|
6 |
|
wenzelm@23152
|
7 |
signature FIXREC_PACKAGE =
|
wenzelm@23152
|
8 |
sig
|
wenzelm@30487
|
9 |
val add_fixrec: bool -> (binding * typ option * mixfix) list
|
wenzelm@30487
|
10 |
-> (Attrib.binding * term) list -> local_theory -> local_theory
|
wenzelm@30487
|
11 |
val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
|
huffman@30158
|
12 |
-> (Attrib.binding * string) list -> local_theory -> local_theory
|
wenzelm@30487
|
13 |
val add_fixpat: Thm.binding * term list -> theory -> theory
|
wenzelm@30487
|
14 |
val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
|
huffman@30131
|
15 |
val add_matchers: (string * string) list -> theory -> theory
|
huffman@30131
|
16 |
val setup: theory -> theory
|
wenzelm@23152
|
17 |
end;
|
wenzelm@23152
|
18 |
|
wenzelm@23152
|
19 |
structure FixrecPackage: FIXREC_PACKAGE =
|
wenzelm@23152
|
20 |
struct
|
wenzelm@23152
|
21 |
|
huffman@26045
|
22 |
val fix_eq2 = @{thm fix_eq2};
|
huffman@26045
|
23 |
val def_fix_ind = @{thm def_fix_ind};
|
wenzelm@23152
|
24 |
|
wenzelm@23152
|
25 |
|
wenzelm@23152
|
26 |
fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
|
wenzelm@23152
|
27 |
fun fixrec_eq_err thy s eq =
|
wenzelm@26939
|
28 |
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
|
wenzelm@23152
|
29 |
|
huffman@30132
|
30 |
(*************************************************************************)
|
huffman@30132
|
31 |
(***************************** building types ****************************)
|
huffman@30132
|
32 |
(*************************************************************************)
|
huffman@30132
|
33 |
|
wenzelm@23152
|
34 |
(* ->> is taken from holcf_logic.ML *)
|
huffman@30132
|
35 |
fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
|
wenzelm@23152
|
36 |
|
huffman@30132
|
37 |
infixr 6 ->>; val (op ->>) = cfunT;
|
huffman@30132
|
38 |
|
huffman@30912
|
39 |
fun cfunsT (Ts, U) = foldr cfunT U Ts;
|
huffman@30912
|
40 |
|
huffman@30132
|
41 |
fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
|
huffman@30132
|
42 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
|
huffman@30132
|
43 |
|
huffman@30132
|
44 |
fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
|
huffman@30132
|
45 |
| binder_cfun _ = [];
|
huffman@30132
|
46 |
|
huffman@30132
|
47 |
fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
|
huffman@30132
|
48 |
| body_cfun T = T;
|
huffman@30132
|
49 |
|
huffman@30132
|
50 |
fun strip_cfun T : typ list * typ =
|
huffman@30132
|
51 |
(binder_cfun T, body_cfun T);
|
huffman@30132
|
52 |
|
huffman@30132
|
53 |
fun maybeT T = Type(@{type_name "maybe"}, [T]);
|
huffman@30132
|
54 |
|
huffman@30132
|
55 |
fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
|
huffman@30132
|
56 |
| dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
|
huffman@30132
|
57 |
|
huffman@30132
|
58 |
fun tupleT [] = @{typ "unit"}
|
huffman@30132
|
59 |
| tupleT [T] = T
|
huffman@30132
|
60 |
| tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
|
huffman@30132
|
61 |
|
huffman@30912
|
62 |
fun matchT (T, U) =
|
huffman@30912
|
63 |
body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
|
huffman@30912
|
64 |
|
huffman@30132
|
65 |
|
huffman@30132
|
66 |
(*************************************************************************)
|
huffman@30132
|
67 |
(***************************** building terms ****************************)
|
huffman@30132
|
68 |
(*************************************************************************)
|
wenzelm@23152
|
69 |
|
wenzelm@23152
|
70 |
val mk_trp = HOLogic.mk_Trueprop;
|
wenzelm@23152
|
71 |
|
wenzelm@23152
|
72 |
(* splits a cterm into the right and lefthand sides of equality *)
|
wenzelm@23152
|
73 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
|
wenzelm@23152
|
74 |
|
wenzelm@23152
|
75 |
(* similar to Thm.head_of, but for continuous application *)
|
huffman@26045
|
76 |
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
|
wenzelm@23152
|
77 |
| chead_of u = u;
|
wenzelm@23152
|
78 |
|
huffman@30132
|
79 |
fun capply_const (S, T) =
|
huffman@30132
|
80 |
Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
|
huffman@30132
|
81 |
|
huffman@30132
|
82 |
fun cabs_const (S, T) =
|
huffman@30132
|
83 |
Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
|
huffman@30132
|
84 |
|
huffman@30132
|
85 |
fun mk_capply (t, u) =
|
huffman@30132
|
86 |
let val (S, T) =
|
huffman@30132
|
87 |
case Term.fastype_of t of
|
huffman@30132
|
88 |
Type(@{type_name "->"}, [S, T]) => (S, T)
|
huffman@30132
|
89 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
|
huffman@30132
|
90 |
in capply_const (S, T) $ t $ u end;
|
huffman@30132
|
91 |
|
huffman@30132
|
92 |
infix 0 ==; val (op ==) = Logic.mk_equals;
|
huffman@30132
|
93 |
infix 1 ===; val (op ===) = HOLogic.mk_eq;
|
huffman@30132
|
94 |
infix 9 ` ; val (op `) = mk_capply;
|
huffman@30132
|
95 |
|
huffman@30132
|
96 |
|
huffman@30132
|
97 |
fun mk_cpair (t, u) =
|
huffman@30132
|
98 |
let val T = Term.fastype_of t
|
huffman@30132
|
99 |
val U = Term.fastype_of u
|
huffman@30132
|
100 |
val cpairT = T ->> U ->> HOLogic.mk_prodT (T, U)
|
huffman@30132
|
101 |
in Const(@{const_name cpair}, cpairT) ` t ` u end;
|
huffman@30132
|
102 |
|
huffman@30132
|
103 |
fun mk_cfst t =
|
huffman@30132
|
104 |
let val T = Term.fastype_of t;
|
huffman@30132
|
105 |
val (U, _) = HOLogic.dest_prodT T;
|
huffman@30132
|
106 |
in Const(@{const_name cfst}, T ->> U) ` t end;
|
huffman@30132
|
107 |
|
huffman@30132
|
108 |
fun mk_csnd t =
|
huffman@30132
|
109 |
let val T = Term.fastype_of t;
|
huffman@30132
|
110 |
val (_, U) = HOLogic.dest_prodT T;
|
huffman@30132
|
111 |
in Const(@{const_name csnd}, T ->> U) ` t end;
|
huffman@30132
|
112 |
|
huffman@30132
|
113 |
fun mk_csplit t =
|
huffman@30132
|
114 |
let val (S, TU) = dest_cfunT (Term.fastype_of t);
|
huffman@30132
|
115 |
val (T, U) = dest_cfunT TU;
|
huffman@30132
|
116 |
val csplitT = (S ->> T ->> U) ->> HOLogic.mk_prodT (S, T) ->> U;
|
huffman@30132
|
117 |
in Const(@{const_name csplit}, csplitT) ` t end;
|
wenzelm@23152
|
118 |
|
wenzelm@23152
|
119 |
(* builds the expression (LAM v. rhs) *)
|
huffman@30132
|
120 |
fun big_lambda v rhs =
|
huffman@30132
|
121 |
cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
|
wenzelm@23152
|
122 |
|
wenzelm@23152
|
123 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *)
|
wenzelm@23152
|
124 |
fun big_lambdas [] rhs = rhs
|
wenzelm@23152
|
125 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
|
wenzelm@23152
|
126 |
|
wenzelm@23152
|
127 |
(* builds the expression (LAM <v1,v2,..,vn>. rhs) *)
|
huffman@30132
|
128 |
fun lambda_ctuple [] rhs = big_lambda (Free("unit", HOLogic.unitT)) rhs
|
wenzelm@23152
|
129 |
| lambda_ctuple (v::[]) rhs = big_lambda v rhs
|
wenzelm@23152
|
130 |
| lambda_ctuple (v::vs) rhs =
|
huffman@30132
|
131 |
mk_csplit (big_lambda v (lambda_ctuple vs rhs));
|
wenzelm@23152
|
132 |
|
wenzelm@23152
|
133 |
(* builds the expression <v1,v2,..,vn> *)
|
huffman@30132
|
134 |
fun mk_ctuple [] = @{term "UU::unit"}
|
wenzelm@23152
|
135 |
| mk_ctuple (t::[]) = t
|
huffman@30132
|
136 |
| mk_ctuple (t::ts) = mk_cpair (t, mk_ctuple ts);
|
huffman@30132
|
137 |
|
huffman@30132
|
138 |
fun mk_return t =
|
huffman@30132
|
139 |
let val T = Term.fastype_of t
|
huffman@30132
|
140 |
in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
|
huffman@30132
|
141 |
|
huffman@30132
|
142 |
fun mk_bind (t, u) =
|
huffman@30132
|
143 |
let val (T, mU) = dest_cfunT (Term.fastype_of u);
|
huffman@30132
|
144 |
val bindT = maybeT T ->> (T ->> mU) ->> mU;
|
huffman@30132
|
145 |
in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
|
huffman@30132
|
146 |
|
huffman@30132
|
147 |
fun mk_mplus (t, u) =
|
huffman@30132
|
148 |
let val mT = Term.fastype_of t
|
huffman@30132
|
149 |
in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
|
huffman@30132
|
150 |
|
huffman@30132
|
151 |
fun mk_run t =
|
huffman@30132
|
152 |
let val mT = Term.fastype_of t
|
huffman@30132
|
153 |
val T = dest_maybeT mT
|
huffman@30132
|
154 |
in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
|
huffman@30132
|
155 |
|
huffman@30132
|
156 |
fun mk_fix t =
|
huffman@30132
|
157 |
let val (T, _) = dest_cfunT (Term.fastype_of t)
|
huffman@30132
|
158 |
in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
|
wenzelm@23152
|
159 |
|
wenzelm@23152
|
160 |
(*************************************************************************)
|
wenzelm@23152
|
161 |
(************* fixed-point definitions and unfolding theorems ************)
|
wenzelm@23152
|
162 |
(*************************************************************************)
|
wenzelm@23152
|
163 |
|
huffman@30158
|
164 |
fun add_fixdefs
|
huffman@30158
|
165 |
(fixes : ((binding * typ) * mixfix) list)
|
huffman@30158
|
166 |
(spec : (Attrib.binding * term) list)
|
huffman@30158
|
167 |
(lthy : local_theory) =
|
wenzelm@23152
|
168 |
let
|
wenzelm@30227
|
169 |
val names = map (Binding.name_of o fst o fst) fixes;
|
huffman@30158
|
170 |
val all_names = space_implode "_" names;
|
huffman@30158
|
171 |
val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
|
huffman@30132
|
172 |
val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
|
wenzelm@23152
|
173 |
|
huffman@30158
|
174 |
fun one_def (l as Free(n,_)) r =
|
wenzelm@30364
|
175 |
let val b = Long_Name.base_name n
|
huffman@30158
|
176 |
in ((Binding.name (b^"_def"), []), r) end
|
wenzelm@23152
|
177 |
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
|
wenzelm@23152
|
178 |
fun defs [] _ = []
|
wenzelm@23152
|
179 |
| defs (l::[]) r = [one_def l r]
|
huffman@30132
|
180 |
| defs (l::ls) r = one_def l (mk_cfst r) :: defs ls (mk_csnd r);
|
huffman@30158
|
181 |
val fixdefs = defs lhss fixpoint;
|
huffman@30158
|
182 |
val define_all = fold_map (LocalTheory.define Thm.definitionK);
|
huffman@30158
|
183 |
val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
|
huffman@30158
|
184 |
|> define_all (map (apfst fst) fixes ~~ fixdefs);
|
huffman@30158
|
185 |
fun cpair_equalI (thm1, thm2) = @{thm cpair_equalI} OF [thm1, thm2];
|
huffman@30158
|
186 |
val ctuple_fixdef_thm = foldr1 cpair_equalI (map (snd o snd) fixdef_thms);
|
huffman@30158
|
187 |
val ctuple_induct_thm = ctuple_fixdef_thm RS def_fix_ind;
|
huffman@30158
|
188 |
val ctuple_unfold_thm =
|
huffman@30158
|
189 |
Goal.prove lthy' [] [] (mk_trp (mk_ctuple lhss === mk_ctuple rhss))
|
huffman@30158
|
190 |
(fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
|
huffman@30158
|
191 |
simp_tac (local_simpset_of lthy') 1]);
|
wenzelm@23152
|
192 |
fun unfolds [] thm = []
|
wenzelm@23152
|
193 |
| unfolds (n::[]) thm = [(n^"_unfold", thm)]
|
wenzelm@23152
|
194 |
| unfolds (n::ns) thm = let
|
wenzelm@25132
|
195 |
val thmL = thm RS @{thm cpair_eqD1};
|
wenzelm@25132
|
196 |
val thmR = thm RS @{thm cpair_eqD2};
|
wenzelm@23152
|
197 |
in (n^"_unfold", thmL) :: unfolds ns thmR end;
|
wenzelm@23152
|
198 |
val unfold_thms = unfolds names ctuple_unfold_thm;
|
huffman@30158
|
199 |
fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
|
huffman@30158
|
200 |
val (thmss, lthy'') = lthy'
|
huffman@30158
|
201 |
|> fold_map (LocalTheory.note Thm.theoremK o mk_note)
|
huffman@30158
|
202 |
((all_names ^ "_induct", ctuple_induct_thm) :: unfold_thms);
|
wenzelm@23152
|
203 |
in
|
huffman@30158
|
204 |
(lthy'', names, fixdef_thms, map snd unfold_thms)
|
wenzelm@23152
|
205 |
end;
|
wenzelm@23152
|
206 |
|
wenzelm@23152
|
207 |
(*************************************************************************)
|
wenzelm@23152
|
208 |
(*********** monadic notation and pattern matching compilation ***********)
|
wenzelm@23152
|
209 |
(*************************************************************************)
|
wenzelm@23152
|
210 |
|
huffman@30131
|
211 |
structure FixrecMatchData = TheoryDataFun (
|
huffman@30131
|
212 |
type T = string Symtab.table;
|
huffman@30131
|
213 |
val empty = Symtab.empty;
|
huffman@30131
|
214 |
val copy = I;
|
huffman@30131
|
215 |
val extend = I;
|
huffman@30131
|
216 |
fun merge _ tabs : T = Symtab.merge (K true) tabs;
|
huffman@30131
|
217 |
);
|
huffman@30131
|
218 |
|
huffman@30131
|
219 |
(* associate match functions with pattern constants *)
|
huffman@30131
|
220 |
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
|
huffman@30131
|
221 |
|
huffman@30157
|
222 |
fun taken_names (t : term) : bstring list =
|
huffman@30157
|
223 |
let
|
wenzelm@30364
|
224 |
fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
|
huffman@30157
|
225 |
| taken (Free(a,_) , bs) = insert (op =) a bs
|
huffman@30157
|
226 |
| taken (f $ u , bs) = taken (f, taken (u, bs))
|
huffman@30157
|
227 |
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
|
huffman@30157
|
228 |
| taken (_ , bs) = bs;
|
huffman@30157
|
229 |
in
|
huffman@30157
|
230 |
taken (t, [])
|
huffman@30157
|
231 |
end;
|
wenzelm@23152
|
232 |
|
wenzelm@23152
|
233 |
(* builds a monadic term for matching a constructor pattern *)
|
huffman@30131
|
234 |
fun pre_build match_name pat rhs vs taken =
|
wenzelm@23152
|
235 |
case pat of
|
huffman@26045
|
236 |
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
|
huffman@30131
|
237 |
pre_build match_name f rhs (v::vs) taken
|
huffman@26045
|
238 |
| Const(@{const_name Rep_CFun},_)$f$x =>
|
huffman@30131
|
239 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
|
huffman@30131
|
240 |
in pre_build match_name f rhs' (v::vs) taken' end
|
wenzelm@23152
|
241 |
| Const(c,T) =>
|
wenzelm@23152
|
242 |
let
|
wenzelm@23152
|
243 |
val n = Name.variant taken "v";
|
huffman@26045
|
244 |
fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
|
wenzelm@23152
|
245 |
| result_type T _ = T;
|
wenzelm@23152
|
246 |
val v = Free(n, result_type T vs);
|
huffman@30912
|
247 |
val m = Const(match_name c, matchT (T, fastype_of rhs));
|
huffman@30912
|
248 |
val k = big_lambdas vs rhs;
|
wenzelm@23152
|
249 |
in
|
huffman@30912
|
250 |
(m`v`k, v, n::taken)
|
wenzelm@23152
|
251 |
end
|
wenzelm@23152
|
252 |
| Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
|
wenzelm@23152
|
253 |
| _ => fixrec_err "pre_build: invalid pattern";
|
wenzelm@23152
|
254 |
|
wenzelm@23152
|
255 |
(* builds a monadic term for matching a function definition pattern *)
|
wenzelm@23152
|
256 |
(* returns (name, arity, matcher) *)
|
huffman@30131
|
257 |
fun building match_name pat rhs vs taken =
|
wenzelm@23152
|
258 |
case pat of
|
huffman@26045
|
259 |
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
|
huffman@30131
|
260 |
building match_name f rhs (v::vs) taken
|
huffman@26045
|
261 |
| Const(@{const_name Rep_CFun}, _)$f$x =>
|
huffman@30131
|
262 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
|
huffman@30131
|
263 |
in building match_name f rhs' (v::vs) taken' end
|
huffman@30158
|
264 |
| Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
|
huffman@30158
|
265 |
| Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
|
huffman@30158
|
266 |
| _ => fixrec_err ("function is not declared as constant in theory: "
|
huffman@30158
|
267 |
^ ML_Syntax.print_term pat);
|
wenzelm@23152
|
268 |
|
huffman@30158
|
269 |
fun strip_alls t =
|
huffman@30158
|
270 |
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
|
huffman@30158
|
271 |
|
huffman@30158
|
272 |
fun match_eq match_name eq =
|
huffman@30158
|
273 |
let
|
huffman@30158
|
274 |
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
|
huffman@30131
|
275 |
in
|
huffman@30157
|
276 |
building match_name lhs (mk_return rhs) [] (taken_names eq)
|
huffman@30131
|
277 |
end;
|
wenzelm@23152
|
278 |
|
wenzelm@23152
|
279 |
(* returns the sum (using +++) of the terms in ms *)
|
wenzelm@23152
|
280 |
(* also applies "run" to the result! *)
|
wenzelm@23152
|
281 |
fun fatbar arity ms =
|
wenzelm@23152
|
282 |
let
|
huffman@30132
|
283 |
fun LAM_Ts 0 t = ([], Term.fastype_of t)
|
huffman@30132
|
284 |
| LAM_Ts n (_ $ Abs(_,T,t)) =
|
huffman@30132
|
285 |
let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
|
huffman@30132
|
286 |
| LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
|
wenzelm@23152
|
287 |
fun unLAM 0 t = t
|
wenzelm@23152
|
288 |
| unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
|
wenzelm@23152
|
289 |
| unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
|
huffman@30132
|
290 |
fun reLAM ([], U) t = t
|
huffman@30132
|
291 |
| reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
|
huffman@30132
|
292 |
val msum = foldr1 mk_mplus (map (unLAM arity) ms);
|
huffman@30132
|
293 |
val (Ts, U) = LAM_Ts arity (hd ms)
|
wenzelm@23152
|
294 |
in
|
huffman@30132
|
295 |
reLAM (rev Ts, dest_maybeT U) (mk_run msum)
|
wenzelm@23152
|
296 |
end;
|
wenzelm@23152
|
297 |
|
wenzelm@23152
|
298 |
(* this is the pattern-matching compiler function *)
|
huffman@30158
|
299 |
fun compile_pats match_name eqs =
|
wenzelm@23152
|
300 |
let
|
huffman@30158
|
301 |
val (((n::names),(a::arities)),mats) =
|
huffman@30158
|
302 |
apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
|
wenzelm@23152
|
303 |
val cname = if forall (fn x => n=x) names then n
|
wenzelm@23152
|
304 |
else fixrec_err "all equations in block must define the same function";
|
wenzelm@23152
|
305 |
val arity = if forall (fn x => a=x) arities then a
|
wenzelm@23152
|
306 |
else fixrec_err "all equations in block must have the same arity";
|
wenzelm@23152
|
307 |
val rhs = fatbar arity mats;
|
wenzelm@23152
|
308 |
in
|
huffman@30132
|
309 |
mk_trp (cname === rhs)
|
wenzelm@23152
|
310 |
end;
|
wenzelm@23152
|
311 |
|
wenzelm@23152
|
312 |
(*************************************************************************)
|
wenzelm@23152
|
313 |
(********************** Proving associated theorems **********************)
|
wenzelm@23152
|
314 |
(*************************************************************************)
|
wenzelm@23152
|
315 |
|
wenzelm@23152
|
316 |
(* proves a block of pattern matching equations as theorems, using unfold *)
|
huffman@30158
|
317 |
fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
|
wenzelm@23152
|
318 |
let
|
huffman@30158
|
319 |
val tacs =
|
huffman@30158
|
320 |
[rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
|
huffman@30158
|
321 |
asm_simp_tac (local_simpset_of lthy) 1];
|
huffman@30158
|
322 |
fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
|
huffman@30158
|
323 |
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
|
wenzelm@23152
|
324 |
in
|
wenzelm@23152
|
325 |
map prove_eqn eqns
|
wenzelm@23152
|
326 |
end;
|
wenzelm@23152
|
327 |
|
wenzelm@23152
|
328 |
(*************************************************************************)
|
wenzelm@23152
|
329 |
(************************* Main fixrec function **************************)
|
wenzelm@23152
|
330 |
(*************************************************************************)
|
wenzelm@23152
|
331 |
|
huffman@30158
|
332 |
local
|
huffman@30158
|
333 |
(* code adapted from HOL/Tools/primrec_package.ML *)
|
huffman@30158
|
334 |
|
huffman@30158
|
335 |
fun gen_fixrec
|
huffman@30158
|
336 |
(set_group : bool)
|
wenzelm@30487
|
337 |
prep_spec
|
huffman@30158
|
338 |
(strict : bool)
|
huffman@30158
|
339 |
raw_fixes
|
huffman@30158
|
340 |
raw_spec
|
huffman@30158
|
341 |
(lthy : local_theory) =
|
huffman@30158
|
342 |
let
|
huffman@30158
|
343 |
val (fixes : ((binding * typ) * mixfix) list,
|
huffman@30158
|
344 |
spec : (Attrib.binding * term) list) =
|
wenzelm@30487
|
345 |
fst (prep_spec raw_fixes raw_spec lthy);
|
huffman@30158
|
346 |
val chead_of_spec =
|
huffman@30158
|
347 |
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
|
huffman@30158
|
348 |
fun name_of (Free (n, _)) = n
|
huffman@30158
|
349 |
| name_of t = fixrec_err ("unknown term");
|
huffman@30158
|
350 |
val all_names = map (name_of o chead_of_spec) spec;
|
huffman@30158
|
351 |
val names = distinct (op =) all_names;
|
huffman@30158
|
352 |
fun block_of_name n =
|
huffman@30158
|
353 |
map_filter
|
huffman@30158
|
354 |
(fn (m,eq) => if m = n then SOME eq else NONE)
|
huffman@30158
|
355 |
(all_names ~~ spec);
|
huffman@30158
|
356 |
val blocks = map block_of_name names;
|
huffman@30158
|
357 |
|
huffman@30158
|
358 |
val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
|
huffman@30131
|
359 |
fun match_name c =
|
huffman@30158
|
360 |
case Symtab.lookup matcher_tab c of SOME m => m
|
huffman@30158
|
361 |
| NONE => fixrec_err ("unknown pattern constructor: " ^ c);
|
huffman@30131
|
362 |
|
huffman@30158
|
363 |
val matches = map (compile_pats match_name) (map (map snd) blocks);
|
huffman@30158
|
364 |
val spec' = map (pair Attrib.empty_binding) matches;
|
huffman@30158
|
365 |
val (lthy', cnames, fixdef_thms, unfold_thms) =
|
huffman@30158
|
366 |
add_fixdefs fixes spec' lthy;
|
wenzelm@23152
|
367 |
in
|
wenzelm@23152
|
368 |
if strict then let (* only prove simp rules if strict = true *)
|
huffman@30158
|
369 |
val simps : (Attrib.binding * thm) list list =
|
huffman@30158
|
370 |
map (make_simps lthy') (unfold_thms ~~ blocks);
|
huffman@30158
|
371 |
fun mk_bind n : Attrib.binding =
|
huffman@30158
|
372 |
(Binding.name (n ^ "_simps"),
|
huffman@30158
|
373 |
[Attrib.internal (K Simplifier.simp_add)]);
|
huffman@30158
|
374 |
val simps1 : (Attrib.binding * thm list) list =
|
huffman@30158
|
375 |
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
|
huffman@30158
|
376 |
val simps2 : (Attrib.binding * thm list) list =
|
huffman@30158
|
377 |
map (apsnd (fn thm => [thm])) (List.concat simps);
|
huffman@30158
|
378 |
val (_, lthy'') = lthy'
|
huffman@30158
|
379 |
|> fold_map (LocalTheory.note Thm.theoremK) (simps1 @ simps2);
|
wenzelm@23152
|
380 |
in
|
huffman@30158
|
381 |
lthy''
|
wenzelm@23152
|
382 |
end
|
huffman@30158
|
383 |
else lthy'
|
wenzelm@23152
|
384 |
end;
|
wenzelm@23152
|
385 |
|
huffman@30158
|
386 |
in
|
wenzelm@23152
|
387 |
|
wenzelm@30487
|
388 |
val add_fixrec = gen_fixrec false Specification.check_spec;
|
wenzelm@30487
|
389 |
val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
|
huffman@30158
|
390 |
|
huffman@30158
|
391 |
end; (* local *)
|
wenzelm@23152
|
392 |
|
wenzelm@23152
|
393 |
(*************************************************************************)
|
wenzelm@23152
|
394 |
(******************************** Fixpat *********************************)
|
wenzelm@23152
|
395 |
(*************************************************************************)
|
wenzelm@23152
|
396 |
|
wenzelm@23152
|
397 |
fun fix_pat thy t =
|
wenzelm@23152
|
398 |
let
|
wenzelm@23152
|
399 |
val T = fastype_of t;
|
wenzelm@23152
|
400 |
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
|
wenzelm@23152
|
401 |
val cname = case chead_of t of Const(c,_) => c | _ =>
|
wenzelm@23152
|
402 |
fixrec_err "function is not declared as constant in theory";
|
wenzelm@26343
|
403 |
val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
|
wenzelm@23152
|
404 |
val simp = Goal.prove_global thy [] [] eq
|
wenzelm@23152
|
405 |
(fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
|
wenzelm@23152
|
406 |
in simp end;
|
wenzelm@23152
|
407 |
|
wenzelm@23152
|
408 |
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
|
wenzelm@23152
|
409 |
let
|
wenzelm@23152
|
410 |
val atts = map (prep_attrib thy) srcs;
|
wenzelm@23152
|
411 |
val ts = map (prep_term thy) strings;
|
wenzelm@23152
|
412 |
val simps = map (fix_pat thy) ts;
|
wenzelm@23152
|
413 |
in
|
haftmann@29585
|
414 |
(snd o PureThy.add_thmss [((name, simps), atts)]) thy
|
wenzelm@23152
|
415 |
end;
|
wenzelm@23152
|
416 |
|
wenzelm@30487
|
417 |
val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
|
wenzelm@30487
|
418 |
val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
|
wenzelm@23152
|
419 |
|
wenzelm@23152
|
420 |
|
wenzelm@23152
|
421 |
(*************************************************************************)
|
wenzelm@23152
|
422 |
(******************************** Parsers ********************************)
|
wenzelm@23152
|
423 |
(*************************************************************************)
|
wenzelm@23152
|
424 |
|
wenzelm@23152
|
425 |
local structure P = OuterParse and K = OuterKeyword in
|
wenzelm@23152
|
426 |
|
wenzelm@30487
|
427 |
val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
|
wenzelm@30487
|
428 |
((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
|
wenzelm@30487
|
429 |
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
|
wenzelm@23152
|
430 |
|
wenzelm@30487
|
431 |
val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
|
wenzelm@30487
|
432 |
(SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
|
huffman@30158
|
433 |
|
wenzelm@30487
|
434 |
end;
|
wenzelm@23152
|
435 |
|
huffman@30131
|
436 |
val setup = FixrecMatchData.init;
|
huffman@30131
|
437 |
|
wenzelm@24867
|
438 |
end;
|