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
|
21237
|
10 |
val lexicographic_order : Method.method
|
|
11 |
val setup: theory -> theory
|
21131
|
12 |
end
|
|
13 |
|
|
14 |
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
|
|
15 |
struct
|
|
16 |
|
|
17 |
(* Theory dependencies *)
|
|
18 |
val measures = "List.measures"
|
|
19 |
val wf_measures = thm "wf_measures"
|
|
20 |
val measures_less = thm "measures_less"
|
|
21 |
val measures_lesseq = thm "measures_lesseq"
|
21237
|
22 |
|
21131
|
23 |
fun del_index (n, []) = []
|
|
24 |
| del_index (n, x :: xs) =
|
21237
|
25 |
if n>0 then x :: del_index (n - 1, xs) else xs
|
21131
|
26 |
|
|
27 |
fun transpose ([]::_) = []
|
|
28 |
| transpose xss = map hd xss :: transpose (map tl xss)
|
|
29 |
|
|
30 |
fun mk_sum_case (f1, f2) =
|
|
31 |
case (fastype_of f1, fastype_of f2) of
|
21237
|
32 |
(Type("fun", [A, B]), Type("fun", [C, D])) =>
|
|
33 |
if (B = D) then
|
|
34 |
Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
|
|
35 |
else raise TERM ("mk_sum_case: range type mismatch", [f1, f2])
|
|
36 |
| _ => raise TERM ("mk_sum_case", [f1, f2])
|
|
37 |
|
21131
|
38 |
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
|
|
39 |
| dest_wf t = raise TERM ("dest_wf", [t])
|
21237
|
40 |
|
21131
|
41 |
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
|
21237
|
42 |
|
21131
|
43 |
fun is_Less cell = case cell of (Less _) => true | _ => false
|
21237
|
44 |
|
21131
|
45 |
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
|
21237
|
46 |
|
21131
|
47 |
fun thm_of_cell cell =
|
|
48 |
case cell of
|
21237
|
49 |
Less thm => thm
|
|
50 |
| LessEq thm => thm
|
|
51 |
| False thm => thm
|
|
52 |
| None thm => thm
|
|
53 |
|
21131
|
54 |
fun mk_base_fun_bodys (t : term) (tt : typ) =
|
|
55 |
case tt of
|
21237
|
56 |
Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)
|
|
57 |
| _ => [(t, tt)]
|
|
58 |
|
21131
|
59 |
fun mk_base_fun_header fulltyp (t, typ) =
|
|
60 |
if typ = HOLogic.natT then
|
21237
|
61 |
Abs ("x", fulltyp, t)
|
21131
|
62 |
else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
|
21237
|
63 |
|
21131
|
64 |
fun mk_base_funs (tt: typ) =
|
|
65 |
mk_base_fun_bodys (Bound 0) tt |>
|
21237
|
66 |
map (mk_base_fun_header tt)
|
|
67 |
|
21131
|
68 |
fun mk_ext_base_funs (tt : typ) =
|
|
69 |
case tt of
|
21237
|
70 |
Type("+", [ft, st]) =>
|
|
71 |
product (mk_ext_base_funs ft) (mk_ext_base_funs st)
|
|
72 |
|> map mk_sum_case
|
|
73 |
| _ => mk_base_funs tt
|
|
74 |
|
21131
|
75 |
fun dest_term (t : term) =
|
|
76 |
let
|
21237
|
77 |
val (vars, prop) = (FundefLib.dest_all_all t)
|
|
78 |
val prems = Logic.strip_imp_prems prop
|
|
79 |
val (tuple, rel) = Logic.strip_imp_concl prop
|
|
80 |
|> HOLogic.dest_Trueprop
|
|
81 |
|> HOLogic.dest_mem
|
|
82 |
val (lhs, rhs) = HOLogic.dest_prod tuple
|
21131
|
83 |
in
|
21237
|
84 |
(vars, prems, lhs, rhs, rel)
|
21131
|
85 |
end
|
21237
|
86 |
|
21131
|
87 |
fun mk_goal (vars, prems, lhs, rhs) rel =
|
|
88 |
let
|
21237
|
89 |
val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
|
|
90 |
in
|
|
91 |
Logic.list_implies (prems, concl) |>
|
|
92 |
fold_rev FundefLib.mk_forall vars
|
21131
|
93 |
end
|
21237
|
94 |
|
21131
|
95 |
fun prove (thy: theory) (t: term) =
|
|
96 |
cterm_of thy t |> Goal.init
|
|
97 |
|> SINGLE (CLASIMPSET auto_tac) |> the
|
21237
|
98 |
|
21131
|
99 |
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) =
|
21237
|
100 |
let
|
|
101 |
val goals = mk_goal (vars, prems, lhs, rhs)
|
|
102 |
val less_thm = goals "Orderings.less" |> prove thy
|
21131
|
103 |
in
|
21237
|
104 |
if Thm.no_prems less_thm then
|
|
105 |
Less (Goal.finish less_thm)
|
|
106 |
else
|
|
107 |
let
|
|
108 |
val lesseq_thm = goals "Orderings.less_eq" |> prove thy
|
|
109 |
in
|
|
110 |
if Thm.no_prems lesseq_thm then
|
|
111 |
LessEq (Goal.finish lesseq_thm)
|
|
112 |
else
|
|
113 |
if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
|
|
114 |
else None lesseq_thm
|
|
115 |
end
|
21131
|
116 |
end
|
21237
|
117 |
|
21131
|
118 |
fun mk_row (thy: theory) base_funs (t : term) =
|
|
119 |
let
|
21237
|
120 |
val (vars, prems, lhs, rhs, _) = dest_term t
|
|
121 |
val lhs_list = map (fn x => x $ lhs) base_funs
|
|
122 |
val rhs_list = map (fn x => x $ rhs) base_funs
|
21131
|
123 |
in
|
21237
|
124 |
map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
|
21131
|
125 |
end
|
21237
|
126 |
|
21131
|
127 |
(* simple depth-first search algorithm for the table *)
|
|
128 |
fun search_table table =
|
|
129 |
case table of
|
21237
|
130 |
[] => SOME []
|
|
131 |
| _ =>
|
|
132 |
let
|
|
133 |
val check_col = forall (fn c => is_Less c orelse is_LessEq c)
|
|
134 |
val col = find_index (check_col) (transpose table)
|
|
135 |
in case col of
|
|
136 |
~1 => NONE
|
|
137 |
| _ =>
|
|
138 |
let
|
|
139 |
val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
|
|
140 |
val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
|
|
141 |
in case order_opt of
|
|
142 |
NONE => NONE
|
|
143 |
| SOME order =>SOME (col::(transform_order col order))
|
|
144 |
end
|
|
145 |
end
|
|
146 |
|
21131
|
147 |
fun prove_row row (st : thm) =
|
|
148 |
case row of
|
21237
|
149 |
[] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)"
|
|
150 |
| cell::tail =>
|
|
151 |
case cell of
|
|
152 |
Less less_thm =>
|
|
153 |
let
|
|
154 |
val next_thm = st |> SINGLE (rtac measures_less 1) |> the
|
|
155 |
in
|
|
156 |
implies_elim next_thm less_thm
|
|
157 |
end
|
|
158 |
| LessEq lesseq_thm =>
|
|
159 |
let
|
|
160 |
val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
|
|
161 |
in
|
|
162 |
implies_elim next_thm lesseq_thm
|
|
163 |
|> prove_row tail
|
|
164 |
end
|
|
165 |
| _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
|
|
166 |
|
21131
|
167 |
fun pr_unprovable_subgoals table =
|
|
168 |
filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
|
21237
|
169 |
|> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
|
|
170 |
|
21131
|
171 |
fun pr_goal thy t i =
|
|
172 |
let
|
21237
|
173 |
val (_, prems, lhs, rhs, _) = dest_term t
|
|
174 |
val prterm = string_of_cterm o (cterm_of thy)
|
21131
|
175 |
in
|
21237
|
176 |
(* also show prems? *)
|
21131
|
177 |
i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs)
|
|
178 |
end
|
21237
|
179 |
|
21131
|
180 |
fun pr_fun thy t i =
|
|
181 |
(string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
|
21237
|
182 |
|
21131
|
183 |
fun pr_cell cell = case cell of Less _ => " < "
|
21237
|
184 |
| LessEq _ => " <= "
|
|
185 |
| None _ => " N "
|
|
186 |
| False _ => " F "
|
|
187 |
|
21131
|
188 |
(* fun pr_err: prints the table if tactic failed *)
|
|
189 |
fun pr_err table thy tl base_funs =
|
|
190 |
let
|
21237
|
191 |
val gc = map (fn i => chr (i + 96)) (1 upto (length table))
|
|
192 |
val mc = 1 upto (length base_funs)
|
|
193 |
val tstr = (" " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ " ") mc))) ::
|
|
194 |
(map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
|
|
195 |
val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
|
|
196 |
val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))
|
|
197 |
val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
|
21131
|
198 |
in
|
21237
|
199 |
tstr @ gstr @ mstr @ ustr
|
21131
|
200 |
end
|
21237
|
201 |
|
21131
|
202 |
(* the main function: create table, search table, create relation,
|
|
203 |
and prove the subgoals *)
|
|
204 |
fun lexicographic_order_tac (st: thm) =
|
|
205 |
let
|
21237
|
206 |
val thy = theory_of_thm st
|
|
207 |
val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
|
|
208 |
val next_st = SINGLE (rtac termination_thm 1) st |> the
|
|
209 |
val premlist = prems_of next_st
|
21131
|
210 |
in
|
21237
|
211 |
case premlist of
|
21131
|
212 |
[] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal"
|
|
213 |
| (wf::tl) => let
|
21237
|
214 |
val (var, prop) = FundefLib.dest_all wf
|
|
215 |
val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
|
|
216 |
val crel = cterm_of thy rel
|
|
217 |
val base_funs = mk_ext_base_funs (fastype_of var)
|
|
218 |
val _ = writeln "Creating table"
|
|
219 |
val table = map (mk_row thy base_funs) tl
|
|
220 |
val _ = writeln "Searching for lexicographic order"
|
|
221 |
val possible_order = search_table table
|
|
222 |
in
|
|
223 |
case possible_order of
|
|
224 |
NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
|
|
225 |
| SOME order => let
|
|
226 |
val clean_table = map (fn x => map (nth x) order) table
|
|
227 |
val funs = map (nth base_funs) order
|
|
228 |
val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
|
|
229 |
val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
|
|
230 |
val crelterm = cterm_of thy relterm
|
|
231 |
val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
|
|
232 |
val _ = writeln "Proving subgoals"
|
|
233 |
in
|
|
234 |
next_st |> cterm_instantiate [(crel, crelterm)]
|
|
235 |
|> SINGLE (rtac wf_measures 1) |> the
|
|
236 |
|> fold prove_row clean_table
|
|
237 |
|> Seq.single
|
21131
|
238 |
end
|
|
239 |
end
|
|
240 |
end
|
|
241 |
|
21201
|
242 |
val lexicographic_order = Method.SIMPLE_METHOD lexicographic_order_tac
|
|
243 |
|
|
244 |
val setup = Method.add_methods [("lexicographic_order", Method.no_args lexicographic_order, "termination prover for lexicographic orderings")]
|
21131
|
245 |
|
|
246 |
end |