equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/function_package/lexicographic_order.ML |
1 (* Title: HOL/Tools/function_package/lexicographic_order.ML |
2 ID: $Id$ |
|
3 Author: Lukas Bulwahn, TU Muenchen |
2 Author: Lukas Bulwahn, TU Muenchen |
4 |
3 |
5 Method for termination proofs with lexicographic orderings. |
4 Method for termination proofs with lexicographic orderings. |
6 *) |
5 *) |
7 |
6 |
8 signature LEXICOGRAPHIC_ORDER = |
7 signature LEXICOGRAPHIC_ORDER = |
9 sig |
8 sig |
10 val lexicographic_order : thm list -> Proof.context -> Method.method |
9 val lex_order_tac : Proof.context -> tactic -> tactic |
11 val lexicographic_order_tac : Proof.context -> tactic -> tactic |
10 val lexicographic_order_tac : Proof.context -> tactic |
|
11 val lexicographic_order : Proof.context -> Proof.method |
12 |
12 |
13 val setup: theory -> theory |
13 val setup: theory -> theory |
14 end |
14 end |
15 |
15 |
16 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
16 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
184 in |
184 in |
185 cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) |
185 cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) |
186 end |
186 end |
187 |
187 |
188 (** The Main Function **) |
188 (** The Main Function **) |
189 fun lexicographic_order_tac ctxt solve_tac (st: thm) = |
189 |
190 let |
190 fun lex_order_tac ctxt solve_tac (st: thm) = |
191 val thy = theory_of_thm st |
191 let |
|
192 val thy = ProofContext.theory_of ctxt |
192 val ((trueprop $ (wf $ rel)) :: tl) = prems_of st |
193 val ((trueprop $ (wf $ rel)) :: tl) = prems_of st |
193 |
194 |
194 val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) |
195 val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) |
195 |
196 |
196 val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *) |
197 val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *) |
211 THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) |
212 THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) |
212 THEN (rtac @{thm "wf_empty"} 1) |
213 THEN (rtac @{thm "wf_empty"} 1) |
213 THEN EVERY (map prove_row clean_table)) |
214 THEN EVERY (map prove_row clean_table)) |
214 end |
215 end |
215 |
216 |
216 fun lexicographic_order thms ctxt = |
217 fun lexicographic_order_tac ctxt = |
217 Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1) |
218 TRY (FundefCommon.apply_termination_rule ctxt 1) |
218 THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))) |
219 THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) |
219 |
220 |
220 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, |
221 val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac |
|
222 |
|
223 val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order, |
221 "termination prover for lexicographic orderings")] |
224 "termination prover for lexicographic orderings")] |
222 #> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order [])) |
225 #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order) |
223 |
226 |
224 end |
227 end; |
|
228 |