|
1 (* Title: HOL/Tools/Function/function_core.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A package for general recursive function definitions: |
|
5 Main functionality. |
|
6 *) |
|
7 |
|
8 signature FUNCTION_CORE = |
|
9 sig |
|
10 val trace: bool Unsynchronized.ref |
|
11 |
|
12 val prepare_function : Function_Common.function_config |
|
13 -> string (* defname *) |
|
14 -> ((bstring * typ) * mixfix) list (* defined symbol *) |
|
15 -> ((bstring * typ) list * term list * term * term) list (* specification *) |
|
16 -> local_theory |
|
17 |
|
18 -> (term (* f *) |
|
19 * thm (* goalstate *) |
|
20 * (thm -> Function_Common.function_result) (* continuation *) |
|
21 ) * local_theory |
|
22 |
|
23 end |
|
24 |
|
25 structure Function_Core : FUNCTION_CORE = |
|
26 struct |
|
27 |
|
28 val trace = Unsynchronized.ref false; |
|
29 fun trace_msg msg = if ! trace then tracing (msg ()) else (); |
|
30 |
|
31 val boolT = HOLogic.boolT |
|
32 val mk_eq = HOLogic.mk_eq |
|
33 |
|
34 open Function_Lib |
|
35 open Function_Common |
|
36 |
|
37 datatype globals = |
|
38 Globals of { |
|
39 fvar: term, |
|
40 domT: typ, |
|
41 ranT: typ, |
|
42 h: term, |
|
43 y: term, |
|
44 x: term, |
|
45 z: term, |
|
46 a: term, |
|
47 P: term, |
|
48 D: term, |
|
49 Pbool:term |
|
50 } |
|
51 |
|
52 |
|
53 datatype rec_call_info = |
|
54 RCInfo of |
|
55 { |
|
56 RIvs: (string * typ) list, (* Call context: fixes and assumes *) |
|
57 CCas: thm list, |
|
58 rcarg: term, (* The recursive argument *) |
|
59 |
|
60 llRI: thm, |
|
61 h_assum: term |
|
62 } |
|
63 |
|
64 |
|
65 datatype clause_context = |
|
66 ClauseContext of |
|
67 { |
|
68 ctxt : Proof.context, |
|
69 |
|
70 qs : term list, |
|
71 gs : term list, |
|
72 lhs: term, |
|
73 rhs: term, |
|
74 |
|
75 cqs: cterm list, |
|
76 ags: thm list, |
|
77 case_hyp : thm |
|
78 } |
|
79 |
|
80 |
|
81 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = |
|
82 ClauseContext { ctxt = ProofContext.transfer thy ctxt, |
|
83 qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } |
|
84 |
|
85 |
|
86 datatype clause_info = |
|
87 ClauseInfo of |
|
88 { |
|
89 no: int, |
|
90 qglr : ((string * typ) list * term list * term * term), |
|
91 cdata : clause_context, |
|
92 |
|
93 tree: Function_Ctx_Tree.ctx_tree, |
|
94 lGI: thm, |
|
95 RCs: rec_call_info list |
|
96 } |
|
97 |
|
98 |
|
99 (* Theory dependencies. *) |
|
100 val Pair_inject = @{thm Product_Type.Pair_inject}; |
|
101 |
|
102 val acc_induct_rule = @{thm accp_induct_rule}; |
|
103 |
|
104 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}; |
|
105 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}; |
|
106 val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}; |
|
107 |
|
108 val acc_downward = @{thm accp_downward}; |
|
109 val accI = @{thm accp.accI}; |
|
110 val case_split = @{thm HOL.case_split}; |
|
111 val fundef_default_value = @{thm FunDef.fundef_default_value}; |
|
112 val not_acc_down = @{thm not_accp_down}; |
|
113 |
|
114 |
|
115 |
|
116 fun find_calls tree = |
|
117 let |
|
118 fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) |
|
119 | add_Ri _ _ _ _ = raise Match |
|
120 in |
|
121 rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) |
|
122 end |
|
123 |
|
124 |
|
125 (** building proof obligations *) |
|
126 |
|
127 fun mk_compat_proof_obligations domT ranT fvar f glrs = |
|
128 let |
|
129 fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
|
130 let |
|
131 val shift = incr_boundvars (length qs') |
|
132 in |
|
133 Logic.mk_implies |
|
134 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
|
135 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
|
136 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
|
137 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
|
138 |> curry abstract_over fvar |
|
139 |> curry subst_bound f |
|
140 end |
|
141 in |
|
142 map mk_impl (unordered_pairs glrs) |
|
143 end |
|
144 |
|
145 |
|
146 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
|
147 let |
|
148 fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = |
|
149 HOLogic.mk_Trueprop Pbool |
|
150 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |
|
151 |> fold_rev (curry Logic.mk_implies) gs |
|
152 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
153 in |
|
154 HOLogic.mk_Trueprop Pbool |
|
155 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
|
156 |> mk_forall_rename ("x", x) |
|
157 |> mk_forall_rename ("P", Pbool) |
|
158 end |
|
159 |
|
160 (** making a context with it's own local bindings **) |
|
161 |
|
162 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
|
163 let |
|
164 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |
|
165 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
|
166 |
|
167 val thy = ProofContext.theory_of ctxt' |
|
168 |
|
169 fun inst t = subst_bounds (rev qs, t) |
|
170 val gs = map inst pre_gs |
|
171 val lhs = inst pre_lhs |
|
172 val rhs = inst pre_rhs |
|
173 |
|
174 val cqs = map (cterm_of thy) qs |
|
175 val ags = map (assume o cterm_of thy) gs |
|
176 |
|
177 val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) |
|
178 in |
|
179 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
|
180 cqs = cqs, ags = ags, case_hyp = case_hyp } |
|
181 end |
|
182 |
|
183 |
|
184 (* lowlevel term function. FIXME: remove *) |
|
185 fun abstract_over_list vs body = |
|
186 let |
|
187 fun abs lev v tm = |
|
188 if v aconv tm then Bound lev |
|
189 else |
|
190 (case tm of |
|
191 Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) |
|
192 | t $ u => abs lev v t $ abs lev v u |
|
193 | t => t); |
|
194 in |
|
195 fold_index (fn (i, v) => fn t => abs i v t) vs body |
|
196 end |
|
197 |
|
198 |
|
199 |
|
200 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
|
201 let |
|
202 val Globals {h, fvar, x, ...} = globals |
|
203 |
|
204 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
|
205 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
206 |
|
207 (* Instantiate the GIntro thm with "f" and import into the clause context. *) |
|
208 val lGI = GIntro_thm |
|
209 |> forall_elim (cert f) |
|
210 |> fold forall_elim cqs |
|
211 |> fold Thm.elim_implies ags |
|
212 |
|
213 fun mk_call_info (rcfix, rcassm, rcarg) RI = |
|
214 let |
|
215 val llRI = RI |
|
216 |> fold forall_elim cqs |
|
217 |> fold (forall_elim o cert o Free) rcfix |
|
218 |> fold Thm.elim_implies ags |
|
219 |> fold Thm.elim_implies rcassm |
|
220 |
|
221 val h_assum = |
|
222 HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |
|
223 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
224 |> fold_rev (Logic.all o Free) rcfix |
|
225 |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] |
|
226 |> abstract_over_list (rev qs) |
|
227 in |
|
228 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
|
229 end |
|
230 |
|
231 val RC_infos = map2 mk_call_info RCs RIntro_thms |
|
232 in |
|
233 ClauseInfo |
|
234 { |
|
235 no=no, |
|
236 cdata=cdata, |
|
237 qglr=qglr, |
|
238 |
|
239 lGI=lGI, |
|
240 RCs=RC_infos, |
|
241 tree=tree |
|
242 } |
|
243 end |
|
244 |
|
245 |
|
246 |
|
247 |
|
248 |
|
249 |
|
250 |
|
251 (* replace this by a table later*) |
|
252 fun store_compat_thms 0 thms = [] |
|
253 | store_compat_thms n thms = |
|
254 let |
|
255 val (thms1, thms2) = chop n thms |
|
256 in |
|
257 (thms1 :: store_compat_thms (n - 1) thms2) |
|
258 end |
|
259 |
|
260 (* expects i <= j *) |
|
261 fun lookup_compat_thm i j cts = |
|
262 nth (nth cts (i - 1)) (j - i) |
|
263 |
|
264 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
|
265 (* if j < i, then turn around *) |
|
266 fun get_compat_thm thy cts i j ctxi ctxj = |
|
267 let |
|
268 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi |
|
269 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj |
|
270 |
|
271 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
|
272 in if j < i then |
|
273 let |
|
274 val compat = lookup_compat_thm j i cts |
|
275 in |
|
276 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
|
277 |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
|
278 |> fold Thm.elim_implies agsj |
|
279 |> fold Thm.elim_implies agsi |
|
280 |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
|
281 end |
|
282 else |
|
283 let |
|
284 val compat = lookup_compat_thm i j cts |
|
285 in |
|
286 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
|
287 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
|
288 |> fold Thm.elim_implies agsi |
|
289 |> fold Thm.elim_implies agsj |
|
290 |> Thm.elim_implies (assume lhsi_eq_lhsj) |
|
291 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
|
292 end |
|
293 end |
|
294 |
|
295 |
|
296 |
|
297 |
|
298 (* Generates the replacement lemma in fully quantified form. *) |
|
299 fun mk_replacement_lemma thy h ih_elim clause = |
|
300 let |
|
301 val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause |
|
302 local open Conv in |
|
303 val ih_conv = arg1_conv o arg_conv o arg_conv |
|
304 end |
|
305 |
|
306 val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim |
|
307 |
|
308 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
|
309 val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
|
310 |
|
311 val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree |
|
312 |
|
313 val replace_lemma = (eql RS meta_eq_to_obj_eq) |
|
314 |> implies_intr (cprop_of case_hyp) |
|
315 |> fold_rev (implies_intr o cprop_of) h_assums |
|
316 |> fold_rev (implies_intr o cprop_of) ags |
|
317 |> fold_rev forall_intr cqs |
|
318 |> Thm.close_derivation |
|
319 in |
|
320 replace_lemma |
|
321 end |
|
322 |
|
323 |
|
324 fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj = |
|
325 let |
|
326 val Globals {h, y, x, fvar, ...} = globals |
|
327 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
|
328 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
|
329 |
|
330 val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} |
|
331 = mk_clause_context x ctxti cdescj |
|
332 |
|
333 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
|
334 val compat = get_compat_thm thy compat_store i j cctxi cctxj |
|
335 val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
|
336 |
|
337 val RLj_import = |
|
338 RLj |> fold forall_elim cqsj' |
|
339 |> fold Thm.elim_implies agsj' |
|
340 |> fold Thm.elim_implies Ghsj' |
|
341 |
|
342 val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) |
|
343 val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) |
|
344 in |
|
345 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
|
346 |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
|
347 |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
|
348 |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
|
349 |> fold_rev (implies_intr o cprop_of) Ghsj' |
|
350 |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |
|
351 |> implies_intr (cprop_of y_eq_rhsj'h) |
|
352 |> implies_intr (cprop_of lhsi_eq_lhsj') |
|
353 |> fold_rev forall_intr (cterm_of thy h :: cqsj') |
|
354 end |
|
355 |
|
356 |
|
357 |
|
358 fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = |
|
359 let |
|
360 val Globals {x, y, ranT, fvar, ...} = globals |
|
361 val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
|
362 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
|
363 |
|
364 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro |
|
365 |
|
366 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |
|
367 |> fold_rev (implies_intr o cprop_of) CCas |
|
368 |> fold_rev (forall_intr o cterm_of thy o Free) RIvs |
|
369 |
|
370 val existence = fold (curry op COMP o prep_RC) RCs lGI |
|
371 |
|
372 val P = cterm_of thy (mk_eq (y, rhsC)) |
|
373 val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) |
|
374 |
|
375 val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas |
|
376 |
|
377 val uniqueness = G_cases |
|
378 |> forall_elim (cterm_of thy lhs) |
|
379 |> forall_elim (cterm_of thy y) |
|
380 |> forall_elim P |
|
381 |> Thm.elim_implies G_lhs_y |
|
382 |> fold Thm.elim_implies unique_clauses |
|
383 |> implies_intr (cprop_of G_lhs_y) |
|
384 |> forall_intr (cterm_of thy y) |
|
385 |
|
386 val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) |
|
387 |
|
388 val exactly_one = |
|
389 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
|
390 |> curry (op COMP) existence |
|
391 |> curry (op COMP) uniqueness |
|
392 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) |
|
393 |> implies_intr (cprop_of case_hyp) |
|
394 |> fold_rev (implies_intr o cprop_of) ags |
|
395 |> fold_rev forall_intr cqs |
|
396 |
|
397 val function_value = |
|
398 existence |
|
399 |> implies_intr ihyp |
|
400 |> implies_intr (cprop_of case_hyp) |
|
401 |> forall_intr (cterm_of thy x) |
|
402 |> forall_elim (cterm_of thy lhs) |
|
403 |> curry (op RS) refl |
|
404 in |
|
405 (exactly_one, function_value) |
|
406 end |
|
407 |
|
408 |
|
409 |
|
410 |
|
411 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = |
|
412 let |
|
413 val Globals {h, domT, ranT, x, ...} = globals |
|
414 val thy = ProofContext.theory_of ctxt |
|
415 |
|
416 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
|
417 val ihyp = Term.all domT $ Abs ("z", domT, |
|
418 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
|
419 HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ |
|
420 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
|
421 |> cterm_of thy |
|
422 |
|
423 val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0 |
|
424 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
|
425 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
|
426 |> instantiate' [] [NONE, SOME (cterm_of thy h)] |
|
427 |
|
428 val _ = trace_msg (K "Proving Replacement lemmas...") |
|
429 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
|
430 |
|
431 val _ = trace_msg (K "Proving cases for unique existence...") |
|
432 val (ex1s, values) = |
|
433 split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) |
|
434 |
|
435 val _ = trace_msg (K "Proving: Graph is a function") |
|
436 val graph_is_function = complete |
|
437 |> Thm.forall_elim_vars 0 |
|
438 |> fold (curry op COMP) ex1s |
|
439 |> implies_intr (ihyp) |
|
440 |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
|
441 |> forall_intr (cterm_of thy x) |
|
442 |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
|
443 |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
|
444 |
|
445 val goalstate = Conjunction.intr graph_is_function complete |
|
446 |> Thm.close_derivation |
|
447 |> Goal.protect |
|
448 |> fold_rev (implies_intr o cprop_of) compat |
|
449 |> implies_intr (cprop_of complete) |
|
450 in |
|
451 (goalstate, values) |
|
452 end |
|
453 |
|
454 |
|
455 fun define_graph Gname fvar domT ranT clauses RCss lthy = |
|
456 let |
|
457 val GT = domT --> ranT --> boolT |
|
458 val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)])) |
|
459 |
|
460 fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = |
|
461 let |
|
462 fun mk_h_assm (rcfix, rcassm, rcarg) = |
|
463 HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) |
|
464 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
465 |> fold_rev (Logic.all o Free) rcfix |
|
466 in |
|
467 HOLogic.mk_Trueprop (Gvar $ lhs $ rhs) |
|
468 |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
|
469 |> fold_rev (curry Logic.mk_implies) gs |
|
470 |> fold_rev Logic.all (fvar :: qs) |
|
471 end |
|
472 |
|
473 val G_intros = map2 mk_GIntro clauses RCss |
|
474 |
|
475 val (GIntro_thms, (G, G_elim, G_induct, lthy)) = |
|
476 Function_Inductive_Wrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) |
|
477 in |
|
478 ((G, GIntro_thms, G_elim, G_induct), lthy) |
|
479 end |
|
480 |
|
481 |
|
482 |
|
483 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
|
484 let |
|
485 val f_def = |
|
486 Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ |
|
487 Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
|
488 |> Syntax.check_term lthy |
|
489 |
|
490 val ((f, (_, f_defthm)), lthy) = |
|
491 LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy |
|
492 in |
|
493 ((f, f_defthm), lthy) |
|
494 end |
|
495 |
|
496 |
|
497 fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy = |
|
498 let |
|
499 |
|
500 val RT = domT --> domT --> boolT |
|
501 val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)])) |
|
502 |
|
503 fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = |
|
504 HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs) |
|
505 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
506 |> fold_rev (curry Logic.mk_implies) gs |
|
507 |> fold_rev (Logic.all o Free) rcfix |
|
508 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
509 (* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
|
510 |
|
511 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
|
512 |
|
513 val (RIntro_thmss, (R, R_elim, _, lthy)) = |
|
514 fold_burrow Function_Inductive_Wrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy) |
|
515 in |
|
516 ((R, RIntro_thmss, R_elim), lthy) |
|
517 end |
|
518 |
|
519 |
|
520 fun fix_globals domT ranT fvar ctxt = |
|
521 let |
|
522 val ([h, y, x, z, a, D, P, Pbool],ctxt') = |
|
523 Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
|
524 in |
|
525 (Globals {h = Free (h, domT --> ranT), |
|
526 y = Free (y, ranT), |
|
527 x = Free (x, domT), |
|
528 z = Free (z, domT), |
|
529 a = Free (a, domT), |
|
530 D = Free (D, domT --> boolT), |
|
531 P = Free (P, domT --> boolT), |
|
532 Pbool = Free (Pbool, boolT), |
|
533 fvar = fvar, |
|
534 domT = domT, |
|
535 ranT = ranT |
|
536 }, |
|
537 ctxt') |
|
538 end |
|
539 |
|
540 |
|
541 |
|
542 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = |
|
543 let |
|
544 fun inst_term t = subst_bound(f, abstract_over (fvar, t)) |
|
545 in |
|
546 (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) |
|
547 end |
|
548 |
|
549 |
|
550 |
|
551 (********************************************************** |
|
552 * PROVING THE RULES |
|
553 **********************************************************) |
|
554 |
|
555 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
|
556 let |
|
557 val Globals {domT, z, ...} = globals |
|
558 |
|
559 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
|
560 let |
|
561 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
|
562 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
|
563 in |
|
564 ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) |
|
565 |> (fn it => it COMP graph_is_function) |
|
566 |> implies_intr z_smaller |
|
567 |> forall_intr (cterm_of thy z) |
|
568 |> (fn it => it COMP valthm) |
|
569 |> implies_intr lhs_acc |
|
570 |> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
|
571 |> fold_rev (implies_intr o cprop_of) ags |
|
572 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
573 end |
|
574 in |
|
575 map2 mk_psimp clauses valthms |
|
576 end |
|
577 |
|
578 |
|
579 (** Induction rule **) |
|
580 |
|
581 |
|
582 val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct} |
|
583 |
|
584 |
|
585 fun mk_partial_induct_rule thy globals R complete_thm clauses = |
|
586 let |
|
587 val Globals {domT, x, z, a, P, D, ...} = globals |
|
588 val acc_R = mk_acc domT R |
|
589 |
|
590 val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
|
591 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
|
592 |
|
593 val D_subset = cterm_of thy (Logic.all x |
|
594 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
|
595 |
|
596 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
|
597 Logic.all x |
|
598 (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
|
599 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
|
600 HOLogic.mk_Trueprop (D $ z))))) |
|
601 |> cterm_of thy |
|
602 |
|
603 |
|
604 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
|
605 val ihyp = Term.all domT $ Abs ("z", domT, |
|
606 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
|
607 HOLogic.mk_Trueprop (P $ Bound 0))) |
|
608 |> cterm_of thy |
|
609 |
|
610 val aihyp = assume ihyp |
|
611 |
|
612 fun prove_case clause = |
|
613 let |
|
614 val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, |
|
615 qglr = (oqs, _, _, _), ...} = clause |
|
616 |
|
617 val case_hyp_conv = K (case_hyp RS eq_reflection) |
|
618 local open Conv in |
|
619 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
|
620 val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp |
|
621 end |
|
622 |
|
623 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = |
|
624 sih |> forall_elim (cterm_of thy rcarg) |
|
625 |> Thm.elim_implies llRI |
|
626 |> fold_rev (implies_intr o cprop_of) CCas |
|
627 |> fold_rev (forall_intr o cterm_of thy o Free) RIvs |
|
628 |
|
629 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
|
630 |
|
631 val step = HOLogic.mk_Trueprop (P $ lhs) |
|
632 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
|
633 |> fold_rev (curry Logic.mk_implies) gs |
|
634 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
|
635 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
636 |> cterm_of thy |
|
637 |
|
638 val P_lhs = assume step |
|
639 |> fold forall_elim cqs |
|
640 |> Thm.elim_implies lhs_D |
|
641 |> fold Thm.elim_implies ags |
|
642 |> fold Thm.elim_implies P_recs |
|
643 |
|
644 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
|
645 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
|
646 |> symmetric (* P lhs == P x *) |
|
647 |> (fn eql => equal_elim eql P_lhs) (* "P x" *) |
|
648 |> implies_intr (cprop_of case_hyp) |
|
649 |> fold_rev (implies_intr o cprop_of) ags |
|
650 |> fold_rev forall_intr cqs |
|
651 in |
|
652 (res, step) |
|
653 end |
|
654 |
|
655 val (cases, steps) = split_list (map prove_case clauses) |
|
656 |
|
657 val istep = complete_thm |
|
658 |> Thm.forall_elim_vars 0 |
|
659 |> fold (curry op COMP) cases (* P x *) |
|
660 |> implies_intr ihyp |
|
661 |> implies_intr (cprop_of x_D) |
|
662 |> forall_intr (cterm_of thy x) |
|
663 |
|
664 val subset_induct_rule = |
|
665 acc_subset_induct |
|
666 |> (curry op COMP) (assume D_subset) |
|
667 |> (curry op COMP) (assume D_dcl) |
|
668 |> (curry op COMP) (assume a_D) |
|
669 |> (curry op COMP) istep |
|
670 |> fold_rev implies_intr steps |
|
671 |> implies_intr a_D |
|
672 |> implies_intr D_dcl |
|
673 |> implies_intr D_subset |
|
674 |
|
675 val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule |
|
676 |
|
677 val simple_induct_rule = |
|
678 subset_induct_rule |
|
679 |> forall_intr (cterm_of thy D) |
|
680 |> forall_elim (cterm_of thy acc_R) |
|
681 |> assume_tac 1 |> Seq.hd |
|
682 |> (curry op COMP) (acc_downward |
|
683 |> (instantiate' [SOME (ctyp_of thy domT)] |
|
684 (map (SOME o cterm_of thy) [R, x, z])) |
|
685 |> forall_intr (cterm_of thy z) |
|
686 |> forall_intr (cterm_of thy x)) |
|
687 |> forall_intr (cterm_of thy a) |
|
688 |> forall_intr (cterm_of thy P) |
|
689 in |
|
690 simple_induct_rule |
|
691 end |
|
692 |
|
693 |
|
694 |
|
695 (* FIXME: This should probably use fixed goals, to be more reliable and faster *) |
|
696 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
|
697 let |
|
698 val thy = ProofContext.theory_of ctxt |
|
699 val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, |
|
700 qglr = (oqs, _, _, _), ...} = clause |
|
701 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
|
702 |> fold_rev (curry Logic.mk_implies) gs |
|
703 |> cterm_of thy |
|
704 in |
|
705 Goal.init goal |
|
706 |> (SINGLE (resolve_tac [accI] 1)) |> the |
|
707 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
|
708 |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the |
|
709 |> Goal.conclude |
|
710 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
711 end |
|
712 |
|
713 |
|
714 |
|
715 (** Termination rule **) |
|
716 |
|
717 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}; |
|
718 val wf_in_rel = @{thm FunDef.wf_in_rel}; |
|
719 val in_rel_def = @{thm FunDef.in_rel_def}; |
|
720 |
|
721 fun mk_nest_term_case thy globals R' ihyp clause = |
|
722 let |
|
723 val Globals {x, z, ...} = globals |
|
724 val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree, |
|
725 qglr=(oqs, _, _, _), ...} = clause |
|
726 |
|
727 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
|
728 |
|
729 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
|
730 let |
|
731 val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub) |
|
732 |
|
733 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
|
734 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
|
735 |> Function_Ctx_Tree.export_term (fixes, assumes) |
|
736 |> fold_rev (curry Logic.mk_implies o prop_of) ags |
|
737 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
738 |> cterm_of thy |
|
739 |
|
740 val thm = assume hyp |
|
741 |> fold forall_elim cqs |
|
742 |> fold Thm.elim_implies ags |
|
743 |> Function_Ctx_Tree.import_thm thy (fixes, assumes) |
|
744 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
|
745 |
|
746 val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg)))) |
|
747 |
|
748 val acc = thm COMP ih_case |
|
749 val z_acc_local = acc |
|
750 |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) |
|
751 |
|
752 val ethm = z_acc_local |
|
753 |> Function_Ctx_Tree.export_thm thy (fixes, |
|
754 z_eq_arg :: case_hyp :: ags @ assumes) |
|
755 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
756 |
|
757 val sub' = sub @ [(([],[]), acc)] |
|
758 in |
|
759 (sub', (hyp :: hyps, ethm :: thms)) |
|
760 end |
|
761 | step _ _ _ _ = raise Match |
|
762 in |
|
763 Function_Ctx_Tree.traverse_tree step tree |
|
764 end |
|
765 |
|
766 |
|
767 fun mk_nest_term_rule thy globals R R_cases clauses = |
|
768 let |
|
769 val Globals { domT, x, z, ... } = globals |
|
770 val acc_R = mk_acc domT R |
|
771 |
|
772 val R' = Free ("R", fastype_of R) |
|
773 |
|
774 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
|
775 val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
|
776 |
|
777 val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) |
|
778 |
|
779 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
|
780 val ihyp = Term.all domT $ Abs ("z", domT, |
|
781 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
|
782 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
|
783 |> cterm_of thy |
|
784 |
|
785 val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 |
|
786 |
|
787 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
|
788 |
|
789 val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) |
|
790 in |
|
791 R_cases |
|
792 |> forall_elim (cterm_of thy z) |
|
793 |> forall_elim (cterm_of thy x) |
|
794 |> forall_elim (cterm_of thy (acc_R $ z)) |
|
795 |> curry op COMP (assume R_z_x) |
|
796 |> fold_rev (curry op COMP) cases |
|
797 |> implies_intr R_z_x |
|
798 |> forall_intr (cterm_of thy z) |
|
799 |> (fn it => it COMP accI) |
|
800 |> implies_intr ihyp |
|
801 |> forall_intr (cterm_of thy x) |
|
802 |> (fn it => Drule.compose_single(it,2,wf_induct_rule)) |
|
803 |> curry op RS (assume wfR') |
|
804 |> forall_intr_vars |
|
805 |> (fn it => it COMP allI) |
|
806 |> fold implies_intr hyps |
|
807 |> implies_intr wfR' |
|
808 |> forall_intr (cterm_of thy R') |
|
809 |> forall_elim (cterm_of thy (inrel_R)) |
|
810 |> curry op RS wf_in_rel |
|
811 |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) |
|
812 |> forall_intr (cterm_of thy Rrel) |
|
813 end |
|
814 |
|
815 |
|
816 |
|
817 (* Tail recursion (probably very fragile) |
|
818 * |
|
819 * FIXME: |
|
820 * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context. |
|
821 * - Must we really replace the fvar by f here? |
|
822 * - Splitting is not configured automatically: Problems with case? |
|
823 *) |
|
824 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps = |
|
825 let |
|
826 val Globals {domT, ranT, fvar, ...} = globals |
|
827 |
|
828 val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) |
|
829 |
|
830 val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) |
|
831 Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] |
|
832 (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) |
|
833 (fn {prems=[a], ...} => |
|
834 ((rtac (G_induct OF [a])) |
|
835 THEN_ALL_NEW (rtac accI) |
|
836 THEN_ALL_NEW (etac R_cases) |
|
837 THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1) |
|
838 |
|
839 val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value) |
|
840 |
|
841 fun mk_trsimp clause psimp = |
|
842 let |
|
843 val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause |
|
844 val thy = ProofContext.theory_of ctxt |
|
845 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
|
846 |
|
847 val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) |
|
848 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) |
|
849 fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def]) |
|
850 in |
|
851 Goal.prove ctxt [] [] trsimp |
|
852 (fn _ => |
|
853 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 |
|
854 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 |
|
855 THEN (simp_default_tac (simpset_of ctxt) 1) |
|
856 THEN (etac not_acc_down 1) |
|
857 THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1) |
|
858 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
859 end |
|
860 in |
|
861 map2 mk_trsimp clauses psimps |
|
862 end |
|
863 |
|
864 |
|
865 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
|
866 let |
|
867 val FunctionConfig {domintros, tailrec, default=default_str, ...} = config |
|
868 |
|
869 val fvar = Free (fname, fT) |
|
870 val domT = domain_type fT |
|
871 val ranT = range_type fT |
|
872 |
|
873 val default = Syntax.parse_term lthy default_str |
|
874 |> TypeInfer.constrain fT |> Syntax.check_term lthy |
|
875 |
|
876 val (globals, ctxt') = fix_globals domT ranT fvar lthy |
|
877 |
|
878 val Globals { x, h, ... } = globals |
|
879 |
|
880 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
|
881 |
|
882 val n = length abstract_qglrs |
|
883 |
|
884 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
|
885 Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs |
|
886 |
|
887 val trees = map build_tree clauses |
|
888 val RCss = map find_calls trees |
|
889 |
|
890 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
|
891 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
|
892 |
|
893 val ((f, f_defthm), lthy) = |
|
894 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
|
895 |
|
896 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
|
897 val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
|
898 |
|
899 val ((R, RIntro_thmss, R_elim), lthy) = |
|
900 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy |
|
901 |
|
902 val (_, lthy) = |
|
903 LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
|
904 |
|
905 val newthy = ProofContext.theory_of lthy |
|
906 val clauses = map (transfer_clause_ctx newthy) clauses |
|
907 |
|
908 val cert = cterm_of (ProofContext.theory_of lthy) |
|
909 |
|
910 val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss |
|
911 |
|
912 val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume |
|
913 val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume) |
|
914 |
|
915 val compat_store = store_compat_thms n compat |
|
916 |
|
917 val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm |
|
918 |
|
919 val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses |
|
920 |
|
921 fun mk_partial_rules provedgoal = |
|
922 let |
|
923 val newthy = theory_of_thm provedgoal (*FIXME*) |
|
924 |
|
925 val (graph_is_function, complete_thm) = |
|
926 provedgoal |
|
927 |> Conjunction.elim |
|
928 |> apfst (Thm.forall_elim_vars 0) |
|
929 |
|
930 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
|
931 |
|
932 val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
|
933 |
|
934 val simple_pinduct = PROFILE "Proving partial induction rule" |
|
935 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
|
936 |
|
937 |
|
938 val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses |
|
939 |
|
940 val dom_intros = if domintros |
|
941 then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
|
942 else NONE |
|
943 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE |
|
944 |
|
945 in |
|
946 FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
|
947 psimps=psimps, simple_pinducts=[simple_pinduct], |
|
948 termination=total_intro, trsimps=trsimps, |
|
949 domintros=dom_intros} |
|
950 end |
|
951 in |
|
952 ((f, goalstate, mk_partial_rules), lthy) |
|
953 end |
|
954 |
|
955 |
|
956 end |