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