src/HOL/Tools/Function/termination.ML
author krauss
Sun, 29 Apr 2012 01:17:25 +0200
changeset 47835 2d48bf79b725
parent 47433 07f4bf913230
child 52723 2ebcc81f599c
permissions -rw-r--r--
dependency graphs: fixed direction of edges
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 30607
diff changeset
     1
(*  Title:       HOL/Tools/Function/termination.ML
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     2
    Author:      Alexander Krauss, TU Muenchen
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     3
41114
f9ae7c2abf7e tuned headers
krauss
parents: 39924
diff changeset
     4
Context data for termination proofs.
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     5
*)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     6
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     7
signature TERMINATION =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     8
sig
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
     9
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    10
  type data
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
    11
  datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    12
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    13
  val mk_sumcases : data -> typ -> term list -> term
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    14
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    15
  val get_num_points : data -> int
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    16
  val get_types      : data -> int -> typ
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    17
  val get_measures   : data -> int -> term list
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    18
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    19
  val get_chain      : data -> term -> term -> thm option option
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    20
  val get_descent    : data -> term -> term -> term -> cell option
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    21
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    22
  val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    23
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    24
  val CALLS : (term list * int -> tactic) -> int -> tactic
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    25
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
    26
  (* Termination tactics *)
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
    27
  type ttac = data -> int -> tactic
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    28
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
    29
  val TERMINATION : Proof.context -> tactic -> ttac -> int -> tactic
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    30
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30304
diff changeset
    31
  val wf_union_tac : Proof.context -> tactic
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
    32
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
    33
  val decompose_tac : ttac
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    34
end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    35
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    36
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    37
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    38
structure Termination : TERMINATION =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    39
struct
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    40
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32683
diff changeset
    41
open Function_Lib
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    42
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35404
diff changeset
    43
val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 31775
diff changeset
    44
structure Term2tab = Table(type key = term * term val ord = term2_ord);
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35404
diff changeset
    45
structure Term3tab =
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35404
diff changeset
    46
  Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord);
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    47
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    48
(** Analyzing binary trees **)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    49
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    50
(* Skeleton of a tree structure *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    51
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    52
datatype skel =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    53
  SLeaf of int (* index *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    54
| SBranch of (skel * skel)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    55
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    56
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    57
(* abstract make and dest functions *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    58
fun mk_tree leaf branch =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    59
  let fun mk (SLeaf i) = leaf i
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    60
        | mk (SBranch (s, t)) = branch (mk s, mk t)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    61
  in mk end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    62
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    63
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    64
fun dest_tree split =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    65
  let fun dest (SLeaf i) x = [(i, x)]
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    66
        | dest (SBranch (s, t)) x =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    67
          let val (l, r) = split x
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    68
          in dest s l @ dest t r end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    69
  in dest end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    70
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    71
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    72
(* concrete versions for sum types *)
32602
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
    73
fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
    74
  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    75
  | is_inj _ = false
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    76
32602
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
    77
fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    78
  | dest_inl _ = NONE
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    79
32602
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
    80
fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    81
  | dest_inr _ = NONE
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    82
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    83
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    84
fun mk_skel ps =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    85
  let
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    86
    fun skel i ps =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    87
      if forall is_inj ps andalso not (null ps)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    88
      then let
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    89
          val (j, s) = skel i (map_filter dest_inl ps)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    90
          val (k, t) = skel j (map_filter dest_inr ps)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    91
        in (k, SBranch (s, t)) end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    92
      else (i + 1, SLeaf i)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    93
  in
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    94
    snd (skel 0 ps)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    95
  end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    96
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    97
(* compute list of types for nodes *)
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37391
diff changeset
    98
fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
    99
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   100
(* find index and raw term *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   101
fun dest_inj (SLeaf i) trm = (i, trm)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   102
  | dest_inj (SBranch (s, t)) trm =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   103
    case dest_inl trm of
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   104
      SOME trm' => dest_inj s trm'
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   105
    | _ => dest_inj t (the (dest_inr trm))
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   106
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   107
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   108
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   109
(** Matrix cell datatype **)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   110
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   111
datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm;
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   112
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   113
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   114
type data =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   115
  skel                            (* structure of the sum type encoding "program points" *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   116
  * (int -> typ)                  (* types of program points *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   117
  * (term list Inttab.table)      (* measures for program points *)
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   118
  * (term * term -> thm option)   (* which calls form chains? (cached) *)
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   119
  * (term * (term * term) -> cell)(* local descents (cached) *)
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   120
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   121
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   122
(* Build case expression *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   123
fun mk_sumcases (sk, _, _, _, _) T fs =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   124
  mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   125
          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   126
          sk
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   127
  |> fst
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   128
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   129
fun mk_sum_skel rel =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   130
  let
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32683
diff changeset
   131
    val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
32602
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
   132
    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   133
      let
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   134
        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   135
          = Term.strip_qnt_body @{const_name Ex} c
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   136
      in cons r o cons l end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   137
  in
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   138
    mk_skel (fold collect_pats cs [])
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   139
  end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   140
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   141
fun prove_chain thy chain_tac (c1, c2) =
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   142
  let
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   143
    val goal =
47433
07f4bf913230 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents: 46218
diff changeset
   144
      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   145
        Const (@{const_abbrev Set.empty}, fastype_of c1))
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   146
      |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   147
  in
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   148
    case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   149
      Function_Lib.Solved thm => SOME thm
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   150
    | _ => NONE
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   151
  end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   152
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   153
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   154
fun dest_call' sk (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   155
  let
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   156
    val vs = Term.strip_qnt_vars @{const_name Ex} c
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   157
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   158
    (* FIXME: throw error "dest_call" for malformed terms *)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   159
    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
38557
9926c47ad1a1 more antiquotations
haftmann
parents: 38549
diff changeset
   160
      = Term.strip_qnt_body @{const_name Ex} c
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   161
    val (p, l') = dest_inj sk l
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   162
    val (q, r') = dest_inj sk r
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   163
  in
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   164
    (vs, p, l', q, r', Gam)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   165
  end
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   166
  | dest_call' _ _ = error "dest_call"
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   167
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   168
fun dest_call (sk, _, _, _, _) = dest_call' sk
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   169
34229
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   170
fun mk_desc thy tac vs Gam l r m1 m2 =
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   171
  let
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   172
    fun try rel =
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   173
      try_proof (cterm_of thy
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 45740
diff changeset
   174
        (Logic.list_all (vs,
34229
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   175
           Logic.mk_implies (HOLogic.mk_Trueprop Gam,
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   176
             HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   177
               $ (m2 $ r) $ (m1 $ l)))))) tac
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   178
  in
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 34974
diff changeset
   179
    case try @{const_name Orderings.less} of
34229
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   180
       Solved thm => Less thm
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   181
     | Stuck thm =>
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 34974
diff changeset
   182
       (case try @{const_name Orderings.less_eq} of
34229
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   183
          Solved thm2 => LessEq (thm2, thm)
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   184
        | Stuck thm2 =>
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 42793
diff changeset
   185
          if prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
34229
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   186
          then False thm2 else None (thm2, thm)
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   187
        | _ => raise Match) (* FIXME *)
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   188
     | _ => raise Match
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   189
end
f66bb6536f6a simplified
krauss
parents: 34228
diff changeset
   190
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   191
fun prove_descent thy tac sk (c, (m1, m2)) =
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   192
  let
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   193
    val (vs, _, l, _, r, Gam) = dest_call' sk c
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   194
  in 
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   195
    mk_desc thy tac vs Gam l r m1 m2
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   196
  end
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   197
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   198
fun create ctxt chain_tac descent_tac T rel =
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   199
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41114
diff changeset
   200
    val thy = Proof_Context.theory_of ctxt
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   201
    val sk = mk_sum_skel rel
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   202
    val Ts = node_types sk T
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   203
    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   204
    val chain_cache = Cache.create Term2tab.empty Term2tab.lookup Term2tab.update
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   205
      (prove_chain thy chain_tac)
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   206
    val descent_cache = Cache.create Term3tab.empty Term3tab.lookup Term3tab.update
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   207
      (prove_descent thy descent_tac sk)
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   208
  in
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   209
    (sk, nth Ts, M, chain_cache, descent_cache)
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   210
  end
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   211
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   212
fun get_num_points (sk, _, _, _, _) =
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   213
  let
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   214
    fun num (SLeaf i) = i + 1
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   215
      | num (SBranch (s, t)) = num t
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   216
  in num sk end
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   217
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   218
fun get_types (_, T, _, _, _) = T
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   219
fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   220
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   221
fun get_chain (_, _, _, C, _) c1 c2 =
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   222
  SOME (C (c1, c2))
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   223
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   224
fun get_descent (_, _, _, _, D) c m1 m2 =
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   225
  SOME (D (c, (m1, m2)))
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   226
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   227
fun CALLS tac i st =
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   228
  if Thm.no_prems st then all_tac st
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   229
  else case Thm.term_of (Thm.cprem_of st i) of
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32683
diff changeset
   230
    (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   231
  |_ => no_tac st
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   232
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   233
type ttac = data -> int -> tactic
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   234
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   235
fun TERMINATION ctxt atac tac =
32602
f2b741473860 more antiquotations
haftmann
parents: 32149
diff changeset
   236
  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   237
  let
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   238
    val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   239
  in
39923
0e1bd289c8ea use Cache structure instead of passing tables around explicitly
krauss
parents: 38864
diff changeset
   240
    tac (create ctxt atac atac T rel) i
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   241
  end)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   242
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   243
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   244
(* A tactic to convert open to closed termination goals *)
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   245
local
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   246
fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   247
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   248
    val (vars, prop) = Function_Lib.dest_all_all t
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   249
    val (prems, concl) = Logic.strip_horn prop
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   250
    val (lhs, rhs) = concl
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   251
      |> HOLogic.dest_Trueprop
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   252
      |> HOLogic.dest_mem |> fst
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   253
      |> HOLogic.dest_prod
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   254
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   255
    (vars, prems, lhs, rhs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   256
  end
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   257
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   258
fun mk_pair_compr (T, qs, l, r, conds) =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   259
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   260
    val pT = HOLogic.mk_prodT (T, T)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   261
    val n = length qs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   262
    val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 42793
diff changeset
   263
    val conds' = if null conds then [@{term True}] else conds
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   264
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   265
    HOLogic.Collect_const pT $
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   266
    Abs ("uu_", pT,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   267
      (foldr1 HOLogic.mk_conj (peq :: conds')
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   268
      |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   269
  end
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   270
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   271
in
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   272
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30304
diff changeset
   273
fun wf_union_tac ctxt st =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   274
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41114
diff changeset
   275
    val thy = Proof_Context.theory_of ctxt
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   276
    val cert = cterm_of (theory_of_thm st)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   277
    val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   278
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   279
    fun mk_compr ineq =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   280
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   281
        val (vars, prems, lhs, rhs) = dest_term ineq
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   282
      in
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35408
diff changeset
   283
        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   284
      end
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   285
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   286
    val relation =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   287
      if null ineqs
35402
115a5a95710a clarified @{const_name} vs. @{const_abbrev};
wenzelm
parents: 35092
diff changeset
   288
      then Const (@{const_abbrev Set.empty}, fastype_of rel)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   289
      else map mk_compr ineqs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   290
        |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   291
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   292
    fun solve_membership_tac i =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   293
      (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   294
      THEN' (fn j => TRY (rtac @{thm UnI1} j))
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   295
      THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   296
      THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   297
      THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   298
        ORELSE' ((rtac @{thm conjI})
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   299
          THEN' (rtac @{thm refl})
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   300
          THEN' (blast_tac ctxt)))    (* Solve rest of context... not very elegant *)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   301
      ) i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   302
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   303
    ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   304
     THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   305
  end
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   306
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   307
end
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   308
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   309
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   310
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   311
(*** DEPENDENCY GRAPHS ***)
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   312
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   313
fun mk_dgraph D cs =
35404
de56579ae229 just one copy of structure Term_Graph (in Pure);
wenzelm
parents: 35402
diff changeset
   314
  Term_Graph.empty
de56579ae229 just one copy of structure Term_Graph (in Pure);
wenzelm
parents: 35402
diff changeset
   315
  |> fold (fn c => Term_Graph.new_node (c, ())) cs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   316
  |> fold_product (fn c1 => fn c2 =>
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   317
     if is_none (get_chain D c1 c2 |> the_default NONE)
47835
2d48bf79b725 dependency graphs: fixed direction of edges
krauss
parents: 47433
diff changeset
   318
     then Term_Graph.add_edge (c2, c1) else I)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   319
     cs cs
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   320
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   321
fun ucomp_empty_tac T =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   322
  REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   323
    ORELSE' rtac @{thm union_comp_emptyL}
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   324
    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   325
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   326
fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   327
 let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   328
   val is = map (fn c => find_index (curry op aconv c) cs') cs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   329
 in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   330
   CONVERSION (Conv.arg_conv (Conv.arg_conv
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   331
     (Function_Lib.regroup_union_conv is))) i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   332
 end)
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   333
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   334
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   335
fun solve_trivial_tac D = CALLS (fn ([c], i) =>
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   336
  (case get_chain D c c of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   337
     SOME (SOME thm) => rtac @{thm wf_no_loop} i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   338
                        THEN rtac thm i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   339
   | _ => no_tac)
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   340
  | _ => no_tac)
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   341
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   342
fun decompose_tac D = CALLS (fn (cs, i) =>
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   343
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   344
    val G = mk_dgraph D cs
35404
de56579ae229 just one copy of structure Term_Graph (in Pure);
wenzelm
parents: 35402
diff changeset
   345
    val sccs = Term_Graph.strong_conn G
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   346
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   347
    fun split [SCC] i = TRY (solve_trivial_tac D i)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   348
      | split (SCC::rest) i =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   349
        regroup_calls_tac SCC i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   350
        THEN rtac @{thm wf_union_compatible} i
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   351
        THEN rtac @{thm less_by_empty} (i + 2)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   352
        THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   353
        THEN split rest (i + 1)
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   354
        THEN TRY (solve_trivial_tac D i)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   355
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   356
    if length sccs > 1 then split sccs i
39924
f4d3e70ed3a8 discontinued continuations to simplify control flow; dropped optimization in scnp
krauss
parents: 39923
diff changeset
   357
    else solve_trivial_tac D i
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 34229
diff changeset
   358
  end)
34228
bc0cea4cae52 absorb structures Decompose and Descent into Termination, to simplify further restructuring
krauss
parents: 33855
diff changeset
   359
29125
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   360
d41182a8135c method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff changeset
   361
end