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