author  krauss 
Mon, 02 Feb 2009 15:12:22 +0100  
changeset 29713  55c30d1117ef 
parent 28287  c86fa4e0aedb 
child 30304  d8e4cd2ac2a1 
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 
29713  11 
val lexicographic_order_tac : Proof.context > tactic > tactic 
21510
7e72185e4b24
exported mk_base_funs for use by sizechange tools
krauss
parents:
21319
diff
changeset

12 

21237  13 
val setup: theory > theory 
21131  14 
end 
15 

16 
structure LexicographicOrder : LEXICOGRAPHIC_ORDER = 

17 
struct 

18 

27790
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

19 
open FundefLib 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

20 

23074  21 
(** General stuff **) 
22 

23 
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

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

25 
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

26 
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

27 
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

28 
 mk_ms (f::fs) = 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26529
diff
changeset

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

31 
mk_ms mfuns 
23074  32 
end 
33 

34 
fun del_index n [] = [] 

35 
 del_index n (x :: xs) = 

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

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

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

40 

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

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

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

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

23633  47 

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

23633  50 

23437  51 
fun pr_cell (Less _ ) = " < " 
23633  52 
 pr_cell (LessEq _) = " <=" 
23437  53 
 pr_cell (None _) = " ? " 
54 
 pr_cell (False _) = " F " 

23074  55 

56 

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

23633  58 

21131  59 
fun dest_term (t : term) = 
60 
let 

23074  61 
val (vars, prop) = FundefLib.dest_all_all t 
26529  62 
val (prems, concl) = Logic.strip_horn prop 
63 
val (lhs, rhs) = concl 

23633  64 
> HOLogic.dest_Trueprop 
23074  65 
> HOLogic.dest_mem > fst 
23633  66 
> HOLogic.dest_prod 
21131  67 
in 
23074  68 
(vars, prems, lhs, rhs) 
21131  69 
end 
23633  70 

21131  71 
fun mk_goal (vars, prems, lhs, rhs) rel = 
23633  72 
let 
21237  73 
val concl = HOLogic.mk_binrel rel (lhs, rhs) > HOLogic.mk_Trueprop 
23633  74 
in 
27330  75 
fold_rev Logic.all vars (Logic.list_implies (prems, concl)) 
21131  76 
end 
23633  77 

78 
fun prove thy solve_tac t = 

79 
cterm_of thy t > Goal.init 

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

80 
> SINGLE solve_tac > the 
23633  81 

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

83 
let 

27790
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

84 
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs) 
21131  85 
in 
27790
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

86 
case try_proof (goals @{const_name HOL.less}) solve_tac of 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

87 
Solved thm => Less thm 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

88 
 Stuck thm => 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

89 
(case try_proof (goals @{const_name HOL.less_eq}) solve_tac of 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

90 
Solved thm2 => LessEq (thm2, thm) 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

91 
 Stuck thm2 => 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

92 
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

93 
else None (thm2, thm) 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

94 
 _ => raise Match) (* FIXME *) 
37b4e65d1dbf
FundefLib.try_proof : attempt a proof and see if it works
krauss
parents:
27721
diff
changeset

95 
 _ => raise Match 
21131  96 
end 
23074  97 

98 

99 
(** Search algorithms **) 

22309  100 

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

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

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

21131  107 
(* simple depthfirst search algorithm for the table *) 
108 
fun search_table table = 

109 
case table of 

21237  110 
[] => SOME [] 
111 
 _ => 

112 
let 

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

114 
in case col of 

23633  115 
~1 => NONE 
21237  116 
 _ => 
117 
let 

22309  118 
val order_opt = (table, col) > transform_table > search_table 
21237  119 
in case order_opt of 
120 
NONE => NONE 

23074  121 
 SOME order =>SOME (col :: transform_order col order) 
21237  122 
end 
123 
end 

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

124 

23074  125 
(** Proof Reconstruction **) 
126 

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

128 
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

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

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

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

133 
THEN PRIMITIVE (Thm.elim_implies lesseq_thm) 
23074  134 
THEN prove_row tail 
135 
 prove_row _ = sys_error "lexicographic_order" 

136 

137 

138 
(** Error reporting **) 

139 

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

23633  141 

142 
fun pr_goals ctxt st = 

24961  143 
Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st 
23437  144 
> Pretty.chunks 
145 
> Pretty.string_of 

146 

147 
fun row_index i = chr (i + 97) 

148 
fun col_index j = string_of_int (j + 1) 

149 

23633  150 
fun pr_unprovable_cell _ ((i,j), Less _) = "" 
151 
 pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = 

152 
"(" ^ 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

153 
 pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = 
23633  154 
"(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less 
155 
^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq 

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

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

23437  158 

23633  159 
fun pr_unprovable_subgoals ctxt table = 
23437  160 
table 
161 
> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) 

162 
> flat 

23633  163 
> map (pr_unprovable_cell ctxt) 
23437  164 

23633  165 
fun no_order_msg ctxt table tl measure_funs = 
166 
let 

24920  167 
val prterm = Syntax.string_of_term ctxt 
23633  168 
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t 
23074  169 

23633  170 
fun pr_goal t i = 
23074  171 
let 
23633  172 
val (_, _, lhs, rhs) = dest_term t 
23074  173 
in (* also show prems? *) 
23128  174 
i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs 
23074  175 
end 
176 

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

178 
val mc = 1 upto length measure_funs 

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

23633  183 
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table 
21131  184 
in 
23437  185 
cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."]) 
21131  186 
end 
23633  187 

23074  188 
(** The Main Function **) 
23633  189 
fun lexicographic_order_tac ctxt solve_tac (st: thm) = 
21131  190 
let 
21237  191 
val thy = theory_of_thm st 
23074  192 
val ((trueprop $ (wf $ rel)) :: tl) = prems_of st 
193 

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

195 

26875
e18574413bc4
Measure functions can now be declared via special rules, allowing for a
krauss
parents:
26749
diff
changeset

196 
val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *) 
23633  197 

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

200 

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

23633  202 
handle Option => error (no_order_msg ctxt table tl measure_funs) 
23074  203 

21237  204 
val clean_table = map (fn x => map (nth x) order) table 
23074  205 

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

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

209 
in (* 4: proof reconstruction *) 

210 
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

211 
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

212 
THEN (rtac @{thm "wf_empty"} 1) 
23074  213 
THEN EVERY (map prove_row clean_table)) 
21131  214 
end 
215 

25545
21cd20c1ce98
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
krauss
parents:
25538
diff
changeset

216 
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

217 
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

218 
THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))) 
21201  219 

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

221 
"termination prover for lexicographic orderings")] 
28287
c86fa4e0aedb
termination prover for "fun" can be configured using context data.
krauss
parents:
27790
diff
changeset

222 
#> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order [])) 
21131  223 

21590  224 
end 