src/HOL/Tools/function_package/lexicographic_order.ML

definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
do not depend on "termination" setup.

(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
    ID:          $Id$
    Author:      Lukas Bulwahn, TU Muenchen

Method for termination proofs with lexicographic orderings.
*)

signature LEXICOGRAPHIC_ORDER =
sig
  val lexicographic_order : Proof.context -> Method.method

  (* exported for use by size-change termination prototype.
     FIXME: provide a common interface later *)
  val mk_base_funs : typ -> term list
  (* exported for debugging *)
  val setup: theory -> theory
end

structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
struct

(* Theory dependencies *)
val measures = "List.measures"
val wf_measures = thm "wf_measures"
val measures_less = thm "measures_less"
val measures_lesseq = thm "measures_lesseq"
                      
fun del_index (n, []) = []
  | del_index (n, x :: xs) =
    if n>0 then x :: del_index (n - 1, xs) else xs 

fun transpose ([]::_) = []
  | transpose xss = map hd xss :: transpose (map tl xss)

fun mk_sum_case (f1, f2) =
    case (fastype_of f1, fastype_of f2) of
      (Type("fun", [A, B]), Type("fun", [C, D])) =>
      if (B = D) then
        Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
      else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
    | _ => raise TERM ("mk_sum_case", [f1, f2])
                 
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
  | dest_wf t = raise TERM ("dest_wf", [t])
                      
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
         
fun is_Less cell = case cell of (Less _) => true | _ => false  
                                                        
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
                                                            
fun thm_of_cell cell =
    case cell of 
      Less thm => thm
    | LessEq thm => thm
    | False thm => thm
    | None thm => thm
                  
fun mk_base_fun_bodys (t : term) (tt : typ) =
    case tt of
      Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
    | _ => [(t, tt)]
           
fun mk_base_fun_header fulltyp (t, typ) =
    Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
         
fun mk_base_funs (tt: typ) = 
    mk_base_fun_bodys (Bound 0) tt |>
                      map (mk_base_fun_header tt)

fun mk_funorder_funs (tt : typ) (one : bool) : Term.term list =
    case tt of
      Type("+", [ft, st]) => let
                               val ft_funs = mk_funorder_funs ft
                               val st_funs = mk_funorder_funs st 
                             in
                               (if one then 
                                 (product (ft_funs true) (st_funs false)) @ (product (ft_funs false) (st_funs true))
                               else
                                 product (ft_funs false) (st_funs false)) 
                                    |> map mk_sum_case
                             end
    | _ => if one then [Abs ("x", tt, HOLogic.Suc_zero)] else [Abs ("x", tt, HOLogic.zero)]

fun mk_ext_base_funs (tt : typ) =
    case tt of
      Type("+", [ft, st]) =>
      product (mk_ext_base_funs ft) (mk_ext_base_funs st)
              |> map mk_sum_case
    | _ => mk_base_funs tt

fun mk_all_measure_funs (tt : typ) =
    case tt of
      Type("+", _) => (mk_ext_base_funs tt) @ (mk_funorder_funs tt true)
    | _ => mk_base_funs tt
           
fun dest_term (t : term) =
    let
      val (vars, prop) = (FundefLib.dest_all_all t)
      val prems = Logic.strip_imp_prems prop
      val (tuple, rel) = Logic.strip_imp_concl prop
                         |> HOLogic.dest_Trueprop 
                         |> HOLogic.dest_mem
      val (lhs, rhs) = HOLogic.dest_prod tuple
    in
      (vars, prems, lhs, rhs, rel)
    end
    
fun mk_goal (vars, prems, lhs, rhs) rel =
    let 
      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
    in  
      Logic.list_implies (prems, concl) |>
                         fold_rev FundefLib.mk_forall vars
    end
    
fun prove (thy: theory) (t: term) =
    cterm_of thy t |> Goal.init 
    |> SINGLE (CLASIMPSET auto_tac) |> the
    
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
    let 
      val goals = mk_goal (vars, prems, lhs, rhs) 
      val less_thm = goals "Orderings.less" |> prove thy
    in
      if Thm.no_prems less_thm then
        Less (Goal.finish less_thm)
      else
        let
          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
        in
          if Thm.no_prems lesseq_thm then
            LessEq (Goal.finish lesseq_thm)
          else 
            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
            else None lesseq_thm
        end
    end
    
fun mk_row (thy: theory) measure_funs (t : term) =
    let
      val (vars, prems, lhs, rhs, _) = dest_term t
      val lhs_list = map (fn x => x $ lhs) measure_funs
      val rhs_list = map (fn x => x $ rhs) measure_funs
    in
      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
    end
    
fun pr_cell cell = case cell of Less _ => " <  " 
                              | LessEq _ => " <= " 
                              | None _ => " N  "
                              | False _ => " F  "

fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))

fun check_col ls = (forall (fn c => is_Less c orelse is_LessEq c) ls) andalso not (forall (fn c => is_LessEq c) ls)

fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col)

fun transform_order col order = map (fn x => if x>=col then x+1 else x) order
      
(* simple depth-first search algorithm for the table *)
fun search_table table =
    case table of
      [] => SOME []
    | _ =>
      let
        val col = find_index (check_col) (transpose table)
      in case col of
           ~1 => NONE 
         | _ =>
           let
             val order_opt = (table, col) |-> transform_table |> search_table
           in case order_opt of
                NONE => NONE
              | SOME order =>SOME (col::(transform_order col order))
           end
      end

(* find all positions of elements in a list *) 
fun find_index_list pred =
  let fun find _ [] = []
        | find n (x :: xs) = if pred x then n::(find (n + 1) xs) else find (n + 1) xs;
  in find 0 end;

(* simple breadth-first search algorithm for the table *) 
fun bfs_search_table nodes =
    case nodes of
      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)" 
    | (node::rnodes) => let
	val (order, table) = node
      in
        case table of
          [] => SOME (foldr (fn (c, order) => c::transform_order c order) [] (rev order))
        | _ => let
	    val cols = find_index_list (check_col) (transpose table)
          in
            case cols of
	      [] => NONE
            | _ => let 
              val newtables = map (transform_table table) cols 
              val neworders = map (fn c => c::order) cols
              val newnodes = neworders ~~ newtables
            in
              bfs_search_table (rnodes @ newnodes)
            end 
          end
      end

fun nsearch_table table = bfs_search_table [([], table)] 	       

fun prove_row row (st : thm) =
    case row of
      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
    | cell::tail =>
      case cell of
        Less less_thm =>
        let
          val next_thm = st |> SINGLE (rtac measures_less 1) |> the
        in
          implies_elim next_thm less_thm
        end
      | LessEq lesseq_thm =>
        let
          val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
        in
          implies_elim next_thm lesseq_thm 
          |> prove_row tail
        end
      | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
             
fun pr_unprovable_subgoals table =
    filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
    
fun pr_goal thy t i = 
    let
      val (_, prems, lhs, rhs, _) = dest_term t 
      val prterm = string_of_cterm o (cterm_of thy)
    in
      (* also show prems? *)
        i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
    end
    
fun pr_fun thy t i =
    (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
                                             
(* fun pr_err: prints the table if tactic failed *)
fun pr_err table thy tl measure_funs =  
    let 
      val gc = map (fn i => chr (i + 96)) (1 upto (length table))
      val mc = 1 upto (length measure_funs)
      val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
                 (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
      val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
      val mstr = ("Measures:"::(map2 (pr_fun thy) measure_funs mc))   
      val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
    in
      tstr @ gstr @ mstr @ ustr
    end
      
(* the main function: create table, search table, create relation,
   and prove the subgoals *)  
fun lexicographic_order_tac ctxt (st: thm) = 
    let
      val thy = theory_of_thm st
      val premlist = prems_of st
    in
      case premlist of 
            [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
          | (wfR::tl) => let
    val trueprop $ (wf $ rel) = wfR
    val crel = cterm_of thy rel
    val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
    val measure_funs = mk_all_measure_funs domT
    val _ = writeln "Creating table"
    val table = map (mk_row thy measure_funs) tl
    val _ = writeln "Searching for lexicographic order"
    (* val _ = pr_table table *)
    val possible_order = search_table table
      in
    case possible_order of 
        NONE => error (cat_lines ("Could not find lexicographic termination order:"::(pr_err table thy tl measure_funs)))
      | SOME order  => let
      val clean_table = map (fn x => map (nth x) order) table
      val funs = map (nth measure_funs) order
      val list = HOLogic.mk_list (domT --> HOLogic.natT) funs
      val relterm = Const(measures, (fastype_of list) --> (fastype_of rel)) $ list
      val crelterm = cterm_of thy relterm
      val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
      val _ = writeln "Proving subgoals"
        in
      st |> cterm_instantiate [(crel, crelterm)]
        |> SINGLE (rtac wf_measures 1) |> the
        |> fold prove_row clean_table
        |> Seq.single
                    end
            end
    end

(* FIXME goal addressing ?? *)
val lexicographic_order = Method.SIMPLE_METHOD o (fn ctxt => FundefCommon.apply_termination_rule ctxt 1 
                                                              THEN lexicographic_order_tac ctxt)

val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]

end