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