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