src/HOL/Tools/function_package/lexicographic_order.ML
author krauss
Fri, 30 Nov 2007 16:23:52 +0100
changeset 25509 e537c91b043d
parent 24977 9f98751c9628
child 25538 58e8ba3b792b
permissions -rw-r--r--
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
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
25509
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    22
(** User-declared size functions **)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    23
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    24
structure SizeFunsData = GenericDataFun
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    25
(
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    26
  type T = term NetRules.T;
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    27
  val empty = NetRules.init (op aconv) I
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    28
  val copy = I
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    29
  val extend = I
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    30
  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    31
);
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    32
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    33
fun add_sfun f ctxt = 
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    34
  SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    35
val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f))))
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    36
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    37
fun get_sfuns T thy =
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    38
    map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    39
                                                                (domain_type (fastype_of f), T)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    40
                                                                Vartab.empty) 
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    41
                                                f)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    42
                   handle Type.TYPE_MATCH => NONE)
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    43
               (NetRules.rules (SizeFunsData.get (Context.Theory thy)))
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
    44
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    45
(** General stuff **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    46
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    47
fun mk_measures domT mfuns =
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    48
    let 
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    49
        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    50
        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    51
        fun mk_ms [] = Const (@{const_name "{}"}, relT)
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    52
          | mk_ms (f::fs) = 
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    53
            Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    54
    in
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    55
        mk_ms mfuns
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    56
    end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    57
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    58
fun del_index n [] = []
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    59
  | del_index n (x :: xs) =
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    60
    if n > 0 then x :: del_index (n - 1) xs else xs
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    61
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    62
fun transpose ([]::_) = []
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    63
  | transpose xss = map hd xss :: transpose (map tl xss)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    64
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    65
(** Matrix cell datatype **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    66
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
    67
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
    68
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    69
fun is_Less (Less _) = true
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    70
  | is_Less _ = false
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    71
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    72
fun is_LessEq (LessEq _) = true
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    73
  | is_LessEq _ = false
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    74
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    75
fun thm_of_cell (Less thm) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    76
  | thm_of_cell (LessEq (thm, _)) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    77
  | thm_of_cell (False thm) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    78
  | thm_of_cell (None (thm, _)) = thm
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    79
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    80
fun pr_cell (Less _ ) = " < "
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    81
  | pr_cell (LessEq _) = " <="
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    82
  | pr_cell (None _) = " ? "
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
    83
  | pr_cell (False _) = " F "
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    84
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    85
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    86
(** Generating Measure Functions **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    87
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    88
fun mk_comp g f =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    89
    let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
    90
      val fT = fastype_of f
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    91
      val gT as (Type ("fun", [xT, _])) = fastype_of g
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    92
      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
    93
    in
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    94
      Envir.beta_norm (comp $ f $ g)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    95
    end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    96
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    97
fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    98
      map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
    99
    @ 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
   100
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   101
  | mk_base_funs thy T = (* default: size function, if available *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   102
    if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
25509
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
   103
    then (HOLogic.size_const T) :: get_sfuns T thy
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
   104
    else get_sfuns T thy
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   105
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   106
fun mk_sum_case f1 f2 =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   107
    let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   108
      val Type ("fun", [fT, Q]) = fastype_of f1
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   109
      val Type ("fun", [sT, _]) = fastype_of f2
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   110
    in
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   111
      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
   112
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   113
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   114
fun constant_0 T = Abs ("x", T, HOLogic.zero)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   115
fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   116
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   117
fun mk_funorder_funs (Type ("+", [fT, sT])) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   118
      map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   119
    @ 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
   120
  | mk_funorder_funs T = [ constant_1 T ]
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   121
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   122
fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   123
    product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   124
       |> map (uncurry mk_sum_case)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   125
  | mk_ext_base_funs thy T = mk_base_funs thy T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   126
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   127
fun mk_all_measure_funs thy (T as Type ("+", _)) =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   128
    mk_ext_base_funs thy T @ mk_funorder_funs T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   129
  | mk_all_measure_funs thy T = mk_base_funs thy T
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   130
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   131
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   132
(** Proof attempts to build the matrix **)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   133
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   134
fun dest_term (t : term) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   135
    let
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   136
      val (vars, prop) = FundefLib.dest_all_all t
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   137
      val prems = Logic.strip_imp_prems prop
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   138
      val (lhs, rhs) = Logic.strip_imp_concl prop
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   139
                         |> HOLogic.dest_Trueprop
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   140
                         |> HOLogic.dest_mem |> fst
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   141
                         |> HOLogic.dest_prod
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   142
    in
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   143
      (vars, prems, lhs, rhs)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   144
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   145
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   146
fun mk_goal (vars, prems, lhs, rhs) rel =
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   147
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   148
      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
   149
    in
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   150
      Logic.list_implies (prems, concl)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   151
        |> fold_rev FundefLib.mk_forall vars
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   152
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   153
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   154
fun prove thy solve_tac t =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   155
    cterm_of thy t |> Goal.init
23055
34158639dc12 Method "lexicographic_order" now takes the same arguments as "auto"
krauss
parents: 22997
diff changeset
   156
    |> SINGLE solve_tac |> the
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   157
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   158
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
   159
    let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   160
      val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23633
diff changeset
   161
      val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   162
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   163
      if Thm.no_prems less_thm then
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   164
        Less (Goal.finish less_thm)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   165
      else
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   166
        let
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23633
diff changeset
   167
          val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   168
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   169
          if Thm.no_prems lesseq_thm then
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   170
            LessEq (Goal.finish lesseq_thm, less_thm)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   171
          else
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   172
            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   173
            else None (lesseq_thm, less_thm)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   174
        end
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   175
    end
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   176
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   177
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   178
(** Search algorithms **)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   179
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   180
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
   181
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   182
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
   183
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   184
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
   185
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   186
(* simple depth-first search algorithm for the table *)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   187
fun search_table table =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   188
    case table of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   189
      [] => SOME []
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   190
    | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   191
      let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   192
        val col = find_index (check_col) (transpose table)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   193
      in case col of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   194
           ~1 => NONE
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   195
         | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   196
           let
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   197
             val order_opt = (table, col) |-> transform_table |> search_table
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   198
           in case order_opt of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   199
                NONE => NONE
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   200
              | SOME order =>SOME (col :: transform_order col order)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   201
           end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   202
      end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   203
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   204
(* find all positions of elements in a list *)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   205
fun find_index_list P =
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   206
    let fun find _ [] = []
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   207
          | 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
   208
    in find 0 end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   209
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   210
(* simple breadth-first search algorithm for the table *)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   211
fun bfs_search_table nodes =
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   212
    case nodes of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   213
      [] => 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
   214
    | (node::rnodes) => let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   215
        val (order, table) = node
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   216
      in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   217
        case table of
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   218
          [] => SOME (foldr (fn (c, order) => c :: transform_order c order) [] (rev order))
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   219
        | _ => let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   220
            val cols = find_index_list (check_col) (transpose table)
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   221
          in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   222
            case cols of
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   223
              [] => NONE
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   224
            | _ => let
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   225
              val newtables = map (transform_table table) cols
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   226
              val neworders = map (fn c => c :: order) cols
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   227
              val newnodes = neworders ~~ newtables
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   228
            in
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   229
              bfs_search_table (rnodes @ newnodes)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   230
            end
22309
87ec1ca65312 improved lexicographic order termination tactic
bulwahn
parents: 22258
diff changeset
   231
          end
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   232
      end
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   233
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   234
fun nsearch_table table = bfs_search_table [([], table)]
22258
0967b03844b5 changes in lexicographic_order termination tactic
bulwahn
parents: 21817
diff changeset
   235
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   236
(** Proof Reconstruction **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   237
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   238
(* prove row :: cell list -> tactic *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   239
fun prove_row (Less less_thm :: _) =
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
   240
    (rtac @{thm "mlex_less"} 1)
24977
9f98751c9628 replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents: 24961
diff changeset
   241
    THEN PRIMITIVE (Thm.elim_implies less_thm)
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   242
  | prove_row (LessEq (lesseq_thm, _) :: tail) =
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
   243
    (rtac @{thm "mlex_leq"} 1)
24977
9f98751c9628 replaced (flip Thm.implies_elim) by Thm.elim_implies;
wenzelm
parents: 24961
diff changeset
   244
    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   245
    THEN prove_row tail
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   246
  | prove_row _ = sys_error "lexicographic_order"
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   247
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   248
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   249
(** Error reporting **)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   250
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   251
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
   252
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   253
fun pr_goals ctxt st =
24961
5298ee9c3fe5 moved ProofContext.pp to Syntax.pp;
wenzelm
parents: 24920
diff changeset
   254
    Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   255
     |> Pretty.chunks
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   256
     |> Pretty.string_of
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   257
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   258
fun row_index i = chr (i + 97)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   259
fun col_index j = string_of_int (j + 1)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   260
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   261
fun pr_unprovable_cell _ ((i,j), Less _) = ""
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   262
  | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   263
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   264
  | pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   265
      "(" ^ 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
   266
      ^ "\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
   267
  | pr_unprovable_cell ctxt ((i,j), False st) =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   268
      "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   269
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   270
fun pr_unprovable_subgoals ctxt table =
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   271
    table
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   272
     |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   273
     |> flat
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   274
     |> map (pr_unprovable_cell ctxt)
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   275
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   276
fun no_order_msg ctxt table tl measure_funs =
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   277
    let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24576
diff changeset
   278
      val prterm = Syntax.string_of_term ctxt
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   279
      fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   280
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   281
      fun pr_goal t i =
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   282
          let
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   283
            val (_, _, lhs, rhs) = dest_term t
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   284
          in (* also show prems? *)
23128
8e0abe0fa80f clarified error message
krauss
parents: 23074
diff changeset
   285
               i ^ ") " ^ prterm rhs ^ " ~> " ^ prterm lhs
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   286
          end
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   287
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   288
      val gc = map (fn i => chr (i + 96)) (1 upto length table)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   289
      val mc = 1 upto length measure_funs
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   290
      val tstr = "Result matrix:" ::  "   " ^ concat (map (enclose " " " " o string_of_int) mc)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   291
                 :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   292
      val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   293
      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
   294
      val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   295
    in
23437
4a44fcc9dba9 tuned error msg
krauss
parents: 23128
diff changeset
   296
      cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   297
    end
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   298
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   299
(** The Main Function **)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   300
fun lexicographic_order_tac ctxt solve_tac (st: thm) =
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   301
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   302
      val thy = theory_of_thm st
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   303
      val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   304
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   305
      val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   306
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   307
      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
   308
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   309
      (* 2: create table *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   310
      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
   311
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   312
      val order = the (search_table table) (* 3: search table *)
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   313
          handle Option => error (no_order_msg ctxt table tl measure_funs)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   314
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   315
      val clean_table = map (fn x => map (nth x) order) table
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   316
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   317
      val relation = mk_measures domT (map (nth measure_funs) order)
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24576
diff changeset
   318
      val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   319
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   320
    in (* 4: proof reconstruction *)
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   321
      st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
24576
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
   322
              THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
32ddd902b0ad lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
krauss
parents: 23881
diff changeset
   323
              THEN (rtac @{thm "wf_empty"} 1)
23074
a53cb8ddb052 some optimizations, cleanup
krauss
parents: 23056
diff changeset
   324
              THEN EVERY (map prove_row clean_table))
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   325
    end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   326
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   327
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
   328
                                                         THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt)))
21201
803bc7672d17 method exported
krauss
parents: 21131
diff changeset
   329
23633
f25b1566f7b5 pr_goals: adapted Display.pretty_goals_aux;
wenzelm
parents: 23437
diff changeset
   330
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
   331
                                 "termination prover for lexicographic orderings")]
25509
e537c91b043d new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
krauss
parents: 24977
diff changeset
   332
    #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   333
21590
ef7278f553eb tuned spaces/comments;
wenzelm
parents: 21510
diff changeset
   334
end