src/HOL/Nominal/nominal_permeq.ML
author urbanc
Sat Apr 07 11:36:35 2007 +0200 (2007-04-07)
changeset 22610 c8b5133045f3
parent 22609 40ade470e319
child 22656 13302b2d0948
permissions -rw-r--r--
tuned slightly the previous commit
berghofe@19494
     1
(*  Title:      HOL/Nominal/nominal_permeq.ML
berghofe@19494
     2
    ID:         $Id$
urbanc@22418
     3
    Authors:    Christian Urban, Julien Narboux, 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
urbanc@22418
    36
  val perm_simp_meth : Method.src -> Proof.context -> Proof.method
urbanc@22418
    37
  val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
urbanc@22418
    38
  val perm_full_simp_meth : Method.src -> Proof.context -> Proof.method
urbanc@22418
    39
  val perm_full_simp_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
urbanc@22418
    42
  val finite_guess_meth : Method.src -> Proof.context -> Proof.method
urbanc@22418
    43
  val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
urbanc@22418
    44
  val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
urbanc@22418
    45
  val fresh_guess_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
urbanc@22418
    51
(* some lemmas needed below *)
berghofe@22274
    52
val finite_emptyI = thm "finite.emptyI";
urbanc@22418
    53
val finite_Un     = thm "finite_Un";
urbanc@22418
    54
val conj_absorb   = thm "conj_absorb";
urbanc@22418
    55
val not_false     = thm "not_False_eq_True"
urbanc@22418
    56
val perm_fun_def  = thm "Nominal.perm_fun_def"
urbanc@22418
    57
val perm_eq_app   = thm "Nominal.pt_fun_app_eq"
urbanc@22418
    58
val supports_def  = thm "Nominal.op supports_def";
urbanc@22418
    59
val fresh_def     = thm "Nominal.fresh_def";
urbanc@22418
    60
val fresh_prod    = thm "Nominal.fresh_prod";
urbanc@22418
    61
val fresh_unit    = thm "Nominal.fresh_unit";
urbanc@22418
    62
val supports_rule = thm "supports_finite";
urbanc@22418
    63
val supp_prod     = thm "supp_prod";
urbanc@22418
    64
val supp_unit     = thm "supp_unit";
urbanc@22418
    65
val pt_perm_compose_aux = thm "pt_perm_compose_aux";
urbanc@22418
    66
val cp1_aux             = thm "cp1_aux";
urbanc@22418
    67
val perm_aux_fold       = thm "perm_aux_fold"; 
urbanc@22418
    68
val supports_fresh_rule = thm "supports_fresh";
wenzelm@21669
    69
berghofe@19987
    70
(* pulls out dynamically a thm via the proof state *)
berghofe@19987
    71
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
urbanc@22418
    72
fun dynamic_thm  st name = PureThy.get_thm  (theory_of_thm st) (Name name);
urbanc@22418
    73
urbanc@18012
    74
urbanc@22418
    75
(* needed in the process of fully simplifying permutations *)
urbanc@22418
    76
val strong_congs = [thm "if_cong"]
urbanc@22418
    77
(* needed to avoid warnings about overwritten congs *)
urbanc@22418
    78
val weak_congs   = [thm "if_weak_cong"]
urbanc@22418
    79
narboux@22595
    80
(* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *)
narboux@22595
    81
narboux@22595
    82
fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
urbanc@22418
    83
urbanc@22418
    84
(* debugging *)
urbanc@22418
    85
fun DEBUG_tac (msg,tac) = 
urbanc@22418
    86
    CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
urbanc@22418
    87
fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
urbanc@22418
    88
urbanc@19477
    89
urbanc@22418
    90
(* simproc that deals with instances of permutations in front *)
urbanc@22418
    91
(* of applications; just adding this rule to the simplifier   *)
urbanc@22418
    92
(* would loop; it also needs careful tuning with the simproc  *)
urbanc@22418
    93
(* for functions to avoid further possibilities for looping   *)
urbanc@22418
    94
fun perm_simproc_app st sg ss redex =
urbanc@22418
    95
  let 
urbanc@22418
    96
    (* the "application" case is only applicable when the head of f is not a *)
urbanc@22418
    97
    (* constant or when (f x) is a permuation with two or more arguments     *)
urbanc@22418
    98
    fun applicable_app t = 
urbanc@22418
    99
          (case (strip_comb t) of
urbanc@22418
   100
	      (Const ("Nominal.perm",_),ts) => (length ts) >= 2
urbanc@22418
   101
            | (Const _,_) => false
urbanc@22418
   102
            | _ => true)
urbanc@22418
   103
  in
urbanc@22418
   104
    case redex of 
urbanc@19169
   105
        (* case pi o (f x) == (pi o f) (pi o x)          *)
berghofe@19494
   106
        (Const("Nominal.perm",
urbanc@19169
   107
          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
urbanc@22418
   108
            (if (applicable_app f) then
urbanc@22418
   109
              let
urbanc@22418
   110
                val name = Sign.base_name n
urbanc@22418
   111
                val at_inst     = dynamic_thm st ("at_"^name^"_inst")
urbanc@22418
   112
                val pt_inst     = dynamic_thm st ("pt_"^name^"_inst")  
urbanc@22418
   113
              in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
urbanc@22418
   114
            else NONE)
urbanc@22418
   115
      | _ => NONE
urbanc@22418
   116
  end
urbanc@19139
   117
urbanc@22418
   118
(* a simproc that deals with instances in front of functions  *)
urbanc@22418
   119
fun perm_simproc_fun st sg ss redex = 
urbanc@22418
   120
   let 
urbanc@22418
   121
     fun applicable_fun t =
urbanc@22418
   122
       (case (strip_comb t) of
urbanc@22418
   123
          (Abs _ ,[]) => true
urbanc@22418
   124
	| (Const ("Nominal.perm",_),_) => false
urbanc@22418
   125
        | (Const _, _) => true
urbanc@22418
   126
	| _ => false)
urbanc@22418
   127
   in
urbanc@22418
   128
     case redex of 
urbanc@22418
   129
       (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
urbanc@22418
   130
       (Const("Nominal.perm",_) $ pi $ f)  => 
urbanc@22418
   131
          (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
urbanc@22418
   132
      | _ => NONE
urbanc@22418
   133
   end
urbanc@19139
   134
urbanc@22418
   135
(* function for simplyfying permutations *)
narboux@22562
   136
fun perm_simp_gen dyn_thms f ss i = 
urbanc@22418
   137
    ("general simplification of permutations", fn st =>
urbanc@22418
   138
    let
urbanc@22418
   139
urbanc@22418
   140
       val perm_sp_fun = Simplifier.simproc (theory_of_thm st) "perm_simproc_fun" 
urbanc@22418
   141
	                 ["Nominal.perm pi x"] (perm_simproc_fun st);
urbanc@22418
   142
urbanc@22418
   143
       val perm_sp_app = Simplifier.simproc (theory_of_thm st) "perm_simproc_app" 
urbanc@22418
   144
	                 ["Nominal.perm pi x"] (perm_simproc_app st);
urbanc@22418
   145
narboux@22562
   146
       val ss' = ss addsimps ((List.concat (map (dynamic_thms st) dyn_thms))@(f st))
urbanc@22418
   147
                    delcongs weak_congs
urbanc@22418
   148
                    addcongs strong_congs
urbanc@22418
   149
                    addsimprocs [perm_sp_fun, perm_sp_app]
urbanc@19477
   150
    in
urbanc@22418
   151
      asm_full_simp_tac ss' i st
berghofe@19987
   152
    end);
urbanc@19477
   153
urbanc@22418
   154
(* general simplification of permutations and permutation that arose from eqvt-problems *)
urbanc@22610
   155
val perm_simp = 
urbanc@22610
   156
    let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
urbanc@22610
   157
    in 
urbanc@22610
   158
	perm_simp_gen simps (fn st => [])
urbanc@22610
   159
    end;
urbanc@22610
   160
urbanc@22610
   161
val eqvt_simp = 
urbanc@22610
   162
    let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
urbanc@22610
   163
	fun eqvts_thms st = NominalThmDecls.get_eqvt_thms (theory_of_thm st);
urbanc@22610
   164
    in 
urbanc@22610
   165
	perm_simp_gen simps eqvts_thms
urbanc@22610
   166
    end;
narboux@22562
   167
narboux@22562
   168
(* FIXME removes the name lookup for these theorems use an ml value instead *)
urbanc@22418
   169
urbanc@22418
   170
(* main simplification tactics for permutations *)
urbanc@22418
   171
(* FIXME: perm_simp_tac should simplify more permutations *)
urbanc@22418
   172
fun perm_simp_tac tactical ss i = DETERM (tactical (perm_simp ss i));
urbanc@22418
   173
fun eqvt_simp_tac tactical ss i = DETERM (tactical (eqvt_simp ss i)); 
urbanc@22418
   174
urbanc@22418
   175
urbanc@19477
   176
(* applies the perm_compose rule such that                             *)
urbanc@19477
   177
(*   pi o (pi' o lhs) = rhs                                            *)
urbanc@19477
   178
(* is transformed to                                                   *) 
urbanc@19477
   179
(*  (pi o pi') o (pi' o lhs) = rhs                                     *)
urbanc@19477
   180
(*                                                                     *)
urbanc@19477
   181
(* this rule would loop in the simplifier, so some trick is used with  *)
urbanc@19477
   182
(* generating perm_aux'es for the outermost permutation and then un-   *)
urbanc@19477
   183
(* folding the definition                                              *)
urbanc@19477
   184
fun perm_compose_tac ss i = 
urbanc@19477
   185
    let
urbanc@19477
   186
	fun perm_compose_simproc sg ss redex =
urbanc@19477
   187
	(case redex of
berghofe@19494
   188
           (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
berghofe@19494
   189
             [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
urbanc@19477
   190
               Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
urbanc@19477
   191
                pi2 $ t)) =>
urbanc@19350
   192
        let
urbanc@19350
   193
	    val tname' = Sign.base_name tname
urbanc@19477
   194
            val uname' = Sign.base_name uname
urbanc@19350
   195
        in
urbanc@19477
   196
            if pi1 <> pi2 then  (* only apply the composition rule in this case *)
urbanc@19477
   197
               if T = U then    
urbanc@19350
   198
                SOME (Drule.instantiate'
urbanc@19350
   199
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19350
   200
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19350
   201
		      (mk_meta_eq ([PureThy.get_thm sg (Name ("pt_"^tname'^"_inst")),
urbanc@19477
   202
	               PureThy.get_thm sg (Name ("at_"^tname'^"_inst"))] MRS pt_perm_compose_aux)))
urbanc@19477
   203
               else
urbanc@19477
   204
                SOME (Drule.instantiate'
urbanc@19477
   205
	              [SOME (ctyp_of sg (fastype_of t))]
urbanc@19477
   206
		      [SOME (cterm_of sg pi1), SOME (cterm_of sg pi2), SOME (cterm_of sg t)]
urbanc@19477
   207
		      (mk_meta_eq (PureThy.get_thm sg (Name ("cp_"^tname'^"_"^uname'^"_inst")) RS 
urbanc@19477
   208
                       cp1_aux)))
urbanc@19350
   209
            else NONE
urbanc@19350
   210
        end
urbanc@19350
   211
       | _ => NONE);
urbanc@19477
   212
	  
urbanc@19477
   213
      val perm_compose  =
urbanc@19350
   214
	Simplifier.simproc (the_context()) "perm_compose" 
berghofe@19494
   215
	["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc;
urbanc@19477
   216
urbanc@22418
   217
      val ss' = Simplifier.theory_context (the_context ()) empty_ss (* FIXME: get rid of the_context *)	  
urbanc@19477
   218
urbanc@18012
   219
    in
urbanc@19477
   220
	("analysing permutation compositions on the lhs",
urbanc@19477
   221
         EVERY [rtac trans i,
urbanc@19477
   222
                asm_full_simp_tac (ss' addsimprocs [perm_compose]) i,
urbanc@19477
   223
                asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i])
urbanc@18012
   224
    end
urbanc@18012
   225
urbanc@22418
   226
urbanc@18012
   227
(* applying Stefan's smart congruence tac *)
urbanc@18012
   228
fun apply_cong_tac i = 
urbanc@18012
   229
    ("application of congruence",
urbanc@19477
   230
     (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
berghofe@17870
   231
urbanc@22418
   232
urbanc@19477
   233
(* unfolds the definition of permutations     *)
urbanc@19477
   234
(* applied to functions such that             *)
urbanc@22418
   235
(*     pi o f = rhs                           *)  
urbanc@19477
   236
(* is transformed to                          *)
urbanc@22418
   237
(*     %x. pi o (f ((rev pi) o x)) = rhs      *)
urbanc@18012
   238
fun unfold_perm_fun_def_tac i = 
urbanc@18012
   239
    let
berghofe@19494
   240
	val perm_fun_def = thm "Nominal.perm_fun_def"
urbanc@18012
   241
    in
urbanc@18012
   242
	("unfolding of permutations on functions", 
urbanc@19477
   243
         rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i)
berghofe@17870
   244
    end
berghofe@17870
   245
urbanc@19477
   246
(* applies the ext-rule such that      *)
urbanc@19477
   247
(*                                     *)
urbanc@22418
   248
(*    f = g   goes to  /\x. f x = g x  *)
urbanc@19477
   249
fun ext_fun_tac i = ("extensionality expansion of functions", rtac ext i);
berghofe@17870
   250
berghofe@17870
   251
urbanc@22418
   252
(* perm_full_simp_tac is perm_simp plus additional tactics        *)
urbanc@19477
   253
(* to decide equation that come from support problems             *)
urbanc@19477
   254
(* since it contains looping rules the "recursion" - depth is set *)
urbanc@19477
   255
(* to 10 - this seems to be sufficient in most cases              *)
urbanc@19477
   256
fun perm_full_simp_tac tactical ss =
urbanc@19477
   257
  let fun perm_full_simp_tac_aux tactical ss n = 
urbanc@19477
   258
	  if n=0 then K all_tac
urbanc@19477
   259
	  else DETERM o 
urbanc@19477
   260
	       (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
urbanc@22418
   261
                       fn i => tactical (perm_simp ss i),
urbanc@19477
   262
		       fn i => tactical (perm_compose_tac ss i),
urbanc@19477
   263
		       fn i => tactical (apply_cong_tac i), 
urbanc@19477
   264
                       fn i => tactical (unfold_perm_fun_def_tac i),
urbanc@22418
   265
                       fn i => tactical (ext_fun_tac i)]
urbanc@19477
   266
		      THEN_ALL_NEW (TRY o (perm_full_simp_tac_aux tactical ss (n-1))))
urbanc@19477
   267
  in perm_full_simp_tac_aux tactical ss 10 end;
urbanc@19151
   268
urbanc@22418
   269
urbanc@22418
   270
(* tactic that tries to solve "supports"-goals; first it *)
urbanc@22418
   271
(* unfolds the support definition and strips off the     *)
urbanc@22418
   272
(* intros, then applies eqvt_simp_tac                    *)
urbanc@18012
   273
fun supports_tac tactical ss i =
urbanc@18012
   274
  let 
urbanc@22418
   275
     val simps        = [supports_def,symmetric fresh_def,fresh_prod]
berghofe@17870
   276
  in
urbanc@19477
   277
      EVERY [tactical ("unfolding of supports   ", simp_tac (HOL_basic_ss addsimps simps) i),
urbanc@19477
   278
             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
urbanc@19477
   279
             tactical ("geting rid of the imps  ", rtac impI i),
urbanc@19477
   280
             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
urbanc@22418
   281
             tactical ("applying eqvt_simp      ", eqvt_simp_tac tactical ss i )]
berghofe@17870
   282
  end;
berghofe@17870
   283
urbanc@19151
   284
urbanc@22418
   285
(* tactic that guesses the finite-support of a goal        *)
urbanc@22418
   286
(* it first collects all free variables and tries to show  *)
urbanc@22418
   287
(* that the support of these free variables (op supports)  *)
urbanc@22418
   288
(* the goal                                                *)
haftmann@20854
   289
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
haftmann@20854
   290
  | collect_vars i (v as Free _) vs = insert (op =) v vs
haftmann@20854
   291
  | collect_vars i (v as Var _) vs = insert (op =) v vs
urbanc@19151
   292
  | collect_vars i (Const _) vs = vs
urbanc@19151
   293
  | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
urbanc@19151
   294
  | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
urbanc@19151
   295
urbanc@19151
   296
fun finite_guess_tac tactical ss i st =
urbanc@19151
   297
    let val goal = List.nth(cprems_of st, i-1)
urbanc@19151
   298
    in
urbanc@19151
   299
      case Logic.strip_assums_concl (term_of goal) of
berghofe@22274
   300
          _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
urbanc@19151
   301
          let
wenzelm@22578
   302
            val cert = Thm.cterm_of (Thm.theory_of_thm st);
urbanc@19151
   303
            val ps = Logic.strip_params (term_of goal);
urbanc@19151
   304
            val Ts = rev (map snd ps);
urbanc@19151
   305
            val vs = collect_vars 0 x [];
haftmann@21078
   306
            val s = Library.foldr (fn (v, s) =>
urbanc@19151
   307
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
haftmann@21078
   308
              (vs, HOLogic.unit);
urbanc@19151
   309
            val s' = list_abs (ps,
berghofe@19494
   310
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
urbanc@19151
   311
            val supports_rule' = Thm.lift_rule goal supports_rule;
urbanc@19151
   312
            val _ $ (_ $ S $ _) =
urbanc@19151
   313
              Logic.strip_assums_concl (hd (prems_of supports_rule'));
urbanc@19151
   314
            val supports_rule'' = Drule.cterm_instantiate
urbanc@19151
   315
              [(cert (head_of S), cert s')] supports_rule'
urbanc@22418
   316
            val fin_supp = dynamic_thms st ("fin_supp")
urbanc@22418
   317
            val ss' = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
urbanc@19151
   318
          in
urbanc@19151
   319
            (tactical ("guessing of the right supports-set",
urbanc@19151
   320
                      EVERY [compose_tac (false, supports_rule'', 2) i,
berghofe@19987
   321
                             asm_full_simp_tac ss' (i+1),
urbanc@19151
   322
                             supports_tac tactical ss i])) st
urbanc@19151
   323
          end
urbanc@19151
   324
        | _ => Seq.empty
urbanc@19151
   325
    end
urbanc@19151
   326
    handle Subscript => Seq.empty
urbanc@19151
   327
narboux@22595
   328
urbanc@22418
   329
(* tactic that guesses whether an atom is fresh for an expression  *)
urbanc@22418
   330
(* it first collects all free variables and tries to show that the *) 
urbanc@22418
   331
(* support of these free variables (op supports) the goal          *)
berghofe@19857
   332
fun fresh_guess_tac tactical ss i st =
berghofe@19857
   333
    let 
berghofe@19857
   334
	val goal = List.nth(cprems_of st, i-1)
urbanc@22418
   335
        val fin_supp = dynamic_thms st ("fin_supp")
urbanc@22418
   336
        val fresh_atm = dynamic_thms st ("fresh_atm")
urbanc@22418
   337
	val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
urbanc@22418
   338
        val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
berghofe@19857
   339
    in
berghofe@19857
   340
      case Logic.strip_assums_concl (term_of goal) of
berghofe@19857
   341
          _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) => 
berghofe@19857
   342
          let
wenzelm@22578
   343
            val cert = Thm.cterm_of (Thm.theory_of_thm st);
berghofe@19857
   344
            val ps = Logic.strip_params (term_of goal);
berghofe@19857
   345
            val Ts = rev (map snd ps);
berghofe@19857
   346
            val vs = collect_vars 0 t [];
haftmann@21078
   347
            val s = Library.foldr (fn (v, s) =>
berghofe@19857
   348
                HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
haftmann@21078
   349
              (vs, HOLogic.unit);
berghofe@19857
   350
            val s' = list_abs (ps,
berghofe@19857
   351
              Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
berghofe@19857
   352
            val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
berghofe@19857
   353
            val _ $ (_ $ S $ _) =
berghofe@19857
   354
              Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
berghofe@19857
   355
            val supports_fresh_rule'' = Drule.cterm_instantiate
berghofe@19857
   356
              [(cert (head_of S), cert s')] supports_fresh_rule'
berghofe@19857
   357
          in
urbanc@22418
   358
            (tactical ("guessing of the right set that supports the goal", 
urbanc@22418
   359
                      (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
urbanc@19993
   360
                             asm_full_simp_tac ss1 (i+2),
urbanc@19993
   361
                             asm_full_simp_tac ss2 (i+1), 
urbanc@22418
   362
                             supports_tac tactical ss i]))) st
berghofe@19857
   363
          end
urbanc@22418
   364
          (* when a term-constructor contains more than one binder, it is useful    *) 
urbanc@22418
   365
          (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
urbanc@22418
   366
        | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",   
urbanc@22418
   367
                          (asm_full_simp_tac (HOL_ss addsimps [fresh_prod]@fresh_atm) i))) st
berghofe@19857
   368
    end
urbanc@22418
   369
    handle Subscript => Seq.empty;
urbanc@22418
   370
urbanc@22418
   371
(* setup so that the simpset is used which is active at the moment when the tactic is called *)
urbanc@22418
   372
fun local_simp_meth_setup tac =
urbanc@18046
   373
  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
urbanc@22418
   374
  (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
berghofe@17870
   375
narboux@22595
   376
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
narboux@22595
   377
urbanc@22418
   378
fun basic_simp_meth_setup tac =
urbanc@22418
   379
  Method.sectioned_args 
urbanc@22418
   380
   (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
urbanc@22418
   381
   (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
narboux@22595
   382
   (fn _ => Method.SIMPLE_METHOD' o (fn ss => SOLVEI (tac ss)) o local_simpset_of);
urbanc@22418
   383
berghofe@17870
   384
urbanc@22418
   385
val perm_simp_meth            = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
urbanc@22418
   386
val perm_simp_meth_debug      = local_simp_meth_setup (perm_simp_tac DEBUG_tac);
urbanc@22418
   387
val perm_full_simp_meth       = local_simp_meth_setup (perm_full_simp_tac NO_DEBUG_tac);
urbanc@22418
   388
val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac);
urbanc@22418
   389
val supports_meth             = local_simp_meth_setup (supports_tac NO_DEBUG_tac);
urbanc@22418
   390
val supports_meth_debug       = local_simp_meth_setup (supports_tac DEBUG_tac);
urbanc@22418
   391
val finite_guess_meth         = basic_simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
urbanc@22418
   392
val finite_guess_meth_debug   = basic_simp_meth_setup (finite_guess_tac DEBUG_tac);
urbanc@22418
   393
val fresh_guess_meth          = basic_simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
urbanc@22418
   394
val fresh_guess_meth_debug    = basic_simp_meth_setup (fresh_guess_tac DEBUG_tac);
urbanc@22418
   395
berghofe@19987
   396
val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
berghofe@19987
   397
val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;
berghofe@19987
   398
val supports_tac = supports_tac NO_DEBUG_tac;
berghofe@19987
   399
val finite_guess_tac = finite_guess_tac NO_DEBUG_tac;
berghofe@19987
   400
val fresh_guess_tac = fresh_guess_tac NO_DEBUG_tac;
berghofe@17870
   401
wenzelm@20289
   402
end