haftmann@31738
|
1 |
(* Title: HOLCF/Tools/fixrec.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 |
|
haftmann@31738
|
7 |
signature FIXREC =
|
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@33414
|
16 |
val fixrec_simp_tac: Proof.context -> int -> tactic
|
huffman@30131
|
17 |
val setup: theory -> theory
|
wenzelm@23152
|
18 |
end;
|
wenzelm@23152
|
19 |
|
haftmann@31738
|
20 |
structure Fixrec :> FIXREC =
|
wenzelm@23152
|
21 |
struct
|
wenzelm@23152
|
22 |
|
huffman@35513
|
23 |
open HOLCF_Library;
|
huffman@35513
|
24 |
|
huffman@35513
|
25 |
infixr 6 ->>;
|
huffman@35513
|
26 |
infix -->>;
|
huffman@35513
|
27 |
infix 9 `;
|
huffman@35513
|
28 |
|
huffman@31095
|
29 |
val def_cont_fix_eq = @{thm def_cont_fix_eq};
|
huffman@31095
|
30 |
val def_cont_fix_ind = @{thm def_cont_fix_ind};
|
wenzelm@23152
|
31 |
|
wenzelm@23152
|
32 |
fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
|
wenzelm@23152
|
33 |
fun fixrec_eq_err thy s eq =
|
wenzelm@26939
|
34 |
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
|
wenzelm@23152
|
35 |
|
huffman@30132
|
36 |
(*************************************************************************)
|
huffman@30132
|
37 |
(***************************** building types ****************************)
|
huffman@30132
|
38 |
(*************************************************************************)
|
huffman@30132
|
39 |
|
huffman@33401
|
40 |
local
|
huffman@33401
|
41 |
|
huffman@35511
|
42 |
fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
|
huffman@33401
|
43 |
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
|
huffman@33401
|
44 |
| binder_cfun _ = [];
|
huffman@33401
|
45 |
|
huffman@35511
|
46 |
fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
|
huffman@33401
|
47 |
| body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
|
huffman@33401
|
48 |
| body_cfun T = T;
|
huffman@33401
|
49 |
|
huffman@33401
|
50 |
fun strip_cfun T : typ list * typ =
|
huffman@33401
|
51 |
(binder_cfun T, body_cfun T);
|
huffman@33401
|
52 |
|
huffman@33401
|
53 |
in
|
huffman@33401
|
54 |
|
huffman@35513
|
55 |
fun matcherT (T, U) =
|
huffman@35513
|
56 |
body_cfun T ->> (binder_cfun T -->> U) ->> U;
|
huffman@30912
|
57 |
|
huffman@33401
|
58 |
end
|
huffman@30132
|
59 |
|
huffman@30132
|
60 |
(*************************************************************************)
|
huffman@30132
|
61 |
(***************************** building terms ****************************)
|
huffman@30132
|
62 |
(*************************************************************************)
|
wenzelm@23152
|
63 |
|
wenzelm@23152
|
64 |
val mk_trp = HOLogic.mk_Trueprop;
|
wenzelm@23152
|
65 |
|
wenzelm@23152
|
66 |
(* splits a cterm into the right and lefthand sides of equality *)
|
wenzelm@23152
|
67 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
|
wenzelm@23152
|
68 |
|
wenzelm@23152
|
69 |
(* similar to Thm.head_of, but for continuous application *)
|
huffman@26045
|
70 |
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
|
wenzelm@23152
|
71 |
| chead_of u = u;
|
wenzelm@23152
|
72 |
|
huffman@30132
|
73 |
infix 0 ==; val (op ==) = Logic.mk_equals;
|
huffman@30132
|
74 |
infix 1 ===; val (op ===) = HOLogic.mk_eq;
|
huffman@30132
|
75 |
|
huffman@30132
|
76 |
fun mk_mplus (t, u) =
|
huffman@30132
|
77 |
let val mT = Term.fastype_of t
|
huffman@30132
|
78 |
in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
|
huffman@30132
|
79 |
|
huffman@30132
|
80 |
fun mk_run t =
|
huffman@30132
|
81 |
let val mT = Term.fastype_of t
|
huffman@35513
|
82 |
val T = dest_matchT mT
|
huffman@30132
|
83 |
in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
|
huffman@30132
|
84 |
|
huffman@31095
|
85 |
|
wenzelm@23152
|
86 |
(*************************************************************************)
|
wenzelm@23152
|
87 |
(************* fixed-point definitions and unfolding theorems ************)
|
wenzelm@23152
|
88 |
(*************************************************************************)
|
wenzelm@23152
|
89 |
|
wenzelm@33519
|
90 |
structure FixrecUnfoldData = Generic_Data
|
wenzelm@33519
|
91 |
(
|
huffman@33414
|
92 |
type T = thm Symtab.table;
|
huffman@33414
|
93 |
val empty = Symtab.empty;
|
huffman@33414
|
94 |
val extend = I;
|
wenzelm@33519
|
95 |
fun merge data : T = Symtab.merge (K true) data;
|
huffman@33414
|
96 |
);
|
huffman@33414
|
97 |
|
huffman@33414
|
98 |
local
|
huffman@33414
|
99 |
|
huffman@33414
|
100 |
fun name_of (Const (n, T)) = n
|
huffman@33414
|
101 |
| name_of (Free (n, T)) = n
|
huffman@35770
|
102 |
| name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]);
|
huffman@33414
|
103 |
|
huffman@33414
|
104 |
val lhs_name =
|
huffman@35770
|
105 |
name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
|
huffman@33414
|
106 |
|
huffman@33414
|
107 |
in
|
huffman@33414
|
108 |
|
wenzelm@33449
|
109 |
val add_unfold : attribute =
|
huffman@33414
|
110 |
Thm.declaration_attribute
|
huffman@33414
|
111 |
(fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th)));
|
huffman@33414
|
112 |
|
huffman@33414
|
113 |
end
|
huffman@33414
|
114 |
|
huffman@30158
|
115 |
fun add_fixdefs
|
huffman@30158
|
116 |
(fixes : ((binding * typ) * mixfix) list)
|
huffman@30158
|
117 |
(spec : (Attrib.binding * term) list)
|
huffman@30158
|
118 |
(lthy : local_theory) =
|
wenzelm@23152
|
119 |
let
|
huffman@31095
|
120 |
val thy = ProofContext.theory_of lthy;
|
wenzelm@30227
|
121 |
val names = map (Binding.name_of o fst o fst) fixes;
|
huffman@30158
|
122 |
val all_names = space_implode "_" names;
|
wenzelm@32149
|
123 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
|
huffman@31095
|
124 |
val functional = lambda_tuple lhss (mk_tuple rhss);
|
huffman@31095
|
125 |
val fixpoint = mk_fix (mk_cabs functional);
|
huffman@36987
|
126 |
|
huffman@31095
|
127 |
val cont_thm =
|
huffman@36987
|
128 |
let
|
huffman@36987
|
129 |
val prop = mk_trp (mk_cont functional);
|
huffman@36987
|
130 |
fun err () = error (
|
huffman@36987
|
131 |
"Continuity proof failed; please check that cont2cont rules\n" ^
|
huffman@36987
|
132 |
"are configured for all non-HOLCF constants.\n" ^
|
huffman@36987
|
133 |
"The error occurred for the goal statement:\n" ^
|
huffman@36987
|
134 |
Syntax.string_of_term lthy prop);
|
huffman@36987
|
135 |
fun check th = case Thm.nprems_of th of 0 => all_tac th | n => err ();
|
huffman@36987
|
136 |
val tac = simp_tac (simpset_of lthy) 1 THEN check;
|
huffman@36987
|
137 |
in
|
huffman@36987
|
138 |
Goal.prove lthy [] [] prop (K tac)
|
huffman@36987
|
139 |
end;
|
huffman@31095
|
140 |
|
huffman@30158
|
141 |
fun one_def (l as Free(n,_)) r =
|
wenzelm@30364
|
142 |
let val b = Long_Name.base_name n
|
huffman@30158
|
143 |
in ((Binding.name (b^"_def"), []), r) end
|
wenzelm@23152
|
144 |
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
|
wenzelm@23152
|
145 |
fun defs [] _ = []
|
wenzelm@23152
|
146 |
| defs (l::[]) r = [one_def l r]
|
huffman@31095
|
147 |
| defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
|
huffman@30158
|
148 |
val fixdefs = defs lhss fixpoint;
|
huffman@35772
|
149 |
val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy
|
wenzelm@33812
|
150 |
|> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs);
|
huffman@31095
|
151 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
|
huffman@31095
|
152 |
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
|
huffman@31095
|
153 |
val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
|
huffman@31095
|
154 |
val predicate = lambda_tuple lhss (list_comb (P, lhss));
|
huffman@31095
|
155 |
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
|
huffman@31095
|
156 |
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
|
wenzelm@35624
|
157 |
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
|
huffman@31095
|
158 |
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
|
huffman@35772
|
159 |
|> Local_Defs.unfold lthy @{thms split_conv};
|
wenzelm@23152
|
160 |
fun unfolds [] thm = []
|
huffman@33414
|
161 |
| unfolds (n::[]) thm = [(n, thm)]
|
wenzelm@23152
|
162 |
| unfolds (n::ns) thm = let
|
huffman@31095
|
163 |
val thmL = thm RS @{thm Pair_eqD1};
|
huffman@31095
|
164 |
val thmR = thm RS @{thm Pair_eqD2};
|
huffman@33414
|
165 |
in (n, thmL) :: unfolds ns thmR end;
|
huffman@31095
|
166 |
val unfold_thms = unfolds names tuple_unfold_thm;
|
huffman@33414
|
167 |
val induct_note : Attrib.binding * Thm.thm list =
|
huffman@33414
|
168 |
let
|
huffman@35769
|
169 |
val thm_name = Binding.qualify true all_names (Binding.name "induct");
|
huffman@33414
|
170 |
in
|
huffman@33414
|
171 |
((thm_name, []), [tuple_induct_thm])
|
huffman@33414
|
172 |
end;
|
huffman@33414
|
173 |
fun unfold_note (name, thm) : Attrib.binding * Thm.thm list =
|
huffman@33414
|
174 |
let
|
huffman@35769
|
175 |
val thm_name = Binding.qualify true name (Binding.name "unfold");
|
huffman@33414
|
176 |
val src = Attrib.internal (K add_unfold);
|
huffman@33414
|
177 |
in
|
huffman@33414
|
178 |
((thm_name, [src]), [thm])
|
huffman@33414
|
179 |
end;
|
huffman@35772
|
180 |
val (thmss, lthy) = lthy
|
wenzelm@33673
|
181 |
|> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms);
|
wenzelm@23152
|
182 |
in
|
huffman@35772
|
183 |
(lthy, names, fixdef_thms, map snd unfold_thms)
|
wenzelm@23152
|
184 |
end;
|
wenzelm@23152
|
185 |
|
wenzelm@23152
|
186 |
(*************************************************************************)
|
wenzelm@23152
|
187 |
(*********** monadic notation and pattern matching compilation ***********)
|
wenzelm@23152
|
188 |
(*************************************************************************)
|
wenzelm@23152
|
189 |
|
wenzelm@33522
|
190 |
structure FixrecMatchData = Theory_Data
|
wenzelm@33522
|
191 |
(
|
huffman@30131
|
192 |
type T = string Symtab.table;
|
huffman@30131
|
193 |
val empty = Symtab.empty;
|
huffman@30131
|
194 |
val extend = I;
|
wenzelm@33522
|
195 |
fun merge data = Symtab.merge (K true) data;
|
huffman@30131
|
196 |
);
|
huffman@30131
|
197 |
|
huffman@30131
|
198 |
(* associate match functions with pattern constants *)
|
huffman@30131
|
199 |
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
|
huffman@30131
|
200 |
|
huffman@30157
|
201 |
fun taken_names (t : term) : bstring list =
|
huffman@30157
|
202 |
let
|
wenzelm@30364
|
203 |
fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
|
huffman@30157
|
204 |
| taken (Free(a,_) , bs) = insert (op =) a bs
|
huffman@30157
|
205 |
| taken (f $ u , bs) = taken (f, taken (u, bs))
|
huffman@30157
|
206 |
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
|
huffman@30157
|
207 |
| taken (_ , bs) = bs;
|
huffman@30157
|
208 |
in
|
huffman@30157
|
209 |
taken (t, [])
|
huffman@30157
|
210 |
end;
|
wenzelm@23152
|
211 |
|
wenzelm@23152
|
212 |
(* builds a monadic term for matching a constructor pattern *)
|
huffman@30131
|
213 |
fun pre_build match_name pat rhs vs taken =
|
wenzelm@23152
|
214 |
case pat of
|
huffman@26045
|
215 |
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
|
huffman@30131
|
216 |
pre_build match_name f rhs (v::vs) taken
|
huffman@26045
|
217 |
| Const(@{const_name Rep_CFun},_)$f$x =>
|
huffman@30131
|
218 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
|
huffman@30131
|
219 |
in pre_build match_name f rhs' (v::vs) taken' end
|
huffman@33401
|
220 |
| f$(v as Free(n,T)) =>
|
huffman@33401
|
221 |
pre_build match_name f rhs (v::vs) taken
|
huffman@33401
|
222 |
| f$x =>
|
huffman@33401
|
223 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
|
huffman@33401
|
224 |
in pre_build match_name f rhs' (v::vs) taken' end
|
wenzelm@23152
|
225 |
| Const(c,T) =>
|
wenzelm@23152
|
226 |
let
|
wenzelm@23152
|
227 |
val n = Name.variant taken "v";
|
huffman@35511
|
228 |
fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
|
huffman@33401
|
229 |
| result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
|
wenzelm@23152
|
230 |
| result_type T _ = T;
|
wenzelm@23152
|
231 |
val v = Free(n, result_type T vs);
|
huffman@35513
|
232 |
val m = Const(match_name c, matcherT (T, fastype_of rhs));
|
huffman@30912
|
233 |
val k = big_lambdas vs rhs;
|
wenzelm@23152
|
234 |
in
|
huffman@30912
|
235 |
(m`v`k, v, n::taken)
|
wenzelm@23152
|
236 |
end
|
wenzelm@23152
|
237 |
| Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
|
wenzelm@23152
|
238 |
| _ => fixrec_err "pre_build: invalid pattern";
|
wenzelm@23152
|
239 |
|
wenzelm@23152
|
240 |
(* builds a monadic term for matching a function definition pattern *)
|
wenzelm@23152
|
241 |
(* returns (name, arity, matcher) *)
|
huffman@30131
|
242 |
fun building match_name pat rhs vs taken =
|
wenzelm@23152
|
243 |
case pat of
|
huffman@26045
|
244 |
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
|
huffman@30131
|
245 |
building match_name f rhs (v::vs) taken
|
huffman@26045
|
246 |
| Const(@{const_name Rep_CFun}, _)$f$x =>
|
huffman@30131
|
247 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
|
huffman@30131
|
248 |
in building match_name f rhs' (v::vs) taken' end
|
huffman@30158
|
249 |
| Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
|
huffman@30158
|
250 |
| Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
|
huffman@30158
|
251 |
| _ => fixrec_err ("function is not declared as constant in theory: "
|
huffman@30158
|
252 |
^ ML_Syntax.print_term pat);
|
wenzelm@23152
|
253 |
|
huffman@30158
|
254 |
fun strip_alls t =
|
huffman@30158
|
255 |
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
|
huffman@30158
|
256 |
|
huffman@30158
|
257 |
fun match_eq match_name eq =
|
huffman@30158
|
258 |
let
|
huffman@30158
|
259 |
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
|
huffman@30131
|
260 |
in
|
huffman@30157
|
261 |
building match_name lhs (mk_return rhs) [] (taken_names eq)
|
huffman@30131
|
262 |
end;
|
wenzelm@23152
|
263 |
|
wenzelm@23152
|
264 |
(* returns the sum (using +++) of the terms in ms *)
|
wenzelm@23152
|
265 |
(* also applies "run" to the result! *)
|
wenzelm@23152
|
266 |
fun fatbar arity ms =
|
wenzelm@23152
|
267 |
let
|
huffman@30132
|
268 |
fun LAM_Ts 0 t = ([], Term.fastype_of t)
|
huffman@30132
|
269 |
| LAM_Ts n (_ $ Abs(_,T,t)) =
|
huffman@30132
|
270 |
let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
|
huffman@30132
|
271 |
| LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
|
wenzelm@23152
|
272 |
fun unLAM 0 t = t
|
wenzelm@23152
|
273 |
| unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
|
wenzelm@23152
|
274 |
| unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
|
huffman@30132
|
275 |
fun reLAM ([], U) t = t
|
huffman@30132
|
276 |
| reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
|
huffman@30132
|
277 |
val msum = foldr1 mk_mplus (map (unLAM arity) ms);
|
huffman@30132
|
278 |
val (Ts, U) = LAM_Ts arity (hd ms)
|
wenzelm@23152
|
279 |
in
|
huffman@35513
|
280 |
reLAM (rev Ts, dest_matchT U) (mk_run msum)
|
wenzelm@23152
|
281 |
end;
|
wenzelm@23152
|
282 |
|
wenzelm@23152
|
283 |
(* this is the pattern-matching compiler function *)
|
huffman@30158
|
284 |
fun compile_pats match_name eqs =
|
wenzelm@23152
|
285 |
let
|
huffman@35901
|
286 |
val ((names, arities), mats) =
|
huffman@30158
|
287 |
apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
|
huffman@35901
|
288 |
val cname =
|
huffman@35901
|
289 |
case distinct (op =) names of
|
huffman@35901
|
290 |
[n] => n
|
huffman@35901
|
291 |
| _ => fixrec_err "all equations in block must define the same function";
|
huffman@35901
|
292 |
val arity =
|
huffman@35901
|
293 |
case distinct (op =) arities of
|
huffman@35901
|
294 |
[a] => a
|
huffman@35901
|
295 |
| _ => fixrec_err "all equations in block must have the same arity";
|
wenzelm@23152
|
296 |
val rhs = fatbar arity mats;
|
wenzelm@23152
|
297 |
in
|
huffman@30132
|
298 |
mk_trp (cname === rhs)
|
wenzelm@23152
|
299 |
end;
|
wenzelm@23152
|
300 |
|
wenzelm@23152
|
301 |
(*************************************************************************)
|
wenzelm@23152
|
302 |
(********************** Proving associated theorems **********************)
|
wenzelm@23152
|
303 |
(*************************************************************************)
|
wenzelm@23152
|
304 |
|
huffman@37064
|
305 |
(* tactic to perform eta-contraction on subgoal *)
|
huffman@37064
|
306 |
fun eta_tac (ctxt : Proof.context) : int -> tactic =
|
huffman@37064
|
307 |
EqSubst.eqsubst_tac ctxt [0] @{thms refl};
|
huffman@33414
|
308 |
|
huffman@33414
|
309 |
fun fixrec_simp_tac ctxt =
|
huffman@33414
|
310 |
let
|
huffman@33414
|
311 |
val tab = FixrecUnfoldData.get (Context.Proof ctxt);
|
huffman@37064
|
312 |
val ss = Simplifier.simpset_of ctxt;
|
huffman@33414
|
313 |
fun concl t =
|
huffman@33414
|
314 |
if Logic.is_all t then concl (snd (Logic.dest_all t))
|
huffman@33414
|
315 |
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
|
huffman@33414
|
316 |
fun tac (t, i) =
|
huffman@33419
|
317 |
let
|
huffman@35901
|
318 |
val (c, T) =
|
huffman@35901
|
319 |
(dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t;
|
huffman@33419
|
320 |
val unfold_thm = the (Symtab.lookup tab c);
|
huffman@33419
|
321 |
val rule = unfold_thm RS @{thm ssubst_lhs};
|
huffman@33419
|
322 |
in
|
huffman@37064
|
323 |
CHANGED (rtac rule i THEN eta_tac ctxt i THEN asm_simp_tac ss i)
|
huffman@33419
|
324 |
end
|
huffman@33414
|
325 |
in
|
huffman@33505
|
326 |
SUBGOAL (fn ti => the_default no_tac (try tac ti))
|
huffman@33414
|
327 |
end;
|
huffman@33414
|
328 |
|
wenzelm@23152
|
329 |
(* proves a block of pattern matching equations as theorems, using unfold *)
|
wenzelm@32149
|
330 |
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
|
wenzelm@23152
|
331 |
let
|
huffman@37064
|
332 |
val ss = Simplifier.simpset_of ctxt;
|
huffman@36616
|
333 |
val rule = unfold_thm RS @{thm ssubst_lhs};
|
huffman@37064
|
334 |
val tac = rtac rule 1 THEN eta_tac ctxt 1 THEN asm_simp_tac ss 1;
|
huffman@36616
|
335 |
fun prove_term t = Goal.prove ctxt [] [] t (K tac);
|
huffman@30158
|
336 |
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
|
wenzelm@23152
|
337 |
in
|
wenzelm@23152
|
338 |
map prove_eqn eqns
|
wenzelm@23152
|
339 |
end;
|
wenzelm@23152
|
340 |
|
wenzelm@23152
|
341 |
(*************************************************************************)
|
wenzelm@23152
|
342 |
(************************* Main fixrec function **************************)
|
wenzelm@23152
|
343 |
(*************************************************************************)
|
wenzelm@23152
|
344 |
|
huffman@30158
|
345 |
local
|
haftmann@31738
|
346 |
(* code adapted from HOL/Tools/primrec.ML *)
|
huffman@30158
|
347 |
|
huffman@30158
|
348 |
fun gen_fixrec
|
wenzelm@30487
|
349 |
prep_spec
|
huffman@30158
|
350 |
(strict : bool)
|
huffman@30158
|
351 |
raw_fixes
|
huffman@30158
|
352 |
raw_spec
|
huffman@30158
|
353 |
(lthy : local_theory) =
|
huffman@30158
|
354 |
let
|
huffman@30158
|
355 |
val (fixes : ((binding * typ) * mixfix) list,
|
huffman@30158
|
356 |
spec : (Attrib.binding * term) list) =
|
wenzelm@30487
|
357 |
fst (prep_spec raw_fixes raw_spec lthy);
|
huffman@30158
|
358 |
val chead_of_spec =
|
huffman@30158
|
359 |
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
|
huffman@30158
|
360 |
fun name_of (Free (n, _)) = n
|
huffman@30158
|
361 |
| name_of t = fixrec_err ("unknown term");
|
huffman@30158
|
362 |
val all_names = map (name_of o chead_of_spec) spec;
|
huffman@30158
|
363 |
val names = distinct (op =) all_names;
|
huffman@30158
|
364 |
fun block_of_name n =
|
huffman@30158
|
365 |
map_filter
|
huffman@30158
|
366 |
(fn (m,eq) => if m = n then SOME eq else NONE)
|
huffman@30158
|
367 |
(all_names ~~ spec);
|
huffman@30158
|
368 |
val blocks = map block_of_name names;
|
huffman@30158
|
369 |
|
huffman@30158
|
370 |
val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
|
huffman@30131
|
371 |
fun match_name c =
|
huffman@30158
|
372 |
case Symtab.lookup matcher_tab c of SOME m => m
|
huffman@30158
|
373 |
| NONE => fixrec_err ("unknown pattern constructor: " ^ c);
|
huffman@30131
|
374 |
|
huffman@30158
|
375 |
val matches = map (compile_pats match_name) (map (map snd) blocks);
|
huffman@30158
|
376 |
val spec' = map (pair Attrib.empty_binding) matches;
|
huffman@35772
|
377 |
val (lthy, cnames, fixdef_thms, unfold_thms) =
|
huffman@30158
|
378 |
add_fixdefs fixes spec' lthy;
|
wenzelm@23152
|
379 |
in
|
wenzelm@23152
|
380 |
if strict then let (* only prove simp rules if strict = true *)
|
huffman@30158
|
381 |
val simps : (Attrib.binding * thm) list list =
|
huffman@35772
|
382 |
map (make_simps lthy) (unfold_thms ~~ blocks);
|
huffman@30158
|
383 |
fun mk_bind n : Attrib.binding =
|
huffman@35769
|
384 |
(Binding.qualify true n (Binding.name "simps"),
|
huffman@30158
|
385 |
[Attrib.internal (K Simplifier.simp_add)]);
|
huffman@30158
|
386 |
val simps1 : (Attrib.binding * thm list) list =
|
huffman@30158
|
387 |
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
|
huffman@30158
|
388 |
val simps2 : (Attrib.binding * thm list) list =
|
wenzelm@32952
|
389 |
map (apsnd (fn thm => [thm])) (flat simps);
|
huffman@35772
|
390 |
val (_, lthy) = lthy
|
wenzelm@33673
|
391 |
|> fold_map Local_Theory.note (simps1 @ simps2);
|
wenzelm@23152
|
392 |
in
|
huffman@35772
|
393 |
lthy
|
wenzelm@23152
|
394 |
end
|
huffman@35772
|
395 |
else lthy
|
wenzelm@23152
|
396 |
end;
|
wenzelm@23152
|
397 |
|
huffman@30158
|
398 |
in
|
wenzelm@23152
|
399 |
|
wenzelm@33736
|
400 |
val add_fixrec = gen_fixrec Specification.check_spec;
|
wenzelm@33736
|
401 |
val add_fixrec_cmd = gen_fixrec Specification.read_spec;
|
huffman@30158
|
402 |
|
huffman@30158
|
403 |
end; (* local *)
|
wenzelm@23152
|
404 |
|
wenzelm@23152
|
405 |
(*************************************************************************)
|
wenzelm@23152
|
406 |
(******************************** Fixpat *********************************)
|
wenzelm@23152
|
407 |
(*************************************************************************)
|
wenzelm@23152
|
408 |
|
wenzelm@23152
|
409 |
fun fix_pat thy t =
|
wenzelm@23152
|
410 |
let
|
wenzelm@23152
|
411 |
val T = fastype_of t;
|
wenzelm@23152
|
412 |
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
|
wenzelm@23152
|
413 |
val cname = case chead_of t of Const(c,_) => c | _ =>
|
wenzelm@23152
|
414 |
fixrec_err "function is not declared as constant in theory";
|
huffman@35769
|
415 |
val unfold_thm = PureThy.get_thm thy (cname^".unfold");
|
wenzelm@23152
|
416 |
val simp = Goal.prove_global thy [] [] eq
|
wenzelm@32149
|
417 |
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
|
wenzelm@23152
|
418 |
in simp end;
|
wenzelm@23152
|
419 |
|
wenzelm@23152
|
420 |
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
|
wenzelm@23152
|
421 |
let
|
wenzelm@36872
|
422 |
val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
|
wenzelm@23152
|
423 |
val atts = map (prep_attrib thy) srcs;
|
wenzelm@23152
|
424 |
val ts = map (prep_term thy) strings;
|
wenzelm@23152
|
425 |
val simps = map (fix_pat thy) ts;
|
wenzelm@23152
|
426 |
in
|
haftmann@29585
|
427 |
(snd o PureThy.add_thmss [((name, simps), atts)]) thy
|
wenzelm@23152
|
428 |
end;
|
wenzelm@23152
|
429 |
|
wenzelm@30487
|
430 |
val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
|
wenzelm@30487
|
431 |
val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
|
wenzelm@23152
|
432 |
|
wenzelm@23152
|
433 |
|
wenzelm@23152
|
434 |
(*************************************************************************)
|
wenzelm@23152
|
435 |
(******************************** Parsers ********************************)
|
wenzelm@23152
|
436 |
(*************************************************************************)
|
wenzelm@23152
|
437 |
|
wenzelm@36970
|
438 |
val _ =
|
wenzelm@36970
|
439 |
Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
|
wenzelm@36970
|
440 |
((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
|
wenzelm@36970
|
441 |
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
|
wenzelm@23152
|
442 |
|
wenzelm@36970
|
443 |
val _ =
|
wenzelm@36970
|
444 |
Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
|
wenzelm@36970
|
445 |
(Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
|
wenzelm@23152
|
446 |
|
huffman@33414
|
447 |
val setup =
|
huffman@37064
|
448 |
Method.setup @{binding fixrec_simp}
|
huffman@37064
|
449 |
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
|
huffman@37064
|
450 |
"pattern prover for fixrec constants";
|
huffman@30131
|
451 |
|
wenzelm@24867
|
452 |
end;
|