269 |
269 |
270 fun prove_termination lthy = |
270 fun prove_termination lthy = |
271 Function.prove_termination NONE |
271 Function.prove_termination NONE |
272 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
272 (Lexicographic_Order.lexicographic_order_tac true lthy) lthy |
273 |
273 |
274 val (info, lthy') = Function.add_function all_fv_names all_fv_eqs |
274 val (_, lthy') = Function.add_function all_fv_names all_fv_eqs |
275 Function_Common.default_config pat_completeness_auto lthy |
275 Function_Common.default_config pat_completeness_auto lthy |
276 |
276 |
277 val lthy'' = prove_termination (Local_Theory.restore lthy') |
277 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
|
278 |
|
279 val {fs, simps, ...} = info; |
278 |
280 |
279 val morphism = ProofContext.export_morphism lthy'' lthy |
281 val morphism = ProofContext.export_morphism lthy'' lthy |
280 val fv_frees_exp = map (Morphism.term morphism) fv_frees |
282 val fs_exp = map (Morphism.term morphism) fs |
281 val fv_bns_exp = map (Morphism.term morphism) fv_bns |
283 |
282 |
284 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
283 in |
285 val simps_exp = Morphism.fact morphism (the simps) |
284 ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'') |
286 in |
285 end |
287 ((fv_frees_exp, fv_bns_exp), simps_exp, lthy'') |
286 *} |
288 end |
287 |
289 *} |
288 end |
290 |
|
291 end |