src/HOL/Nominal/nominal_permeq.ML
author haftmann
Wed Oct 04 14:17:38 2006 +0200 (2006-10-04)
changeset 20854 f9cf9e62d11c
parent 20431 eef4e9081bea
child 21078 101aefd61aac
permissions -rw-r--r--
insert replacing ins ins_int ins_string
berghofe@19494
     1
(*  Title:      HOL/Nominal/nominal_permeq.ML
berghofe@19494
     2
    ID:         $Id$
berghofe@19494
     3
    Author:     Christian Urban, TU Muenchen
berghofe@17870
     4
berghofe@19494
     5
Methods for simplifying permutations and
berghofe@19494
     6
for analysing equations involving permutations.
berghofe@19494
     7
*)
berghofe@17870
     8
urbanc@20431
     9
(*
urbanc@20431
    10
FIXMES:
urbanc@20431
    11
urbanc@20431
    12
 - allow the user to give an explicit set S in the
urbanc@20431
    13
   fresh_guess tactic which is then verified
urbanc@20431
    14
urbanc@20431
    15
 - the perm_compose tactic does not do an "outermost
urbanc@20431
    16
   rewriting" and can therefore not deal with goals
urbanc@20431
    17
   like
urbanc@20431
    18
urbanc@20431
    19
      [(a,b)] o pi1 o pi2 = ....
urbanc@20431
    20
urbanc@20431
    21
   rather it tries to permute pi1 over pi2, which 
urbanc@20431
    22
   results in a failure when used with the 
urbanc@20431
    23
   perm_(full)_simp tactics
urbanc@20431
    24
urbanc@20431
    25
*)
urbanc@20431
    26
urbanc@20431
    27
berghofe@19987
    28
signature NOMINAL_PERMEQ =
berghofe@19987
    29
sig
berghofe@19987
    30
  val perm_simp_tac : simpset -> int -> tactic
berghofe@19987
    31
  val perm_full_simp_tac : simpset -> int -> tactic
berghofe@19987
    32
  val supports_tac : simpset -> int -> tactic
berghofe@19987
    33
  val finite_guess_tac : simpset -> int -> tactic
berghofe@19987
    34
  val fresh_guess_tac : simpset -> int -> tactic
berghofe@17870
    35
wenzelm@20289
    36
  val perm_eq_meth : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    37
  val perm_eq_meth_debug : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    38
  val perm_full_eq_meth : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    39
  val perm_full_eq_meth_debug : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    40
  val supports_meth : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    41
  val supports_meth_debug : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    42
  val finite_gs_meth : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    43
  val finite_gs_meth_debug : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    44
  val fresh_gs_meth : Method.src -> Proof.context -> Proof.method
wenzelm@20289
    45
  val fresh_gs_meth_debug : Method.src -> Proof.context -> Proof.method
berghofe@19987
    46
end
berghofe@19987
    47
berghofe@19987
    48
structure NominalPermeq : NOMINAL_PERMEQ =
berghofe@19987
    49
struct
berghofe@19987
    50
berghofe@19987
    51
(* pulls out dynamically a thm via the proof state *)
berghofe@19987
    52
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
berghofe@19987
    53
fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
urbanc@18012
    54
urbanc@19477
    55
(* a tactic simplyfying permutations *)
berghofe@19494
    56
val perm_fun_def = thm "Nominal.perm_fun_def"
berghofe@19494
    57
val perm_eq_app = thm "Nominal.pt_fun_app_eq"
urbanc@19477
    58
berghofe@19987
    59
fun perm_eval_tac ss i = ("general simplification step", fn st =>
urbanc@18012
    60
    let
urbanc@19139
    61
        fun perm_eval_simproc sg ss redex =
urbanc@19169
    62
        let 
urbanc@19477
    63
	   (* the "application" case below is only applicable when the head   *)
urbanc@19169
    64
           (* of f is not a constant  or when it is a permuattion with two or *) 
urbanc@19169
    65
           (* more arguments                                                  *)
urbanc@19169
    66
           fun applicable t = 
urbanc@19169
    67
	       (case (strip_comb t) of
berghofe@19494
    68
		  (Const ("Nominal.perm",_),ts) => (length ts) >= 2
urbanc@19169
    69
		| (Const _,_) => false
urbanc@19169
    70
		| _ => true)
urbanc@19169
    71
urbanc@19169
    72
	in
urbanc@19139
    73
        (case redex of 
urbanc@19169
    74
        (* case pi o (f x) == (pi o f) (pi o x)          *)
urbanc@19169
    75
        (* special treatment according to the head of f  *)
berghofe@19494
    76
        (Const("Nominal.perm",
urbanc@19169
    77
          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
urbanc@19169
    78
	   (case (applicable f) of
urbanc@19169
    79
                false => NONE  
urbanc@19163
    80
              | _ => 
urbanc@19163
    81
		let
urbanc@19163
    82
		    val name = Sign.base_name n
berghofe@19987
    83
		    val at_inst     = dynamic_thm st ("at_"^name^"_inst")
berghofe@19987
    84
		    val pt_inst     = dynamic_thm st ("pt_"^name^"_inst")  
urbanc@19163
    85
		in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end)
urbanc@19139
    86
urbanc@19139
    87
        (* case pi o (%x. f x) == (%x. pi o (f ((rev pi)o x))) *)
berghofe@19494
    88
        | (Const("Nominal.perm",_) $ pi $ (Abs _)) => SOME (perm_fun_def)
urbanc@19139
    89
urbanc@19139
    90
        (* no redex otherwise *) 
urbanc@19169
    91
        | _ => NONE) end
urbanc@19139
    92
urbanc@19139
    93
	val perm_eval =
urbanc@19139
    94
	    Simplifier.simproc (Theory.sign_of (the_context ())) "perm_eval" 
berghofe@19494
    95
	    ["Nominal.perm pi x"] perm_eval_simproc;
urbanc@19139
    96
urbanc@19477
    97
      (* these lemmas are created dynamically according to the atom types *) 
berghofe@19987
    98
      val perm_swap        = dynamic_thms st "perm_swap"
berghofe@19987
    99
      val perm_fresh       = dynamic_thms st "perm_fresh_fresh"
berghofe@19987
   100
      val perm_bij         = dynamic_thms st "perm_bij"
berghofe@19987
   101
      val perm_pi_simp     = dynamic_thms st "perm_pi_simp"
urbanc@19477
   102
      val ss' = ss addsimps (perm_swap@perm_fresh@perm_bij@perm_pi_simp)
urbanc@19477
   103
    in
berghofe@19987
   104
      asm_full_simp_tac (ss' addsimprocs [perm_eval]) i st
berghofe@19987
   105
    end);
urbanc@19477
   106
urbanc@19477
   107
(* applies the perm_compose rule such that                             *)
urbanc@19477
   108
(*                                                                     *)
urbanc@19477
   109
(*   pi o (pi' o lhs) = rhs                                            *)
urbanc@19477
   110
(*                                                                     *)
urbanc@19477
   111
(* is transformed to                                                   *) 
urbanc@19477
   112
(*                                                                     *)
urbanc@19477
   113
(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
urbanc@19477
   114
(*                                                                     *)
urbanc@19477
   115
(* this rule would loop in the simplifier, so some trick is used with  *)
urbanc@19477
   116
(* generating perm_aux'es for the outermost permutation and then un-   *)
urbanc@19477
   117
(* folding the definition                                              *)
urbanc@19477
   118
val pt_perm_compose_aux = thm "pt_perm_compose_aux";
urbanc@19477
   119
val cp1_aux             = thm "cp1_aux";
urbanc@19477
   120
val perm_aux_fold       = thm "perm_aux_fold"; 
urbanc@19477
   121
urbanc@19477
   122
fun perm_compose_tac ss i = 
urbanc@19477
   123
    let
urbanc@19477
   124
	fun perm_compose_simproc sg ss redex =
urbanc@19477
   125
	(case redex of
berghofe@19494
   126
           (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
berghofe@19494
   127
             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
urbanc@19477
   128
               Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
urbanc@19477
   129
                pi2 $ t)) =>
urbanc@19350
   130
        let
urbanc@19350
   131
	    val tname' = Sign.base_name tname
urbanc@19477
   132
            val uname' = Sign.base_name uname
urbanc@19350
   133
        in
urbanc@19477
   134
            if pi1 <> pi2 then  (* only apply the composition rule in this case *)
urbanc@19477
   135
               if T = U then    
urbanc@19350
   136
                SOME (Drule.instantiate'
urbanc@19350
   137
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19350
   138
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19350
   139
		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
urbanc@19477
   140
	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
urbanc@19477
   141
               else
urbanc@19477
   142
                SOME (Drule.instantiate'
urbanc@19477
   143
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19477
   144
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19477
   145
		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
urbanc@19477
   146
                       cp1_aux)))
urbanc@19350
   147
            else NONE
urbanc@19350
   148
        end
urbanc@19350
   149
       | _ => NONE);
urbanc@19477
   150
	  
urbanc@19477
   151
      val perm_compose  =
urbanc@19350
   152
	Simplifier.simproc (the_context()) "perm_compose" 
berghofe@19494
   153
	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
urbanc@19477
   154
urbanc@19477
   155
      val ss' = Simplifier.theory_context (the_context ()) empty_ss	  
urbanc@19477
   156
urbanc@18012
   157
    in
urbanc@19477
   158
	("analysing permutation compositions on the lhs",
urbanc@19477
   159
         EVERY [rtac trans i,
urbanc@19477
   160
                asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
urbanc@19477
   161
                asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
urbanc@18012
   162
    end
urbanc@18012
   163
urbanc@18012
   164
(* applying Stefan's smart congruence tac *)
urbanc@18012
   165
fun apply_cong_tac i = 
urbanc@18012
   166
    ("application of congruence",
urbanc@19477
   167
     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
berghofe@17870
   168
urbanc@19477
   169
(* unfolds the definition of permutations     *)
urbanc@19477
   170
(* applied to functions such that             *)
urbanc@19477
   171
(*                                            *)
urbanc@19477
   172
(*   pi o f = rhs                             *)  
urbanc@19477
   173
(*                                            *)
urbanc@19477
   174
(* is transformed to                          *)
urbanc@19477
   175
(*                                            *)
urbanc@19477
   176
(*   %x. pi o (f ((rev pi) o x)) = rhs        *)
urbanc@18012
   177
fun unfold_perm_fun_def_tac i = 
urbanc@18012
   178
    let
berghofe@19494
   179
	val perm_fun_def = thm "Nominal.perm_fun_def"
urbanc@18012
   180
    in
urbanc@18012
   181
	("unfolding of permutations on functions", 
urbanc@19477
   182
         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
berghofe@17870
   183
    end
berghofe@17870
   184
urbanc@19477
   185
(* applies the ext-rule such that      *)
urbanc@19477
   186
(*                                     *)
urbanc@19477
   187
(*    f = g    goes to /\x. f x = g x  *)
urbanc@19477
   188
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
berghofe@17870
   189
urbanc@19477
   190
(* FIXME FIXME FIXME *)
urbanc@19477
   191
(* should be able to analyse pi o fresh_fun () = fresh_fun instances *) 
urbanc@19477
   192
fun fresh_fun_eqvt_tac i =
urbanc@19477
   193
    let
berghofe@19494
   194
	val fresh_fun_equiv = thm "Nominal.fresh_fun_equiv_ineq"
urbanc@19477
   195
    in
urbanc@19477
   196
	("fresh_fun equivariance", rtac (fresh_fun_equiv RS trans) i)
urbanc@19477
   197
    end		       
urbanc@19477
   198
		       
berghofe@17870
   199
(* debugging *)
berghofe@17870
   200
fun DEBUG_tac (msg,tac) = 
urbanc@19169
   201
    CHANGED (EVERY [tac, print_tac ("after "^msg)]); 
berghofe@17870
   202
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
berghofe@17870
   203
urbanc@19477
   204
(* Main Tactics *)
urbanc@18012
   205
fun perm_simp_tac tactical ss i = 
urbanc@19139
   206
    DETERM (tactical (perm_eval_tac ss i));
urbanc@19139
   207
urbanc@19477
   208
(* perm_full_simp_tac is perm_simp_tac plus additional tactics    *)
urbanc@19477
   209
(* to decide equation that come from support problems             *)
urbanc@19477
   210
(* since it contains looping rules the "recursion" - depth is set *)
urbanc@19477
   211
(* to 10 - this seems to be sufficient in most cases              *)
urbanc@19477
   212
fun perm_full_simp_tac tactical ss =
urbanc@19477
   213
  let fun perm_full_simp_tac_aux tactical ss n = 
urbanc@19477
   214
	  if n=0 then K all_tac
urbanc@19477
   215
	  else DETERM o 
urbanc@19477
   216
	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
urbanc@19477
   217
                       fn i => tactical (perm_eval_tac ss i),
urbanc@19477
   218
		       fn i => tactical (perm_compose_tac ss i),
urbanc@19477
   219
		       fn i => tactical (apply_cong_tac i), 
urbanc@19477
   220
                       fn i => tactical (unfold_perm_fun_def_tac i),
urbanc@19477
   221
                       fn i => tactical (ext_fun_tac i), 
urbanc@19477
   222
                       fn i => tactical (fresh_fun_eqvt_tac i)]
urbanc@19477
   223
		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
urbanc@19477
   224
  in perm_full_simp_tac_aux tactical ss 10 end;
urbanc@19151
   225
urbanc@19477
   226
(* tactic that first unfolds the support definition           *)
urbanc@19477
   227
(* and strips off the intros, then applies perm_full_simp_tac *)
urbanc@18012
   228
fun supports_tac tactical ss i =
urbanc@18012
   229
  let 
berghofe@19494
   230
      val supports_def = thm "Nominal.op supports_def";
berghofe@19494
   231
      val fresh_def    = thm "Nominal.fresh_def";
berghofe@19494
   232
      val fresh_prod   = thm "Nominal.fresh_prod";
urbanc@18012
   233
      val simps        = [supports_def,symmetric fresh_def,fresh_prod]
berghofe@17870
   234
  in
urbanc@19477
   235
      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
urbanc@19477
   236
             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
urbanc@19477
   237
             tactical ("geting rid of the imps  ", rtac impI i),
urbanc@19477
   238
             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
urbanc@19477
   239
             tactical ("applying perm_full_simp ", perm_full_simp_tac tactical ss i
urbanc@19477
   240
                                                   (*perm_simp_tac tactical ss i*))]
berghofe@17870
   241
  end;
berghofe@17870
   242
urbanc@19151
   243
urbanc@19477
   244
(* tactic that guesses the finite-support of a goal       *)
urbanc@19477
   245
(* it collects all free variables and tries to show       *)
urbanc@19477
   246
(* that the support of these free variables (op supports) *)
urbanc@19477
   247
(* the goal                                               *)
haftmann@20854
   248
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
haftmann@20854
   249
  | collect_vars i (v as Free _) vs = insert (op =) v vs
haftmann@20854
   250
  | collect_vars i (v as Var _) vs = insert (op =) v vs
urbanc@19151
   251
  | collect_vars i (Const _) vs = vs
urbanc@19151
   252
  | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
urbanc@19151
   253
  | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
urbanc@19151
   254
urbanc@19151
   255
val supports_rule = thm "supports_finite";
urbanc@19151
   256
berghofe@19987
   257
val supp_prod = thm "supp_prod";
berghofe@19987
   258
val supp_unit = thm "supp_unit";
berghofe@19987
   259
urbanc@19151
   260
fun finite_guess_tac tactical ss i st =
urbanc@19151
   261
    let val goal = List.nth(cprems_of st, i-1)
urbanc@19151
   262
    in
urbanc@19151
   263
      case Logic.strip_assums_concl (term_of goal) of
berghofe@19494
   264
          _ $ (Const ("op :", _) $ (Const ("Nominal.supp", T) $ x) $
urbanc@19151
   265
            Const ("Finite_Set.Finites", _)) =>
urbanc@19151
   266
          let
urbanc@19151
   267
            val cert = Thm.cterm_of (sign_of_thm st);
urbanc@19151
   268
            val ps = Logic.strip_params (term_of goal);
urbanc@19151
   269
            val Ts = rev (map snd ps);
urbanc@19151
   270
            val vs = collect_vars 0 x [];
urbanc@19151
   271
            val s = foldr (fn (v, s) =>
urbanc@19151
   272
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
urbanc@19151
   273
              HOLogic.unit vs;
urbanc@19151
   274
            val s' = list_abs (ps,
berghofe@19494
   275
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
urbanc@19151
   276
            val supports_rule' = Thm.lift_rule goal supports_rule;
urbanc@19151
   277
            val _ $ (_ $ S $ _) =
urbanc@19151
   278
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
urbanc@19151
   279
            val supports_rule'' = Drule.cterm_instantiate
urbanc@19151
   280
              [(cert (head_of S), cert s')] supports_rule'
berghofe@19987
   281
            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI]
urbanc@19151
   282
          in
urbanc@19151
   283
            (tactical ("guessing of the right supports-set",
urbanc@19151
   284
                      EVERY [compose_tac (false, supports_rule'', 2) i,
berghofe@19987
   285
                             asm_full_simp_tac ss' (i+1),
urbanc@19151
   286
                             supports_tac tactical ss i])) st
urbanc@19151
   287
          end
urbanc@19151
   288
        | _ => Seq.empty
urbanc@19151
   289
    end
urbanc@19151
   290
    handle Subscript => Seq.empty
urbanc@19151
   291
berghofe@19857
   292
val supports_fresh_rule = thm "supports_fresh";
urbanc@19993
   293
val fresh_def           = thm "Nominal.fresh_def";
urbanc@19993
   294
val fresh_prod          = thm "Nominal.fresh_prod";
urbanc@19993
   295
val fresh_unit          = thm "Nominal.fresh_unit";
berghofe@19857
   296
berghofe@19857
   297
fun fresh_guess_tac tactical ss i st =
berghofe@19857
   298
    let 
berghofe@19857
   299
	val goal = List.nth(cprems_of st, i-1)
berghofe@19857
   300
    in
berghofe@19857
   301
      case Logic.strip_assums_concl (term_of goal) of
berghofe@19857
   302
          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
berghofe@19857
   303
          let
berghofe@19857
   304
            val cert = Thm.cterm_of (sign_of_thm st);
berghofe@19857
   305
            val ps = Logic.strip_params (term_of goal);
berghofe@19857
   306
            val Ts = rev (map snd ps);
berghofe@19857
   307
            val vs = collect_vars 0 t [];
berghofe@19857
   308
            val s = foldr (fn (v, s) =>
berghofe@19857
   309
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
berghofe@19857
   310
              HOLogic.unit vs;
berghofe@19857
   311
            val s' = list_abs (ps,
berghofe@19857
   312
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
berghofe@19857
   313
            val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
berghofe@19857
   314
            val _ $ (_ $ S $ _) =
berghofe@19857
   315
              Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
berghofe@19857
   316
            val supports_fresh_rule'' = Drule.cterm_instantiate
berghofe@19857
   317
              [(cert (head_of S), cert s')] supports_fresh_rule'
urbanc@19993
   318
	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
urbanc@19993
   319
            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
urbanc@19993
   320
            (* FIXME sometimes these rewrite rules are already in the ss, *)
urbanc@19993
   321
            (* which produces a warning                                   *)
berghofe@19857
   322
          in
berghofe@19857
   323
            (tactical ("guessing of the right set that supports the goal",
urbanc@19858
   324
                      EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
urbanc@19993
   325
                             asm_full_simp_tac ss1 (i+2),
urbanc@19993
   326
                             asm_full_simp_tac ss2 (i+1), 
urbanc@19858
   327
                             supports_tac tactical ss i])) st
berghofe@19857
   328
          end
berghofe@19857
   329
        | _ => Seq.empty
berghofe@19857
   330
    end
berghofe@19857
   331
    handle Subscript => Seq.empty
berghofe@19857
   332
urbanc@18012
   333
fun simp_meth_setup tac =
urbanc@18046
   334
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
urbanc@18012
   335
  (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
berghofe@17870
   336
urbanc@19477
   337
val perm_eq_meth            = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
urbanc@19477
   338
val perm_eq_meth_debug      = simp_meth_setup (perm_simp_tac DEBUG_tac);
urbanc@19477
   339
val perm_full_eq_meth       = simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
urbanc@19477
   340
val perm_full_eq_meth_debug = simp_meth_setup (perm_full_simp_tac DEBUG_tac);
urbanc@19477
   341
val supports_meth           = simp_meth_setup (supports_tac NO_DEBUG_tac);
urbanc@19477
   342
val supports_meth_debug     = simp_meth_setup (supports_tac DEBUG_tac);
urbanc@19477
   343
val finite_gs_meth          = simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
urbanc@19477
   344
val finite_gs_meth_debug    = simp_meth_setup (finite_guess_tac DEBUG_tac);
berghofe@19857
   345
val fresh_gs_meth           = simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
berghofe@19857
   346
val fresh_gs_meth_debug     = simp_meth_setup (fresh_guess_tac DEBUG_tac);
berghofe@17870
   347
berghofe@19987
   348
(* FIXME: get rid of "debug" versions? *)
berghofe@19987
   349
val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
berghofe@19987
   350
val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;
berghofe@19987
   351
val supports_tac = supports_tac NO_DEBUG_tac;
berghofe@19987
   352
val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
berghofe@19987
   353
val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
berghofe@17870
   354
wenzelm@20289
   355
end