author  wenzelm 
Thu, 11 Oct 2007 19:10:19 +0200  
changeset 24977  9f98751c9628 
parent 24961  5298ee9c3fe5 
child 25509  e537c91b043d 
permissions  rwrr 
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 sizechange tools
krauss
parents:
21319
diff
changeset

11 

7e72185e4b24
exported mk_base_funs for use by sizechange tools
krauss
parents:
21319
diff
changeset

12 
(* exported for use by sizechange termination prototype. 
7e72185e4b24
exported mk_base_funs for use by sizechange 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 = 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

25 
let 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

26 
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

27 
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

28 
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

29 
 mk_ms (f::fs) = 
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

30 
Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs 
23074  31 
in 
24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

32 
mk_ms mfuns 
23074  33 
end 
34 

35 
fun del_index n [] = [] 

36 
 del_index n (x :: xs) = 

23633  37 
if n > 0 then x :: del_index (n  1) xs else xs 
21131  38 

39 
fun transpose ([]::_) = [] 

40 
 transpose xss = map hd xss :: transpose (map tl xss) 

41 

23074  42 
(** Matrix cell datatype **) 
43 

24576
32ddd902b0ad
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents:
23881
diff
changeset

44 
datatype cell = Less of thm LessEq of (thm * thm)  None of (thm * thm)  False of thm; 
23633  45 

23074  46 
fun is_Less (Less _) = true 
47 
 is_Less _ = false 

23633  48 

23074  49 
fun is_LessEq (LessEq _) = true 
50 
 is_LessEq _ = false 

23633  51 

52 
fun thm_of_cell (Less thm) = thm 

53 
 thm_of_cell (LessEq (thm, _)) = thm 

54 
 thm_of_cell (False thm) = thm 

55 
 thm_of_cell (None (thm, _)) = thm 

56 

23437  57 
fun pr_cell (Less _ ) = " < " 
23633  58 
 pr_cell (LessEq _) = " <=" 
23437  59 
 pr_cell (None _) = " ? " 
60 
 pr_cell (False _) = " F " 

23074  61 

62 

63 
(** Generating Measure Functions **) 

64 

23633  65 
fun mk_comp g f = 
66 
let 

67 
val fT = fastype_of f 

23074  68 
val gT as (Type ("fun", [xT, _])) = fastype_of g 
69 
val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0)))) 

70 
in 

71 
Envir.beta_norm (comp $ f $ g) 

72 
end 

73 

74 
fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *) 

75 
map (mk_comp (Const ("fst", T > fT))) (mk_base_funs thy fT) 

76 
@ 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

77 

23074  78 
 mk_base_funs thy T = (* default: size function, if available *) 
79 
if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size]) 

80 
then [HOLogic.size_const T] 

81 
else [] 

82 

83 
fun mk_sum_case f1 f2 = 

84 
let 

23633  85 
val Type ("fun", [fT, Q]) = fastype_of f1 
23074  86 
val Type ("fun", [sT, _]) = fastype_of f2 
87 
in 

88 
Const (@{const_name "Sum_Type.sum_case"}, (fT > Q) > (sT > Q) > Type("+", [fT, sT]) > Q) $ f1 $ f2 

89 
end 

23633  90 

23074  91 
fun constant_0 T = Abs ("x", T, HOLogic.zero) 
92 
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero) 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

93 

23074  94 
fun mk_funorder_funs (Type ("+", [fT, sT])) = 
95 
map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT) 

96 
@ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT) 

23633  97 
 mk_funorder_funs T = [ constant_1 T ] 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

98 

23074  99 
fun mk_ext_base_funs thy (Type("+", [fT, sT])) = 
100 
product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT) 

101 
> map (uncurry mk_sum_case) 

102 
 mk_ext_base_funs thy T = mk_base_funs thy T 

103 

104 
fun mk_all_measure_funs thy (T as Type ("+", _)) = 

105 
mk_ext_base_funs thy T @ mk_funorder_funs T 

106 
 mk_all_measure_funs thy T = mk_base_funs thy T 

107 

108 

109 
(** Proof attempts to build the matrix **) 

23633  110 

21131  111 
fun dest_term (t : term) = 
112 
let 

23074  113 
val (vars, prop) = FundefLib.dest_all_all t 
21237  114 
val prems = Logic.strip_imp_prems prop 
23074  115 
val (lhs, rhs) = Logic.strip_imp_concl prop 
23633  116 
> HOLogic.dest_Trueprop 
23074  117 
> HOLogic.dest_mem > fst 
23633  118 
> HOLogic.dest_prod 
21131  119 
in 
23074  120 
(vars, prems, lhs, rhs) 
21131  121 
end 
23633  122 

21131  123 
fun mk_goal (vars, prems, lhs, rhs) rel = 
23633  124 
let 
21237  125 
val concl = HOLogic.mk_binrel rel (lhs, rhs) > HOLogic.mk_Trueprop 
23633  126 
in 
127 
Logic.list_implies (prems, concl) 

23074  128 
> fold_rev FundefLib.mk_forall vars 
21131  129 
end 
23633  130 

131 
fun prove thy solve_tac t = 

132 
cterm_of thy t > Goal.init 

23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

133 
> SINGLE solve_tac > the 
23633  134 

135 
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = 

136 
let 

137 
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 

23881  138 
val less_thm = goals @{const_name HOL.less} > prove thy solve_tac 
21131  139 
in 
21237  140 
if Thm.no_prems less_thm then 
141 
Less (Goal.finish less_thm) 

142 
else 

143 
let 

23881  144 
val lesseq_thm = goals @{const_name HOL.less_eq} > prove thy solve_tac 
21237  145 
in 
146 
if Thm.no_prems lesseq_thm then 

23437  147 
LessEq (Goal.finish lesseq_thm, less_thm) 
23633  148 
else 
21237  149 
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm 
23437  150 
else None (lesseq_thm, less_thm) 
21237  151 
end 
21131  152 
end 
23074  153 

154 

155 
(** Search algorithms **) 

22309  156 

23074  157 
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls) 
22309  158 

23074  159 
fun transform_table table col = table > filter_out (fn x => is_Less (nth x col)) > map (del_index col) 
22309  160 

23074  161 
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order 
23633  162 

21131  163 
(* simple depthfirst search algorithm for the table *) 
164 
fun search_table table = 

165 
case table of 

21237  166 
[] => SOME [] 
167 
 _ => 

168 
let 

169 
val col = find_index (check_col) (transpose table) 

170 
in case col of 

23633  171 
~1 => NONE 
21237  172 
 _ => 
173 
let 

22309  174 
val order_opt = (table, col) > transform_table > search_table 
21237  175 
in case order_opt of 
176 
NONE => NONE 

23074  177 
 SOME order =>SOME (col :: transform_order col order) 
21237  178 
end 
179 
end 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

180 

23633  181 
(* find all positions of elements in a list *) 
23074  182 
fun find_index_list P = 
183 
let fun find _ [] = [] 

184 
 find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs 

185 
in find 0 end 

22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

186 

23633  187 
(* simple breadthfirst search algorithm for the table *) 
22309  188 
fun bfs_search_table nodes = 
189 
case nodes of 

23633  190 
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic  fun search_table (breadth search finished)" 
22309  191 
 (node::rnodes) => let 
23633  192 
val (order, table) = node 
22309  193 
in 
194 
case table of 

23074  195 
[] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order)) 
22309  196 
 _ => let 
23633  197 
val cols = find_index_list (check_col) (transpose table) 
22309  198 
in 
199 
case cols of 

23633  200 
[] => NONE 
201 
 _ => let 

202 
val newtables = map (transform_table table) cols 

23074  203 
val neworders = map (fn c => c :: order) cols 
22309  204 
val newnodes = neworders ~~ newtables 
205 
in 

206 
bfs_search_table (rnodes @ newnodes) 

23633  207 
end 
22309  208 
end 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

209 
end 
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

210 

23633  211 
fun nsearch_table table = bfs_search_table [([], table)] 
22258
0967b03844b5
changes in lexicographic_order termination tactic
bulwahn
parents:
21817
diff
changeset

212 

23074  213 
(** Proof Reconstruction **) 
214 

215 
(* prove row :: cell list > tactic *) 

216 
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

217 
(rtac @{thm "mlex_less"} 1) 
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset

218 
THEN PRIMITIVE (Thm.elim_implies less_thm) 
23437  219 
 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

220 
(rtac @{thm "mlex_leq"} 1) 
24977
9f98751c9628
replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents:
24961
diff
changeset

221 
THEN PRIMITIVE (Thm.elim_implies lesseq_thm) 
23074  222 
THEN prove_row tail 
223 
 prove_row _ = sys_error "lexicographic_order" 

224 

225 

226 
(** Error reporting **) 

227 

228 
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) 

23633  229 

230 
fun pr_goals ctxt st = 

24961  231 
Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st 
23437  232 
> Pretty.chunks 
233 
> Pretty.string_of 

234 

235 
fun row_index i = chr (i + 97) 

236 
fun col_index j = string_of_int (j + 1) 

237 

23633  238 
fun pr_unprovable_cell _ ((i,j), Less _) = "" 
239 
 pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = 

240 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st 

241 
 pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) = 

242 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less 

243 
^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq 

244 
 pr_unprovable_cell ctxt ((i,j), False st) = 

245 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st 

23437  246 

23633  247 
fun pr_unprovable_subgoals ctxt table = 
23437  248 
table 
249 
> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) 

250 
> flat 

23633  251 
> map (pr_unprovable_cell ctxt) 
23437  252 

23633  253 
fun no_order_msg ctxt table tl measure_funs = 
254 
let 

24920  255 
val prterm = Syntax.string_of_term ctxt 
23633  256 
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t 
23074  257 

23633  258 
fun pr_goal t i = 
23074  259 
let 
23633  260 
val (_, _, lhs, rhs) = dest_term t 
23074  261 
in (* also show prems? *) 
23128  262 
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs 
23074  263 
end 
264 

265 
val gc = map (fn i => chr (i + 96)) (1 upto length table) 

266 
val mc = 1 upto length measure_funs 

23437  267 
val tstr = "Result matrix:" :: " " ^ concat (map (enclose " " " " o string_of_int) mc) 
23074  268 
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc 
23437  269 
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc 
270 
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc 

23633  271 
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table 
21131  272 
in 
23437  273 
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) 
21131  274 
end 
23633  275 

23074  276 
(** The Main Function **) 
23633  277 
fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
21131  278 
let 
21237  279 
val thy = theory_of_thm st 
23074  280 
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st 
281 

282 
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) 

283 

284 
val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *) 

23633  285 

23074  286 
(* 2: create table *) 
287 
val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl 

288 

289 
val order = the (search_table table) (* 3: search table *) 

23633  290 
handle Option => error (no_order_msg ctxt table tl measure_funs) 
23074  291 

21237  292 
val clean_table = map (fn x => map (nth x) order) table 
23074  293 

294 
val relation = mk_measures domT (map (nth measure_funs) order) 

24920  295 
val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation)) 
23074  296 

297 
in (* 4: proof reconstruction *) 

298 
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

299 
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

300 
THEN (rtac @{thm "wf_empty"} 1) 
23074  301 
THEN EVERY (map prove_row clean_table)) 
21131  302 
end 
303 

23633  304 
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

305 
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt))) 
21201  306 

23633  307 
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

308 
"termination prover for lexicographic orderings")] 
21131  309 

21590  310 
end 