author | haftmann |
Fri, 20 Jul 2007 14:28:25 +0200 | |
changeset 23881 | 851c74f1bb69 |
parent 23633 | f25b1566f7b5 |
child 24576 | 32ddd902b0ad |
permissions | -rw-r--r-- |
21131 | 1 |
(* Title: HOL/Tools/function_package/lexicographic_order.ML |
21201 | 2 |
ID: $Id$ |
21131 | 3 |
Author: Lukas Bulwahn, TU Muenchen |
4 |
||
5 |
Method for termination proofs with lexicographic orderings. |
|
6 |
*) |
|
7 |
||
8 |
signature LEXICOGRAPHIC_ORDER = |
|
9 |
sig |
|
23056 | 10 |
val lexicographic_order : thm list -> Proof.context -> Method.method |
21510
7e72185e4b24
exported mk_base_funs for use by size-change tools
krauss
parents:
21319
diff
changeset
|
11 |
|
7e72185e4b24
exported mk_base_funs for use by size-change tools
krauss
parents:
21319
diff
changeset
|
12 |
(* exported for use by size-change termination prototype. |
7e72185e4b24
exported mk_base_funs for use by size-change tools
krauss
parents:
21319
diff
changeset
|
13 |
FIXME: provide a common interface later *) |
23074 | 14 |
val mk_base_funs : theory -> typ -> term list |
22309 | 15 |
(* exported for debugging *) |
21237 | 16 |
val setup: theory -> theory |
21131 | 17 |
end |
18 |
||
19 |
structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
|
20 |
struct |
|
21 |
||
23074 | 22 |
(** General stuff **) |
23 |
||
24 |
fun mk_measures domT mfuns = |
|
25 |
let val list = HOLogic.mk_list (domT --> HOLogic.natT) mfuns |
|
26 |
in |
|
27 |
Const (@{const_name "List.measures"}, fastype_of list --> (HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))) $ list |
|
28 |
end |
|
29 |
||
30 |
fun del_index n [] = [] |
|
31 |
| del_index n (x :: xs) = |
|
23633 | 32 |
if n > 0 then x :: del_index (n - 1) xs else xs |
21131 | 33 |
|
34 |
fun transpose ([]::_) = [] |
|
35 |
| transpose xss = map hd xss :: transpose (map tl xss) |
|
36 |
||
23074 | 37 |
(** Matrix cell datatype **) |
38 |
||
23437 | 39 |
datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm; |
23633 | 40 |
|
23074 | 41 |
fun is_Less (Less _) = true |
42 |
| is_Less _ = false |
|
23633 | 43 |
|
23074 | 44 |
fun is_LessEq (LessEq _) = true |
45 |
| is_LessEq _ = false |
|
23633 | 46 |
|
47 |
fun thm_of_cell (Less thm) = thm |
|
48 |
| thm_of_cell (LessEq (thm, _)) = thm |
|
49 |
| thm_of_cell (False thm) = thm |
|
50 |
| thm_of_cell (None (thm, _)) = thm |
|
51 |
||
23437 | 52 |
fun pr_cell (Less _ ) = " < " |
23633 | 53 |
| pr_cell (LessEq _) = " <=" |
23437 | 54 |
| pr_cell (None _) = " ? " |
55 |
| pr_cell (False _) = " F " |
|
23074 | 56 |
|
57 |
||
58 |
(** Generating Measure Functions **) |
|
59 |
||
23633 | 60 |
fun mk_comp g f = |
61 |
let |
|
62 |
val fT = fastype_of f |
|
23074 | 63 |
val gT as (Type ("fun", [xT, _])) = fastype_of g |
64 |
val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0)))) |
|
65 |
in |
|
66 |
Envir.beta_norm (comp $ f $ g) |
|
67 |
end |
|
68 |
||
69 |
fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *) |
|
70 |
map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT) |
|
71 |
@ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT) |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
72 |
|
23074 | 73 |
| mk_base_funs thy T = (* default: size function, if available *) |
74 |
if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size]) |
|
75 |
then [HOLogic.size_const T] |
|
76 |
else [] |
|
77 |
||
78 |
fun mk_sum_case f1 f2 = |
|
79 |
let |
|
23633 | 80 |
val Type ("fun", [fT, Q]) = fastype_of f1 |
23074 | 81 |
val Type ("fun", [sT, _]) = fastype_of f2 |
82 |
in |
|
83 |
Const (@{const_name "Sum_Type.sum_case"}, (fT --> Q) --> (sT --> Q) --> Type("+", [fT, sT]) --> Q) $ f1 $ f2 |
|
84 |
end |
|
23633 | 85 |
|
23074 | 86 |
fun constant_0 T = Abs ("x", T, HOLogic.zero) |
87 |
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
88 |
|
23074 | 89 |
fun mk_funorder_funs (Type ("+", [fT, sT])) = |
90 |
map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT) |
|
91 |
@ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT) |
|
23633 | 92 |
| mk_funorder_funs T = [ constant_1 T ] |
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
93 |
|
23074 | 94 |
fun mk_ext_base_funs thy (Type("+", [fT, sT])) = |
95 |
product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT) |
|
96 |
|> map (uncurry mk_sum_case) |
|
97 |
| mk_ext_base_funs thy T = mk_base_funs thy T |
|
98 |
||
99 |
fun mk_all_measure_funs thy (T as Type ("+", _)) = |
|
100 |
mk_ext_base_funs thy T @ mk_funorder_funs T |
|
101 |
| mk_all_measure_funs thy T = mk_base_funs thy T |
|
102 |
||
103 |
||
104 |
(** Proof attempts to build the matrix **) |
|
23633 | 105 |
|
21131 | 106 |
fun dest_term (t : term) = |
107 |
let |
|
23074 | 108 |
val (vars, prop) = FundefLib.dest_all_all t |
21237 | 109 |
val prems = Logic.strip_imp_prems prop |
23074 | 110 |
val (lhs, rhs) = Logic.strip_imp_concl prop |
23633 | 111 |
|> HOLogic.dest_Trueprop |
23074 | 112 |
|> HOLogic.dest_mem |> fst |
23633 | 113 |
|> HOLogic.dest_prod |
21131 | 114 |
in |
23074 | 115 |
(vars, prems, lhs, rhs) |
21131 | 116 |
end |
23633 | 117 |
|
21131 | 118 |
fun mk_goal (vars, prems, lhs, rhs) rel = |
23633 | 119 |
let |
21237 | 120 |
val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop |
23633 | 121 |
in |
122 |
Logic.list_implies (prems, concl) |
|
23074 | 123 |
|> fold_rev FundefLib.mk_forall vars |
21131 | 124 |
end |
23633 | 125 |
|
126 |
fun prove thy solve_tac t = |
|
127 |
cterm_of thy t |> Goal.init |
|
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset
|
128 |
|> SINGLE solve_tac |> the |
23633 | 129 |
|
130 |
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = |
|
131 |
let |
|
132 |
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) |
|
23881 | 133 |
val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac |
21131 | 134 |
in |
21237 | 135 |
if Thm.no_prems less_thm then |
136 |
Less (Goal.finish less_thm) |
|
137 |
else |
|
138 |
let |
|
23881 | 139 |
val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac |
21237 | 140 |
in |
141 |
if Thm.no_prems lesseq_thm then |
|
23437 | 142 |
LessEq (Goal.finish lesseq_thm, less_thm) |
23633 | 143 |
else |
21237 | 144 |
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm |
23437 | 145 |
else None (lesseq_thm, less_thm) |
21237 | 146 |
end |
21131 | 147 |
end |
23074 | 148 |
|
149 |
||
150 |
(** Search algorithms **) |
|
22309 | 151 |
|
23074 | 152 |
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls) |
22309 | 153 |
|
23074 | 154 |
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col) |
22309 | 155 |
|
23074 | 156 |
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order |
23633 | 157 |
|
21131 | 158 |
(* simple depth-first search algorithm for the table *) |
159 |
fun search_table table = |
|
160 |
case table of |
|
21237 | 161 |
[] => SOME [] |
162 |
| _ => |
|
163 |
let |
|
164 |
val col = find_index (check_col) (transpose table) |
|
165 |
in case col of |
|
23633 | 166 |
~1 => NONE |
21237 | 167 |
| _ => |
168 |
let |
|
22309 | 169 |
val order_opt = (table, col) |-> transform_table |> search_table |
21237 | 170 |
in case order_opt of |
171 |
NONE => NONE |
|
23074 | 172 |
| SOME order =>SOME (col :: transform_order col order) |
21237 | 173 |
end |
174 |
end |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
175 |
|
23633 | 176 |
(* find all positions of elements in a list *) |
23074 | 177 |
fun find_index_list P = |
178 |
let fun find _ [] = [] |
|
179 |
| find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs |
|
180 |
in find 0 end |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
181 |
|
23633 | 182 |
(* simple breadth-first search algorithm for the table *) |
22309 | 183 |
fun bfs_search_table nodes = |
184 |
case nodes of |
|
23633 | 185 |
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)" |
22309 | 186 |
| (node::rnodes) => let |
23633 | 187 |
val (order, table) = node |
22309 | 188 |
in |
189 |
case table of |
|
23074 | 190 |
[] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order)) |
22309 | 191 |
| _ => let |
23633 | 192 |
val cols = find_index_list (check_col) (transpose table) |
22309 | 193 |
in |
194 |
case cols of |
|
23633 | 195 |
[] => NONE |
196 |
| _ => let |
|
197 |
val newtables = map (transform_table table) cols |
|
23074 | 198 |
val neworders = map (fn c => c :: order) cols |
22309 | 199 |
val newnodes = neworders ~~ newtables |
200 |
in |
|
201 |
bfs_search_table (rnodes @ newnodes) |
|
23633 | 202 |
end |
22309 | 203 |
end |
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
204 |
end |
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
205 |
|
23633 | 206 |
fun nsearch_table table = bfs_search_table [([], table)] |
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
207 |
|
23074 | 208 |
(** Proof Reconstruction **) |
209 |
||
210 |
(* prove row :: cell list -> tactic *) |
|
211 |
fun prove_row (Less less_thm :: _) = |
|
212 |
(rtac @{thm "measures_less"} 1) |
|
213 |
THEN PRIMITIVE (flip implies_elim less_thm) |
|
23437 | 214 |
| prove_row (LessEq (lesseq_thm, _) :: tail) = |
23074 | 215 |
(rtac @{thm "measures_lesseq"} 1) |
216 |
THEN PRIMITIVE (flip implies_elim lesseq_thm) |
|
217 |
THEN prove_row tail |
|
218 |
| prove_row _ = sys_error "lexicographic_order" |
|
219 |
||
220 |
||
221 |
(** Error reporting **) |
|
222 |
||
223 |
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) |
|
23633 | 224 |
|
225 |
fun pr_goals ctxt st = |
|
226 |
Display.pretty_goals_aux (ProofContext.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |
|
23437 | 227 |
|> Pretty.chunks |
228 |
|> Pretty.string_of |
|
229 |
||
230 |
fun row_index i = chr (i + 97) |
|
231 |
fun col_index j = string_of_int (j + 1) |
|
232 |
||
23633 | 233 |
fun pr_unprovable_cell _ ((i,j), Less _) = "" |
234 |
| pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = |
|
235 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st |
|
236 |
| pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) = |
|
237 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less |
|
238 |
^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq |
|
239 |
| pr_unprovable_cell ctxt ((i,j), False st) = |
|
240 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st |
|
23437 | 241 |
|
23633 | 242 |
fun pr_unprovable_subgoals ctxt table = |
23437 | 243 |
table |
244 |
|> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) |
|
245 |
|> flat |
|
23633 | 246 |
|> map (pr_unprovable_cell ctxt) |
23437 | 247 |
|
23633 | 248 |
fun no_order_msg ctxt table tl measure_funs = |
249 |
let |
|
250 |
val prterm = ProofContext.string_of_term ctxt |
|
251 |
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t |
|
23074 | 252 |
|
23633 | 253 |
fun pr_goal t i = |
23074 | 254 |
let |
23633 | 255 |
val (_, _, lhs, rhs) = dest_term t |
23074 | 256 |
in (* also show prems? *) |
23128 | 257 |
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs |
23074 | 258 |
end |
259 |
||
260 |
val gc = map (fn i => chr (i + 96)) (1 upto length table) |
|
261 |
val mc = 1 upto length measure_funs |
|
23437 | 262 |
val tstr = "Result matrix:" :: " " ^ concat (map (enclose " " " " o string_of_int) mc) |
23074 | 263 |
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc |
23437 | 264 |
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc |
265 |
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc |
|
23633 | 266 |
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table |
21131 | 267 |
in |
23437 | 268 |
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) |
21131 | 269 |
end |
23633 | 270 |
|
23074 | 271 |
(** The Main Function **) |
23633 | 272 |
fun lexicographic_order_tac ctxt solve_tac (st: thm) = |
21131 | 273 |
let |
21237 | 274 |
val thy = theory_of_thm st |
23074 | 275 |
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st |
276 |
||
277 |
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) |
|
278 |
||
279 |
val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *) |
|
23633 | 280 |
|
23074 | 281 |
(* 2: create table *) |
282 |
val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl |
|
283 |
||
284 |
val order = the (search_table table) (* 3: search table *) |
|
23633 | 285 |
handle Option => error (no_order_msg ctxt table tl measure_funs) |
23074 | 286 |
|
21237 | 287 |
val clean_table = map (fn x => map (nth x) order) table |
23074 | 288 |
|
289 |
val relation = mk_measures domT (map (nth measure_funs) order) |
|
290 |
val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation)) |
|
291 |
||
292 |
in (* 4: proof reconstruction *) |
|
293 |
st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) |
|
294 |
THEN rtac @{thm "wf_measures"} 1 |
|
295 |
THEN EVERY (map prove_row clean_table)) |
|
21131 | 296 |
end |
297 |
||
23633 | 298 |
fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1 |
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset
|
299 |
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt))) |
21201 | 300 |
|
23633 | 301 |
val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, |
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset
|
302 |
"termination prover for lexicographic orderings")] |
21131 | 303 |
|
21590 | 304 |
end |