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