src/HOL/Nominal/nominal_permeq.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 62913 13252110a6fe
child 67710 cc2db3239932
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Nominal/nominal_permeq.ML
     2     Author:     Christian Urban, TU Muenchen
     3     Author:     Julien Narboux, TU Muenchen
     4 
     5 Methods for simplifying permutations and for analysing equations
     6 involving permutations.
     7 *)
     8 
     9 (*
    10 FIXMES:
    11 
    12  - allow the user to give an explicit set S in the
    13    fresh_guess tactic which is then verified
    14 
    15  - the perm_compose tactic does not do an "outermost
    16    rewriting" and can therefore not deal with goals
    17    like
    18 
    19       [(a,b)] o pi1 o pi2 = ....
    20 
    21    rather it tries to permute pi1 over pi2, which
    22    results in a failure when used with the
    23    perm_(full)_simp tactics
    24 
    25 *)
    26 
    27 
    28 signature NOMINAL_PERMEQ =
    29 sig
    30   val perm_simproc_fun : simproc
    31   val perm_simproc_app : simproc
    32 
    33   val perm_simp_tac : Proof.context -> int -> tactic
    34   val perm_extend_simp_tac : Proof.context -> int -> tactic
    35   val supports_tac : Proof.context -> int -> tactic
    36   val finite_guess_tac : Proof.context -> int -> tactic
    37   val fresh_guess_tac : Proof.context -> int -> tactic
    38 
    39   val perm_simp_meth : (Proof.context -> Proof.method) context_parser
    40   val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
    41   val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
    42   val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
    43   val supports_meth : (Proof.context -> Proof.method) context_parser
    44   val supports_meth_debug : (Proof.context -> Proof.method) context_parser
    45   val finite_guess_meth : (Proof.context -> Proof.method) context_parser
    46   val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
    47   val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
    48   val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
    49 end
    50 
    51 structure NominalPermeq : NOMINAL_PERMEQ =
    52 struct
    53 
    54 (* some lemmas needed below *)
    55 val finite_emptyI = @{thm "finite.emptyI"};
    56 val finite_Un     = @{thm "finite_Un"};
    57 val conj_absorb   = @{thm "conj_absorb"};
    58 val not_false     = @{thm "not_False_eq_True"}
    59 val perm_fun_def  = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
    60 val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
    61 val supports_def  = Simpdata.mk_eq @{thm "Nominal.supports_def"};
    62 val fresh_def     = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
    63 val fresh_prod    = @{thm "Nominal.fresh_prod"};
    64 val fresh_unit    = @{thm "Nominal.fresh_unit"};
    65 val supports_rule = @{thm "supports_finite"};
    66 val supp_prod     = @{thm "supp_prod"};
    67 val supp_unit     = @{thm "supp_unit"};
    68 val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"};
    69 val cp1_aux             = @{thm "cp1_aux"};
    70 val perm_aux_fold       = @{thm "perm_aux_fold"};
    71 val supports_fresh_rule = @{thm "supports_fresh"};
    72 
    73 (* needed in the process of fully simplifying permutations *)
    74 val strong_congs = [@{thm "if_cong"}]
    75 (* needed to avoid warnings about overwritten congs *)
    76 val weak_congs   = [@{thm "if_weak_cong"}]
    77 
    78 (* debugging *)
    79 fun DEBUG ctxt (msg,tac) =
    80     CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]);
    81 fun NO_DEBUG _ (_,tac) = CHANGED tac;
    82 
    83 
    84 (* simproc that deals with instances of permutations in front *)
    85 (* of applications; just adding this rule to the simplifier   *)
    86 (* would loop; it also needs careful tuning with the simproc  *)
    87 (* for functions to avoid further possibilities for looping   *)
    88 fun perm_simproc_app' ctxt ct =
    89   let
    90     val thy = Proof_Context.theory_of ctxt
    91     val redex = Thm.term_of ct
    92     (* the "application" case is only applicable when the head of f is not a *)
    93     (* constant or when (f x) is a permuation with two or more arguments     *)
    94     fun applicable_app t =
    95           (case (strip_comb t) of
    96               (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
    97             | (Const _,_) => false
    98             | _ => true)
    99   in
   100     case redex of
   101         (* case pi o (f x) == (pi o f) (pi o x)          *)
   102         (Const(@{const_name Nominal.perm},
   103           Type(@{type_name fun},
   104             [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
   105             (if (applicable_app f) then
   106               let
   107                 val name = Long_Name.base_name n
   108                 val at_inst = Global_Theory.get_thm thy ("at_" ^ name ^ "_inst")
   109                 val pt_inst = Global_Theory.get_thm thy ("pt_" ^ name ^ "_inst")
   110               in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
   111             else NONE)
   112       | _ => NONE
   113   end
   114 
   115 val perm_simproc_app =
   116   Simplifier.make_simproc @{context} "perm_simproc_app"
   117    {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app'}
   118 
   119 (* a simproc that deals with permutation instances in front of functions  *)
   120 fun perm_simproc_fun' ctxt ct =
   121    let
   122      val redex = Thm.term_of ct
   123      fun applicable_fun t =
   124        (case (strip_comb t) of
   125           (Abs _ ,[]) => true
   126         | (Const (@{const_name Nominal.perm},_),_) => false
   127         | (Const _, _) => true
   128         | _ => false)
   129    in
   130      case redex of
   131        (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
   132        (Const(@{const_name Nominal.perm},_) $ pi $ f)  =>
   133           (if applicable_fun f then SOME perm_fun_def else NONE)
   134       | _ => NONE
   135    end
   136 
   137 val perm_simproc_fun =
   138   Simplifier.make_simproc @{context} "perm_simproc_fun"
   139    {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun'}
   140 
   141 (* function for simplyfying permutations          *)
   142 (* stac contains the simplifiation tactic that is *)
   143 (* applied (see (no_asm) options below            *)
   144 fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i =
   145     ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
   146     let
   147        val ctxt' = ctxt
   148          addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
   149          addsimprocs [perm_simproc_fun, perm_simproc_app]
   150          |> fold Simplifier.del_cong weak_congs
   151          |> fold Simplifier.add_cong strong_congs
   152     in
   153       stac ctxt' i
   154     end) i st);
   155 
   156 (* general simplification of permutations and permutation that arose from eqvt-problems *)
   157 fun perm_simp stac ctxt =
   158     let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
   159     in
   160         perm_simp_gen stac simps [] ctxt
   161     end;
   162 
   163 fun eqvt_simp stac ctxt =
   164     let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
   165         val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt;
   166     in
   167         perm_simp_gen stac simps eqvts_thms ctxt
   168     end;
   169 
   170 
   171 (* main simplification tactics for permutations *)
   172 fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
   173 fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i));
   174 
   175 val perm_simp_tac_i          = perm_simp_tac_gen_i simp_tac
   176 val perm_asm_simp_tac_i      = perm_simp_tac_gen_i asm_simp_tac
   177 val perm_full_simp_tac_i     = perm_simp_tac_gen_i full_simp_tac
   178 val perm_asm_lr_simp_tac_i   = perm_simp_tac_gen_i asm_lr_simp_tac
   179 val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac
   180 val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac
   181 
   182 (* applies the perm_compose rule such that                             *)
   183 (*   pi o (pi' o lhs) = rhs                                            *)
   184 (* is transformed to                                                   *)
   185 (*  (pi o pi') o (pi' o lhs) = rhs                                     *)
   186 (*                                                                     *)
   187 (* this rule would loop in the simplifier, so some trick is used with  *)
   188 (* generating perm_aux'es for the outermost permutation and then un-   *)
   189 (* folding the definition                                              *)
   190 
   191 fun perm_compose_simproc' ctxt ct =
   192   (case Thm.term_of ct of
   193      (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
   194        [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm},
   195          Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
   196           pi2 $ t)) =>
   197     let
   198       val thy = Proof_Context.theory_of ctxt
   199       val tname' = Long_Name.base_name tname
   200       val uname' = Long_Name.base_name uname
   201     in
   202       if pi1 <> pi2 then  (* only apply the composition rule in this case *)
   203         if T = U then
   204           SOME (Thm.instantiate'
   205             [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   206             [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   207             (mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"),
   208              Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
   209         else
   210           SOME (Thm.instantiate'
   211             [SOME (Thm.global_ctyp_of thy (fastype_of t))]
   212             [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
   213             (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS
   214              cp1_aux)))
   215       else NONE
   216     end
   217   | _ => NONE);
   218 
   219 val perm_compose_simproc =
   220   Simplifier.make_simproc @{context} "perm_compose"
   221    {lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}],
   222     proc = K perm_compose_simproc'}
   223 
   224 fun perm_compose_tac ctxt i =
   225   ("analysing permutation compositions on the lhs",
   226    fn st => EVERY
   227      [resolve_tac ctxt [trans] i,
   228       asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
   229       asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
   230 
   231 fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
   232 
   233 
   234 (* unfolds the definition of permutations     *)
   235 (* applied to functions such that             *)
   236 (*     pi o f = rhs                           *)
   237 (* is transformed to                          *)
   238 (*     %x. pi o (f ((rev pi) o x)) = rhs      *)
   239 fun unfold_perm_fun_def_tac ctxt i =
   240     ("unfolding of permutations on functions",
   241       resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i)
   242 
   243 (* applies the ext-rule such that      *)
   244 (*                                     *)
   245 (*    f = g   goes to  /\x. f x = g x  *)
   246 fun ext_fun_tac ctxt i =
   247   ("extensionality expansion of functions", resolve_tac ctxt @{thms ext} i);
   248 
   249 
   250 (* perm_extend_simp_tac_i is perm_simp plus additional tactics        *)
   251 (* to decide equation that come from support problems             *)
   252 (* since it contains looping rules the "recursion" - depth is set *)
   253 (* to 10 - this seems to be sufficient in most cases              *)
   254 fun perm_extend_simp_tac_i tactical ctxt =
   255   let fun perm_extend_simp_tac_aux tactical ctxt n =
   256           if n=0 then K all_tac
   257           else DETERM o
   258                (FIRST'
   259                  [fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i),
   260                   fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
   261                   fn i => tactical ctxt (perm_compose_tac ctxt i),
   262                   fn i => tactical ctxt (apply_cong_tac ctxt i),
   263                   fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i),
   264                   fn i => tactical ctxt (ext_fun_tac ctxt i)]
   265                 THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
   266   in perm_extend_simp_tac_aux tactical ctxt 10 end;
   267 
   268 
   269 (* tactic that tries to solve "supports"-goals; first it *)
   270 (* unfolds the support definition and strips off the     *)
   271 (* intros, then applies eqvt_simp_tac                    *)
   272 fun supports_tac_i tactical ctxt i =
   273   let
   274      val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
   275   in
   276       EVERY [tactical ctxt ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
   277              tactical ctxt ("stripping of foralls    ", REPEAT_DETERM (resolve_tac ctxt [allI] i)),
   278              tactical ctxt ("geting rid of the imps  ", resolve_tac ctxt [impI] i),
   279              tactical ctxt ("eliminating conjuncts   ", REPEAT_DETERM (eresolve_tac ctxt [conjE] i)),
   280              tactical ctxt ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i)]
   281   end;
   282 
   283 
   284 (* tactic that guesses the finite-support of a goal        *)
   285 (* it first collects all free variables and tries to show  *)
   286 (* that the support of these free variables (op supports)  *)
   287 (* the goal                                                *)
   288 fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
   289   | collect_vars i (v as Free _) vs = insert (op =) v vs
   290   | collect_vars i (v as Var _) vs = insert (op =) v vs
   291   | collect_vars i (Const _) vs = vs
   292   | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
   293   | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
   294 
   295 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
   296 fun finite_guess_tac_i tactical ctxt i st =
   297     let val goal = nth (cprems_of st) (i - 1)
   298     in
   299       case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
   300           _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
   301           let
   302             val ps = Logic.strip_params (Thm.term_of goal);
   303             val Ts = rev (map snd ps);
   304             val vs = collect_vars 0 x [];
   305             val s = fold_rev (fn v => fn s =>
   306                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   307               vs HOLogic.unit;
   308             val s' = fold_rev Term.abs ps
   309               (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) -->
   310                 Term.range_type T) $ s);
   311             val supports_rule' = Thm.lift_rule goal supports_rule;
   312             val _ $ (_ $ S $ _) =
   313               Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
   314             val supports_rule'' =
   315               infer_instantiate ctxt
   316                 [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_rule';
   317             val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
   318             val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   319           in
   320             (tactical ctxt ("guessing of the right supports-set",
   321                       EVERY [compose_tac ctxt (false, supports_rule'', 2) i,
   322                              asm_full_simp_tac ctxt' (i+1),
   323                              supports_tac_i tactical ctxt i])) st
   324           end
   325         | _ => Seq.empty
   326     end
   327     handle General.Subscript => Seq.empty
   328 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
   329 
   330 
   331 (* tactic that guesses whether an atom is fresh for an expression  *)
   332 (* it first collects all free variables and tries to show that the *)
   333 (* support of these free variables (op supports) the goal          *)
   334 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
   335 fun fresh_guess_tac_i tactical ctxt i st =
   336     let
   337         val goal = nth (cprems_of st) (i - 1)
   338         val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
   339         val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
   340         val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
   341         val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
   342     in
   343       case Logic.strip_assums_concl (Thm.term_of goal) of
   344           _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) =>
   345           let
   346             val ps = Logic.strip_params (Thm.term_of goal);
   347             val Ts = rev (map snd ps);
   348             val vs = collect_vars 0 t [];
   349             val s = fold_rev (fn v => fn s =>
   350                 HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   351               vs HOLogic.unit;
   352             val s' =
   353               fold_rev Term.abs ps
   354                 (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
   355             val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
   356             val _ $ (_ $ S $ _) =
   357               Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
   358             val supports_fresh_rule'' =
   359               infer_instantiate ctxt
   360                 [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_fresh_rule';
   361           in
   362             (tactical ctxt ("guessing of the right set that supports the goal",
   363                       (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
   364                              asm_full_simp_tac ctxt1 (i+2),
   365                              asm_full_simp_tac ctxt2 (i+1),
   366                              supports_tac_i tactical ctxt i]))) st
   367           end
   368           (* when a term-constructor contains more than one binder, it is useful    *)
   369           (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
   370         | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",
   371                           (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
   372     end
   373     handle General.Subscript => Seq.empty;
   374 (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
   375 
   376 val eqvt_simp_tac        = eqvt_asm_full_simp_tac_i NO_DEBUG;
   377 
   378 val perm_simp_tac        = perm_asm_full_simp_tac_i NO_DEBUG;
   379 val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG;
   380 val supports_tac         = supports_tac_i NO_DEBUG;
   381 val finite_guess_tac     = finite_guess_tac_i NO_DEBUG;
   382 val fresh_guess_tac      = fresh_guess_tac_i NO_DEBUG;
   383 
   384 val dperm_simp_tac        = perm_asm_full_simp_tac_i DEBUG;
   385 val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG;
   386 val dsupports_tac         = supports_tac_i DEBUG;
   387 val dfinite_guess_tac     = finite_guess_tac_i DEBUG;
   388 val dfresh_guess_tac      = fresh_guess_tac_i DEBUG;
   389 
   390 (* Code opied from the Simplifer for setting up the perm_simp method   *)
   391 (* behaves nearly identical to the simp-method, for example can handle *)
   392 (* options like (no_asm) etc.                                          *)
   393 val no_asmN = "no_asm";
   394 val no_asm_useN = "no_asm_use";
   395 val no_asm_simpN = "no_asm_simp";
   396 val asm_lrN = "asm_lr";
   397 
   398 val perm_simp_options =
   399  (Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG) ||
   400   Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG) ||
   401   Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG) ||
   402   Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG) ||
   403   Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG));
   404 
   405 val perm_simp_meth =
   406   Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
   407   (fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac ctxt));
   408 
   409 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
   410 fun local_simp_meth_setup tac =
   411   Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   412   (K (SIMPLE_METHOD' o tac));
   413 
   414 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
   415 
   416 fun basic_simp_meth_setup debug tac =
   417   Scan.depend (fn context => Scan.succeed (Simplifier.map_ss (put_simpset HOL_basic_ss) context, ())) --
   418   Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   419   (K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac)));
   420 
   421 val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
   422 val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
   423 val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac;
   424 val supports_meth               = local_simp_meth_setup supports_tac;
   425 val supports_meth_debug         = local_simp_meth_setup dsupports_tac;
   426 
   427 val finite_guess_meth         = basic_simp_meth_setup false finite_guess_tac;
   428 val finite_guess_meth_debug   = basic_simp_meth_setup true  dfinite_guess_tac;
   429 val fresh_guess_meth          = basic_simp_meth_setup false fresh_guess_tac;
   430 val fresh_guess_meth_debug    = basic_simp_meth_setup true  dfresh_guess_tac;
   431 
   432 end