1(*  Title:       HOL/Tools/Function/lexicographic_order.ML
2    Author:      Lukas Bulwahn, TU Muenchen
3    Author:      Alexander Krauss, TU Muenchen
4
5Termination proofs with lexicographic orders.
6*)
7
8signature LEXICOGRAPHIC_ORDER =
9sig
10  val lex_order_tac : bool -> Proof.context -> tactic -> tactic
11  val lexicographic_order_tac : bool -> Proof.context -> tactic
12end
13
14structure Lexicographic_Order : LEXICOGRAPHIC_ORDER =
15struct
16
17open Function_Lib
18
19(** General stuff **)
20
21fun mk_measures domT mfuns =
22  let
23    val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
24    val mlexT = (domT --> HOLogic.natT) --> relT --> relT
25    fun mk_ms [] = Const (\<^const_abbrev>\<open>Set.empty\<close>, relT)
26      | mk_ms (f::fs) =
27        Const (\<^const_name>\<open>mlex_prod\<close>, mlexT) $ f $ mk_ms fs
28  in
29    mk_ms mfuns
30  end
31
32fun del_index n [] = []
33  | del_index n (x :: xs) =
34  if n > 0 then x :: del_index (n - 1) xs else xs
35
36fun transpose ([]::_) = []
37  | transpose xss = map hd xss :: transpose (map tl xss)
38
39(** Matrix cell datatype **)
40
41datatype cell =
42  Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
43
44fun is_Less lcell = case Lazy.force lcell of Less _ => true | _ => false;
45fun is_LessEq lcell = case Lazy.force lcell of LessEq _ => true | _ => false;
46
47
48(** Proof attempts to build the matrix **)
49
50fun dest_term t =
51  let
52    val (vars, prop) = Function_Lib.dest_all_all t
53    val (prems, concl) = Logic.strip_horn prop
54    val (lhs, rhs) = concl
55      |> HOLogic.dest_Trueprop
56      |> HOLogic.dest_mem |> fst
57      |> HOLogic.dest_prod
58  in
59    (vars, prems, lhs, rhs)
60  end
61
62fun mk_goal (vars, prems, lhs, rhs) rel =
63  let
64    val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
65  in
66    fold_rev Logic.all vars (Logic.list_implies (prems, concl))
67  end
68
69fun mk_cell ctxt solve_tac (vars, prems, lhs, rhs) mfun = Lazy.lazy (fn _ =>
70  let
71    val goals = Thm.cterm_of ctxt o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
72  in
73    (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less\<close>) solve_tac of
74      Solved thm => Less thm
75    | Stuck thm =>
76        (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less_eq\<close>) solve_tac of
77          Solved thm2 => LessEq (thm2, thm)
78        | Stuck thm2 =>
79            if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] then False thm2
80            else None (thm2, thm)
81        | _ => raise Match) (* FIXME *)
82    | _ => raise Match)
83  end);
84
85
86(** Search algorithms **)
87
88fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall is_LessEq ls)
89
90fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
91
92fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
93
94(* simple depth-first search algorithm for the table *)
95fun search_table [] = SOME []
96  | search_table table =
97    case find_index check_col (transpose table) of
98       ~1 => NONE
99     | col =>
100         (case (table, col) |-> transform_table |> search_table of
101            NONE => NONE
102          | SOME order => SOME (col :: transform_order col order))
103
104
105(** Proof Reconstruction **)
106
107fun prove_row_tac ctxt (c :: cs) =
108      (case Lazy.force c of
109        Less thm =>
110          resolve_tac ctxt @{thms mlex_less} 1
111          THEN PRIMITIVE (Thm.elim_implies thm)
112      | LessEq (thm, _) =>
113          resolve_tac ctxt @{thms mlex_leq} 1
114          THEN PRIMITIVE (Thm.elim_implies thm)
115          THEN prove_row_tac ctxt cs
116      | _ => raise General.Fail "lexicographic_order")
117  | prove_row_tac _ [] = no_tac;
118
119
120(** Error reporting **)
121
122fun row_index i = chr (i + 97)  (* FIXME not scalable wrt. chr range *)
123fun col_index j = string_of_int (j + 1)  (* FIXME not scalable wrt. table layout *)
124
125fun pr_unprovable_cell _ ((i,j), Less _) = []
126  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
127      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
128       Goal_Display.string_of_goal ctxt st]
129  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
130      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
131       Goal_Display.string_of_goal ctxt st_less ^
132       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
133       Goal_Display.string_of_goal ctxt st_leq]
134  | pr_unprovable_cell ctxt ((i,j), False st) =
135      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
136       Goal_Display.string_of_goal ctxt st]
137
138fun pr_unprovable_subgoals ctxt table =
139  table
140  |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
141  |> flat
142  |> maps (pr_unprovable_cell ctxt)
143
144fun pr_cell (Less _ ) = " < "
145  | pr_cell (LessEq _) = " <="
146  | pr_cell (None _) = " ? "
147  | pr_cell (False _) = " F "
148
149fun no_order_msg ctxt ltable tl measure_funs =
150  let
151    val table = map (map Lazy.force) ltable
152    val prterm = Syntax.string_of_term ctxt
153    fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
154
155    fun pr_goal t i =
156      let
157        val (_, _, lhs, rhs) = dest_term t
158      in (* also show prems? *)
159           i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
160      end
161
162    val gc = map (fn i => chr (i + 96)) (1 upto length table)
163    val mc = 1 upto length measure_funs
164    val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
165      :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
166    val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
167    val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
168    val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
169  in
170    cat_lines (ustr @ gstr @ mstr @ tstr @
171    ["", "Could not find lexicographic termination order."])
172  end
173
174(** The Main Function **)
175
176fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
177  let
178    val ((_ $ (_ $ rel)) :: tl) = Thm.prems_of st
179
180    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
181
182    val measure_funs = (* 1: generate measures *)
183      Measure_Functions.get_measure_functions ctxt domT
184
185    val table = (* 2: create table *)
186      map (fn t => map (mk_cell ctxt solve_tac (dest_term t)) measure_funs) tl
187  in
188    fn st =>
189      case search_table table of
190        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
191      | SOME order =>
192        let
193          val clean_table = map (fn x => map (nth x) order) table
194          val relation = mk_measures domT (map (nth measure_funs) order)
195          val _ =
196            if not quiet then
197              Pretty.writeln (Pretty.block
198                [Pretty.str "Found termination order:", Pretty.brk 1,
199                  Pretty.quote (Syntax.pretty_term ctxt relation)])
200            else ()
201  
202        in (* 4: proof reconstruction *)
203          st |>
204          (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
205            THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
206            THEN (resolve_tac ctxt @{thms wf_empty} 1)
207            THEN EVERY (map (prove_row_tac ctxt) clean_table))
208        end
209  end) 1 st;
210
211fun lexicographic_order_tac quiet ctxt =
212  TRY (Function_Common.termination_rule_tac ctxt 1) THEN
213  lex_order_tac quiet ctxt
214    (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp})))
215
216val _ =
217  Theory.setup
218    (Context.theory_map
219      (Function_Common.set_termination_prover lexicographic_order_tac))
220
221end;
222