author | krauss |
Mon, 04 Aug 2008 18:24:27 +0200 | |
changeset 27721 | 50a67d1977d7 |
parent 27330 | 1af2598b5f7d |
child 27790 | 37b4e65d1dbf |
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 |
|
22309 | 12 |
(* exported for debugging *) |
21237 | 13 |
val setup: theory -> theory |
21131 | 14 |
end |
15 |
||
16 |
structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
|
17 |
struct |
|
18 |
||
23074 | 19 |
(** General stuff **) |
20 |
||
21 |
fun mk_measures domT mfuns = |
|
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
22 |
let |
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
23 |
val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) |
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
24 |
val mlexT = (domT --> HOLogic.natT) --> relT --> relT |
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
25 |
fun mk_ms [] = Const (@{const_name "{}"}, relT) |
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
26 |
| mk_ms (f::fs) = |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26529
diff
changeset
|
27 |
Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs |
23074 | 28 |
in |
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
29 |
mk_ms mfuns |
23074 | 30 |
end |
31 |
||
32 |
fun del_index n [] = [] |
|
33 |
| del_index n (x :: xs) = |
|
23633 | 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 |
||
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
41 |
datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm; |
23633 | 42 |
|
23074 | 43 |
fun is_Less (Less _) = true |
44 |
| is_Less _ = false |
|
23633 | 45 |
|
23074 | 46 |
fun is_LessEq (LessEq _) = true |
47 |
| is_LessEq _ = false |
|
23633 | 48 |
|
23437 | 49 |
fun pr_cell (Less _ ) = " < " |
23633 | 50 |
| pr_cell (LessEq _) = " <=" |
23437 | 51 |
| pr_cell (None _) = " ? " |
52 |
| pr_cell (False _) = " F " |
|
23074 | 53 |
|
54 |
||
55 |
(** Proof attempts to build the matrix **) |
|
23633 | 56 |
|
21131 | 57 |
fun dest_term (t : term) = |
58 |
let |
|
23074 | 59 |
val (vars, prop) = FundefLib.dest_all_all t |
26529 | 60 |
val (prems, concl) = Logic.strip_horn prop |
61 |
val (lhs, rhs) = concl |
|
23633 | 62 |
|> HOLogic.dest_Trueprop |
23074 | 63 |
|> HOLogic.dest_mem |> fst |
23633 | 64 |
|> HOLogic.dest_prod |
21131 | 65 |
in |
23074 | 66 |
(vars, prems, lhs, rhs) |
21131 | 67 |
end |
23633 | 68 |
|
21131 | 69 |
fun mk_goal (vars, prems, lhs, rhs) rel = |
23633 | 70 |
let |
21237 | 71 |
val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop |
23633 | 72 |
in |
27330 | 73 |
fold_rev Logic.all vars (Logic.list_implies (prems, concl)) |
21131 | 74 |
end |
23633 | 75 |
|
76 |
fun prove thy solve_tac t = |
|
77 |
cterm_of thy t |> Goal.init |
|
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset
|
78 |
|> SINGLE solve_tac |> the |
23633 | 79 |
|
80 |
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = |
|
81 |
let |
|
82 |
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) |
|
23881 | 83 |
val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac |
21131 | 84 |
in |
21237 | 85 |
if Thm.no_prems less_thm then |
86 |
Less (Goal.finish less_thm) |
|
87 |
else |
|
88 |
let |
|
23881 | 89 |
val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac |
21237 | 90 |
in |
91 |
if Thm.no_prems lesseq_thm then |
|
23437 | 92 |
LessEq (Goal.finish lesseq_thm, less_thm) |
23633 | 93 |
else |
21237 | 94 |
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm |
23437 | 95 |
else None (lesseq_thm, less_thm) |
21237 | 96 |
end |
21131 | 97 |
end |
23074 | 98 |
|
99 |
||
100 |
(** Search algorithms **) |
|
22309 | 101 |
|
23074 | 102 |
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls) |
22309 | 103 |
|
23074 | 104 |
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col) |
22309 | 105 |
|
23074 | 106 |
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order |
23633 | 107 |
|
21131 | 108 |
(* simple depth-first search algorithm for the table *) |
109 |
fun search_table table = |
|
110 |
case table of |
|
21237 | 111 |
[] => SOME [] |
112 |
| _ => |
|
113 |
let |
|
114 |
val col = find_index (check_col) (transpose table) |
|
115 |
in case col of |
|
23633 | 116 |
~1 => NONE |
21237 | 117 |
| _ => |
118 |
let |
|
22309 | 119 |
val order_opt = (table, col) |-> transform_table |> search_table |
21237 | 120 |
in case order_opt of |
121 |
NONE => NONE |
|
23074 | 122 |
| SOME order =>SOME (col :: transform_order col order) |
21237 | 123 |
end |
124 |
end |
|
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset
|
125 |
|
23074 | 126 |
(** Proof Reconstruction **) |
127 |
||
128 |
(* prove row :: cell list -> tactic *) |
|
129 |
fun prove_row (Less less_thm :: _) = |
|
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
130 |
(rtac @{thm "mlex_less"} 1) |
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset
|
131 |
THEN PRIMITIVE (Thm.elim_implies less_thm) |
23437 | 132 |
| prove_row (LessEq (lesseq_thm, _) :: tail) = |
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
133 |
(rtac @{thm "mlex_leq"} 1) |
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset
|
134 |
THEN PRIMITIVE (Thm.elim_implies lesseq_thm) |
23074 | 135 |
THEN prove_row tail |
136 |
| prove_row _ = sys_error "lexicographic_order" |
|
137 |
||
138 |
||
139 |
(** Error reporting **) |
|
140 |
||
141 |
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) |
|
23633 | 142 |
|
143 |
fun pr_goals ctxt st = |
|
24961 | 144 |
Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |
23437 | 145 |
|> Pretty.chunks |
146 |
|> Pretty.string_of |
|
147 |
||
148 |
fun row_index i = chr (i + 97) |
|
149 |
fun col_index j = string_of_int (j + 1) |
|
150 |
||
23633 | 151 |
fun pr_unprovable_cell _ ((i,j), Less _) = "" |
152 |
| pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = |
|
153 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st |
|
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
154 |
| pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = |
23633 | 155 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less |
156 |
^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq |
|
157 |
| pr_unprovable_cell ctxt ((i,j), False st) = |
|
158 |
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st |
|
23437 | 159 |
|
23633 | 160 |
fun pr_unprovable_subgoals ctxt table = |
23437 | 161 |
table |
162 |
|> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) |
|
163 |
|> flat |
|
23633 | 164 |
|> map (pr_unprovable_cell ctxt) |
23437 | 165 |
|
23633 | 166 |
fun no_order_msg ctxt table tl measure_funs = |
167 |
let |
|
24920 | 168 |
val prterm = Syntax.string_of_term ctxt |
23633 | 169 |
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t |
23074 | 170 |
|
23633 | 171 |
fun pr_goal t i = |
23074 | 172 |
let |
23633 | 173 |
val (_, _, lhs, rhs) = dest_term t |
23074 | 174 |
in (* also show prems? *) |
23128 | 175 |
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs |
23074 | 176 |
end |
177 |
||
178 |
val gc = map (fn i => chr (i + 96)) (1 upto length table) |
|
179 |
val mc = 1 upto length measure_funs |
|
23437 | 180 |
val tstr = "Result matrix:" :: " " ^ concat (map (enclose " " " " o string_of_int) mc) |
23074 | 181 |
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc |
23437 | 182 |
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc |
183 |
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc |
|
23633 | 184 |
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table |
21131 | 185 |
in |
23437 | 186 |
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) |
21131 | 187 |
end |
23633 | 188 |
|
23074 | 189 |
(** The Main Function **) |
23633 | 190 |
fun lexicographic_order_tac ctxt solve_tac (st: thm) = |
21131 | 191 |
let |
21237 | 192 |
val thy = theory_of_thm st |
23074 | 193 |
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st |
194 |
||
195 |
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) |
|
196 |
||
26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset
|
197 |
val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *) |
23633 | 198 |
|
23074 | 199 |
(* 2: create table *) |
200 |
val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl |
|
201 |
||
202 |
val order = the (search_table table) (* 3: search table *) |
|
23633 | 203 |
handle Option => error (no_order_msg ctxt table tl measure_funs) |
23074 | 204 |
|
21237 | 205 |
val clean_table = map (fn x => map (nth x) order) table |
23074 | 206 |
|
207 |
val relation = mk_measures domT (map (nth measure_funs) order) |
|
24920 | 208 |
val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation)) |
23074 | 209 |
|
210 |
in (* 4: proof reconstruction *) |
|
211 |
st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) |
|
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
212 |
THEN (REPEAT (rtac @{thm "wf_mlex"} 1)) |
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset
|
213 |
THEN (rtac @{thm "wf_empty"} 1) |
23074 | 214 |
THEN EVERY (map prove_row clean_table)) |
21131 | 215 |
end |
216 |
||
25545
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset
|
217 |
fun lexicographic_order thms ctxt = |
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset
|
218 |
Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1) |
26749
397a1aeede7d
* New attribute "termination_simp": Simp rules for termination proofs
krauss
parents:
26748
diff
changeset
|
219 |
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))) |
21201 | 220 |
|
23633 | 221 |
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
|
222 |
"termination prover for lexicographic orderings")] |
21131 | 223 |
|
21590 | 224 |
end |