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