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