author  krauss 
Tue, 22 May 2007 17:25:26 +0200  
changeset 23074  a53cb8ddb052 
parent 23056  448827ccd9e9 
child 23128  8e0abe0fa80f 
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 = 

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) = 

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 

21131  39 
datatype cell = Less of thm  LessEq of thm  None of thm  False of thm; 
21237  40 

23074  41 
fun is_Less (Less _) = true 
42 
 is_Less _ = false 

21237  43 

23074  44 
fun is_LessEq (LessEq _) = true 
45 
 is_LessEq _ = false 

21237  46 

23074  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 

21237  51 

23074  52 
fun pr_cell (Less _ ) = " < " 
53 
 pr_cell (LessEq _) = " <= " 

54 
 pr_cell (None _) = " N " 

55 
 pr_cell (False _) = " F " 

56 

57 

58 
(** Generating Measure Functions **) 

59 

60 
fun mk_comp g f = 

61 
let 

62 
val fT = fastype_of f 

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 

80 
val Type ("fun", [fT, Q]) = fastype_of f1 

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 

85 

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) 

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 **) 

21237  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 
21237  111 
> HOLogic.dest_Trueprop 
23074  112 
> HOLogic.dest_mem > fst 
113 
> HOLogic.dest_prod 

21131  114 
in 
23074  115 
(vars, prems, lhs, rhs) 
21131  116 
end 
21237  117 

21131  118 
fun mk_goal (vars, prems, lhs, rhs) rel = 
119 
let 

21237  120 
val concl = HOLogic.mk_binrel rel (lhs, rhs) > HOLogic.mk_Trueprop 
121 
in 

23074  122 
Logic.list_implies (prems, concl) 
123 
> fold_rev FundefLib.mk_forall vars 

21131  124 
end 
21237  125 

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

126 
fun prove (thy: theory) solve_tac (t: term) = 
21131  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 
21237  129 

23074  130 
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun = 
21237  131 
let 
23074  132 
val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

133 
val less_thm = goals "Orderings.ord_class.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 

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

139 
val lesseq_thm = goals "Orderings.ord_class.less_eq" > prove thy solve_tac 
21237  140 
in 
141 
if Thm.no_prems lesseq_thm then 

142 
LessEq (Goal.finish lesseq_thm) 

143 
else 

144 
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm 

145 
else None lesseq_thm 

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 
21237  157 

21131  158 
(* simple depthfirst 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 

166 
~1 => NONE 

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 

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

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 

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

182 
(* simple breadthfirst search algorithm for the table *) 
22309  183 
fun bfs_search_table nodes = 
184 
case nodes of 

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

185 
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic  fun search_table (breadth search finished)" 
22309  186 
 (node::rnodes) => let 
187 
val (order, table) = node 

188 
in 

189 
case table of 

23074  190 
[] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order)) 
22309  191 
 _ => let 
192 
val cols = find_index_list (check_col) (transpose table) 

193 
in 

194 
case cols of 

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) 

202 
end 

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 

22309  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) 

214 
 prove_row (LessEq lesseq_thm :: tail) = 

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)) 

224 

21131  225 
fun pr_unprovable_subgoals table = 
23074  226 
filter_out (fn x => is_Less x orelse is_LessEq x) (flat table) 
21237  227 
> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell) 
228 

23074  229 
fun no_order_msg table thy tl measure_funs = 
230 
let 

231 
fun pr_fun t i = string_of_int i ^ ") " ^ string_of_cterm (cterm_of thy t) 

232 

233 
fun pr_goal t i = 

234 
let 

235 
val (_, _, lhs, rhs) = dest_term t 

236 
val prterm = string_of_cterm o (cterm_of thy) 

237 
in (* also show prems? *) 

238 
i ^ ") " ^ prterm lhs ^ " '<' " ^ prterm rhs 

239 
end 

240 

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

242 
val mc = 1 upto length measure_funs 

243 
val tstr = " " ^ concat (map (enclose " " " " o string_of_int) mc) 

244 
:: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc 

245 
val gstr = "Goals:" :: map2 pr_goal tl gc 

246 
val mstr = "Measures:" :: map2 pr_fun measure_funs mc 

247 
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals table 

21131  248 
in 
23074  249 
cat_lines ("Could not find lexicographic termination order:" :: tstr @ gstr @ mstr @ ustr) 
21131  250 
end 
21237  251 

23074  252 
(** The Main Function **) 
23055
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

253 
fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
21131  254 
let 
21237  255 
val thy = theory_of_thm st 
23074  256 
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st 
257 

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

259 

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

261 

262 
(* 2: create table *) 

263 
val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl 

264 

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

266 
handle Option => error (no_order_msg table thy tl measure_funs) 

267 

21237  268 
val clean_table = map (fn x => map (nth x) order) table 
23074  269 

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

271 
val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation)) 

272 

273 
in (* 4: proof reconstruction *) 

274 
st > (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)]) 

275 
THEN rtac @{thm "wf_measures"} 1 

276 
THEN EVERY (map prove_row clean_table)) 

21131  277 
end 
278 

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

279 
fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1 
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

280 
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt))) 
21201  281 

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

282 
val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, 
34158639dc12
Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents:
22997
diff
changeset

283 
"termination prover for lexicographic orderings")] 
21131  284 

21590  285 
end 