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