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