src/HOL/Library/rewrite.ML
author noschinl
Thu Apr 16 15:55:55 2015 +0200 (2015-04-16)
changeset 60088 0a064330a885
parent 60079 ef4fe30e9ef1
child 60102 820e8e704ba6
child 60108 d7fe3e0aca85
permissions -rw-r--r--
rewrite: use distinct names for unnamed abstractions
wenzelm@59975
     1
(*  Title:      HOL/Library/rewrite.ML
wenzelm@59975
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
noschinl@59739
     3
wenzelm@59975
     4
This is a rewrite method that supports subterm-selection based on patterns.
noschinl@59739
     5
wenzelm@59975
     6
The patterns accepted by rewrite are of the following form:
wenzelm@59975
     7
  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
wenzelm@59975
     8
  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
wenzelm@59975
     9
  <args>    ::= [<pattern>] ("to" <term>) <thms>
noschinl@59739
    10
wenzelm@59975
    11
This syntax was clearly inspired by Gonthier's and Tassi's language of
wenzelm@59975
    12
patterns but has diverged significantly during its development.
noschinl@59739
    13
wenzelm@59975
    14
We also allow introduction of identifiers for bound variables,
wenzelm@59975
    15
which can then be used to match arbitrary subterms inside abstractions.
noschinl@59739
    16
*)
noschinl@59739
    17
wenzelm@59975
    18
signature REWRITE =
wenzelm@59975
    19
sig
noschinl@60079
    20
  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
noschinl@60079
    21
noschinl@60079
    22
  val mk_hole: int -> typ -> term
noschinl@60079
    23
noschinl@60079
    24
  val rewrite: Proof.context
noschinl@60079
    25
    -> (term * (string * typ) list, string * typ option) pattern list * term option
noschinl@60079
    26
    -> thm list
noschinl@60079
    27
    -> cterm
noschinl@60079
    28
    -> thm Seq.seq
noschinl@60079
    29
noschinl@60079
    30
  val rewrite_tac: Proof.context
noschinl@60079
    31
    -> (term * (string * typ) list, string * typ option) pattern list * term option
noschinl@60079
    32
    -> thm list
noschinl@60079
    33
    -> int
noschinl@60079
    34
    -> tactic
noschinl@59739
    35
end
noschinl@59739
    36
wenzelm@59975
    37
structure Rewrite : REWRITE =
noschinl@59739
    38
struct
noschinl@59739
    39
noschinl@59739
    40
datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
noschinl@59739
    41
noschinl@59739
    42
fun map_term_pattern f (Term x) = f x
noschinl@59739
    43
  | map_term_pattern _ (For ss) = (For ss)
noschinl@59739
    44
  | map_term_pattern _ At = At
noschinl@59739
    45
  | map_term_pattern _ In = In
noschinl@59739
    46
  | map_term_pattern _ Concl = Concl
noschinl@59739
    47
  | map_term_pattern _ Asm = Asm
noschinl@59739
    48
noschinl@59739
    49
noschinl@59739
    50
exception NO_TO_MATCH
noschinl@59739
    51
noschinl@59739
    52
fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq
noschinl@59739
    53
noschinl@59739
    54
(* We rewrite subterms using rewrite conversions. These are conversions
noschinl@59739
    55
   that also take a context and a list of identifiers for bound variables
noschinl@59739
    56
   as parameters. *)
noschinl@59739
    57
type rewrite_conv = Proof.context -> (string * term) list -> conv
noschinl@59739
    58
noschinl@59739
    59
(* To apply such a rewrite conversion to a subterm of our goal, we use
noschinl@59739
    60
   subterm positions, which are just functions that map a rewrite conversion,
noschinl@59739
    61
   working on the top level, to a new rewrite conversion, working on
noschinl@59739
    62
   a specific subterm.
noschinl@59739
    63
noschinl@59739
    64
   During substitution, we are traversing the goal to find subterms that
noschinl@59739
    65
   we can rewrite. For each of these subterms, a subterm position is
noschinl@59739
    66
   created and later used in creating a conversion that we use to try and
noschinl@59739
    67
   rewrite this subterm. *)
noschinl@59739
    68
type subterm_position = rewrite_conv -> rewrite_conv
noschinl@59739
    69
noschinl@59739
    70
(* A focusterm represents a subterm. It is a tuple (t, p), consisting
noschinl@59739
    71
  of the subterm t itself and its subterm position p. *)
noschinl@60088
    72
type focusterm = (Type.tyenv * Proof.context) * term * subterm_position
noschinl@59739
    73
noschinl@59739
    74
val dummyN = Name.internal "__dummy"
noschinl@59739
    75
val holeN = Name.internal "_hole"
noschinl@59739
    76
noschinl@59739
    77
fun prep_meta_eq ctxt =
noschinl@59739
    78
  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
noschinl@59739
    79
noschinl@59739
    80
noschinl@59739
    81
(* rewrite conversions *)
noschinl@59739
    82
noschinl@59739
    83
fun abs_rewr_cconv ident : subterm_position =
noschinl@59739
    84
  let
noschinl@59739
    85
    fun add_ident NONE _ l = l
noschinl@59739
    86
      | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
wenzelm@59975
    87
    fun inner rewr ctxt idents =
wenzelm@59975
    88
      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
noschinl@59739
    89
  in inner end
wenzelm@59975
    90
noschinl@59739
    91
val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
noschinl@59739
    92
val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
noschinl@60050
    93
val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
noschinl@60054
    94
val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr
noschinl@59739
    95
noschinl@59739
    96
noschinl@59739
    97
(* focus terms *)
noschinl@59739
    98
noschinl@60088
    99
fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) =
noschinl@59739
   100
  case try (fastype_of #> dest_funT) u of
noschinl@59739
   101
    NONE => raise TERM ("ft_abs: no function type", [u])
noschinl@59739
   102
  | SOME (U, _) =>
wenzelm@59975
   103
      let
wenzelm@59975
   104
        val tyenv' =
wenzelm@59975
   105
          if T = dummyT then tyenv
wenzelm@59975
   106
          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
noschinl@60088
   107
        val (s', u_ctxt') =
noschinl@60088
   108
          case s of
noschinl@60088
   109
           NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt
noschinl@60088
   110
          | SOME s => (s, u_ctxt)
noschinl@60088
   111
        val x = Free (s', Envir.norm_type tyenv' T)
wenzelm@59975
   112
        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
wenzelm@59975
   113
        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
wenzelm@59975
   114
        val (u', pos') =
wenzelm@59975
   115
          case u of
wenzelm@59975
   116
            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
wenzelm@59975
   117
          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
noschinl@60088
   118
      in ((tyenv', u_ctxt'), u', pos') end
wenzelm@59975
   119
      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
noschinl@59739
   120
noschinl@59739
   121
fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
noschinl@59739
   122
  | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
noschinl@59739
   123
  | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
noschinl@59739
   124
noschinl@60050
   125
local
noschinl@60050
   126
noschinl@60050
   127
fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv)
noschinl@60050
   128
  | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft
noschinl@60050
   129
  | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t])
noschinl@60050
   130
noschinl@60050
   131
in
noschinl@60050
   132
noschinl@60050
   133
val ft_arg = ft_arg_gen arg_rewr_cconv
noschinl@60050
   134
val ft_imp = ft_arg_gen imp_rewr_cconv
noschinl@60050
   135
noschinl@60050
   136
end
noschinl@59739
   137
noschinl@59739
   138
(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
noschinl@59739
   139
fun ft_params ctxt (ft as (_, t, _) : focusterm) =
noschinl@59739
   140
  case t of
noschinl@59739
   141
    Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) =>
noschinl@59739
   142
      (ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft
noschinl@59739
   143
  | Const (@{const_name "Pure.all"}, _) =>
noschinl@59739
   144
      (ft_params ctxt o ft_arg ctxt) ft
noschinl@59739
   145
  | _ => ft
noschinl@59739
   146
noschinl@59739
   147
fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) =
noschinl@59739
   148
    let
noschinl@59739
   149
      val def_U = T |> dest_funT |> fst |> dest_funT |> fst
noschinl@59739
   150
      val ident' = apsnd (the_default (def_U)) ident
noschinl@59739
   151
    in (ft_abs ctxt ident' o ft_arg ctxt) ft end
noschinl@59739
   152
  | ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t])
noschinl@59739
   153
noschinl@59739
   154
fun ft_for ctxt idents (ft as (_, t, _) : focusterm) =
noschinl@59739
   155
  let
noschinl@59739
   156
    fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) =
noschinl@59739
   157
        let
noschinl@59739
   158
         val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
noschinl@59739
   159
        in
noschinl@59739
   160
          case rev_idents' of
noschinl@59739
   161
            [] => ([], desc o ft_all ctxt (NONE, NONE))
noschinl@59739
   162
          | (x :: xs) => (xs , desc o ft_all ctxt x)
noschinl@59739
   163
        end
noschinl@59739
   164
      | f rev_idents _ = (rev_idents, I)
wenzelm@59975
   165
  in
wenzelm@59975
   166
    case f (rev idents) t of
noschinl@59739
   167
      ([], ft') => SOME (ft' ft)
noschinl@59739
   168
    | _ => NONE
noschinl@59739
   169
  end
noschinl@59739
   170
noschinl@59739
   171
fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
noschinl@59739
   172
  case t of
noschinl@60050
   173
    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
noschinl@59739
   174
  | _ => ft
noschinl@59739
   175
noschinl@60054
   176
fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) =
noschinl@60054
   177
      (tyenv, l, pos o with_prems_rewr_cconv)
noschinl@60054
   178
  | ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t])
noschinl@59739
   179
noschinl@59739
   180
fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
wenzelm@59970
   181
  if Object_Logic.is_judgment ctxt t
noschinl@59739
   182
  then ft_arg ctxt ft
noschinl@59739
   183
  else ft
noschinl@59739
   184
noschinl@60055
   185
(* Find all subterms that might be a valid point to apply a rule. *)
noschinl@60055
   186
fun valid_match_points ctxt (ft : focusterm) =
noschinl@59739
   187
  let
noschinl@60055
   188
    fun descend (_, _ $ _, _) = [ft_fun ctxt, ft_arg ctxt]
noschinl@60055
   189
      | descend (_, Abs (_, T, _), _) = [ft_abs ctxt (NONE, T)]
noschinl@60055
   190
      | descend _ = []
noschinl@60055
   191
    fun subseq ft =
noschinl@60055
   192
      descend ft |> Seq.of_list |> Seq.maps (fn f => ft |> f |> valid_match_points ctxt)
noschinl@59739
   193
    fun is_valid (l $ _) = is_valid l
noschinl@59739
   194
      | is_valid (Abs (_, _, a)) = is_valid a
noschinl@59739
   195
      | is_valid (Var _) = false
noschinl@59739
   196
      | is_valid (Bound _) = false
noschinl@59739
   197
      | is_valid _ = true
noschinl@59739
   198
  in
noschinl@60055
   199
    Seq.make (fn () => SOME (ft, subseq ft))
noschinl@60055
   200
    |> Seq.filter (#2 #> is_valid)
noschinl@59739
   201
  end
noschinl@59739
   202
noschinl@60079
   203
fun mk_hole i T = Var ((holeN, i), T)
noschinl@60079
   204
noschinl@59739
   205
fun is_hole (Var ((name, _), _)) = (name = holeN)
noschinl@59739
   206
  | is_hole _ = false
noschinl@59739
   207
noschinl@59739
   208
fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true
noschinl@59739
   209
  | is_hole_const _ = false
noschinl@59739
   210
noschinl@59739
   211
val hole_syntax =
noschinl@59739
   212
  let
noschinl@59739
   213
    (* Modified variant of Term.replace_hole *)
noschinl@59739
   214
    fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i =
noschinl@60079
   215
          (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
noschinl@59739
   216
      | replace_hole Ts (Abs (x, T, t)) i =
noschinl@59739
   217
          let val (t', i') = replace_hole (T :: Ts) t i
noschinl@59739
   218
          in (Abs (x, T, t'), i') end
noschinl@59739
   219
      | replace_hole Ts (t $ u) i =
noschinl@59739
   220
          let
noschinl@59739
   221
            val (t', i') = replace_hole Ts t i
noschinl@59739
   222
            val (u', i'') = replace_hole Ts u i'
noschinl@59739
   223
          in (t' $ u', i'') end
noschinl@59739
   224
      | replace_hole _ a i = (a, i)
noschinl@59739
   225
    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
noschinl@59739
   226
  in
noschinl@59739
   227
    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
noschinl@59739
   228
    #> Proof_Context.set_mode Proof_Context.mode_pattern
noschinl@59739
   229
  end
noschinl@59739
   230
noschinl@59739
   231
(* Find a subterm of the focusterm matching the pattern. *)
noschinl@59739
   232
fun find_matches ctxt pattern_list =
noschinl@59739
   233
  let
noschinl@59739
   234
    fun move_term ctxt (t, off) (ft : focusterm) =
noschinl@59739
   235
      let
noschinl@59739
   236
        val thy = Proof_Context.theory_of ctxt
noschinl@59739
   237
noschinl@59739
   238
        val eta_expands =
noschinl@59739
   239
          let val (_, ts) = strip_comb t
noschinl@59739
   240
          in map fastype_of (snd (take_suffix is_Var ts)) end
noschinl@59739
   241
noschinl@60088
   242
        fun do_match ((tyenv, u_ctxt), u, pos) =
noschinl@60088
   243
          case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of
noschinl@59739
   244
            NONE => NONE
noschinl@60088
   245
          | SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos))
noschinl@59739
   246
noschinl@59739
   247
        fun match_argT T u =
noschinl@59739
   248
          let val (U, _) = dest_funT (fastype_of u)
noschinl@59739
   249
          in try (Sign.typ_match thy (T,U)) end
noschinl@59739
   250
          handle TYPE _ => K NONE
noschinl@59739
   251
noschinl@59739
   252
        fun desc [] ft = do_match ft
noschinl@60088
   253
          | desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) =
noschinl@59739
   254
            case do_match ft of
noschinl@59739
   255
              NONE =>
noschinl@59739
   256
                (case match_argT T u tyenv of
noschinl@59739
   257
                  NONE => NONE
noschinl@60088
   258
                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos)))
noschinl@59739
   259
            | SOME ft => SOME ft
noschinl@59739
   260
      in desc eta_expands ft end
noschinl@59739
   261
noschinl@60052
   262
    fun move_assms ctxt (ft: focusterm) =
noschinl@60052
   263
      let
noschinl@60052
   264
        fun f () = case try (ft_assm ctxt) ft of
noschinl@60052
   265
            NONE => NONE
noschinl@60052
   266
          | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
noschinl@60052
   267
      in Seq.make f end
noschinl@59739
   268
noschinl@59739
   269
    fun apply_pat At = Seq.map (ft_judgment ctxt)
noschinl@59739
   270
      | apply_pat In = Seq.maps (valid_match_points ctxt)
noschinl@60052
   271
      | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
noschinl@59739
   272
      | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
noschinl@59739
   273
      | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
noschinl@59739
   274
      | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
noschinl@59739
   275
noschinl@59739
   276
    fun apply_pats ft = ft
noschinl@59739
   277
      |> Seq.single
noschinl@59739
   278
      |> fold apply_pat pattern_list
noschinl@59739
   279
  in
noschinl@59739
   280
    apply_pats
noschinl@59739
   281
  end
noschinl@59739
   282
noschinl@59739
   283
fun instantiate_normalize_env ctxt env thm =
noschinl@59739
   284
  let
noschinl@59739
   285
    fun certs f = map (apply2 (f ctxt))
noschinl@59739
   286
    val prop = Thm.prop_of thm
noschinl@59739
   287
    val norm_type = Envir.norm_type o Envir.type_env
noschinl@59739
   288
    val insts = Term.add_vars prop []
noschinl@59739
   289
      |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
noschinl@59739
   290
      |> certs Thm.cterm_of
noschinl@59739
   291
    val tyinsts = Term.add_tvars prop []
noschinl@59739
   292
      |> map (fn x => (TVar x, norm_type env (TVar x)))
noschinl@59739
   293
      |> certs Thm.ctyp_of
noschinl@59739
   294
  in Drule.instantiate_normalize (tyinsts, insts) thm end
noschinl@59739
   295
noschinl@59739
   296
fun unify_with_rhs context to env thm =
noschinl@59739
   297
  let
noschinl@59739
   298
    val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
noschinl@59739
   299
    val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
noschinl@59739
   300
      handle Pattern.Unif => raise NO_TO_MATCH
noschinl@59739
   301
  in env' end
noschinl@59739
   302
noschinl@59739
   303
fun inst_thm_to _ (NONE, _) thm = thm
noschinl@59739
   304
  | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
noschinl@59739
   305
      instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
noschinl@59739
   306
noschinl@59739
   307
fun inst_thm ctxt idents (to, tyenv) thm =
noschinl@59739
   308
  let
noschinl@59739
   309
    (* Replace any identifiers with their corresponding bound variables. *)
noschinl@59739
   310
    val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
noschinl@59739
   311
    val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
noschinl@59739
   312
    val replace_idents =
noschinl@59739
   313
      let
noschinl@59739
   314
        fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
noschinl@59739
   315
          | subst _ t = t
noschinl@59739
   316
      in Term.map_aterms (subst idents) end
noschinl@59739
   317
noschinl@60051
   318
    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
noschinl@59739
   319
    val thm' = Thm.incr_indexes (maxidx + 1) thm
noschinl@59739
   320
  in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end
noschinl@59739
   321
  handle NO_TO_MATCH => NONE
noschinl@59739
   322
noschinl@60079
   323
local
noschinl@60079
   324
noschinl@60079
   325
fun rewrite_raw ctxt (pattern, to) thms ct =
noschinl@59739
   326
  let
noschinl@60079
   327
    fun interpret_term_patterns ctxt =
noschinl@60079
   328
      let
noschinl@60079
   329
    
noschinl@60079
   330
        fun descend_hole fixes (Abs (_, _, t)) =
noschinl@60079
   331
            (case descend_hole fixes t of
noschinl@60079
   332
              NONE => NONE
noschinl@60079
   333
            | SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix))
noschinl@60079
   334
            | SOME ([], _) => raise Match (* XXX -- check phases modified binding *))
noschinl@60079
   335
          | descend_hole fixes (t as l $ r) =
noschinl@60079
   336
            let val (f, _) = strip_comb t
noschinl@60079
   337
            in
noschinl@60079
   338
              if is_hole f
noschinl@60079
   339
              then SOME (fixes, I)
noschinl@60079
   340
              else
noschinl@60079
   341
                (case descend_hole fixes l of
noschinl@60079
   342
                  SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt)
noschinl@60079
   343
                | NONE =>
noschinl@60079
   344
                  (case descend_hole fixes r of
noschinl@60079
   345
                    SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt)
noschinl@60079
   346
                  | NONE => NONE))
noschinl@60079
   347
            end
noschinl@60079
   348
          | descend_hole fixes t =
noschinl@60079
   349
            if is_hole t then SOME (fixes, I) else NONE
noschinl@60079
   350
    
noschinl@60079
   351
        fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t)
noschinl@60079
   352
    
noschinl@60079
   353
      in map (map_term_pattern f) end
noschinl@60079
   354
noschinl@60079
   355
    val pattern' = interpret_term_patterns ctxt pattern
noschinl@60088
   356
    val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I)
noschinl@60079
   357
noschinl@60079
   358
    val thms' = maps (prep_meta_eq ctxt) thms
noschinl@59739
   359
noschinl@59739
   360
    fun rewrite_conv insty ctxt bounds =
noschinl@60079
   361
      CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) thms')
noschinl@59739
   362
noschinl@59739
   363
    fun distinct_prems th =
noschinl@59739
   364
      case Seq.pull (distinct_subgoals_tac th) of
noschinl@59739
   365
        NONE => th
noschinl@59739
   366
      | SOME (th', _) => th'
noschinl@59739
   367
noschinl@60088
   368
    fun conv (((tyenv, _), _, position) : focusterm) =
noschinl@60079
   369
      distinct_prems o position (rewrite_conv (to, tyenv)) ctxt []
noschinl@60079
   370
noschinl@60079
   371
  in Seq.map (fn ft => conv ft) matches end
noschinl@60079
   372
noschinl@60079
   373
in
noschinl@60079
   374
noschinl@60079
   375
fun rewrite ctxt pat thms ct =
noschinl@60079
   376
  rewrite_raw ctxt pat thms ct |> Seq.map_filter (fn cv => try cv ct)
noschinl@59739
   377
noschinl@60079
   378
fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
noschinl@59739
   379
  let
noschinl@60079
   380
    val export = case pat_ctxt of
noschinl@60079
   381
        NONE => I
noschinl@60079
   382
      | SOME inner => singleton (Proof_Context.export inner ctxt)
noschinl@60079
   383
    val tac = CSUBGOAL (fn (ct, i) =>
noschinl@60079
   384
      rewrite_raw ctxt pat thms ct
noschinl@60079
   385
      |> Seq.map (fn cv => CCONVERSION (export o cv) i)
noschinl@60079
   386
      |> SEQ_CONCAT)
noschinl@59739
   387
  in tac end
noschinl@59739
   388
noschinl@60079
   389
fun rewrite_tac ctxt pat = rewrite_export_tac ctxt (pat, NONE)
noschinl@60079
   390
noschinl@60079
   391
end
noschinl@60079
   392
wenzelm@59975
   393
val _ =
wenzelm@59975
   394
  Theory.setup
noschinl@59739
   395
  let
noschinl@59739
   396
    fun mk_fix s = (Binding.name s, NONE, NoSyn)
noschinl@59739
   397
noschinl@59739
   398
    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
noschinl@59739
   399
      let
noschinl@59739
   400
        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
noschinl@59739
   401
        val atom =  (Args.$$$ "asm" >> K Asm) ||
noschinl@59739
   402
          (Args.$$$ "concl" >> K Concl) ||
noschinl@59739
   403
          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
noschinl@59739
   404
          (Parse.term >> Term)
noschinl@59739
   405
        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
noschinl@59739
   406
noschinl@59739
   407
        fun append_default [] = [Concl, In]
noschinl@59739
   408
          | append_default (ps as Term _ :: _) = Concl :: In :: ps
noschinl@59739
   409
          | append_default ps = ps
noschinl@59739
   410
noschinl@59739
   411
      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
noschinl@59739
   412
wenzelm@59975
   413
    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
noschinl@59739
   414
      let
noschinl@59739
   415
        val (r, toks') = scan toks
wenzelm@59975
   416
        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
wenzelm@59975
   417
      in (r', (context', toks' : Token.T list)) end
noschinl@59739
   418
noschinl@59739
   419
    fun read_fixes fixes ctxt =
noschinl@59739
   420
      let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
noschinl@59739
   421
      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
noschinl@59739
   422
noschinl@59739
   423
    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
noschinl@59739
   424
      let
noschinl@59739
   425
        fun add_constrs ctxt n (Abs (x, T, t)) =
noschinl@59739
   426
            let
noschinl@59739
   427
              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
noschinl@59739
   428
            in
noschinl@59739
   429
              (case add_constrs ctxt' (n+1) t of
noschinl@59739
   430
                NONE => NONE
noschinl@59739
   431
              | SOME ((ctxt'', n', xs), t') =>
noschinl@59739
   432
                  let
noschinl@59739
   433
                    val U = Type_Infer.mk_param n []
noschinl@59739
   434
                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
noschinl@59739
   435
                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
noschinl@59739
   436
            end
noschinl@59739
   437
          | add_constrs ctxt n (l $ r) =
noschinl@59739
   438
            (case add_constrs ctxt n l of
noschinl@59739
   439
              SOME (c, l') => SOME (c, l' $ r)
noschinl@59739
   440
            | NONE =>
noschinl@59739
   441
              (case add_constrs ctxt n r of
noschinl@59739
   442
                SOME (c, r') => SOME (c, l $ r')
noschinl@59739
   443
              | NONE => NONE))
noschinl@59739
   444
          | add_constrs ctxt n t =
noschinl@59739
   445
            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
noschinl@59739
   446
noschinl@59739
   447
        fun prep (Term s) (n, ctxt) =
noschinl@59739
   448
            let
noschinl@59739
   449
              val t = Syntax.parse_term ctxt s
noschinl@59739
   450
              val ((ctxt', n', bs), t') =
noschinl@59739
   451
                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
noschinl@59739
   452
            in (Term (t', bs), (n', ctxt')) end
noschinl@59739
   453
          | prep (For ss) (n, ctxt) =
noschinl@59739
   454
            let val (ns, ctxt') = read_fixes ss ctxt
noschinl@59739
   455
            in (For ns, (n, ctxt')) end
noschinl@59739
   456
          | prep At (n,ctxt) = (At, (n, ctxt))
noschinl@59739
   457
          | prep In (n,ctxt) = (In, (n, ctxt))
noschinl@59739
   458
          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
noschinl@59739
   459
          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
noschinl@59739
   460
noschinl@59739
   461
        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
noschinl@59739
   462
noschinl@59739
   463
      in (xs, ctxt') end
noschinl@59739
   464
noschinl@59739
   465
    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
noschinl@59739
   466
      let
noschinl@59739
   467
noschinl@59739
   468
        fun check_terms ctxt ps to =
noschinl@59739
   469
          let
noschinl@59739
   470
            fun safe_chop (0: int) xs = ([], xs)
noschinl@59739
   471
              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
noschinl@59739
   472
              | safe_chop _ _ = raise Match
noschinl@59739
   473
noschinl@59739
   474
            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
noschinl@59739
   475
                let val (cs', ts') = safe_chop (length cs) ts
noschinl@59739
   476
                in (Term (t, map dest_Free cs'), ts') end
noschinl@59739
   477
              | reinsert_pat _ (Term _) [] = raise Match
noschinl@59739
   478
              | reinsert_pat ctxt (For ss) ts =
noschinl@59739
   479
                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
noschinl@59739
   480
                in (For fixes, ts) end
noschinl@59739
   481
              | reinsert_pat _ At ts = (At, ts)
noschinl@59739
   482
              | reinsert_pat _ In ts = (In, ts)
noschinl@59739
   483
              | reinsert_pat _ Concl ts = (Concl, ts)
noschinl@59739
   484
              | reinsert_pat _ Asm ts = (Asm, ts)
noschinl@59739
   485
noschinl@59739
   486
            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
noschinl@59739
   487
            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
noschinl@59739
   488
              | mk_free_constrs _ = []
noschinl@59739
   489
noschinl@60051
   490
            val ts = maps mk_free_constrs ps @ the_list to
noschinl@59739
   491
              |> Syntax.check_terms (hole_syntax ctxt)
noschinl@59739
   492
            val ctxt' = fold Variable.declare_term ts ctxt
noschinl@59739
   493
            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
noschinl@59739
   494
              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
noschinl@59739
   495
            val _ = case ts' of (_ :: _) => raise Match | [] => ()
noschinl@59739
   496
          in ((ps', to'), ctxt') end
noschinl@59739
   497
noschinl@59739
   498
        val (pats, ctxt') = prep_pats ctxt raw_pats
noschinl@59739
   499
noschinl@59739
   500
        val ths = Attrib.eval_thms ctxt' raw_ths
noschinl@59739
   501
        val to = Option.map (Syntax.parse_term ctxt') raw_to
noschinl@59739
   502
noschinl@59739
   503
        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
noschinl@59739
   504
noschinl@60079
   505
      in ((pats', ths, (to', ctxt)), ctxt'') end
noschinl@59739
   506
noschinl@59739
   507
    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
noschinl@59739
   508
noschinl@59739
   509
    val subst_parser =
noschinl@59739
   510
      let val scan = raw_pattern -- to_parser -- Parse.xthms1
wenzelm@59975
   511
      in context_lift scan prep_args end
noschinl@59739
   512
  in
noschinl@59739
   513
    Method.setup @{binding rewrite} (subst_parser >>
noschinl@60079
   514
      (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
noschinl@60079
   515
        SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
noschinl@59739
   516
      "single-step rewriting, allowing subterm selection via patterns."
noschinl@59739
   517
  end
noschinl@59739
   518
end