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