src/HOL/Tools/Function/lexicographic_order.ML
author haftmann
Wed Feb 10 14:12:04 2010 +0100 (2010-02-10)
changeset 35092 cfe605c54e50
parent 34974 18b41bba42b5
child 35402 115a5a95710a
permissions -rw-r--r--
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
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
krauss@34232
    27
    fun mk_ms [] = Const (@{const_name 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@34232
    44
  Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
wenzelm@23633
    45
krauss@23074
    46
fun is_Less (Less _) = true
krauss@23074
    47
  | is_Less _ = false
wenzelm@23633
    48
krauss@23074
    49
fun is_LessEq (LessEq _) = true
krauss@23074
    50
  | is_LessEq _ = false
wenzelm@23633
    51
krauss@23437
    52
fun pr_cell (Less _ ) = " < "
wenzelm@23633
    53
  | pr_cell (LessEq _) = " <="
krauss@23437
    54
  | pr_cell (None _) = " ? "
krauss@23437
    55
  | pr_cell (False _) = " F "
krauss@23074
    56
krauss@23074
    57
krauss@23074
    58
(** Proof attempts to build the matrix **)
wenzelm@23633
    59
bulwahn@21131
    60
fun dest_term (t : term) =
krauss@34232
    61
  let
krauss@34232
    62
    val (vars, prop) = Function_Lib.dest_all_all t
krauss@34232
    63
    val (prems, concl) = Logic.strip_horn prop
krauss@34232
    64
    val (lhs, rhs) = concl
krauss@34232
    65
      |> HOLogic.dest_Trueprop
krauss@34232
    66
      |> HOLogic.dest_mem |> fst
krauss@34232
    67
      |> HOLogic.dest_prod
krauss@34232
    68
  in
krauss@34232
    69
    (vars, prems, lhs, rhs)
krauss@34232
    70
  end
wenzelm@23633
    71
bulwahn@21131
    72
fun mk_goal (vars, prems, lhs, rhs) rel =
krauss@34232
    73
  let
krauss@34232
    74
    val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
krauss@34232
    75
  in
krauss@34232
    76
    fold_rev Logic.all vars (Logic.list_implies (prems, concl))
krauss@34232
    77
  end
wenzelm@23633
    78
wenzelm@23633
    79
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
krauss@34232
    80
  let
krauss@34232
    81
    val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
krauss@34232
    82
  in
haftmann@35092
    83
    case try_proof (goals @{const_name Orderings.less}) solve_tac of
krauss@34232
    84
      Solved thm => Less thm
krauss@34232
    85
    | Stuck thm =>
haftmann@35092
    86
      (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
krauss@34232
    87
         Solved thm2 => LessEq (thm2, thm)
krauss@34232
    88
       | Stuck thm2 =>
krauss@34232
    89
         if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
krauss@34232
    90
         else None (thm2, thm)
krauss@34232
    91
       | _ => raise Match) (* FIXME *)
krauss@34232
    92
    | _ => raise Match
krauss@34232
    93
  end
krauss@23074
    94
krauss@23074
    95
krauss@23074
    96
(** Search algorithms **)
bulwahn@22309
    97
krauss@23074
    98
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls)
bulwahn@22309
    99
krauss@23074
   100
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
bulwahn@22309
   101
krauss@23074
   102
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
wenzelm@23633
   103
bulwahn@21131
   104
(* simple depth-first search algorithm for the table *)
bulwahn@21131
   105
fun search_table table =
krauss@34232
   106
  case table of
krauss@34232
   107
    [] => SOME []
krauss@34232
   108
  | _ =>
krauss@34232
   109
    let
krauss@34232
   110
      val col = find_index (check_col) (transpose table)
krauss@34232
   111
    in case col of
krauss@34232
   112
         ~1 => NONE
krauss@34232
   113
       | _ =>
krauss@34232
   114
         let
krauss@34232
   115
           val order_opt = (table, col) |-> transform_table |> search_table
krauss@34232
   116
         in case order_opt of
krauss@34232
   117
              NONE => NONE
krauss@34232
   118
            | SOME order =>SOME (col :: transform_order col order)
krauss@34232
   119
         end
krauss@34232
   120
    end
bulwahn@22258
   121
krauss@23074
   122
(** Proof Reconstruction **)
krauss@23074
   123
krauss@23074
   124
(* prove row :: cell list -> tactic *)
krauss@23074
   125
fun prove_row (Less less_thm :: _) =
krauss@24576
   126
    (rtac @{thm "mlex_less"} 1)
wenzelm@24977
   127
    THEN PRIMITIVE (Thm.elim_implies less_thm)
krauss@23437
   128
  | prove_row (LessEq (lesseq_thm, _) :: tail) =
krauss@24576
   129
    (rtac @{thm "mlex_leq"} 1)
wenzelm@24977
   130
    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
krauss@23074
   131
    THEN prove_row tail
krauss@23074
   132
  | prove_row _ = sys_error "lexicographic_order"
krauss@23074
   133
krauss@23074
   134
krauss@23074
   135
(** Error reporting **)
krauss@23074
   136
wenzelm@23633
   137
fun pr_goals ctxt st =
krauss@34232
   138
  Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
krauss@34232
   139
  |> Pretty.chunks
krauss@34232
   140
  |> Pretty.string_of
krauss@23437
   141
krauss@23437
   142
fun row_index i = chr (i + 97)
krauss@23437
   143
fun col_index j = string_of_int (j + 1)
krauss@23437
   144
wenzelm@23633
   145
fun pr_unprovable_cell _ ((i,j), Less _) = ""
wenzelm@23633
   146
  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
wenzelm@23633
   147
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
krauss@26875
   148
  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
wenzelm@23633
   149
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
wenzelm@23633
   150
      ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
wenzelm@23633
   151
  | pr_unprovable_cell ctxt ((i,j), False st) =
wenzelm@23633
   152
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
krauss@23437
   153
wenzelm@23633
   154
fun pr_unprovable_subgoals ctxt table =
krauss@34232
   155
  table
krauss@34232
   156
  |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
krauss@34232
   157
  |> flat
krauss@34232
   158
  |> map (pr_unprovable_cell ctxt)
krauss@23437
   159
wenzelm@23633
   160
fun no_order_msg ctxt table tl measure_funs =
krauss@34232
   161
  let
krauss@34232
   162
    val prterm = Syntax.string_of_term ctxt
krauss@34232
   163
    fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
krauss@23074
   164
krauss@34232
   165
    fun pr_goal t i =
krauss@34232
   166
      let
krauss@34232
   167
        val (_, _, lhs, rhs) = dest_term t
krauss@34232
   168
      in (* also show prems? *)
krauss@34232
   169
           i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
krauss@34232
   170
      end
krauss@23074
   171
krauss@34232
   172
    val gc = map (fn i => chr (i + 96)) (1 upto length table)
krauss@34232
   173
    val mc = 1 upto length measure_funs
krauss@34232
   174
    val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
krauss@34232
   175
      :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
krauss@34232
   176
    val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
krauss@34232
   177
    val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
krauss@34232
   178
    val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
krauss@34232
   179
  in
krauss@34232
   180
    cat_lines (ustr @ gstr @ mstr @ tstr @
krauss@34232
   181
    ["", "Could not find lexicographic termination order."])
krauss@34232
   182
  end
wenzelm@23633
   183
krauss@23074
   184
(** The Main Function **)
wenzelm@30493
   185
krauss@33351
   186
fun lex_order_tac quiet ctxt solve_tac (st: thm) =
krauss@34232
   187
  let
krauss@34232
   188
    val thy = ProofContext.theory_of ctxt
krauss@34232
   189
    val ((_ $ (_ $ rel)) :: tl) = prems_of st
krauss@23074
   190
krauss@34232
   191
    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
krauss@23074
   192
krauss@34232
   193
    val measure_funs = (* 1: generate measures *)
krauss@34232
   194
      MeasureFunctions.get_measure_functions ctxt domT
wenzelm@23633
   195
krauss@34232
   196
    val table = (* 2: create table *)
krauss@34232
   197
      Par_List.map (fn t => Par_List.map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
krauss@34232
   198
  in
krauss@34232
   199
    case search_table table of
krauss@34232
   200
      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
krauss@34232
   201
    | SOME order =>
krauss@34232
   202
      let
krauss@34232
   203
        val clean_table = map (fn x => map (nth x) order) table
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@33099
   228
  #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
bulwahn@21131
   229
wenzelm@30493
   230
end;