src/HOL/Tools/function_package/lexicographic_order.ML
author krauss
Fri, 24 Nov 2006 13:39:22 +0100
changeset 21510 7e72185e4b24
parent 21319 cf814e36f788
child 21590 ef7278f553eb
permissions -rw-r--r--
exported mk_base_funs for use by size-change tools
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
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21237
diff changeset
    10
  val lexicographic_order : 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 *)
7e72185e4b24 exported mk_base_funs for use by size-change tools
krauss
parents: 21319
diff changeset
    14
  val mk_base_funs : typ -> term list
7e72185e4b24 exported mk_base_funs for use by size-change tools
krauss
parents: 21319
diff changeset
    15
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
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    22
(* Theory dependencies *)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    23
val measures = "List.measures"
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    24
val wf_measures = thm "wf_measures"
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    25
val measures_less = thm "measures_less"
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    26
val measures_lesseq = thm "measures_lesseq"
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    27
                      
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    28
fun del_index (n, []) = []
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    29
  | del_index (n, x :: xs) =
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    30
    if n>0 then x :: del_index (n - 1, xs) else xs 
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    31
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    32
fun transpose ([]::_) = []
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    33
  | transpose xss = map hd xss :: transpose (map tl xss)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    34
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    35
fun mk_sum_case (f1, f2) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    36
    case (fastype_of f1, fastype_of f2) of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    37
      (Type("fun", [A, B]), Type("fun", [C, D])) =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    38
      if (B = D) then
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    39
        Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    40
      else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    41
    | _ => raise TERM ("mk_sum_case", [f1, f2])
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    42
                 
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    43
fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    44
  | dest_wf t = raise TERM ("dest_wf", [t])
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    45
                      
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    46
datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    47
         
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    48
fun is_Less cell = case cell of (Less _) => true | _ => false  
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    49
                                                        
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    50
fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    51
                                                            
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    52
fun thm_of_cell cell =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    53
    case cell of 
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    54
      Less thm => thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    55
    | LessEq thm => thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    56
    | False thm => thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    57
    | None thm => thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    58
                  
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    59
fun mk_base_fun_bodys (t : term) (tt : typ) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    60
    case tt of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    61
      Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    62
    | _ => [(t, tt)]
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    63
           
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    64
fun mk_base_fun_header fulltyp (t, typ) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    65
    if typ = HOLogic.natT then
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    66
      Abs ("x", fulltyp, t)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    67
    else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    68
         
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    69
fun mk_base_funs (tt: typ) = 
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    70
    mk_base_fun_bodys (Bound 0) tt |>
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    71
                      map (mk_base_fun_header tt)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    72
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    73
fun mk_ext_base_funs (tt : typ) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    74
    case tt of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    75
      Type("+", [ft, st]) =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    76
      product (mk_ext_base_funs ft) (mk_ext_base_funs st)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    77
              |> map mk_sum_case
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    78
    | _ => mk_base_funs tt
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    79
           
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    80
fun dest_term (t : term) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    81
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    82
      val (vars, prop) = (FundefLib.dest_all_all t)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    83
      val prems = Logic.strip_imp_prems prop
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    84
      val (tuple, rel) = Logic.strip_imp_concl prop
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    85
                         |> HOLogic.dest_Trueprop 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    86
                         |> HOLogic.dest_mem
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    87
      val (lhs, rhs) = HOLogic.dest_prod tuple
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    88
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    89
      (vars, prems, lhs, rhs, rel)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    90
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    91
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    92
fun mk_goal (vars, prems, lhs, rhs) rel =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    93
    let 
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    94
      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    95
    in  
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    96
      Logic.list_implies (prems, concl) |>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    97
                         fold_rev FundefLib.mk_forall vars
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
    98
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
    99
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   100
fun prove (thy: theory) (t: term) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   101
    cterm_of thy t |> Goal.init 
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   102
    |> SINGLE (CLASIMPSET auto_tac) |> the
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   103
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   104
fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   105
    let 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   106
      val goals = mk_goal (vars, prems, lhs, rhs) 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   107
      val less_thm = goals "Orderings.less" |> prove thy
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   108
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   109
      if Thm.no_prems less_thm then
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   110
        Less (Goal.finish less_thm)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   111
      else
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   112
        let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   113
          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   114
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   115
          if Thm.no_prems lesseq_thm then
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   116
            LessEq (Goal.finish lesseq_thm)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   117
          else 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   118
            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   119
            else None lesseq_thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   120
        end
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   121
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   122
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   123
fun mk_row (thy: theory) base_funs (t : term) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   124
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   125
      val (vars, prems, lhs, rhs, _) = dest_term t
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   126
      val lhs_list = map (fn x => x $ lhs) base_funs
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   127
      val rhs_list = map (fn x => x $ rhs) base_funs
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   128
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   129
      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   130
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   131
      
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   132
(* simple depth-first search algorithm for the table *)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   133
fun search_table table =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   134
    case table of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   135
      [] => SOME []
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   136
    | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   137
      let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   138
        val check_col = forall (fn c => is_Less c orelse is_LessEq c)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   139
        val col = find_index (check_col) (transpose table)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   140
      in case col of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   141
           ~1 => NONE 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   142
         | _ =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   143
           let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   144
             val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   145
             val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   146
           in case order_opt of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   147
                NONE => NONE
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   148
              | SOME order =>SOME (col::(transform_order col order))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   149
           end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   150
      end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   151
      
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   152
fun prove_row row (st : thm) =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   153
    case row of
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   154
      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   155
    | cell::tail =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   156
      case cell of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   157
        Less less_thm =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   158
        let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   159
          val next_thm = st |> SINGLE (rtac measures_less 1) |> the
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   160
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   161
          implies_elim next_thm less_thm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   162
        end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   163
      | LessEq lesseq_thm =>
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   164
        let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   165
          val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   166
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   167
          implies_elim next_thm lesseq_thm 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   168
          |> prove_row tail
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   169
        end
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   170
      | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   171
             
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   172
fun pr_unprovable_subgoals table =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   173
    filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   174
    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   175
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   176
fun pr_goal thy t i = 
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   177
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   178
      val (_, prems, lhs, rhs, _) = dest_term t 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   179
      val prterm = string_of_cterm o (cterm_of thy)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   180
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   181
      (* also show prems? *)
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   182
        i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   183
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   184
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   185
fun pr_fun thy t i =
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   186
    (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   187
    
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   188
fun pr_cell cell = case cell of Less _ => " <  " 
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   189
                              | LessEq _ => " <= " 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   190
                              | None _ => " N  "
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   191
                              | False _ => " F  "
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   192
                                             
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   193
(* fun pr_err: prints the table if tactic failed *)
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   194
fun pr_err table thy tl base_funs =  
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   195
    let 
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   196
      val gc = map (fn i => chr (i + 96)) (1 upto (length table))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   197
      val mc = 1 upto (length base_funs)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   198
      val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   199
                 (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   200
      val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   201
      val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   202
      val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   203
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   204
      tstr @ gstr @ mstr @ ustr
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   205
    end
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   206
      
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   207
(* the main function: create table, search table, create relation,
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   208
   and prove the subgoals *)
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21237
diff changeset
   209
fun lexicographic_order_tac ctxt (st: thm) = 
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   210
    let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   211
      val thy = theory_of_thm st
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21237
diff changeset
   212
      val termination_thm = the (FundefCommon.get_termination_rule ctxt)
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   213
      val next_st = SINGLE (rtac termination_thm 1) st |> the
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   214
      val premlist = prems_of next_st
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   215
    in
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   216
      case premlist of 
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   217
            [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   218
          | (wf::tl) => let
21237
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   219
    val (var, prop) = FundefLib.dest_all wf
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   220
    val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   221
    val crel = cterm_of thy rel
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   222
    val base_funs = mk_ext_base_funs (fastype_of var)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   223
    val _ = writeln "Creating table"
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   224
    val table = map (mk_row thy base_funs) tl
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   225
    val _ = writeln "Searching for lexicographic order"
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   226
    val possible_order = search_table table
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   227
      in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   228
    case possible_order of 
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   229
        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   230
      | SOME order  => let
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   231
      val clean_table = map (fn x => map (nth x) order) table
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   232
      val funs = map (nth base_funs) order
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   233
      val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   234
      val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   235
      val crelterm = cterm_of thy relterm
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   236
      val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   237
      val _ = writeln "Proving subgoals"
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   238
        in
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   239
      next_st |> cterm_instantiate [(crel, crelterm)]
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   240
        |> SINGLE (rtac wf_measures 1) |> the
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   241
        |> fold prove_row clean_table
b803f9870e97 untabified
krauss
parents: 21201
diff changeset
   242
        |> Seq.single
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   243
                    end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   244
            end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   245
    end
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   246
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21237
diff changeset
   247
val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
21201
803bc7672d17 method exported
krauss
parents: 21131
diff changeset
   248
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21237
diff changeset
   249
val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
21131
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   250
a447addc14af added lexicographic_order tactic
bulwahn
parents:
diff changeset
   251
end