src/HOL/Tools/Function/scnp_reconstruct.ML
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32149 ef59550a55d3
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
haftmann@31775
     1
(*  Title:       HOL/Tools/Function/scnp_reconstruct.ML
krauss@29125
     2
    Author:      Armin Heller, TU Muenchen
krauss@29125
     3
    Author:      Alexander Krauss, TU Muenchen
krauss@29125
     4
krauss@29125
     5
Proof reconstruction for SCNP
krauss@29125
     6
*)
krauss@29125
     7
krauss@29125
     8
signature SCNP_RECONSTRUCT =
krauss@29125
     9
sig
krauss@29125
    10
krauss@29877
    11
  val sizechange_tac : Proof.context -> tactic -> tactic
krauss@29877
    12
wenzelm@30510
    13
  val decomp_scnp : ScnpSolve.label list -> Proof.context -> Proof.method
krauss@29125
    14
krauss@29125
    15
  val setup : theory -> theory
krauss@29125
    16
krauss@29125
    17
  datatype multiset_setup =
krauss@29125
    18
    Multiset of
krauss@29125
    19
    {
krauss@29125
    20
     msetT : typ -> typ,
krauss@29125
    21
     mk_mset : typ -> term list -> term,
krauss@29125
    22
     mset_regroup_conv : int list -> conv,
krauss@29125
    23
     mset_member_tac : int -> int -> tactic,
krauss@29125
    24
     mset_nonempty_tac : int -> tactic,
krauss@29125
    25
     mset_pwleq_tac : int -> tactic,
krauss@29125
    26
     set_of_simps : thm list,
krauss@29125
    27
     smsI' : thm,
krauss@29125
    28
     wmsI2'' : thm,
krauss@29125
    29
     wmsI1 : thm,
krauss@29125
    30
     reduction_pair : thm
krauss@29125
    31
    }
krauss@29125
    32
krauss@29125
    33
krauss@29125
    34
  val multiset_setup : multiset_setup -> theory -> theory
krauss@29125
    35
krauss@29125
    36
end
krauss@29125
    37
krauss@29125
    38
structure ScnpReconstruct : SCNP_RECONSTRUCT =
krauss@29125
    39
struct
krauss@29125
    40
krauss@29125
    41
val PROFILE = FundefCommon.PROFILE
krauss@29125
    42
fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
krauss@29125
    43
krauss@29125
    44
open ScnpSolve
krauss@29125
    45
krauss@29125
    46
val natT = HOLogic.natT
krauss@29125
    47
val nat_pairT = HOLogic.mk_prodT (natT, natT)
krauss@29125
    48
krauss@29125
    49
(* Theory dependencies *)
krauss@29125
    50
krauss@29125
    51
datatype multiset_setup =
krauss@29125
    52
  Multiset of
krauss@29125
    53
  {
krauss@29125
    54
   msetT : typ -> typ,
krauss@29125
    55
   mk_mset : typ -> term list -> term,
krauss@29125
    56
   mset_regroup_conv : int list -> conv,
krauss@29125
    57
   mset_member_tac : int -> int -> tactic,
krauss@29125
    58
   mset_nonempty_tac : int -> tactic,
krauss@29125
    59
   mset_pwleq_tac : int -> tactic,
krauss@29125
    60
   set_of_simps : thm list,
krauss@29125
    61
   smsI' : thm,
krauss@29125
    62
   wmsI2'' : thm,
krauss@29125
    63
   wmsI1 : thm,
krauss@29125
    64
   reduction_pair : thm
krauss@29125
    65
  }
krauss@29125
    66
krauss@29125
    67
structure MultisetSetup = TheoryDataFun
krauss@29125
    68
(
krauss@29125
    69
  type T = multiset_setup option
krauss@29125
    70
  val empty = NONE
krauss@29125
    71
  val copy = I;
krauss@29125
    72
  val extend = I;
krauss@29125
    73
  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
krauss@29125
    74
)
krauss@29125
    75
krauss@29125
    76
val multiset_setup = MultisetSetup.put o SOME
krauss@29125
    77
krauss@29125
    78
fun undef x = error "undef"
krauss@29125
    79
fun get_multiset_setup thy = MultisetSetup.get thy
krauss@29125
    80
  |> the_default (Multiset
krauss@29125
    81
{ msetT = undef, mk_mset=undef,
krauss@29125
    82
  mset_regroup_conv=undef, mset_member_tac = undef,
krauss@29125
    83
  mset_nonempty_tac = undef, mset_pwleq_tac = undef,
krauss@29125
    84
  set_of_simps = [],reduction_pair = refl,
krauss@29125
    85
  smsI'=refl, wmsI2''=refl, wmsI1=refl })
krauss@29125
    86
krauss@29125
    87
fun order_rpair _ MAX = @{thm max_rpair_set}
krauss@29125
    88
  | order_rpair msrp MS  = msrp
krauss@29125
    89
  | order_rpair _ MIN = @{thm min_rpair_set}
krauss@29125
    90
krauss@29125
    91
fun ord_intros_max true =
krauss@29125
    92
    (@{thm smax_emptyI}, @{thm smax_insertI})
krauss@29125
    93
  | ord_intros_max false =
krauss@29125
    94
    (@{thm wmax_emptyI}, @{thm wmax_insertI})
krauss@29125
    95
fun ord_intros_min true =
krauss@29125
    96
    (@{thm smin_emptyI}, @{thm smin_insertI})
krauss@29125
    97
  | ord_intros_min false =
krauss@29125
    98
    (@{thm wmin_emptyI}, @{thm wmin_insertI})
krauss@29125
    99
krauss@29125
   100
fun gen_probl D cs =
krauss@29125
   101
  let
krauss@29125
   102
    val n = Termination.get_num_points D
krauss@29125
   103
    val arity = length o Termination.get_measures D
krauss@29125
   104
    fun measure p i = nth (Termination.get_measures D p) i
krauss@29125
   105
krauss@29125
   106
    fun mk_graph c =
krauss@29125
   107
      let
krauss@29125
   108
        val (_, p, _, q, _, _) = Termination.dest_call D c
krauss@29125
   109
krauss@29125
   110
        fun add_edge i j =
krauss@29125
   111
          case Termination.get_descent D c (measure p i) (measure q j)
krauss@29125
   112
           of SOME (Termination.Less _) => cons (i, GTR, j)
krauss@29125
   113
            | SOME (Termination.LessEq _) => cons (i, GEQ, j)
krauss@29125
   114
            | _ => I
krauss@29125
   115
krauss@29125
   116
        val edges =
krauss@29125
   117
          fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
krauss@29125
   118
      in
krauss@29125
   119
        G (p, q, edges)
krauss@29125
   120
      end
krauss@29125
   121
  in
krauss@29125
   122
    GP (map arity (0 upto n - 1), map mk_graph cs)
krauss@29125
   123
  end
krauss@29125
   124
krauss@29125
   125
(* General reduction pair application *)
krauss@29125
   126
fun rem_inv_img ctxt =
krauss@29125
   127
  let
krauss@29125
   128
    val unfold_tac = LocalDefs.unfold_tac ctxt
krauss@29125
   129
  in
krauss@29125
   130
    rtac @{thm subsetI} 1
krauss@29125
   131
    THEN etac @{thm CollectE} 1
krauss@29125
   132
    THEN REPEAT (etac @{thm exE} 1)
krauss@29125
   133
    THEN unfold_tac @{thms inv_image_def}
krauss@29125
   134
    THEN rtac @{thm CollectI} 1
krauss@29125
   135
    THEN etac @{thm conjE} 1
krauss@29125
   136
    THEN etac @{thm ssubst} 1
krauss@29125
   137
    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
krauss@29183
   138
                     @ @{thms sum.cases})
krauss@29125
   139
  end
krauss@29125
   140
krauss@29125
   141
(* Sets *)
krauss@29125
   142
krauss@29125
   143
val setT = HOLogic.mk_setT
krauss@29125
   144
krauss@29125
   145
fun set_member_tac m i =
krauss@29125
   146
  if m = 0 then rtac @{thm insertI1} i
krauss@29125
   147
  else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
krauss@29125
   148
krauss@29125
   149
val set_nonempty_tac = rtac @{thm insert_not_empty}
krauss@29125
   150
krauss@29125
   151
fun set_finite_tac i =
krauss@29125
   152
  rtac @{thm finite.emptyI} i
krauss@29125
   153
  ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
krauss@29125
   154
krauss@29125
   155
krauss@29125
   156
(* Reconstruction *)
krauss@29125
   157
krauss@29125
   158
fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
krauss@29125
   159
  let
krauss@29125
   160
    val thy = ProofContext.theory_of ctxt
krauss@29125
   161
    val Multiset
krauss@29125
   162
          { msetT, mk_mset,
krauss@29125
   163
            mset_regroup_conv, mset_member_tac,
krauss@29125
   164
            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
krauss@29125
   165
            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
krauss@29125
   166
        = get_multiset_setup thy
krauss@29125
   167
krauss@29125
   168
    fun measure_fn p = nth (Termination.get_measures D p)
krauss@29125
   169
krauss@29125
   170
    fun get_desc_thm cidx m1 m2 bStrict =
krauss@29125
   171
      case Termination.get_descent D (nth cs cidx) m1 m2
krauss@29125
   172
       of SOME (Termination.Less thm) =>
krauss@29125
   173
          if bStrict then thm
krauss@29125
   174
          else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
krauss@29125
   175
        | SOME (Termination.LessEq (thm, _))  =>
krauss@29125
   176
          if not bStrict then thm
krauss@29125
   177
          else sys_error "get_desc_thm"
krauss@29125
   178
        | _ => sys_error "get_desc_thm"
krauss@29125
   179
krauss@29125
   180
    val (label, lev, sl, covering) = certificate
krauss@29125
   181
krauss@29125
   182
    fun prove_lev strict g =
krauss@29125
   183
      let
krauss@29125
   184
        val G (p, q, el) = nth gs g
krauss@29125
   185
krauss@29125
   186
        fun less_proof strict (j, b) (i, a) =
krauss@29125
   187
          let
krauss@29125
   188
            val tag_flag = b < a orelse (not strict andalso b <= a)
krauss@29125
   189
krauss@29125
   190
            val stored_thm =
krauss@29125
   191
              get_desc_thm g (measure_fn p i) (measure_fn q j)
krauss@29125
   192
                             (not tag_flag)
krauss@29125
   193
              |> Conv.fconv_rule (Thm.beta_conversion true)
krauss@29125
   194
krauss@29125
   195
            val rule = if strict
krauss@29125
   196
              then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
krauss@29125
   197
              else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
krauss@29125
   198
          in
krauss@29125
   199
            rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
haftmann@30686
   200
            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
krauss@29125
   201
          end
krauss@29125
   202
krauss@29125
   203
        fun steps_tac MAX strict lq lp =
krauss@29125
   204
          let
krauss@29125
   205
            val (empty, step) = ord_intros_max strict
krauss@29125
   206
          in
krauss@29125
   207
            if length lq = 0
krauss@29125
   208
            then rtac empty 1 THEN set_finite_tac 1
krauss@29125
   209
                 THEN (if strict then set_nonempty_tac 1 else all_tac)
krauss@29125
   210
            else
krauss@29125
   211
              let
krauss@29125
   212
                val (j, b) :: rest = lq
krauss@29125
   213
                val (i, a) = the (covering g strict j)
krauss@29125
   214
                fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
krauss@29125
   215
                val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
krauss@29125
   216
              in
krauss@29125
   217
                rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
krauss@29125
   218
              end
krauss@29125
   219
          end
krauss@29125
   220
          | steps_tac MIN strict lq lp =
krauss@29125
   221
          let
krauss@29125
   222
            val (empty, step) = ord_intros_min strict
krauss@29125
   223
          in
krauss@29125
   224
            if length lp = 0
krauss@29125
   225
            then rtac empty 1
krauss@29125
   226
                 THEN (if strict then set_nonempty_tac 1 else all_tac)
krauss@29125
   227
            else
krauss@29125
   228
              let
krauss@29125
   229
                val (i, a) :: rest = lp
krauss@29125
   230
                val (j, b) = the (covering g strict i)
krauss@29125
   231
                fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
krauss@29125
   232
                val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
krauss@29125
   233
              in
krauss@29125
   234
                rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
krauss@29125
   235
              end
krauss@29125
   236
          end
krauss@29125
   237
          | steps_tac MS strict lq lp =
krauss@29125
   238
          let
krauss@29125
   239
            fun get_str_cover (j, b) =
krauss@29125
   240
              if is_some (covering g true j) then SOME (j, b) else NONE
krauss@29125
   241
            fun get_wk_cover (j, b) = the (covering g false j)
krauss@29125
   242
krauss@29125
   243
            val qs = lq \\ map_filter get_str_cover lq
krauss@29125
   244
            val ps = map get_wk_cover qs
krauss@29125
   245
krauss@29125
   246
            fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
krauss@29125
   247
            val iqs = indices lq qs
krauss@29125
   248
            val ips = indices lp ps
krauss@29125
   249
krauss@29125
   250
            local open Conv in
krauss@29125
   251
            fun t_conv a C =
krauss@29125
   252
              params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
krauss@29125
   253
            val goal_rewrite =
krauss@29125
   254
                t_conv arg1_conv (mset_regroup_conv iqs)
krauss@29125
   255
                then_conv t_conv arg_conv (mset_regroup_conv ips)
krauss@29125
   256
            end
krauss@29125
   257
          in
krauss@29125
   258
            CONVERSION goal_rewrite 1
krauss@29125
   259
            THEN (if strict then rtac smsI' 1
krauss@29125
   260
                  else if qs = lq then rtac wmsI2'' 1
krauss@29125
   261
                  else rtac wmsI1 1)
krauss@29125
   262
            THEN mset_pwleq_tac 1
krauss@29125
   263
            THEN EVERY (map2 (less_proof false) qs ps)
krauss@29125
   264
            THEN (if strict orelse qs <> lq
krauss@29125
   265
                  then LocalDefs.unfold_tac ctxt set_of_simps
krauss@29125
   266
                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
krauss@29125
   267
                  else all_tac)
krauss@29125
   268
          end
krauss@29125
   269
      in
krauss@29125
   270
        rem_inv_img ctxt
krauss@29125
   271
        THEN steps_tac label strict (nth lev q) (nth lev p)
krauss@29125
   272
      end
krauss@29125
   273
haftmann@30450
   274
    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (HOLogic.mk_set, setT)
krauss@29125
   275
krauss@29125
   276
    fun tag_pair p (i, tag) =
krauss@29125
   277
      HOLogic.pair_const natT natT $
krauss@29125
   278
        (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
krauss@29125
   279
krauss@29125
   280
    fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
krauss@29125
   281
                           mk_set nat_pairT (map (tag_pair p) lm))
krauss@29125
   282
krauss@29125
   283
    val level_mapping =
krauss@29125
   284
      map_index pt_lev lev
krauss@29125
   285
        |> Termination.mk_sumcases D (setT nat_pairT)
krauss@29125
   286
        |> cterm_of thy
krauss@29125
   287
    in
krauss@29125
   288
      PROFILE "Proof Reconstruction"
krauss@29125
   289
        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
krauss@29125
   290
         THEN (rtac @{thm reduction_pair_lemma} 1)
krauss@29125
   291
         THEN (rtac @{thm rp_inv_image_rp} 1)
krauss@29125
   292
         THEN (rtac (order_rpair ms_rp label) 1)
krauss@29125
   293
         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
wenzelm@30607
   294
         THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
krauss@29125
   295
         THEN LocalDefs.unfold_tac ctxt
krauss@29125
   296
           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
krauss@29125
   297
         THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
krauss@29125
   298
         THEN EVERY (map (prove_lev true) sl)
krauss@29125
   299
         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
krauss@29125
   300
    end
krauss@29125
   301
krauss@29125
   302
krauss@29125
   303
krauss@29125
   304
local open Termination in
krauss@29125
   305
fun print_cell (SOME (Less _)) = "<"
krauss@29125
   306
  | print_cell (SOME (LessEq _)) = "\<le>"
krauss@29125
   307
  | print_cell (SOME (None _)) = "-"
krauss@29125
   308
  | print_cell (SOME (False _)) = "-"
krauss@29125
   309
  | print_cell (NONE) = "?"
krauss@29125
   310
krauss@29125
   311
fun print_error ctxt D = CALLS (fn (cs, i) =>
krauss@29125
   312
  let
krauss@29125
   313
    val np = get_num_points D
krauss@29125
   314
    val ms = map (get_measures D) (0 upto np - 1)
krauss@29125
   315
    val tys = map (get_types D) (0 upto np - 1)
krauss@29125
   316
    fun index xs = (1 upto length xs) ~~ xs
krauss@29125
   317
    fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
krauss@29125
   318
    val ims = index (map index ms)
krauss@29125
   319
    val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
krauss@29125
   320
    fun print_call (k, c) =
krauss@29125
   321
      let
krauss@29125
   322
        val (_, p, _, q, _, _) = dest_call D c
krauss@29125
   323
        val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
krauss@29125
   324
                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
krauss@29125
   325
        val caller_ms = nth ms p
krauss@29125
   326
        val callee_ms = nth ms q
krauss@29125
   327
        val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
krauss@29125
   328
        fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
krauss@29125
   329
        val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
krauss@29125
   330
                                        " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
krauss@29125
   331
                                ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
krauss@29125
   332
      in
krauss@29125
   333
        true
krauss@29125
   334
      end
krauss@29125
   335
    fun list_call (k, c) =
krauss@29125
   336
      let
krauss@29125
   337
        val (_, p, _, q, _, _) = dest_call D c
krauss@29125
   338
        val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
krauss@29125
   339
                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
krauss@29125
   340
                                (Syntax.string_of_term ctxt c))
krauss@29125
   341
      in true end
krauss@29125
   342
    val _ = forall list_call ((1 upto length cs) ~~ cs)
krauss@29125
   343
    val _ = forall print_call ((1 upto length cs) ~~ cs)
krauss@29125
   344
  in
krauss@29125
   345
    all_tac
krauss@29125
   346
  end)
krauss@29125
   347
end
krauss@29125
   348
krauss@29125
   349
krauss@29125
   350
fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
krauss@29125
   351
  let
krauss@29877
   352
    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
krauss@29877
   353
    val orders' = if ms_configured then orders
krauss@29877
   354
                  else filter_out (curry op = MS) orders
krauss@29125
   355
    val gp = gen_probl D cs
krauss@29125
   356
(*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
krauss@29877
   357
    val certificate = generate_certificate use_tags orders' gp
krauss@29125
   358
(*    val _ = TRACE ("Certificate: " ^ makestring certificate)*)
krauss@29125
   359
krauss@29877
   360
  in
krauss@29125
   361
    case certificate
krauss@29125
   362
     of NONE => err_cont D i
krauss@29125
   363
      | SOME cert =>
krauss@29877
   364
          SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
krauss@29877
   365
          THEN (rtac @{thm wf_empty} i ORELSE cont D i)
krauss@29125
   366
  end)
krauss@29125
   367
krauss@29877
   368
fun gen_decomp_scnp_tac orders autom_tac ctxt err_cont =
krauss@29125
   369
  let
krauss@29125
   370
    open Termination
krauss@29125
   371
    val derive_diag = Descent.derive_diag ctxt autom_tac
krauss@29125
   372
    val derive_all = Descent.derive_all ctxt autom_tac
krauss@29125
   373
    val decompose = Decompose.decompose_tac ctxt autom_tac
krauss@29125
   374
    val scnp_no_tags = single_scnp_tac false orders ctxt
krauss@29125
   375
    val scnp_full = single_scnp_tac true orders ctxt
krauss@29125
   376
krauss@29125
   377
    fun first_round c e =
krauss@29125
   378
        derive_diag (REPEAT scnp_no_tags c e)
krauss@29125
   379
krauss@29125
   380
    val second_round =
krauss@29125
   381
        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
krauss@29125
   382
krauss@29125
   383
    val third_round =
krauss@29125
   384
        derive_all oo
krauss@29125
   385
        REPEAT (fn c => fn e =>
krauss@29125
   386
          scnp_full (decompose c c) e)
krauss@29125
   387
krauss@29125
   388
    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
krauss@29125
   389
krauss@29125
   390
    val strategy = Then (Then first_round second_round) third_round
krauss@29125
   391
krauss@29125
   392
  in
krauss@29125
   393
    TERMINATION ctxt (strategy err_cont err_cont)
krauss@29125
   394
  end
krauss@29125
   395
krauss@29877
   396
fun gen_sizechange_tac orders autom_tac ctxt err_cont =
krauss@29877
   397
  TRY (FundefCommon.apply_termination_rule ctxt 1)
wenzelm@30607
   398
  THEN TRY (Termination.wf_union_tac ctxt)
krauss@29877
   399
  THEN
krauss@29877
   400
   (rtac @{thm wf_empty} 1
krauss@29877
   401
    ORELSE gen_decomp_scnp_tac orders autom_tac ctxt err_cont 1)
krauss@29877
   402
krauss@29877
   403
fun sizechange_tac ctxt autom_tac =
krauss@29877
   404
  gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt (K (K all_tac))
krauss@29877
   405
krauss@29125
   406
fun decomp_scnp orders ctxt =
krauss@29125
   407
  let
wenzelm@31902
   408
    val extra_simps = FundefCommon.Termination_Simps.get ctxt
krauss@29125
   409
    val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
krauss@29125
   410
  in
wenzelm@30510
   411
    SIMPLE_METHOD
krauss@29877
   412
      (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
krauss@29125
   413
  end
krauss@29125
   414
krauss@29125
   415
krauss@29125
   416
(* Method setup *)
krauss@29125
   417
krauss@29125
   418
val orders =
wenzelm@31242
   419
  Scan.repeat1
krauss@29125
   420
    ((Args.$$$ "max" >> K MAX) ||
krauss@29125
   421
     (Args.$$$ "min" >> K MIN) ||
krauss@29125
   422
     (Args.$$$ "ms" >> K MS))
wenzelm@31242
   423
  || Scan.succeed [MAX, MS, MIN]
krauss@29125
   424
wenzelm@31242
   425
val setup = Method.setup @{binding sizechange}
wenzelm@31242
   426
  (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
wenzelm@31242
   427
  "termination prover with graph decomposition and the NP subset of size change termination"
krauss@29125
   428
krauss@29125
   429
end