src/HOL/Tools/Function/lexicographic_order.ML
author wenzelm
Sat Aug 16 19:20:11 2014 +0200 (2014-08-16)
changeset 57959 1bfed12a7646
parent 56231 b98813774a63
child 58819 aa43c6f05bca
permissions -rw-r--r--
updated to named_theorems;
modernized module name and setup;
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@49856
   123
fun row_index i = chr (i + 97)  (* FIXME not scalable wrt. chr range *)
wenzelm@49856
   124
fun col_index j = string_of_int (j + 1)  (* FIXME not scalable wrt. table layout *)
krauss@23437
   125
wenzelm@49856
   126
fun pr_unprovable_cell _ ((i,j), Less _) = []
wenzelm@23633
   127
  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
wenzelm@51958
   128
      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
wenzelm@51958
   129
       Goal_Display.string_of_goal ctxt st]
krauss@26875
   130
  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
wenzelm@51958
   131
      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
wenzelm@51958
   132
       Goal_Display.string_of_goal ctxt st_less ^
wenzelm@51958
   133
       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
wenzelm@51958
   134
       Goal_Display.string_of_goal ctxt st_leq]
wenzelm@23633
   135
  | pr_unprovable_cell ctxt ((i,j), False st) =
wenzelm@51958
   136
      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
wenzelm@51958
   137
       Goal_Display.string_of_goal ctxt st]
krauss@23437
   138
wenzelm@23633
   139
fun pr_unprovable_subgoals ctxt table =
krauss@34232
   140
  table
krauss@34232
   141
  |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
krauss@34232
   142
  |> flat
wenzelm@49856
   143
  |> maps (pr_unprovable_cell ctxt)
krauss@23437
   144
krauss@39928
   145
fun pr_cell (Less _ ) = " < "
krauss@39928
   146
  | pr_cell (LessEq _) = " <="
krauss@39928
   147
  | pr_cell (None _) = " ? "
krauss@39928
   148
  | pr_cell (False _) = " F "
krauss@39928
   149
krauss@39926
   150
fun no_order_msg ctxt ltable tl measure_funs =
krauss@34232
   151
  let
krauss@39926
   152
    val table = map (map Lazy.force) ltable
krauss@34232
   153
    val prterm = Syntax.string_of_term ctxt
krauss@34232
   154
    fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
krauss@23074
   155
krauss@34232
   156
    fun pr_goal t i =
krauss@34232
   157
      let
krauss@34232
   158
        val (_, _, lhs, rhs) = dest_term t
krauss@34232
   159
      in (* also show prems? *)
krauss@34232
   160
           i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
krauss@34232
   161
      end
krauss@23074
   162
krauss@34232
   163
    val gc = map (fn i => chr (i + 96)) (1 upto length table)
krauss@34232
   164
    val mc = 1 upto length measure_funs
krauss@34232
   165
    val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
krauss@34232
   166
      :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
krauss@34232
   167
    val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
krauss@34232
   168
    val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
krauss@34232
   169
    val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
krauss@34232
   170
  in
krauss@34232
   171
    cat_lines (ustr @ gstr @ mstr @ tstr @
krauss@34232
   172
    ["", "Could not find lexicographic termination order."])
krauss@34232
   173
  end
wenzelm@23633
   174
krauss@23074
   175
(** The Main Function **)
wenzelm@30493
   176
wenzelm@56231
   177
fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
krauss@34232
   178
  let
wenzelm@42361
   179
    val thy = Proof_Context.theory_of ctxt
krauss@34232
   180
    val ((_ $ (_ $ rel)) :: tl) = prems_of st
krauss@23074
   181
krauss@34232
   182
    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
krauss@23074
   183
krauss@34232
   184
    val measure_funs = (* 1: generate measures *)
wenzelm@57959
   185
      Measure_Functions.get_measure_functions ctxt domT
wenzelm@23633
   186
krauss@34232
   187
    val table = (* 2: create table *)
krauss@39926
   188
      map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
krauss@34232
   189
  in
wenzelm@56231
   190
    fn st =>
wenzelm@56231
   191
      case search_table table of
wenzelm@56231
   192
        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
wenzelm@56231
   193
      | SOME order =>
wenzelm@56231
   194
        let
wenzelm@56231
   195
          val clean_table = map (fn x => map (nth x) order) table
wenzelm@56231
   196
          val relation = mk_measures domT (map (nth measure_funs) order)
wenzelm@56231
   197
          val _ =
wenzelm@56231
   198
            if not quiet then
wenzelm@56231
   199
              Pretty.writeln (Pretty.block
wenzelm@56231
   200
                [Pretty.str "Found termination order:", Pretty.brk 1,
wenzelm@56231
   201
                  Pretty.quote (Syntax.pretty_term ctxt relation)])
wenzelm@56231
   202
            else ()
wenzelm@56231
   203
  
wenzelm@56231
   204
        in (* 4: proof reconstruction *)
wenzelm@56231
   205
          st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
wenzelm@56231
   206
          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
wenzelm@56231
   207
          THEN (rtac @{thm "wf_empty"} 1)
wenzelm@56231
   208
          THEN EVERY (map prove_row clean_table))
wenzelm@56231
   209
        end
wenzelm@56231
   210
  end) 1 st;
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@57959
   215
    (auto_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems termination_simp})))
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;