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