author | wenzelm |
Mon, 01 Jun 2015 13:35:16 +0200 | |
changeset 60328 | 9c94e6a30d29 |
parent 59621 | 291934bac95e |
child 60682 | 5a6cd2560549 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/lexicographic_order.ML |
21131 | 2 |
Author: Lukas Bulwahn, TU Muenchen |
39928 | 3 |
Author: Alexander Krauss, TU Muenchen |
21131 | 4 |
|
39928 | 5 |
Termination proofs with lexicographic orders. |
21131 | 6 |
*) |
7 |
||
8 |
signature LEXICOGRAPHIC_ORDER = |
|
9 |
sig |
|
33351 | 10 |
val lex_order_tac : bool -> Proof.context -> tactic -> tactic |
11 |
val lexicographic_order_tac : bool -> Proof.context -> tactic |
|
21131 | 12 |
end |
13 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32952
diff
changeset
|
14 |
structure Lexicographic_Order : LEXICOGRAPHIC_ORDER = |
21131 | 15 |
struct |
16 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32952
diff
changeset
|
17 |
open Function_Lib |
27790
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset
|
18 |
|
23074 | 19 |
(** General stuff **) |
20 |
||
21 |
fun mk_measures domT mfuns = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
22 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
23 |
val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
24 |
val mlexT = (domT --> HOLogic.natT) --> relT --> relT |
35402 | 25 |
fun mk_ms [] = Const (@{const_abbrev Set.empty}, relT) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
26 |
| mk_ms (f::fs) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
27 |
Const (@{const_name mlex_prod}, mlexT) $ f $ mk_ms fs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
28 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
29 |
mk_ms mfuns |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
30 |
end |
23074 | 31 |
|
32 |
fun del_index n [] = [] |
|
33 |
| del_index n (x :: xs) = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
34 |
if n > 0 then x :: del_index (n - 1) xs else xs |
21131 | 35 |
|
36 |
fun transpose ([]::_) = [] |
|
37 |
| transpose xss = map hd xss :: transpose (map tl xss) |
|
38 |
||
23074 | 39 |
(** Matrix cell datatype **) |
40 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
41 |
datatype cell = |
39926
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
42 |
Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm; |
23633 | 43 |
|
39926
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
44 |
fun is_Less lcell = case Lazy.force lcell of Less _ => true | _ => false; |
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
45 |
fun is_LessEq lcell = case Lazy.force lcell of LessEq _ => true | _ => false; |
23633 | 46 |
|
23074 | 47 |
|
48 |
(** Proof attempts to build the matrix **) |
|
23633 | 49 |
|
39928 | 50 |
fun dest_term t = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
51 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
52 |
val (vars, prop) = Function_Lib.dest_all_all t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
53 |
val (prems, concl) = Logic.strip_horn prop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
54 |
val (lhs, rhs) = concl |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
55 |
|> HOLogic.dest_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
56 |
|> HOLogic.dest_mem |> fst |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
57 |
|> HOLogic.dest_prod |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
58 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
59 |
(vars, prems, lhs, rhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
60 |
end |
23633 | 61 |
|
21131 | 62 |
fun mk_goal (vars, prems, lhs, rhs) rel = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
64 |
val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
65 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
fold_rev Logic.all vars (Logic.list_implies (prems, concl)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
67 |
end |
23633 | 68 |
|
59618 | 69 |
fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
70 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
71 |
val goals = Thm.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
72 |
in |
60328 | 73 |
(case try_proof ctxt (goals @{const_name Orderings.less}) solve_tac of |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
74 |
Solved thm => Less thm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
75 |
| Stuck thm => |
60328 | 76 |
(case try_proof ctxt (goals @{const_name Orderings.less_eq}) solve_tac of |
77 |
Solved thm2 => LessEq (thm2, thm) |
|
78 |
| Stuck thm2 => |
|
79 |
if Thm.prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2 |
|
80 |
else None (thm2, thm) |
|
81 |
| _ => raise Match) (* FIXME *) |
|
82 |
| _ => raise Match) |
|
39926
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
83 |
end); |
23074 | 84 |
|
85 |
||
86 |
(** Search algorithms **) |
|
22309 | 87 |
|
39928 | 88 |
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall is_LessEq ls) |
22309 | 89 |
|
23074 | 90 |
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col) |
22309 | 91 |
|
23074 | 92 |
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order |
23633 | 93 |
|
21131 | 94 |
(* simple depth-first search algorithm for the table *) |
39928 | 95 |
fun search_table [] = SOME [] |
96 |
| search_table table = |
|
97 |
case find_index check_col (transpose table) of |
|
98 |
~1 => NONE |
|
99 |
| col => |
|
100 |
(case (table, col) |-> transform_table |> search_table of |
|
101 |
NONE => NONE |
|
102 |
| SOME order => SOME (col :: transform_order col order)) |
|
103 |
||
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
104 |
|
23074 | 105 |
(** Proof Reconstruction **) |
106 |
||
39927 | 107 |
fun prove_row (c :: cs) = |
108 |
(case Lazy.force c of |
|
109 |
Less thm => |
|
110 |
rtac @{thm "mlex_less"} 1 |
|
111 |
THEN PRIMITIVE (Thm.elim_implies thm) |
|
112 |
| LessEq (thm, _) => |
|
113 |
rtac @{thm "mlex_leq"} 1 |
|
114 |
THEN PRIMITIVE (Thm.elim_implies thm) |
|
115 |
THEN prove_row cs |
|
40317
1eac228c52b3
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
39928
diff
changeset
|
116 |
| _ => raise General.Fail "lexicographic_order") |
39927 | 117 |
| prove_row [] = no_tac; |
23074 | 118 |
|
119 |
||
120 |
(** Error reporting **) |
|
121 |
||
49856 | 122 |
fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *) |
123 |
fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *) |
|
23437 | 124 |
|
49856 | 125 |
fun pr_unprovable_cell _ ((i,j), Less _) = [] |
23633 | 126 |
| pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = |
51958
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
127 |
["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
128 |
Goal_Display.string_of_goal ctxt st] |
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
129 |
| pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = |
51958
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
130 |
["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
131 |
Goal_Display.string_of_goal ctxt st_less ^ |
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
132 |
"\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ |
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
133 |
Goal_Display.string_of_goal ctxt st_leq] |
23633 | 134 |
| pr_unprovable_cell ctxt ((i,j), False st) = |
51958
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
135 |
["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
bca32217b304
retain goal display options when printing error messages, to avoid breakdown for huge goals;
wenzelm
parents:
51717
diff
changeset
|
136 |
Goal_Display.string_of_goal ctxt st] |
23437 | 137 |
|
23633 | 138 |
fun pr_unprovable_subgoals ctxt table = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
139 |
table |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
140 |
|> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
141 |
|> flat |
49856 | 142 |
|> maps (pr_unprovable_cell ctxt) |
23437 | 143 |
|
39928 | 144 |
fun pr_cell (Less _ ) = " < " |
145 |
| pr_cell (LessEq _) = " <=" |
|
146 |
| pr_cell (None _) = " ? " |
|
147 |
| pr_cell (False _) = " F " |
|
148 |
||
39926
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
149 |
fun no_order_msg ctxt ltable tl measure_funs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
150 |
let |
39926
4b3b384d3de3
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
krauss
parents:
39125
diff
changeset
|
151 |
val table = map (map Lazy.force) ltable |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
152 |
val prterm = Syntax.string_of_term ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
153 |
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t |
23074 | 154 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
155 |
fun pr_goal t i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
156 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
157 |
val (_, _, lhs, rhs) = dest_term t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
158 |
in (* also show prems? *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
159 |
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
160 |
end |
23074 | 161 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
162 |
val gc = map (fn i => chr (i + 96)) (1 upto length table) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
163 |
val mc = 1 upto length measure_funs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
164 |
val tstr = "Result matrix:" :: (" " ^ implode (map (enclose " " " " o string_of_int) mc)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
165 |
:: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
166 |
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
167 |
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
168 |
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
169 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
170 |
cat_lines (ustr @ gstr @ mstr @ tstr @ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
171 |
["", "Could not find lexicographic termination order."]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
172 |
end |
23633 | 173 |
|
23074 | 174 |
(** The Main Function **) |
30493
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
30304
diff
changeset
|
175 |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
176 |
fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
177 |
let |
59582 | 178 |
val ((_ $ (_ $ rel)) :: tl) = Thm.prems_of st |
23074 | 179 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
180 |
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) |
23074 | 181 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
182 |
val measure_funs = (* 1: generate measures *) |
57959 | 183 |
Measure_Functions.get_measure_functions ctxt domT |
23633 | 184 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
185 |
val table = (* 2: create table *) |
59618 | 186 |
map (fn t => map (mk_cell ctxt solve_tac (dest_term t)) measure_funs) tl |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
187 |
in |
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
188 |
fn st => |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
189 |
case search_table table of |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
190 |
NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs) |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
191 |
| SOME order => |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
192 |
let |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
193 |
val clean_table = map (fn x => map (nth x) order) table |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
194 |
val relation = mk_measures domT (map (nth measure_funs) order) |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
195 |
val _ = |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
196 |
if not quiet then |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
197 |
Pretty.writeln (Pretty.block |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
198 |
[Pretty.str "Found termination order:", Pretty.brk 1, |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
199 |
Pretty.quote (Syntax.pretty_term ctxt relation)]) |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
200 |
else () |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
201 |
|
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
202 |
in (* 4: proof reconstruction *) |
59618 | 203 |
st |> |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
204 |
(PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)]) |
59618 | 205 |
THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) |
206 |
THEN (rtac @{thm "wf_empty"} 1) |
|
207 |
THEN EVERY (map prove_row clean_table)) |
|
56231
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
208 |
end |
b98813774a63
enforce subgoal boundaries via SUBGOAL/SUBGOAL_CASES -- clean tactical failure if out-of-range;
wenzelm
parents:
51958
diff
changeset
|
209 |
end) 1 st; |
21131 | 210 |
|
33351 | 211 |
fun lexicographic_order_tac quiet ctxt = |
59159 | 212 |
TRY (Function_Common.termination_rule_tac ctxt 1) THEN |
42793 | 213 |
lex_order_tac quiet ctxt |
57959 | 214 |
(auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp}))) |
30493
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
30304
diff
changeset
|
215 |
|
58819 | 216 |
val _ = |
217 |
Theory.setup |
|
218 |
(Context.theory_map |
|
219 |
(Function_Common.set_termination_prover (lexicographic_order_tac false))) |
|
21131 | 220 |
|
30493
b8570ea1ce25
provide regular ML interfaces for Isar source language elements;
wenzelm
parents:
30304
diff
changeset
|
221 |
end; |