src/HOL/Tools/Function/termination.ML
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39923 0e1bd289c8ea
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
haftmann@31775
     1
(*  Title:       HOL/Tools/Function/termination.ML
krauss@29125
     2
    Author:      Alexander Krauss, TU Muenchen
krauss@29125
     3
krauss@29125
     4
Context data for termination proofs
krauss@29125
     5
*)
krauss@29125
     6
krauss@29125
     7
krauss@29125
     8
signature TERMINATION =
krauss@29125
     9
sig
krauss@29125
    10
krauss@29125
    11
  type data
krauss@29125
    12
  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
krauss@29125
    13
krauss@29125
    14
  val mk_sumcases : data -> typ -> term list -> term
krauss@29125
    15
krauss@29125
    16
  val get_num_points : data -> int
krauss@29125
    17
  val get_types      : data -> int -> typ
krauss@29125
    18
  val get_measures   : data -> int -> term list
krauss@29125
    19
krauss@29125
    20
  (* read from cache *)
krauss@29125
    21
  val get_chain      : data -> term -> term -> thm option option
krauss@29125
    22
  val get_descent    : data -> term -> term -> term -> cell option
krauss@29125
    23
krauss@29125
    24
  val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
krauss@29125
    25
krauss@29125
    26
  val CALLS : (term list * int -> tactic) -> int -> tactic
krauss@29125
    27
krauss@29125
    28
  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
krauss@29125
    29
  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
krauss@29125
    30
krauss@29125
    31
  val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
krauss@29125
    32
krauss@29125
    33
  val REPEAT : ttac -> ttac
krauss@29125
    34
wenzelm@30607
    35
  val wf_union_tac : Proof.context -> tactic
krauss@34228
    36
krauss@34228
    37
  val decompose_tac : Proof.context -> tactic -> ttac
krauss@34228
    38
krauss@34228
    39
  val derive_diag : Proof.context -> tactic -> 
krauss@34228
    40
    (data -> int -> tactic) -> data -> int -> tactic
krauss@34228
    41
krauss@34228
    42
  val derive_all  : Proof.context -> tactic ->
krauss@34228
    43
    (data -> int -> tactic) -> data -> int -> tactic
krauss@34228
    44
krauss@29125
    45
end
krauss@29125
    46
krauss@29125
    47
krauss@29125
    48
krauss@29125
    49
structure Termination : TERMINATION =
krauss@29125
    50
struct
krauss@29125
    51
krauss@33099
    52
open Function_Lib
krauss@29125
    53
wenzelm@35408
    54
val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
wenzelm@31971
    55
structure Term2tab = Table(type key = term * term val ord = term2_ord);
wenzelm@35408
    56
structure Term3tab =
wenzelm@35408
    57
  Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord);
krauss@29125
    58
krauss@29125
    59
(** Analyzing binary trees **)
krauss@29125
    60
krauss@29125
    61
(* Skeleton of a tree structure *)
krauss@29125
    62
krauss@29125
    63
datatype skel =
krauss@29125
    64
  SLeaf of int (* index *)
krauss@29125
    65
| SBranch of (skel * skel)
krauss@29125
    66
krauss@29125
    67
krauss@29125
    68
(* abstract make and dest functions *)
krauss@29125
    69
fun mk_tree leaf branch =
krauss@29125
    70
  let fun mk (SLeaf i) = leaf i
krauss@29125
    71
        | mk (SBranch (s, t)) = branch (mk s, mk t)
krauss@29125
    72
  in mk end
krauss@29125
    73
krauss@29125
    74
krauss@29125
    75
fun dest_tree split =
krauss@29125
    76
  let fun dest (SLeaf i) x = [(i, x)]
krauss@29125
    77
        | dest (SBranch (s, t)) x =
krauss@29125
    78
          let val (l, r) = split x
krauss@29125
    79
          in dest s l @ dest t r end
krauss@29125
    80
  in dest end
krauss@29125
    81
krauss@29125
    82
krauss@29125
    83
(* concrete versions for sum types *)
haftmann@32602
    84
fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
haftmann@32602
    85
  | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
krauss@29125
    86
  | is_inj _ = false
krauss@29125
    87
haftmann@32602
    88
fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
krauss@29125
    89
  | dest_inl _ = NONE
krauss@29125
    90
haftmann@32602
    91
fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
krauss@29125
    92
  | dest_inr _ = NONE
krauss@29125
    93
krauss@29125
    94
krauss@29125
    95
fun mk_skel ps =
krauss@29125
    96
  let
krauss@29125
    97
    fun skel i ps =
krauss@29125
    98
      if forall is_inj ps andalso not (null ps)
krauss@29125
    99
      then let
krauss@29125
   100
          val (j, s) = skel i (map_filter dest_inl ps)
krauss@29125
   101
          val (k, t) = skel j (map_filter dest_inr ps)
krauss@29125
   102
        in (k, SBranch (s, t)) end
krauss@29125
   103
      else (i + 1, SLeaf i)
krauss@29125
   104
  in
krauss@29125
   105
    snd (skel 0 ps)
krauss@29125
   106
  end
krauss@29125
   107
krauss@29125
   108
(* compute list of types for nodes *)
haftmann@37678
   109
fun node_types sk T = dest_tree (fn Type (@{type_name Sum_Type.sum}, [LT, RT]) => (LT, RT)) sk T |> map snd
krauss@29125
   110
krauss@29125
   111
(* find index and raw term *)
krauss@29125
   112
fun dest_inj (SLeaf i) trm = (i, trm)
krauss@29125
   113
  | dest_inj (SBranch (s, t)) trm =
krauss@29125
   114
    case dest_inl trm of
krauss@29125
   115
      SOME trm' => dest_inj s trm'
krauss@29125
   116
    | _ => dest_inj t (the (dest_inr trm))
krauss@29125
   117
krauss@29125
   118
krauss@29125
   119
krauss@29125
   120
(** Matrix cell datatype **)
krauss@29125
   121
krauss@29125
   122
datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
krauss@29125
   123
krauss@29125
   124
krauss@29125
   125
type data =
krauss@29125
   126
  skel                            (* structure of the sum type encoding "program points" *)
krauss@29125
   127
  * (int -> typ)                  (* types of program points *)
krauss@29125
   128
  * (term list Inttab.table)      (* measures for program points *)
krauss@29125
   129
  * (thm option Term2tab.table)   (* which calls form chains? *)
krauss@29125
   130
  * (cell Term3tab.table)         (* local descents *)
krauss@29125
   131
krauss@29125
   132
krauss@34228
   133
fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
krauss@34228
   134
fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
krauss@29125
   135
krauss@29125
   136
fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
krauss@29125
   137
fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
krauss@29125
   138
krauss@29125
   139
(* Build case expression *)
krauss@29125
   140
fun mk_sumcases (sk, _, _, _, _) T fs =
krauss@29125
   141
  mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
krauss@29125
   142
          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
krauss@29125
   143
          sk
krauss@29125
   144
  |> fst
krauss@29125
   145
krauss@29125
   146
fun mk_sum_skel rel =
krauss@29125
   147
  let
krauss@33099
   148
    val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
haftmann@32602
   149
    fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
krauss@29125
   150
      let
haftmann@38864
   151
        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
haftmann@38557
   152
          = Term.strip_qnt_body @{const_name Ex} c
krauss@29125
   153
      in cons r o cons l end
krauss@29125
   154
  in
krauss@29125
   155
    mk_skel (fold collect_pats cs [])
krauss@29125
   156
  end
krauss@29125
   157
krauss@29125
   158
fun create ctxt T rel =
krauss@29125
   159
  let
krauss@29125
   160
    val sk = mk_sum_skel rel
krauss@29125
   161
    val Ts = node_types sk T
krauss@29125
   162
    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
krauss@29125
   163
  in
krauss@29125
   164
    (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
krauss@29125
   165
  end
krauss@29125
   166
krauss@29125
   167
fun get_num_points (sk, _, _, _, _) =
krauss@29125
   168
  let
krauss@29125
   169
    fun num (SLeaf i) = i + 1
krauss@29125
   170
      | num (SBranch (s, t)) = num t
krauss@29125
   171
  in num sk end
krauss@29125
   172
krauss@29125
   173
fun get_types (_, T, _, _, _) = T
krauss@29125
   174
fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
krauss@29125
   175
krauss@29125
   176
fun get_chain (_, _, _, C, _) c1 c2 =
krauss@29125
   177
  Term2tab.lookup C (c1, c2)
krauss@29125
   178
krauss@29125
   179
fun get_descent (_, _, _, _, D) c m1 m2 =
krauss@29125
   180
  Term3tab.lookup D (c, (m1, m2))
krauss@29125
   181
haftmann@32602
   182
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
krauss@29125
   183
  let
krauss@29125
   184
    val (sk, _, _, _, _) = D
haftmann@38557
   185
    val vs = Term.strip_qnt_vars @{const_name Ex} c
krauss@29125
   186
krauss@29125
   187
    (* FIXME: throw error "dest_call" for malformed terms *)
haftmann@38864
   188
    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
haftmann@38557
   189
      = Term.strip_qnt_body @{const_name Ex} c
krauss@29125
   190
    val (p, l') = dest_inj sk l
krauss@29125
   191
    val (q, r') = dest_inj sk r
krauss@29125
   192
  in
krauss@29125
   193
    (vs, p, l', q, r', Gam)
krauss@29125
   194
  end
krauss@29125
   195
  | dest_call D t = error "dest_call"
krauss@29125
   196
krauss@29125
   197
krauss@34229
   198
fun mk_desc thy tac vs Gam l r m1 m2 =
krauss@34229
   199
  let
krauss@34229
   200
    fun try rel =
krauss@34229
   201
      try_proof (cterm_of thy
krauss@34229
   202
        (Term.list_all (vs,
krauss@34229
   203
           Logic.mk_implies (HOLogic.mk_Trueprop Gam,
krauss@34229
   204
             HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
krauss@34229
   205
               $ (m2 $ r) $ (m1 $ l)))))) tac
krauss@34229
   206
  in
haftmann@35092
   207
    case try @{const_name Orderings.less} of
krauss@34229
   208
       Solved thm => Less thm
krauss@34229
   209
     | Stuck thm =>
haftmann@35092
   210
       (case try @{const_name Orderings.less_eq} of
krauss@34229
   211
          Solved thm2 => LessEq (thm2, thm)
krauss@34229
   212
        | Stuck thm2 =>
krauss@34229
   213
          if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
krauss@34229
   214
          then False thm2 else None (thm2, thm)
krauss@34229
   215
        | _ => raise Match) (* FIXME *)
krauss@34229
   216
     | _ => raise Match
krauss@34229
   217
end
krauss@34229
   218
krauss@34229
   219
fun derive_descent thy tac c m1 m2 D =
krauss@29125
   220
  case get_descent D c m1 m2 of
krauss@29125
   221
    SOME _ => D
krauss@34229
   222
  | NONE => 
krauss@34229
   223
    let
krauss@34229
   224
      val (vs, _, l, _, r, Gam) = dest_call D c
krauss@34229
   225
    in 
krauss@34229
   226
      note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
krauss@34229
   227
    end
krauss@29125
   228
krauss@29125
   229
fun CALLS tac i st =
krauss@29125
   230
  if Thm.no_prems st then all_tac st
krauss@29125
   231
  else case Thm.term_of (Thm.cprem_of st i) of
krauss@33099
   232
    (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
krauss@29125
   233
  |_ => no_tac st
krauss@29125
   234
krauss@29125
   235
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
krauss@29125
   236
krauss@29125
   237
fun TERMINATION ctxt tac =
haftmann@32602
   238
  SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
krauss@29125
   239
  let
krauss@29125
   240
    val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
krauss@29125
   241
  in
krauss@29125
   242
    tac (create ctxt T rel) i
krauss@29125
   243
  end)
krauss@29125
   244
krauss@29125
   245
krauss@29125
   246
(* A tactic to convert open to closed termination goals *)
krauss@29125
   247
local
krauss@29125
   248
fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
krauss@34232
   249
  let
krauss@34232
   250
    val (vars, prop) = Function_Lib.dest_all_all t
krauss@34232
   251
    val (prems, concl) = Logic.strip_horn prop
krauss@34232
   252
    val (lhs, rhs) = concl
krauss@34232
   253
      |> HOLogic.dest_Trueprop
krauss@34232
   254
      |> HOLogic.dest_mem |> fst
krauss@34232
   255
      |> HOLogic.dest_prod
krauss@34232
   256
  in
krauss@34232
   257
    (vars, prems, lhs, rhs)
krauss@34232
   258
  end
krauss@29125
   259
krauss@29125
   260
fun mk_pair_compr (T, qs, l, r, conds) =
krauss@34232
   261
  let
krauss@34232
   262
    val pT = HOLogic.mk_prodT (T, T)
krauss@34232
   263
    val n = length qs
krauss@34232
   264
    val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
krauss@34232
   265
    val conds' = if null conds then [HOLogic.true_const] else conds
krauss@34232
   266
  in
krauss@34232
   267
    HOLogic.Collect_const pT $
krauss@34232
   268
    Abs ("uu_", pT,
krauss@34232
   269
      (foldr1 HOLogic.mk_conj (peq :: conds')
krauss@34232
   270
      |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
krauss@34232
   271
  end
krauss@29125
   272
krauss@29125
   273
in
krauss@29125
   274
wenzelm@30607
   275
fun wf_union_tac ctxt st =
krauss@34232
   276
  let
krauss@34232
   277
    val thy = ProofContext.theory_of ctxt
krauss@34232
   278
    val cert = cterm_of (theory_of_thm st)
krauss@34232
   279
    val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
krauss@29125
   280
krauss@34232
   281
    fun mk_compr ineq =
krauss@34232
   282
      let
krauss@34232
   283
        val (vars, prems, lhs, rhs) = dest_term ineq
krauss@34232
   284
      in
wenzelm@35625
   285
        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
krauss@34232
   286
      end
krauss@29125
   287
krauss@34232
   288
    val relation =
krauss@34232
   289
      if null ineqs
wenzelm@35402
   290
      then Const (@{const_abbrev Set.empty}, fastype_of rel)
krauss@34232
   291
      else map mk_compr ineqs
krauss@34232
   292
        |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
krauss@29125
   293
krauss@34232
   294
    fun solve_membership_tac i =
krauss@34232
   295
      (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
krauss@34232
   296
      THEN' (fn j => TRY (rtac @{thm UnI1} j))
krauss@34232
   297
      THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
krauss@34232
   298
      THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
krauss@34232
   299
      THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
krauss@34232
   300
        ORELSE' ((rtac @{thm conjI})
krauss@34232
   301
          THEN' (rtac @{thm refl})
krauss@34232
   302
          THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
krauss@34232
   303
      ) i
krauss@34232
   304
  in
krauss@34232
   305
    ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
krauss@34232
   306
     THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
krauss@34232
   307
  end
krauss@29125
   308
krauss@29125
   309
end
krauss@29125
   310
krauss@29125
   311
krauss@29125
   312
(* continuation passing repeat combinator *)
krauss@29125
   313
fun REPEAT ttac cont err_cont =
krauss@29125
   314
    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
krauss@29125
   315
krauss@34228
   316
(*** DEPENDENCY GRAPHS ***)
krauss@29125
   317
krauss@34228
   318
fun prove_chain thy chain_tac c1 c2 =
krauss@34228
   319
  let
krauss@34228
   320
    val goal =
krauss@34228
   321
      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
wenzelm@35402
   322
        Const (@{const_abbrev Set.empty}, fastype_of c1))
krauss@34228
   323
      |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
krauss@34228
   324
  in
krauss@34228
   325
    case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
krauss@34228
   326
      Function_Lib.Solved thm => SOME thm
krauss@34228
   327
    | _ => NONE
krauss@34228
   328
  end
krauss@34228
   329
krauss@34228
   330
fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) =>
krauss@34228
   331
  let
krauss@34232
   332
    val thy = ProofContext.theory_of ctxt
krauss@34228
   333
krauss@34232
   334
    fun derive_chain c1 c2 D =
krauss@34232
   335
      if is_some (get_chain D c1 c2) then D else
krauss@34232
   336
      note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
krauss@34228
   337
  in
krauss@34228
   338
    cont (fold_product derive_chain cs cs D) i
krauss@34228
   339
  end)
krauss@34228
   340
krauss@34228
   341
krauss@34228
   342
fun mk_dgraph D cs =
wenzelm@35404
   343
  Term_Graph.empty
wenzelm@35404
   344
  |> fold (fn c => Term_Graph.new_node (c, ())) cs
krauss@34232
   345
  |> fold_product (fn c1 => fn c2 =>
krauss@34232
   346
     if is_none (get_chain D c1 c2 |> the_default NONE)
wenzelm@35404
   347
     then Term_Graph.add_edge (c1, c2) else I)
krauss@34232
   348
     cs cs
krauss@34228
   349
krauss@34228
   350
fun ucomp_empty_tac T =
krauss@34232
   351
  REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
krauss@34232
   352
    ORELSE' rtac @{thm union_comp_emptyL}
krauss@34232
   353
    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
krauss@34228
   354
krauss@34228
   355
fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
krauss@34232
   356
 let
krauss@34232
   357
   val is = map (fn c => find_index (curry op aconv c) cs') cs
krauss@34232
   358
 in
krauss@34232
   359
   CONVERSION (Conv.arg_conv (Conv.arg_conv
krauss@34232
   360
     (Function_Lib.regroup_union_conv is))) i
krauss@34232
   361
 end)
krauss@34228
   362
krauss@34228
   363
krauss@34232
   364
fun solve_trivial_tac D = CALLS (fn ([c], i) =>
krauss@34232
   365
  (case get_chain D c c of
krauss@34232
   366
     SOME (SOME thm) => rtac @{thm wf_no_loop} i
krauss@34232
   367
                        THEN rtac thm i
krauss@34232
   368
   | _ => no_tac)
krauss@34228
   369
  | _ => no_tac)
krauss@34228
   370
krauss@34228
   371
fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
krauss@34232
   372
  let
krauss@34232
   373
    val G = mk_dgraph D cs
wenzelm@35404
   374
    val sccs = Term_Graph.strong_conn G
krauss@34228
   375
krauss@34232
   376
    fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
krauss@34232
   377
      | split (SCC::rest) i =
krauss@34232
   378
        regroup_calls_tac SCC i
krauss@34232
   379
        THEN rtac @{thm wf_union_compatible} i
krauss@34232
   380
        THEN rtac @{thm less_by_empty} (i + 2)
krauss@34232
   381
        THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
krauss@34232
   382
        THEN split rest (i + 1)
krauss@34232
   383
        THEN (solve_trivial_tac D i ORELSE cont D i)
krauss@34232
   384
  in
krauss@34232
   385
    if length sccs > 1 then split sccs i
krauss@34232
   386
    else solve_trivial_tac D i ORELSE err_cont D i
krauss@34232
   387
  end)
krauss@34228
   388
krauss@34228
   389
fun decompose_tac ctxt chain_tac cont err_cont =
krauss@34232
   390
  derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
krauss@34228
   391
krauss@34228
   392
krauss@34228
   393
(*** Local Descent Proofs ***)
krauss@34228
   394
krauss@34228
   395
fun gen_descent diag ctxt tac cont D = CALLS (fn (cs, i) =>
krauss@34228
   396
  let
krauss@34228
   397
    val thy = ProofContext.theory_of ctxt
krauss@34228
   398
    val measures_of = get_measures D
krauss@34228
   399
krauss@34228
   400
    fun derive c D =
krauss@34228
   401
      let
krauss@34228
   402
        val (_, p, _, q, _, _) = dest_call D c
krauss@34228
   403
      in
krauss@34228
   404
        if diag andalso p = q
krauss@34228
   405
        then fold (fn m => derive_descent thy tac c m m) (measures_of p) D
krauss@34228
   406
        else fold_product (derive_descent thy tac c)
krauss@34228
   407
               (measures_of p) (measures_of q) D
krauss@34228
   408
      end
krauss@34228
   409
  in
krauss@34228
   410
    cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
krauss@34228
   411
  end)
krauss@34228
   412
wenzelm@34236
   413
fun derive_diag ctxt = gen_descent true ctxt
wenzelm@34236
   414
fun derive_all ctxt = gen_descent false ctxt
krauss@29125
   415
krauss@29125
   416
krauss@29125
   417
end