src/HOL/Tools/Function/lexicographic_order.ML
author wenzelm
Thu Jul 23 16:52:16 2009 +0200 (2009-07-23)
changeset 32145 220c9e439d39
parent 32089 568a23753e3a
child 32149 ef59550a55d3
permissions -rw-r--r--
clarified pretty_goals, pretty_thm_aux: plain context;
explicit pretty_goals_without_context, print_goals_without_context;
tuned;
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
wenzelm@30493
     9
  val lex_order_tac : Proof.context -> tactic -> tactic
wenzelm@30493
    10
  val lexicographic_order_tac : 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
bulwahn@21131
    16
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
bulwahn@21131
    17
struct
bulwahn@21131
    18
krauss@27790
    19
open FundefLib
krauss@27790
    20
krauss@23074
    21
(** General stuff **)
krauss@23074
    22
krauss@23074
    23
fun mk_measures domT mfuns =
krauss@24576
    24
    let 
krauss@24576
    25
        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
krauss@24576
    26
        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
haftmann@30304
    27
        fun mk_ms [] = Const (@{const_name Set.empty}, relT)
krauss@24576
    28
          | mk_ms (f::fs) = 
krauss@26748
    29
            Const (@{const_name "mlex_prod"}, mlexT) $ f $ mk_ms fs
krauss@23074
    30
    in
krauss@24576
    31
        mk_ms mfuns
krauss@23074
    32
    end
krauss@23074
    33
krauss@23074
    34
fun del_index n [] = []
krauss@23074
    35
  | del_index n (x :: xs) =
wenzelm@23633
    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@24576
    43
datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
wenzelm@23633
    44
krauss@23074
    45
fun is_Less (Less _) = true
krauss@23074
    46
  | is_Less _ = false
wenzelm@23633
    47
krauss@23074
    48
fun is_LessEq (LessEq _) = true
krauss@23074
    49
  | is_LessEq _ = false
wenzelm@23633
    50
krauss@23437
    51
fun pr_cell (Less _ ) = " < "
wenzelm@23633
    52
  | pr_cell (LessEq _) = " <="
krauss@23437
    53
  | pr_cell (None _) = " ? "
krauss@23437
    54
  | pr_cell (False _) = " F "
krauss@23074
    55
krauss@23074
    56
krauss@23074
    57
(** Proof attempts to build the matrix **)
wenzelm@23633
    58
bulwahn@21131
    59
fun dest_term (t : term) =
bulwahn@21131
    60
    let
krauss@23074
    61
      val (vars, prop) = FundefLib.dest_all_all t
krauss@26529
    62
      val (prems, concl) = Logic.strip_horn prop
krauss@26529
    63
      val (lhs, rhs) = concl
wenzelm@23633
    64
                         |> HOLogic.dest_Trueprop
krauss@23074
    65
                         |> HOLogic.dest_mem |> fst
wenzelm@23633
    66
                         |> HOLogic.dest_prod
bulwahn@21131
    67
    in
krauss@23074
    68
      (vars, prems, lhs, rhs)
bulwahn@21131
    69
    end
wenzelm@23633
    70
bulwahn@21131
    71
fun mk_goal (vars, prems, lhs, rhs) rel =
wenzelm@23633
    72
    let
krauss@21237
    73
      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
wenzelm@23633
    74
    in
wenzelm@27330
    75
      fold_rev Logic.all vars (Logic.list_implies (prems, concl))
bulwahn@21131
    76
    end
wenzelm@23633
    77
wenzelm@23633
    78
fun prove thy solve_tac t =
wenzelm@23633
    79
    cterm_of thy t |> Goal.init
krauss@23055
    80
    |> SINGLE solve_tac |> the
wenzelm@23633
    81
wenzelm@23633
    82
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
wenzelm@23633
    83
    let
krauss@27790
    84
      val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
bulwahn@21131
    85
    in
krauss@27790
    86
      case try_proof (goals @{const_name HOL.less}) solve_tac of
krauss@27790
    87
        Solved thm => Less thm
krauss@27790
    88
      | Stuck thm => 
krauss@27790
    89
        (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
krauss@27790
    90
           Solved thm2 => LessEq (thm2, thm)
krauss@27790
    91
         | Stuck thm2 => 
krauss@27790
    92
           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
krauss@27790
    93
           else None (thm2, thm)
krauss@27790
    94
         | _ => raise Match) (* FIXME *)
krauss@27790
    95
      | _ => raise Match
bulwahn@21131
    96
    end
krauss@23074
    97
krauss@23074
    98
krauss@23074
    99
(** Search algorithms **)
bulwahn@22309
   100
krauss@23074
   101
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls)
bulwahn@22309
   102
krauss@23074
   103
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
bulwahn@22309
   104
krauss@23074
   105
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
wenzelm@23633
   106
bulwahn@21131
   107
(* simple depth-first search algorithm for the table *)
bulwahn@21131
   108
fun search_table table =
bulwahn@21131
   109
    case table of
krauss@21237
   110
      [] => SOME []
krauss@21237
   111
    | _ =>
krauss@21237
   112
      let
krauss@21237
   113
        val col = find_index (check_col) (transpose table)
krauss@21237
   114
      in case col of
wenzelm@23633
   115
           ~1 => NONE
krauss@21237
   116
         | _ =>
krauss@21237
   117
           let
bulwahn@22309
   118
             val order_opt = (table, col) |-> transform_table |> search_table
krauss@21237
   119
           in case order_opt of
krauss@21237
   120
                NONE => NONE
krauss@23074
   121
              | SOME order =>SOME (col :: transform_order col order)
krauss@21237
   122
           end
krauss@21237
   123
      end
bulwahn@22258
   124
krauss@23074
   125
(** Proof Reconstruction **)
krauss@23074
   126
krauss@23074
   127
(* prove row :: cell list -> tactic *)
krauss@23074
   128
fun prove_row (Less less_thm :: _) =
krauss@24576
   129
    (rtac @{thm "mlex_less"} 1)
wenzelm@24977
   130
    THEN PRIMITIVE (Thm.elim_implies less_thm)
krauss@23437
   131
  | prove_row (LessEq (lesseq_thm, _) :: tail) =
krauss@24576
   132
    (rtac @{thm "mlex_leq"} 1)
wenzelm@24977
   133
    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
krauss@23074
   134
    THEN prove_row tail
krauss@23074
   135
  | prove_row _ = sys_error "lexicographic_order"
krauss@23074
   136
krauss@23074
   137
krauss@23074
   138
(** Error reporting **)
krauss@23074
   139
krauss@23074
   140
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
wenzelm@23633
   141
wenzelm@23633
   142
fun pr_goals ctxt st =
wenzelm@32145
   143
    Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
krauss@23437
   144
     |> Pretty.chunks
krauss@23437
   145
     |> Pretty.string_of
krauss@23437
   146
krauss@23437
   147
fun row_index i = chr (i + 97)
krauss@23437
   148
fun col_index j = string_of_int (j + 1)
krauss@23437
   149
wenzelm@23633
   150
fun pr_unprovable_cell _ ((i,j), Less _) = ""
wenzelm@23633
   151
  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
wenzelm@23633
   152
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
krauss@26875
   153
  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
wenzelm@23633
   154
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
wenzelm@23633
   155
      ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
wenzelm@23633
   156
  | pr_unprovable_cell ctxt ((i,j), False st) =
wenzelm@23633
   157
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
krauss@23437
   158
wenzelm@23633
   159
fun pr_unprovable_subgoals ctxt table =
krauss@23437
   160
    table
krauss@23437
   161
     |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
krauss@23437
   162
     |> flat
wenzelm@23633
   163
     |> map (pr_unprovable_cell ctxt)
krauss@23437
   164
wenzelm@23633
   165
fun no_order_msg ctxt table tl measure_funs =
wenzelm@23633
   166
    let
wenzelm@24920
   167
      val prterm = Syntax.string_of_term ctxt
wenzelm@23633
   168
      fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
krauss@23074
   169
wenzelm@23633
   170
      fun pr_goal t i =
krauss@23074
   171
          let
wenzelm@23633
   172
            val (_, _, lhs, rhs) = dest_term t
krauss@23074
   173
          in (* also show prems? *)
krauss@23128
   174
               i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
krauss@23074
   175
          end
krauss@23074
   176
krauss@23074
   177
      val gc = map (fn i => chr (i + 96)) (1 upto length table)
krauss@23074
   178
      val mc = 1 upto length measure_funs
wenzelm@30715
   179
      val tstr = "Result matrix:" ::  ("   " ^ concat (map (enclose " " " " o string_of_int) mc))
krauss@23074
   180
                 :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
krauss@23437
   181
      val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
krauss@23437
   182
      val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
wenzelm@23633
   183
      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
bulwahn@21131
   184
    in
krauss@23437
   185
      cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
bulwahn@21131
   186
    end
wenzelm@23633
   187
krauss@23074
   188
(** The Main Function **)
wenzelm@30493
   189
wenzelm@30493
   190
fun lex_order_tac ctxt solve_tac (st: thm) =
bulwahn@21131
   191
    let
wenzelm@30493
   192
      val thy = ProofContext.theory_of ctxt
krauss@23074
   193
      val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
krauss@23074
   194
krauss@23074
   195
      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
krauss@23074
   196
krauss@26875
   197
      val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
wenzelm@23633
   198
krauss@23074
   199
      (* 2: create table *)
krauss@23074
   200
      val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
krauss@23074
   201
krauss@23074
   202
      val order = the (search_table table) (* 3: search table *)
wenzelm@23633
   203
          handle Option => error (no_order_msg ctxt table tl measure_funs)
krauss@23074
   204
krauss@21237
   205
      val clean_table = map (fn x => map (nth x) order) table
krauss@23074
   206
krauss@23074
   207
      val relation = mk_measures domT (map (nth measure_funs) order)
wenzelm@24920
   208
      val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
krauss@23074
   209
krauss@23074
   210
    in (* 4: proof reconstruction *)
krauss@23074
   211
      st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
krauss@24576
   212
              THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
krauss@24576
   213
              THEN (rtac @{thm "wf_empty"} 1)
krauss@23074
   214
              THEN EVERY (map prove_row clean_table))
bulwahn@21131
   215
    end
bulwahn@21131
   216
wenzelm@30493
   217
fun lexicographic_order_tac ctxt =
wenzelm@30493
   218
  TRY (FundefCommon.apply_termination_rule ctxt 1)
wenzelm@31902
   219
  THEN lex_order_tac ctxt
wenzelm@31902
   220
    (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
wenzelm@30493
   221
wenzelm@30510
   222
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
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"
wenzelm@30541
   228
  #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
bulwahn@21131
   229
wenzelm@30493
   230
end;
wenzelm@30493
   231