src/HOL/Tools/function_package/lexicographic_order.ML
author wenzelm
Sat, 07 Jul 2007 18:39:12 +0200
changeset 23633 f25b1566f7b5
parent 23437 4a44fcc9dba9
child 23881 851c74f1bb69
permissions -rw-r--r--
pr_goals: adapted Display.pretty_goals_aux; pr_goals/prterm: proper context; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     1
(*  Title:       HOL/Tools/function_package/lexicographic_order.ML
21201
803bc7672d17 method exported
krauss
parents: 21131
diff changeset
     2
    ID:          $Id$
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     3
    Author:      Lukas Bulwahn, TU Muenchen
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     4
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     5
Method for termination proofs with lexicographic orderings.
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     6
*)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     7
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     8
signature LEXICOGRAPHIC_ORDER =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
     9
sig
23056
448827ccd9e9 fixed signature
krauss
parents: 23055
diff changeset
    10
  val lexicographic_order : thm list -> Proof.context -> Method.method
21510
7e72185e4b24 exported mk_base_funs for use by size-change tools
krauss
parents: 21319
diff changeset
    11
7e72185e4b24 exported mk_base_funs for use by size-change tools
krauss
parents: 21319
diff changeset
    12
  (* exported for use by size-change termination prototype.
7e72185e4b24 exported mk_base_funs for use by size-change tools
krauss
parents: 21319
diff changeset
    13
     FIXME: provide a common interface later *)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    14
  val mk_base_funs : theory -> typ -> term list
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
    15
  (* exported for debugging *)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    16
  val setup: theory -> theory
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    17
end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    18
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    19
structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    20
struct
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    21
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    22
(** General stuff **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    23
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    24
fun mk_measures domT mfuns =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    25
    let val list = HOLogic.mk_list (domT --> HOLogic.natT) mfuns
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    26
    in
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    27
      Const (@{const_name "List.measures"}, fastype_of list --> (HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))) $ list
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    28
    end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    29
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    30
fun del_index n [] = []
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    31
  | del_index n (x :: xs) =
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    32
    if n > 0 then x :: del_index (n - 1) xs else xs
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    33
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    34
fun transpose ([]::_) = []
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    35
  | transpose xss = map hd xss :: transpose (map tl xss)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    36
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    37
(** Matrix cell datatype **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    38
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    39
datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    40
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    41
fun is_Less (Less _) = true
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    42
  | is_Less _ = false
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    43
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    44
fun is_LessEq (LessEq _) = true
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    45
  | is_LessEq _ = false
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    46
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    47
fun thm_of_cell (Less thm) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    48
  | thm_of_cell (LessEq (thm, _)) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    49
  | thm_of_cell (False thm) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    50
  | thm_of_cell (None (thm, _)) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    51
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    52
fun pr_cell (Less _ ) = " < "
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    53
  | pr_cell (LessEq _) = " <="
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    54
  | pr_cell (None _) = " ? "
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    55
  | pr_cell (False _) = " F "
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    56
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    57
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    58
(** Generating Measure Functions **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    59
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    60
fun mk_comp g f =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    61
    let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    62
      val fT = fastype_of f
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    63
      val gT as (Type ("fun", [xT, _])) = fastype_of g
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    64
      val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0))))
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    65
    in
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    66
      Envir.beta_norm (comp $ f $ g)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    67
    end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    68
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    69
fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    70
      map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    71
    @ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT)
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
    72
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    73
  | mk_base_funs thy T = (* default: size function, if available *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    74
    if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    75
    then [HOLogic.size_const T]
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    76
    else []
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    77
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    78
fun mk_sum_case f1 f2 =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    79
    let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    80
      val Type ("fun", [fT, Q]) = fastype_of f1
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    81
      val Type ("fun", [sT, _]) = fastype_of f2
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    82
    in
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    83
      Const (@{const_name "Sum_Type.sum_case"}, (fT --> Q) --> (sT --> Q) --> Type("+", [fT, sT]) --> Q) $ f1 $ f2
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    84
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    85
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    86
fun constant_0 T = Abs ("x", T, HOLogic.zero)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    87
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
    88
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    89
fun mk_funorder_funs (Type ("+", [fT, sT])) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    90
      map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    91
    @ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    92
  | mk_funorder_funs T = [ constant_1 T ]
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
    93
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    94
fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    95
    product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    96
       |> map (uncurry mk_sum_case)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    97
  | mk_ext_base_funs thy T = mk_base_funs thy T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    98
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    99
fun mk_all_measure_funs thy (T as Type ("+", _)) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   100
    mk_ext_base_funs thy T @ mk_funorder_funs T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   101
  | mk_all_measure_funs thy T = mk_base_funs thy T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   102
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   103
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   104
(** Proof attempts to build the matrix **)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   105
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   106
fun dest_term (t : term) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   107
    let
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   108
      val (vars, prop) = FundefLib.dest_all_all t
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   109
      val prems = Logic.strip_imp_prems prop
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   110
      val (lhs, rhs) = Logic.strip_imp_concl prop
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   111
                         |> HOLogic.dest_Trueprop
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   112
                         |> HOLogic.dest_mem |> fst
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   113
                         |> HOLogic.dest_prod
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   114
    in
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   115
      (vars, prems, lhs, rhs)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   116
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   117
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   118
fun mk_goal (vars, prems, lhs, rhs) rel =
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   119
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   120
      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   121
    in
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   122
      Logic.list_implies (prems, concl)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   123
        |> fold_rev FundefLib.mk_forall vars
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   124
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   125
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   126
fun prove thy solve_tac t =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   127
    cterm_of thy t |> Goal.init
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   128
    |> SINGLE solve_tac |> the
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   129
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   130
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   131
    let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   132
      val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   133
      val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   134
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   135
      if Thm.no_prems less_thm then
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   136
        Less (Goal.finish less_thm)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   137
      else
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   138
        let
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   139
          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   140
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   141
          if Thm.no_prems lesseq_thm then
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   142
            LessEq (Goal.finish lesseq_thm, less_thm)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   143
          else
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   144
            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   145
            else None (lesseq_thm, less_thm)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   146
        end
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   147
    end
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   148
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   149
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   150
(** Search algorithms **)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   151
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   152
fun check_col ls = forall (fn c => is_Less c orelse is_LessEq c) ls andalso not (forall (is_LessEq) ls)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   153
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   154
fun transform_table table col = table |> filter_out (fn x => is_Less (nth x col)) |> map (del_index col)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   155
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   156
fun transform_order col order = map (fn x => if x >= col then x + 1 else x) order
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   157
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   158
(* simple depth-first search algorithm for the table *)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   159
fun search_table table =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   160
    case table of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   161
      [] => SOME []
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   162
    | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   163
      let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   164
        val col = find_index (check_col) (transpose table)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   165
      in case col of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   166
           ~1 => NONE
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   167
         | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   168
           let
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   169
             val order_opt = (table, col) |-> transform_table |> search_table
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   170
           in case order_opt of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   171
                NONE => NONE
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   172
              | SOME order =>SOME (col :: transform_order col order)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   173
           end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   174
      end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   175
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   176
(* find all positions of elements in a list *)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   177
fun find_index_list P =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   178
    let fun find _ [] = []
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   179
          | find n (x :: xs) = if P x then n :: find (n + 1) xs else find (n + 1) xs
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   180
    in find 0 end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   181
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   182
(* simple breadth-first search algorithm for the table *)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   183
fun bfs_search_table nodes =
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   184
    case nodes of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   185
      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun search_table (breadth search finished)"
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   186
    | (node::rnodes) => let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   187
        val (order, table) = node
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   188
      in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   189
        case table of
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   190
          [] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order))
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   191
        | _ => let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   192
            val cols = find_index_list (check_col) (transpose table)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   193
          in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   194
            case cols of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   195
              [] => NONE
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   196
            | _ => let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   197
              val newtables = map (transform_table table) cols
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   198
              val neworders = map (fn c => c :: order) cols
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   199
              val newnodes = neworders ~~ newtables
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   200
            in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   201
              bfs_search_table (rnodes @ newnodes)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   202
            end
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   203
          end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   204
      end
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   205
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   206
fun nsearch_table table = bfs_search_table [([], table)]
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   207
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   208
(** Proof Reconstruction **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   209
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   210
(* prove row :: cell list -> tactic *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   211
fun prove_row (Less less_thm :: _) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   212
    (rtac @{thm "measures_less"} 1)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   213
    THEN PRIMITIVE (flip implies_elim less_thm)
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   214
  | prove_row (LessEq (lesseq_thm, _) :: tail) =
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   215
    (rtac @{thm "measures_lesseq"} 1)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   216
    THEN PRIMITIVE (flip implies_elim lesseq_thm)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   217
    THEN prove_row tail
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   218
  | prove_row _ = sys_error "lexicographic_order"
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   219
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   220
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   221
(** Error reporting **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   222
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   223
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   224
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   225
fun pr_goals ctxt st =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   226
    Display.pretty_goals_aux (ProofContext.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   227
     |> Pretty.chunks
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   228
     |> Pretty.string_of
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   229
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   230
fun row_index i = chr (i + 97)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   231
fun col_index j = string_of_int (j + 1)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   232
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   233
fun pr_unprovable_cell _ ((i,j), Less _) = ""
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   234
  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   235
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   236
  | pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   237
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   238
      ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   239
  | pr_unprovable_cell ctxt ((i,j), False st) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   240
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   241
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   242
fun pr_unprovable_subgoals ctxt table =
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   243
    table
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   244
     |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   245
     |> flat
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   246
     |> map (pr_unprovable_cell ctxt)
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   247
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   248
fun no_order_msg ctxt table tl measure_funs =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   249
    let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   250
      val prterm = ProofContext.string_of_term ctxt
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   251
      fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   252
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   253
      fun pr_goal t i =
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   254
          let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   255
            val (_, _, lhs, rhs) = dest_term t
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   256
          in (* also show prems? *)
23128
8e0abe0fa80f clarified error message
krauss
parents: 23074
diff changeset
   257
               i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   258
          end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   259
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   260
      val gc = map (fn i => chr (i + 96)) (1 upto length table)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   261
      val mc = 1 upto length measure_funs
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   262
      val tstr = "Result matrix:" ::  "   " ^ concat (map (enclose " " " " o string_of_int) mc)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   263
                 :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   264
      val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   265
      val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   266
      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   267
    in
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   268
      cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   269
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   270
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   271
(** The Main Function **)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   272
fun lexicographic_order_tac ctxt solve_tac (st: thm) =
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   273
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   274
      val thy = theory_of_thm st
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   275
      val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   276
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   277
      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   278
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   279
      val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   280
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   281
      (* 2: create table *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   282
      val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   283
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   284
      val order = the (search_table table) (* 3: search table *)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   285
          handle Option => error (no_order_msg ctxt table tl measure_funs)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   286
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   287
      val clean_table = map (fn x => map (nth x) order) table
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   288
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   289
      val relation = mk_measures domT (map (nth measure_funs) order)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   290
      val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation))
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   291
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   292
    in (* 4: proof reconstruction *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   293
      st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   294
              THEN rtac @{thm "wf_measures"} 1
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   295
              THEN EVERY (map prove_row clean_table))
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   296
    end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   297
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   298
fun lexicographic_order thms ctxt = Method.SIMPLE_METHOD (FundefCommon.apply_termination_rule ctxt 1
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   299
                                                         THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
21201
803bc7672d17 method exported
krauss
parents: 21131
diff changeset
   300
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   301
val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   302
                                 "termination prover for lexicographic orderings")]
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   303
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 21510
diff changeset
   304
end