author  krauss 
Fri, 30 Nov 2007 16:23:52 +0100  
changeset 25509  e537c91b043d 
parent 24977  9f98751c9628 
child 25538  58e8ba3b792b 
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 

25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

22 
(** Userdeclared size functions **) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

23 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

24 
structure SizeFunsData = GenericDataFun 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

25 
( 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

26 
type T = term NetRules.T; 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

27 
val empty = NetRules.init (op aconv) I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

28 
val copy = I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

29 
val extend = I 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

30 
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

31 
); 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

32 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

33 
fun add_sfun f ctxt = 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

34 
SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

35 
val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f)))) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

36 

e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

37 
fun get_sfuns T thy = 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

38 
map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

39 
(domain_type (fastype_of f), T) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

40 
Vartab.empty) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

41 
f) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

42 
handle Type.TYPE_MATCH => NONE) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

43 
(NetRules.rules (SizeFunsData.get (Context.Theory thy))) 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

44 

23074  45 
(** General stuff **) 
46 

47 
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

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

49 
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

50 
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

51 
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

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

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

55 
mk_ms mfuns 
23074  56 
end 
57 

58 
fun del_index n [] = [] 

59 
 del_index n (x :: xs) = 

23633  60 
if n > 0 then x :: del_index (n  1) xs else xs 
21131  61 

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

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

64 

23074  65 
(** Matrix cell datatype **) 
66 

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

67 
datatype cell = Less of thm LessEq of (thm * thm)  None of (thm * thm)  False of thm; 
23633  68 

23074  69 
fun is_Less (Less _) = true 
70 
 is_Less _ = false 

23633  71 

23074  72 
fun is_LessEq (LessEq _) = true 
73 
 is_LessEq _ = false 

23633  74 

75 
fun thm_of_cell (Less thm) = thm 

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

77 
 thm_of_cell (False thm) = thm 

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

79 

23437  80 
fun pr_cell (Less _ ) = " < " 
23633  81 
 pr_cell (LessEq _) = " <=" 
23437  82 
 pr_cell (None _) = " ? " 
83 
 pr_cell (False _) = " F " 

23074  84 

85 

86 
(** Generating Measure Functions **) 

87 

23633  88 
fun mk_comp g f = 
89 
let 

90 
val fT = fastype_of f 

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

93 
in 

94 
Envir.beta_norm (comp $ f $ g) 

95 
end 

96 

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

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

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

100 

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

25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

103 
then (HOLogic.size_const T) :: get_sfuns T thy 
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

104 
else get_sfuns T thy 
23074  105 

106 
fun mk_sum_case f1 f2 = 

107 
let 

23633  108 
val Type ("fun", [fT, Q]) = fastype_of f1 
23074  109 
val Type ("fun", [sT, _]) = fastype_of f2 
110 
in 

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

112 
end 

23633  113 

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

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

116 

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

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

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

121 

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

124 
> map (uncurry mk_sum_case) 

125 
 mk_ext_base_funs thy T = mk_base_funs thy T 

126 

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

128 
mk_ext_base_funs thy T @ mk_funorder_funs T 

129 
 mk_all_measure_funs thy T = mk_base_funs thy T 

130 

131 

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

23633  133 

21131  134 
fun dest_term (t : term) = 
135 
let 

23074  136 
val (vars, prop) = FundefLib.dest_all_all t 
21237  137 
val prems = Logic.strip_imp_prems prop 
23074  138 
val (lhs, rhs) = Logic.strip_imp_concl prop 
23633  139 
> HOLogic.dest_Trueprop 
23074  140 
> HOLogic.dest_mem > fst 
23633  141 
> HOLogic.dest_prod 
21131  142 
in 
23074  143 
(vars, prems, lhs, rhs) 
21131  144 
end 
23633  145 

21131  146 
fun mk_goal (vars, prems, lhs, rhs) rel = 
23633  147 
let 
21237  148 
val concl = HOLogic.mk_binrel rel (lhs, rhs) > HOLogic.mk_Trueprop 
23633  149 
in 
150 
Logic.list_implies (prems, concl) 

23074  151 
> fold_rev FundefLib.mk_forall vars 
21131  152 
end 
23633  153 

154 
fun prove thy solve_tac t = 

155 
cterm_of thy t > Goal.init 

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

156 
> SINGLE solve_tac > the 
23633  157 

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

159 
let 

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

23881  161 
val less_thm = goals @{const_name HOL.less} > prove thy solve_tac 
21131  162 
in 
21237  163 
if Thm.no_prems less_thm then 
164 
Less (Goal.finish less_thm) 

165 
else 

166 
let 

23881  167 
val lesseq_thm = goals @{const_name HOL.less_eq} > prove thy solve_tac 
21237  168 
in 
169 
if Thm.no_prems lesseq_thm then 

23437  170 
LessEq (Goal.finish lesseq_thm, less_thm) 
23633  171 
else 
21237  172 
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm 
23437  173 
else None (lesseq_thm, less_thm) 
21237  174 
end 
21131  175 
end 
23074  176 

177 

178 
(** Search algorithms **) 

22309  179 

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

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

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

21131  186 
(* simple depthfirst search algorithm for the table *) 
187 
fun search_table table = 

188 
case table of 

21237  189 
[] => SOME [] 
190 
 _ => 

191 
let 

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

193 
in case col of 

23633  194 
~1 => NONE 
21237  195 
 _ => 
196 
let 

22309  197 
val order_opt = (table, col) > transform_table > search_table 
21237  198 
in case order_opt of 
199 
NONE => NONE 

23074  200 
 SOME order =>SOME (col :: transform_order col order) 
21237  201 
end 
202 
end 

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

203 

23633  204 
(* find all positions of elements in a list *) 
23074  205 
fun find_index_list P = 
206 
let fun find _ [] = [] 

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

208 
in find 0 end 

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

209 

23633  210 
(* simple breadthfirst search algorithm for the table *) 
22309  211 
fun bfs_search_table nodes = 
212 
case nodes of 

23633  213 
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic  fun search_table (breadth search finished)" 
22309  214 
 (node::rnodes) => let 
23633  215 
val (order, table) = node 
22309  216 
in 
217 
case table of 

23074  218 
[] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order)) 
22309  219 
 _ => let 
23633  220 
val cols = find_index_list (check_col) (transpose table) 
22309  221 
in 
222 
case cols of 

23633  223 
[] => NONE 
224 
 _ => let 

225 
val newtables = map (transform_table table) cols 

23074  226 
val neworders = map (fn c => c :: order) cols 
22309  227 
val newnodes = neworders ~~ newtables 
228 
in 

229 
bfs_search_table (rnodes @ newnodes) 

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

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

233 

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

235 

23074  236 
(** Proof Reconstruction **) 
237 

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

239 
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

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

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

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

244 
THEN PRIMITIVE (Thm.elim_implies lesseq_thm) 
23074  245 
THEN prove_row tail 
246 
 prove_row _ = sys_error "lexicographic_order" 

247 

248 

249 
(** Error reporting **) 

250 

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

23633  252 

253 
fun pr_goals ctxt st = 

24961  254 
Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st 
23437  255 
> Pretty.chunks 
256 
> Pretty.string_of 

257 

258 
fun row_index i = chr (i + 97) 

259 
fun col_index j = string_of_int (j + 1) 

260 

23633  261 
fun pr_unprovable_cell _ ((i,j), Less _) = "" 
262 
 pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = 

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

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

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

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

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

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

23437  269 

23633  270 
fun pr_unprovable_subgoals ctxt table = 
23437  271 
table 
272 
> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) 

273 
> flat 

23633  274 
> map (pr_unprovable_cell ctxt) 
23437  275 

23633  276 
fun no_order_msg ctxt table tl measure_funs = 
277 
let 

24920  278 
val prterm = Syntax.string_of_term ctxt 
23633  279 
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t 
23074  280 

23633  281 
fun pr_goal t i = 
23074  282 
let 
23633  283 
val (_, _, lhs, rhs) = dest_term t 
23074  284 
in (* also show prems? *) 
23128  285 
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs 
23074  286 
end 
287 

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

289 
val mc = 1 upto length measure_funs 

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

23633  294 
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table 
21131  295 
in 
23437  296 
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) 
21131  297 
end 
23633  298 

23074  299 
(** The Main Function **) 
23633  300 
fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
21131  301 
let 
21237  302 
val thy = theory_of_thm st 
23074  303 
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st 
304 

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

306 

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

23633  308 

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

311 

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

23633  313 
handle Option => error (no_order_msg ctxt table tl measure_funs) 
23074  314 

21237  315 
val clean_table = map (fn x => map (nth x) order) table 
23074  316 

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

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

320 
in (* 4: proof reconstruction *) 

321 
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

322 
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

323 
THEN (rtac @{thm "wf_empty"} 1) 
23074  324 
THEN EVERY (map prove_row clean_table)) 
21131  325 
end 
326 

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

328 
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt))) 
21201  329 

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

331 
"termination prover for lexicographic orderings")] 
25509
e537c91b043d
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents:
24977
diff
changeset

332 
#> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")] 
21131  333 

21590  334 
end 