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