src/HOL/Eisbach/match_method.ML
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 63615 d786d54efc70
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
wenzelm@60248
     1
(*  Title:      HOL/Eisbach/match_method.ML
wenzelm@60119
     2
    Author:     Daniel Matichuk, NICTA/UNSW
wenzelm@60119
     3
wenzelm@60119
     4
Setup for "match" proof method. It provides basic fact/term matching in
wenzelm@60119
     5
addition to premise/conclusion matching through Subgoal.focus, and binds
wenzelm@60119
     6
fact names from matches as well as term patterns within matches.
wenzelm@60119
     7
*)
wenzelm@60119
     8
wenzelm@60119
     9
signature MATCH_METHOD =
wenzelm@60119
    10
sig
wenzelm@60119
    11
  val focus_schematics: Proof.context -> Envir.tenv
wenzelm@60119
    12
  val focus_params: Proof.context -> term list
wenzelm@60119
    13
  (* FIXME proper ML interface for the main thing *)
wenzelm@60119
    14
end
wenzelm@60119
    15
wenzelm@60119
    16
structure Match_Method : MATCH_METHOD =
wenzelm@60119
    17
struct
wenzelm@60119
    18
daniel@62133
    19
(* Filter premises by predicate, with premise order; recovers premise order afterwards.*)
daniel@62133
    20
fun filter_prems_tac' ctxt prem =
wenzelm@60119
    21
  let
wenzelm@60119
    22
    fun Then NONE tac = SOME tac
wenzelm@60119
    23
      | Then (SOME tac) tac' = SOME (tac THEN' tac');
daniel@62133
    24
    fun thins idxH (tac, n, i) =
daniel@62133
    25
       if prem idxH then (tac, n + 1 , i)
daniel@62133
    26
       else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + n);
wenzelm@60119
    27
  in
wenzelm@60119
    28
    SUBGOAL (fn (goal, i) =>
daniel@62133
    29
      let val idxHs = tag_list 0 (Logic.strip_assums_hyp goal) in
daniel@62133
    30
        (case fold thins idxHs (NONE, 0, 0) of
daniel@62133
    31
          (NONE, _, _) => no_tac
daniel@62133
    32
        | (SOME tac, _, n) => tac i THEN rotate_tac (~ n) i)
wenzelm@60119
    33
      end)
wenzelm@60119
    34
  end;
wenzelm@60119
    35
wenzelm@60119
    36
wenzelm@60119
    37
datatype match_kind =
wenzelm@60119
    38
    Match_Term of term Item_Net.T
wenzelm@60119
    39
  | Match_Fact of thm Item_Net.T
wenzelm@60119
    40
  | Match_Concl
wenzelm@60285
    41
  | Match_Prems of bool;
wenzelm@60119
    42
wenzelm@60119
    43
wenzelm@60119
    44
val aconv_net = Item_Net.init (op aconv) single;
wenzelm@60119
    45
wenzelm@60119
    46
val parse_match_kind =
wenzelm@60209
    47
  Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
wenzelm@60285
    48
  Scan.lift (@{keyword "premises"} |-- Args.mode "local") >> Match_Prems ||
wenzelm@60119
    49
  Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
wenzelm@60119
    50
    (fn t => Match_Term (Item_Net.update t aconv_net)) ||
wenzelm@60119
    51
  Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
wenzelm@60119
    52
wenzelm@60119
    53
wenzelm@60285
    54
fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false);
wenzelm@60119
    55
fun prop_match m = (case m of Match_Term _ => false | _ => true);
wenzelm@60119
    56
daniel@63185
    57
val bound_thm : (thm, binding) Parse_Tools.parse_val parser =
daniel@63185
    58
  Parse_Tools.parse_thm_val Parse.binding;
daniel@63185
    59
wenzelm@60119
    60
val bound_term : (term, binding) Parse_Tools.parse_val parser =
wenzelm@60119
    61
  Parse_Tools.parse_term_val Parse.binding;
wenzelm@60119
    62
wenzelm@60119
    63
val fixes =
wenzelm@60287
    64
  Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) --
wenzelm@60248
    65
    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ)
wenzelm@60287
    66
    >> (fn (xs, T) => map (fn (x, pos) => ((x, T), pos)) xs)) >> flat;
wenzelm@60119
    67
wenzelm@60119
    68
val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
wenzelm@60119
    69
wenzelm@60285
    70
fun pos_of dyn = Parse_Tools.the_parse_val dyn |> Binding.pos_of;
wenzelm@60119
    71
wenzelm@60119
    72
(*FIXME: Dynamic facts modify the background theory, so we have to resort
wenzelm@60119
    73
  to token replacement for matched facts. *)
wenzelm@61814
    74
val dynamic_fact =
daniel@63185
    75
  Scan.lift bound_thm -- Attrib.opt_attribs;
wenzelm@60119
    76
wenzelm@60285
    77
type match_args = {multi : bool, cut : int};
wenzelm@60119
    78
wenzelm@60119
    79
val parse_match_args =
wenzelm@61835
    80
  Scan.optional
wenzelm@61835
    81
    (Args.parens
wenzelm@61835
    82
      (Parse.enum1 ","
wenzelm@61835
    83
        (Args.$$$ "multi" >> (fn _ => fn {cut, ...} => {multi = true, cut = cut}) ||
wenzelm@61835
    84
         Args.$$$ "cut" |-- Scan.optional Parse.nat 1
wenzelm@61835
    85
          >> (fn n => fn {multi, ...} => {multi = multi, cut = n})))) []
wenzelm@61835
    86
  >> (fn fs => fold I fs {multi = false, cut = ~1});
wenzelm@60119
    87
wenzelm@60119
    88
fun parse_named_pats match_kind =
wenzelm@61814
    89
  Args.context --
wenzelm@61814
    90
  Parse.and_list1'
wenzelm@61814
    91
    (Scan.option (dynamic_fact --| Scan.lift Args.colon) :--
wenzelm@61814
    92
      (fn opt_dyn =>
wenzelm@61814
    93
        if is_none opt_dyn orelse nameable_match match_kind
wenzelm@61814
    94
        then Scan.lift (Parse_Tools.name_term -- parse_match_args)
wenzelm@61814
    95
        else
wenzelm@61814
    96
          let val b = #1 (the opt_dyn)
wenzelm@61814
    97
          in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) --
wenzelm@61912
    98
  Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.text))
wenzelm@61912
    99
  >> (fn ((ctxt, ts), (fixes, body)) =>
wenzelm@61912
   100
    (case Token.get_value body of
wenzelm@60119
   101
      SOME (Token.Source src) =>
wenzelm@60119
   102
        let
wenzelm@63527
   103
          val text = Method.read ctxt src;
wenzelm@60119
   104
          val ts' =
wenzelm@60119
   105
            map
wenzelm@60119
   106
              (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
wenzelm@60119
   107
                ((Option.map (fn (b, att) =>
wenzelm@60248
   108
                  (Parse_Tools.the_real_val b, att)) b, match_args), v)
wenzelm@60119
   109
                | _ => raise Fail "Expected closed term") ts
wenzelm@60248
   110
          val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes
wenzelm@60119
   111
        in (ts', fixes', text) end
wenzelm@61818
   112
    | _ =>
wenzelm@60119
   113
        let
wenzelm@60469
   114
          val (fix_names, ctxt3) = ctxt
wenzelm@60469
   115
            |> Proof_Context.add_fixes_cmd
wenzelm@60469
   116
              (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
wenzelm@60469
   117
            ||> Proof_Context.set_mode Proof_Context.mode_schematic;
wenzelm@60119
   118
wenzelm@60119
   119
          fun parse_term term =
wenzelm@60119
   120
            if prop_match match_kind
wenzelm@60119
   121
            then Syntax.parse_prop ctxt3 term
wenzelm@60119
   122
            else Syntax.parse_term ctxt3 term;
wenzelm@60119
   123
daniel@62134
   124
          fun drop_judgment_dummy t =
wenzelm@60285
   125
            (case t of
daniel@62134
   126
              Const (judgment, _) $
wenzelm@60285
   127
                (Const (@{syntax_const "_type_constraint_"}, T) $
wenzelm@60285
   128
                  Const (@{const_name Pure.dummy_pattern}, _)) =>
daniel@62134
   129
                if judgment = Object_Logic.judgment_name ctxt then
wenzelm@60285
   130
                    Const (@{syntax_const "_type_constraint_"}, T) $
wenzelm@60285
   131
                      Const (@{const_name Pure.dummy_pattern}, propT)
daniel@62134
   132
                else t
daniel@62134
   133
            | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
daniel@62134
   134
            | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
wenzelm@60285
   135
            | _ => t);
wenzelm@60285
   136
wenzelm@60119
   137
          val pats =
wenzelm@60119
   138
            map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
daniel@62134
   139
            |> map drop_judgment_dummy
wenzelm@60285
   140
            |> (fn ts => fold_map Term.replace_dummy_patterns ts (Variable.maxidx_of ctxt3 + 1))
wenzelm@60285
   141
            |> fst
wenzelm@60119
   142
            |> Syntax.check_terms ctxt3;
wenzelm@60119
   143
wenzelm@60209
   144
          val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
wenzelm@60209
   145
wenzelm@60248
   146
          val _ =
wenzelm@60248
   147
            map2 (fn nm => fn (_, pos) =>
wenzelm@60248
   148
                member (op =) pat_fixes nm orelse
wenzelm@60248
   149
                error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
wenzelm@60407
   150
              fix_names fixes;
wenzelm@60209
   151
wenzelm@60285
   152
          val _ = map (Term.map_types Type.no_tvars) pats;
wenzelm@60209
   153
wenzelm@60119
   154
          val ctxt4 = fold Variable.declare_term pats ctxt3;
wenzelm@60119
   155
wenzelm@60407
   156
          val (real_fixes, ctxt5) = ctxt4
wenzelm@60407
   157
            |> fold_map Proof_Context.inferred_param fix_names |>> map Free;
wenzelm@60119
   158
wenzelm@60119
   159
          fun reject_extra_free (Free (x, _)) () =
wenzelm@60119
   160
                if Variable.is_fixed ctxt5 x then ()
wenzelm@60119
   161
                else error ("Illegal use of free (unfixed) variable " ^ quote x)
wenzelm@60119
   162
            | reject_extra_free _ () = ();
wenzelm@60119
   163
          val _ = (fold o fold_aterms) reject_extra_free pats ();
wenzelm@60119
   164
wenzelm@60119
   165
          val binds =
wenzelm@60119
   166
            map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
wenzelm@60119
   167
wenzelm@60119
   168
          fun upd_ctxt (SOME (b, att)) pat (tms, ctxt) =
wenzelm@60119
   169
                let
wenzelm@60119
   170
                  val ([nm], ctxt') =
wenzelm@60119
   171
                    Variable.variant_fixes [Name.internal (Binding.name_of b)] ctxt;
wenzelm@60119
   172
                  val abs_nms = Term.strip_all_vars pat;
wenzelm@60119
   173
wenzelm@60119
   174
                  val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
wenzelm@60119
   175
                    |> Conjunction.intr_balanced
wenzelm@60248
   176
                    |> Drule.generalize ([], map fst abs_nms)
wenzelm@61852
   177
                    |> Thm.tag_free_dummy;
wenzelm@60119
   178
wenzelm@60248
   179
                  val atts = map (Attrib.attribute ctxt') att;
wenzelm@60248
   180
                  val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
wenzelm@60248
   181
wenzelm@60248
   182
                  fun label_thm thm =
wenzelm@60367
   183
                    Thm.cterm_of ctxt'' (Free (nm, propT))
wenzelm@60119
   184
                    |> Drule.mk_term
wenzelm@60248
   185
                    |> not (null abs_nms) ? Conjunction.intr thm
wenzelm@60248
   186
wenzelm@60248
   187
                  val [head_thm, body_thm] =
wenzelm@60248
   188
                    Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm'])
wenzelm@61852
   189
                    |> map Thm.tag_free_dummy;
wenzelm@60119
   190
wenzelm@60248
   191
                  val ctxt''' =
wenzelm@60248
   192
                    Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt''
wenzelm@60248
   193
                    |> snd
wenzelm@60248
   194
                    |> Variable.declare_maxidx (Thm.maxidx_of head_thm);
wenzelm@60119
   195
                in
daniel@63185
   196
                  (SOME (head_thm, att) :: tms, ctxt''')
wenzelm@60119
   197
                end
wenzelm@60119
   198
            | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
wenzelm@60119
   199
wenzelm@60119
   200
          val (binds, ctxt6) = ctxt5
wenzelm@60119
   201
            |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
wenzelm@60119
   202
            ||> Proof_Context.restore_mode ctxt;
wenzelm@60119
   203
wenzelm@63527
   204
          val (text, src) = Method.read_closure_input ctxt6 (Token.input_of body);
wenzelm@60119
   205
wenzelm@60119
   206
          val morphism =
wenzelm@60119
   207
            Variable.export_morphism ctxt6
wenzelm@60119
   208
              (ctxt
wenzelm@61814
   209
                |> fold Token.declare_maxidx src
wenzelm@60119
   210
                |> Variable.declare_maxidx (Variable.maxidx_of ctxt6));
wenzelm@60119
   211
wenzelm@60119
   212
          val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
wenzelm@60285
   213
          val _ = ListPair.app (fn ((_, (v, _)), t) => Parse_Tools.the_parse_fun v t) (ts, pats');
wenzelm@60119
   214
wenzelm@60248
   215
          fun close_src src =
wenzelm@60248
   216
            let
wenzelm@61814
   217
              val src' = src |> map (Token.closure #> Token.transform morphism);
wenzelm@60248
   218
              val _ =
wenzelm@61814
   219
                (Token.args_of_src src ~~ Token.args_of_src src')
wenzelm@61814
   220
                |> List.app (fn (tok, tok') =>
wenzelm@61814
   221
                  (case Token.get_value tok' of
wenzelm@61814
   222
                    SOME value => ignore (Token.assign (SOME value) tok)
wenzelm@61814
   223
                  | NONE => ()));
wenzelm@60248
   224
            in src' end;
wenzelm@60248
   225
wenzelm@60248
   226
          val binds' =
daniel@63185
   227
            map (Option.map (fn (t, atts) => (Morphism.thm morphism t, map close_src atts))) binds;
wenzelm@60119
   228
wenzelm@60119
   229
          val _ =
wenzelm@60119
   230
            ListPair.app
wenzelm@60285
   231
              (fn ((SOME ((v, _)), _), SOME (t, _)) => Parse_Tools.the_parse_fun v t
wenzelm@60119
   232
                | ((NONE, _), NONE) => ()
wenzelm@60119
   233
                | _ => error "Mismatch between real and parsed bound variables")
wenzelm@60119
   234
              (ts, binds');
wenzelm@60119
   235
wenzelm@60119
   236
          val real_fixes' = map (Morphism.term morphism) real_fixes;
wenzelm@60119
   237
          val _ =
wenzelm@60285
   238
            ListPair.app (fn (((v, _) , _), t) => Parse_Tools.the_parse_fun v t)
wenzelm@60248
   239
              (fixes, real_fixes');
wenzelm@60119
   240
wenzelm@60119
   241
          val match_args = map (fn (_, (_, match_args)) => match_args) ts;
wenzelm@60119
   242
          val binds'' = (binds' ~~ match_args) ~~ pats';
wenzelm@60119
   243
wenzelm@61814
   244
          val src' = map (Token.transform morphism) src;
wenzelm@61912
   245
          val _ = Token.assign (SOME (Token.Source src')) body;
wenzelm@60119
   246
        in
wenzelm@60119
   247
          (binds'', real_fixes', text)
wenzelm@61814
   248
        end));
wenzelm@60119
   249
wenzelm@60119
   250
daniel@63185
   251
fun dest_internal_term t =
wenzelm@60119
   252
  (case try Logic.dest_conjunction t of
wenzelm@60119
   253
    SOME (params, head) =>
wenzelm@60119
   254
     (params |> Logic.dest_conjunctions |> map Logic.dest_term,
wenzelm@60119
   255
      head |> Logic.dest_term)
wenzelm@60119
   256
  | NONE => ([], t |> Logic.dest_term));
wenzelm@60119
   257
daniel@63185
   258
fun dest_internal_fact thm = dest_internal_term (Thm.prop_of thm);
wenzelm@60119
   259
wenzelm@60119
   260
fun inst_thm ctxt env ts params thm =
wenzelm@60119
   261
  let
wenzelm@60119
   262
    val ts' = map (Envir.norm_term env) ts;
wenzelm@60791
   263
    val insts = map (#1 o dest_Var) ts' ~~ map (Thm.cterm_of ctxt) params;
wenzelm@60791
   264
  in infer_instantiate ctxt insts thm end;
wenzelm@60119
   265
wenzelm@60119
   266
fun do_inst fact_insts' env text ctxt =
wenzelm@60119
   267
  let
wenzelm@60119
   268
    val fact_insts =
wenzelm@60119
   269
      map_filter
wenzelm@60119
   270
        (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
wenzelm@60119
   271
          | _ => NONE) fact_insts';
wenzelm@60119
   272
daniel@63185
   273
    fun try_dest_term thm = try (dest_internal_fact #> snd) thm;
wenzelm@60119
   274
wenzelm@60248
   275
    fun expand_fact fact_insts thm =
wenzelm@60119
   276
      the_default [thm]
wenzelm@60119
   277
        (case try_dest_term thm of
wenzelm@60119
   278
          SOME t_ident => AList.lookup (op aconv) fact_insts t_ident
wenzelm@60119
   279
        | NONE => NONE);
wenzelm@60119
   280
wenzelm@60248
   281
    fun fact_morphism fact_insts =
wenzelm@60119
   282
      Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
wenzelm@60209
   283
      Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
wenzelm@60248
   284
      Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts));
wenzelm@60119
   285
wenzelm@60248
   286
    fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) =
wenzelm@60248
   287
      let
wenzelm@60248
   288
        val morphism = fact_morphism fact_insts;
wenzelm@61814
   289
        val atts' = map (Attrib.attribute ctxt o map (Token.transform morphism)) atts;
wenzelm@60248
   290
        val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt;
wenzelm@60248
   291
      in ((head, fact'') :: fact_insts, ctxt') end;
wenzelm@60248
   292
wenzelm@60248
   293
     (*TODO: What to do about attributes that raise errors?*)
wenzelm@60248
   294
    val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt);
wenzelm@60248
   295
wenzelm@61814
   296
    val text' = (Method.map_source o map) (Token.transform (fact_morphism fact_insts')) text;
wenzelm@60119
   297
  in
wenzelm@60119
   298
    (text', ctxt')
wenzelm@60119
   299
  end;
wenzelm@60119
   300
wenzelm@60119
   301
fun prep_fact_pat ((x, args), pat) ctxt =
wenzelm@60119
   302
  let
wenzelm@60695
   303
    val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
wenzelm@60119
   304
    val params' = map (Free o snd) params;
wenzelm@60119
   305
wenzelm@60119
   306
    val morphism =
wenzelm@60119
   307
      Variable.export_morphism ctxt'
wenzelm@60119
   308
        (ctxt |> Variable.declare_maxidx (Variable.maxidx_of ctxt'));
wenzelm@60119
   309
    val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
wenzelm@60119
   310
wenzelm@60119
   311
    fun prep_head (t, att) = (dest_internal_fact t, att);
wenzelm@60119
   312
  in
wenzelm@60119
   313
    ((((Option.map prep_head x, args), params''), pat''), ctxt')
wenzelm@60119
   314
  end;
wenzelm@60119
   315
wenzelm@60285
   316
fun morphism_env morphism env =
wenzelm@60209
   317
  let
wenzelm@60285
   318
    val tenv = Envir.term_env env
wenzelm@60248
   319
      |> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t)));
wenzelm@60285
   320
    val tyenv = Envir.type_env env
wenzelm@60285
   321
      |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
wenzelm@60285
   322
   in Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv, tyenv = tyenv} end;
wenzelm@60209
   323
wenzelm@60285
   324
fun export_with_params ctxt morphism (SOME ts, params) thm env =
wenzelm@60285
   325
      let
wenzelm@60285
   326
        val outer_env = morphism_env morphism env;
wenzelm@60285
   327
        val thm' = Morphism.thm morphism thm;
wenzelm@60285
   328
      in inst_thm ctxt outer_env params ts thm' end
wenzelm@60552
   329
  | export_with_params _ morphism (NONE, _) thm _ = Morphism.thm morphism thm;
wenzelm@60209
   330
wenzelm@60285
   331
fun match_filter_env is_newly_fixed pat_vars fixes params env =
wenzelm@60285
   332
  let
wenzelm@60119
   333
    val param_vars = map Term.dest_Var params;
wenzelm@60209
   334
wenzelm@60285
   335
    val tenv = Envir.term_env env;
wenzelm@60285
   336
    val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars;
wenzelm@60119
   337
wenzelm@60119
   338
    val fixes_vars = map Term.dest_Var fixes;
wenzelm@60119
   339
wenzelm@60119
   340
    val all_vars = Vartab.keys tenv;
wenzelm@60119
   341
    val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
wenzelm@60119
   342
wenzelm@60285
   343
    val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars;
wenzelm@60119
   344
    val env' =
wenzelm@61846
   345
      Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env};
wenzelm@60209
   346
wenzelm@60552
   347
    val all_params_bound = forall (fn SOME (_, Free (x, _)) => is_newly_fixed x | _ => false) params';
wenzelm@61846
   348
    val all_params_distinct = not (has_duplicates (eq_option (eq_pair (op =) (op aconv))) params');
wenzelm@60209
   349
wenzelm@60209
   350
    val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
wenzelm@60248
   351
    val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
wenzelm@60119
   352
  in
wenzelm@60285
   353
    if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct
wenzelm@60285
   354
    then SOME env'
wenzelm@60119
   355
    else NONE
wenzelm@60119
   356
  end;
wenzelm@60119
   357
wenzelm@60119
   358
wenzelm@60119
   359
(* Slightly hacky way of uniquely identifying focus premises *)
wenzelm@60119
   360
val prem_idN = "premise_id";
wenzelm@60119
   361
wenzelm@60119
   362
fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id';
wenzelm@60119
   363
wenzelm@60119
   364
val prem_rules : (int * thm) Item_Net.T =
wenzelm@60285
   365
  Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd);
wenzelm@60119
   366
wenzelm@60119
   367
fun raw_thm_to_id thm =
wenzelm@60119
   368
  (case Properties.get (Thm.get_tags thm) prem_idN of NONE => NONE | SOME id => Int.fromString id)
wenzelm@60119
   369
  |> the_default ~1;
wenzelm@60119
   370
wenzelm@60119
   371
structure Focus_Data = Proof_Data
wenzelm@60119
   372
(
wenzelm@60119
   373
  type T =
wenzelm@60119
   374
    (int * (int * thm) Item_Net.T) *  (*prems*)
wenzelm@60119
   375
    Envir.tenv *  (*schematics*)
wenzelm@60119
   376
    term list  (*params*)
wenzelm@60119
   377
  fun init _ : T = ((0, prem_rules), Vartab.empty, [])
wenzelm@60119
   378
);
wenzelm@60119
   379
wenzelm@60119
   380
wenzelm@60119
   381
(* focus prems *)
wenzelm@60119
   382
wenzelm@60119
   383
val focus_prems = #1 o Focus_Data.get;
wenzelm@60119
   384
daniel@62133
   385
fun transfer_focus_prems from_ctxt =
daniel@62133
   386
  Focus_Data.map (@{apply 3(1)} (K (focus_prems from_ctxt)))
wenzelm@60285
   387
wenzelm@60285
   388
wenzelm@60119
   389
fun add_focus_prem prem =
wenzelm@60285
   390
  `(Focus_Data.get #> #1 #> #1) ##>
wenzelm@60119
   391
  (Focus_Data.map o @{apply 3(1)}) (fn (next, net) =>
wenzelm@60119
   392
    (next + 1, Item_Net.update (next, Thm.tag_rule (prem_idN, string_of_int next) prem) net));
wenzelm@60119
   393
wenzelm@60285
   394
fun remove_focus_prem' (ident, thm) =
wenzelm@60119
   395
  (Focus_Data.map o @{apply 3(1)} o apsnd)
wenzelm@60285
   396
    (Item_Net.remove (ident, thm));
wenzelm@60285
   397
wenzelm@60285
   398
fun remove_focus_prem thm = remove_focus_prem' (raw_thm_to_id thm, thm);
wenzelm@60119
   399
wenzelm@60119
   400
(*TODO: Preliminary analysis to see if we're trying to clear in a non-focus match?*)
wenzelm@60119
   401
val _ =
wenzelm@60119
   402
  Theory.setup
wenzelm@60119
   403
    (Attrib.setup @{binding "thin"}
wenzelm@60119
   404
      (Scan.succeed
wenzelm@60119
   405
        (Thm.declaration_attribute (fn th => Context.mapping I (remove_focus_prem th))))
wenzelm@60119
   406
        "clear premise inside match method");
wenzelm@60119
   407
wenzelm@60119
   408
wenzelm@60119
   409
(* focus schematics *)
wenzelm@60119
   410
wenzelm@60119
   411
val focus_schematics = #2 o Focus_Data.get;
wenzelm@60119
   412
wenzelm@60642
   413
fun add_focus_schematics schematics =
wenzelm@60119
   414
  (Focus_Data.map o @{apply 3(2)})
wenzelm@60642
   415
    (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics);
wenzelm@60119
   416
wenzelm@60119
   417
wenzelm@60119
   418
(* focus params *)
wenzelm@60119
   419
wenzelm@60119
   420
val focus_params = #3 o Focus_Data.get;
wenzelm@60119
   421
wenzelm@60119
   422
fun add_focus_params params =
wenzelm@60119
   423
  (Focus_Data.map o @{apply 3(3)})
wenzelm@60119
   424
    (append (map (fn (_, ct) => Thm.term_of ct) params));
wenzelm@60119
   425
wenzelm@60119
   426
wenzelm@60119
   427
(* Add focus elements as proof data *)
wenzelm@60285
   428
fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) =
wenzelm@60119
   429
  let
wenzelm@60285
   430
    val {context, params, prems, asms, concl, schematics} = focus;
wenzelm@60285
   431
wenzelm@60552
   432
    val (prem_ids, ctxt') = context
wenzelm@60119
   433
      |> add_focus_params params
wenzelm@60119
   434
      |> add_focus_schematics (snd schematics)
wenzelm@60285
   435
      |> fold_map add_focus_prem (rev prems)
wenzelm@60285
   436
wenzelm@60119
   437
  in
wenzelm@60552
   438
    (prem_ids,
daniel@62133
   439
      {context = ctxt',
wenzelm@60552
   440
       params = params,
wenzelm@60552
   441
       prems = prems,
wenzelm@60552
   442
       concl = concl,
wenzelm@60552
   443
       schematics = schematics,
wenzelm@60552
   444
       asms = asms})
wenzelm@60119
   445
  end;
wenzelm@60119
   446
wenzelm@60119
   447
wenzelm@60119
   448
(* Fix schematics in the goal *)
wenzelm@60695
   449
fun focus_concl ctxt i bindings goal =
wenzelm@60119
   450
  let
wenzelm@60367
   451
    val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
wenzelm@60695
   452
      Subgoal.focus_params ctxt i bindings goal;
wenzelm@60119
   453
wenzelm@60367
   454
    val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
wenzelm@60805
   455
    val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst);
wenzelm@60119
   456
wenzelm@60119
   457
    val goal'' = Thm.instantiate ([], schematic_terms) goal';
wenzelm@60119
   458
    val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
wenzelm@60119
   459
    val (schematic_types, schematic_terms') = schematics;
wenzelm@60119
   460
    val schematics' = (schematic_types, schematic_terms @ schematic_terms');
wenzelm@60119
   461
  in
wenzelm@60367
   462
    ({context = ctxt'', concl = concl', params = params, prems = prems,
wenzelm@60119
   463
      schematics = schematics', asms = asms} : Subgoal.focus, goal'')
wenzelm@60119
   464
  end;
wenzelm@60119
   465
wenzelm@60209
   466
wenzelm@60209
   467
fun deduplicate eq prev seq =
wenzelm@60209
   468
  Seq.make (fn () =>
wenzelm@60285
   469
    (case Seq.pull seq of
wenzelm@60209
   470
      SOME (x, seq') =>
wenzelm@60209
   471
        if member eq prev x
wenzelm@60209
   472
        then Seq.pull (deduplicate eq prev seq')
wenzelm@60248
   473
        else SOME (x, deduplicate eq (x :: prev) seq')
wenzelm@60209
   474
    | NONE => NONE));
wenzelm@60209
   475
wenzelm@60285
   476
wenzelm@60209
   477
fun consistent_env env =
wenzelm@60209
   478
  let
wenzelm@60209
   479
    val tenv = Envir.term_env env;
wenzelm@60209
   480
    val tyenv = Envir.type_env env;
wenzelm@60209
   481
  in
wenzelm@60209
   482
    forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
wenzelm@60209
   483
  end;
wenzelm@60209
   484
wenzelm@60552
   485
fun term_eq_wrt (env1, env2) (t1, t2) =
wenzelm@60285
   486
  Envir.eta_contract (Envir.norm_term env1 t1) aconv
wenzelm@60285
   487
  Envir.eta_contract (Envir.norm_term env2 t2);
wenzelm@60285
   488
wenzelm@60552
   489
fun type_eq_wrt (env1, env2) (T1, T2) =
wenzelm@60552
   490
  Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2;
wenzelm@60285
   491
wenzelm@60285
   492
wenzelm@60248
   493
fun eq_env (env1, env2) =
wenzelm@60209
   494
    Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
wenzelm@60209
   495
    ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
wenzelm@60552
   496
        (var = var' andalso term_eq_wrt (env1, env2) (t, t')))
wenzelm@60209
   497
      (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
wenzelm@60209
   498
    andalso
wenzelm@60248
   499
    ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
wenzelm@60552
   500
        var = var' andalso type_eq_wrt (env1, env2) (T, T'))
wenzelm@60285
   501
      (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2));
wenzelm@60285
   502
wenzelm@60285
   503
wenzelm@60552
   504
fun merge_env (env1, env2) =
wenzelm@60285
   505
  let
wenzelm@60285
   506
    val tenv =
wenzelm@60285
   507
      Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2);
wenzelm@60285
   508
    val tyenv =
wenzelm@60285
   509
      Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =))
wenzelm@60552
   510
        (Envir.type_env env1, Envir.type_env env2);
wenzelm@60285
   511
    val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2);
wenzelm@60285
   512
  in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end;
wenzelm@60285
   513
wenzelm@60209
   514
wenzelm@60285
   515
fun import_with_tags thms ctxt =
wenzelm@60285
   516
  let
wenzelm@60285
   517
    val ((_, thms'), ctxt') = Variable.import false thms ctxt;
wenzelm@60285
   518
    val thms'' = map2 (fn thm => Thm.map_tags (K (Thm.get_tags thm))) thms thms';
wenzelm@60285
   519
  in (thms'', ctxt') end;
wenzelm@60285
   520
wenzelm@60285
   521
wenzelm@60285
   522
fun try_merge (env, env') = SOME (merge_env (env, env')) handle Vartab.DUP _ => NONE
wenzelm@60285
   523
wenzelm@60285
   524
wenzelm@60285
   525
fun Seq_retrieve seq f =
wenzelm@60285
   526
  let
wenzelm@60285
   527
    fun retrieve' (list, seq) f =
wenzelm@60285
   528
      (case Seq.pull seq of
wenzelm@60285
   529
        SOME (x, seq') =>
wenzelm@60285
   530
          if f x then (SOME x, (list, seq'))
wenzelm@60285
   531
          else retrieve' (list @ [x], seq') f
wenzelm@60285
   532
      | NONE => (NONE, (list, seq)));
wenzelm@60285
   533
wenzelm@60285
   534
    val (result, (list, seq)) = retrieve' ([], seq) f;
wenzelm@60285
   535
  in (result, Seq.append (Seq.of_list list) seq) end;
wenzelm@60209
   536
wenzelm@60119
   537
fun match_facts ctxt fixes prop_pats get =
wenzelm@60119
   538
  let
wenzelm@60119
   539
    fun is_multi (((_, x : match_args), _), _) = #multi x;
wenzelm@60285
   540
    fun get_cut (((_, x : match_args), _), _) = #cut x;
wenzelm@60285
   541
    fun do_cut n = if n = ~1 then I else Seq.take n;
wenzelm@60285
   542
wenzelm@60285
   543
    val raw_thmss = map (get o snd) prop_pats;
wenzelm@60552
   544
    val (thmss, ctxt') = fold_burrow import_with_tags raw_thmss ctxt;
wenzelm@60119
   545
wenzelm@60285
   546
    val newly_fixed = Variable.is_newly_fixed ctxt' ctxt;
wenzelm@60285
   547
wenzelm@60285
   548
    val morphism = Variable.export_morphism ctxt' ctxt;
wenzelm@60285
   549
wenzelm@60285
   550
    fun match_thm (((x, params), pat), thm)  =
wenzelm@60119
   551
      let
wenzelm@60209
   552
        val pat_vars = Term.add_vars pat [];
wenzelm@60209
   553
wenzelm@60119
   554
        val ts = Option.map (fst o fst) (fst x);
wenzelm@60209
   555
wenzelm@60285
   556
        val item' = Thm.prop_of thm;
wenzelm@60119
   557
wenzelm@60119
   558
        val matches =
wenzelm@60285
   559
          (Unify.matchers (Context.Proof ctxt) [(pat, item')])
wenzelm@60209
   560
          |> Seq.filter consistent_env
wenzelm@60119
   561
          |> Seq.map_filter (fn env' =>
wenzelm@60285
   562
              (case match_filter_env newly_fixed pat_vars fixes params env' of
wenzelm@60552
   563
                SOME env'' => SOME (export_with_params ctxt morphism (ts, params) thm env', env'')
wenzelm@60285
   564
              | NONE => NONE))
wenzelm@60209
   565
          |> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
wenzelm@60285
   566
          |> deduplicate (eq_pair Thm.eq_thm_prop eq_env) []
wenzelm@60285
   567
      in matches end;
wenzelm@60119
   568
wenzelm@60119
   569
    val all_matches =
wenzelm@60285
   570
      map2 pair prop_pats thmss
wenzelm@60119
   571
      |> map (fn (pat, matches) => (pat, map (fn thm => match_thm (pat, thm)) matches));
wenzelm@60119
   572
wenzelm@60119
   573
    fun proc_multi_match (pat, thmenvs) (pats, env) =
wenzelm@60285
   574
      do_cut (get_cut pat)
wenzelm@60285
   575
        (if is_multi pat then
wenzelm@60285
   576
          let
wenzelm@60285
   577
            fun maximal_set tail seq envthms =
wenzelm@60285
   578
              Seq.make (fn () =>
wenzelm@60285
   579
                (case Seq.pull seq of
wenzelm@60285
   580
                  SOME ((thm, env'), seq') =>
wenzelm@60285
   581
                    let
wenzelm@60285
   582
                      val (result, envthms') =
wenzelm@60285
   583
                        Seq_retrieve envthms (fn (env, _) => eq_env (env, env'));
daniel@62133
   584
                    in        
wenzelm@60285
   585
                      (case result of
wenzelm@60552
   586
                        SOME (_, thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
wenzelm@60285
   587
                      | NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms'))
wenzelm@60285
   588
                    end
wenzelm@60285
   589
                 | NONE => Seq.pull (Seq.append envthms (Seq.of_list tail))));
wenzelm@60119
   590
wenzelm@60285
   591
            val maximal_sets = fold (maximal_set []) thmenvs Seq.empty;
wenzelm@60285
   592
          in
wenzelm@60285
   593
            maximal_sets
wenzelm@60285
   594
            |> Seq.map swap
wenzelm@60285
   595
            |> Seq.filter (fn (thms, _) => not (null thms))
wenzelm@60285
   596
            |> Seq.map_filter (fn (thms, env') =>
wenzelm@60285
   597
              (case try_merge (env, env') of
wenzelm@60285
   598
                SOME env'' => SOME ((pat, thms) :: pats, env'')
wenzelm@60285
   599
              | NONE => NONE))
wenzelm@60285
   600
          end
wenzelm@60285
   601
        else
wenzelm@60285
   602
          let
wenzelm@60285
   603
            fun just_one (thm, env') =
wenzelm@60552
   604
              (case try_merge (env, env') of
wenzelm@60552
   605
                SOME env'' => SOME ((pat, [thm]) :: pats, env'')
wenzelm@60285
   606
              | NONE => NONE);
wenzelm@60285
   607
          in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end);
wenzelm@60119
   608
wenzelm@60119
   609
    val all_matches =
wenzelm@63615
   610
      Seq.EVERY (map proc_multi_match all_matches) ([], Envir.init);
wenzelm@60119
   611
  in
wenzelm@60285
   612
    all_matches
wenzelm@60285
   613
    |> Seq.map (apsnd (morphism_env morphism))
wenzelm@60119
   614
  end;
wenzelm@60119
   615
daniel@62133
   616
fun real_match using outer_ctxt fixes m text pats st =
daniel@62133
   617
  let              
daniel@62133
   618
    val goal_ctxt =
daniel@62133
   619
      fold Variable.declare_term fixes outer_ctxt
daniel@62133
   620
      (*FIXME Is this a good idea? We really only care about the maxidx*)
daniel@62133
   621
      |> fold (fn (_, t) => Variable.declare_term t) pats;
daniel@62133
   622
wenzelm@60119
   623
    fun make_fact_matches ctxt get =
wenzelm@60119
   624
      let
wenzelm@60119
   625
        val (pats', ctxt') = fold_map prep_fact_pat pats ctxt;
wenzelm@60119
   626
      in
wenzelm@60119
   627
        match_facts ctxt' fixes pats' get
wenzelm@60119
   628
        |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt')
wenzelm@60119
   629
      end;
wenzelm@60119
   630
wenzelm@60119
   631
    fun make_term_matches ctxt get =
wenzelm@60119
   632
      let
wenzelm@61839
   633
        val pats' = map
wenzelm@61839
   634
          (fn ((SOME _, _), _) => error "Cannot name term match"
wenzelm@61839
   635
            | ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats;
wenzelm@60119
   636
wenzelm@60119
   637
        val thm_of = Drule.mk_term o Thm.cterm_of ctxt;
wenzelm@60119
   638
        fun get' t = get (Logic.dest_term t) |> map thm_of;
wenzelm@60119
   639
      in
wenzelm@60119
   640
        match_facts ctxt fixes pats' get'
wenzelm@60119
   641
        |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt)
wenzelm@60119
   642
      end;
wenzelm@60119
   643
  in
wenzelm@60119
   644
    (case m of
wenzelm@60119
   645
      Match_Fact net =>
wenzelm@61841
   646
        make_fact_matches goal_ctxt (Item_Net.retrieve net)
wenzelm@61841
   647
        |> Seq.map (fn (text, ctxt') =>
wenzelm@63527
   648
          Method.evaluate_runtime text ctxt' using (ctxt', st)
daniel@62133
   649
          |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
wenzelm@60119
   650
    | Match_Term net =>
wenzelm@61841
   651
        make_term_matches goal_ctxt (Item_Net.retrieve net)
wenzelm@61841
   652
        |> Seq.map (fn (text, ctxt') =>
wenzelm@63527
   653
          Method.evaluate_runtime text ctxt' using (ctxt', st)
daniel@62133
   654
          |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
wenzelm@60119
   655
    | match_kind =>
wenzelm@61839
   656
        if Thm.no_prems st then Seq.empty
wenzelm@60119
   657
        else
wenzelm@60119
   658
          let
wenzelm@60119
   659
            fun focus_cases f g =
wenzelm@60119
   660
              (case match_kind of
wenzelm@60285
   661
                Match_Prems b => f b
wenzelm@60119
   662
              | Match_Concl => g
wenzelm@60119
   663
              | _ => raise Fail "Match kind fell through");
wenzelm@60119
   664
daniel@62133
   665
            val ((local_premids, {context = focus_ctxt, params, asms, concl, prems, ...}), focused_goal) =
daniel@62133
   666
              focus_cases (K Subgoal.focus_prems) focus_concl goal_ctxt 1 NONE st
wenzelm@60119
   667
              |>> augment_focus;
daniel@62133
   668
            
wenzelm@60119
   669
            val texts =
wenzelm@60119
   670
              focus_cases
wenzelm@60285
   671
                (fn is_local => fn _ =>
wenzelm@60119
   672
                  make_fact_matches focus_ctxt
wenzelm@60285
   673
                    (Item_Net.retrieve (focus_prems focus_ctxt |> snd)
wenzelm@60552
   674
                     #> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids)
wenzelm@60285
   675
                     #> order_list))
wenzelm@60119
   676
                (fn _ =>
wenzelm@61839
   677
                  make_term_matches focus_ctxt
wenzelm@61839
   678
                    (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
wenzelm@60119
   679
                ();
wenzelm@60119
   680
wenzelm@60119
   681
            (*TODO: How to handle cases? *)
wenzelm@60119
   682
daniel@62133
   683
            fun do_retrofit (inner_ctxt, st1) =
wenzelm@60119
   684
              let
daniel@62133
   685
                val (_, before_prems) = focus_prems focus_ctxt;
daniel@62133
   686
                val (_, after_prems) = focus_prems inner_ctxt;
wenzelm@60285
   687
daniel@62133
   688
                val removed_prems =
wenzelm@62165
   689
                  Item_Net.filter (null o Item_Net.lookup after_prems) before_prems
wenzelm@60285
   690
daniel@62133
   691
                val removed_local_prems = Item_Net.content removed_prems
daniel@62133
   692
                  |> filter (fn (id, _) => member (op =) local_premids id)
daniel@62133
   693
                  |> map (fn (_, prem) => Thm.prop_of prem)
wenzelm@60285
   694
daniel@62133
   695
                fun filter_removed_prems prems =
wenzelm@62165
   696
                  Item_Net.filter (null o Item_Net.lookup removed_prems) prems;
daniel@62133
   697
                                     
daniel@62133
   698
                val outer_ctxt' = outer_ctxt 
daniel@62133
   699
                  |> Focus_Data.map (@{apply 3(1)} (apsnd filter_removed_prems));
daniel@62133
   700
daniel@62133
   701
                val n_subgoals = Thm.nprems_of st1;
wenzelm@60285
   702
daniel@62133
   703
                val removed_prem_idxs = 
daniel@62133
   704
                  prems
daniel@62133
   705
                  |> tag_list 0
daniel@62133
   706
                  |> filter (member (op aconv) removed_local_prems o Thm.prop_of o snd)
daniel@62133
   707
                  |> map fst
wenzelm@60119
   708
daniel@62133
   709
                fun filter_prem (i, _) = not (member (op =) removed_prem_idxs i); 
daniel@62133
   710
wenzelm@60119
   711
              in
daniel@62133
   712
                Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st1 st
daniel@62133
   713
                |> focus_cases 
daniel@62133
   714
                   (fn _ => (n_subgoals > 0 andalso length removed_local_prems > 0) ?
wenzelm@61840
   715
                    (Seq.map (Goal.restrict 1 n_subgoals)
wenzelm@61840
   716
                      #> Seq.maps (ALLGOALS (fn i =>
daniel@62133
   717
                          DETERM (filter_prems_tac' goal_ctxt filter_prem i)))
daniel@62133
   718
                      #> Seq.map (Goal.unrestrict 1)))
daniel@62133
   719
                   I
daniel@62133
   720
                |> Seq.map (pair outer_ctxt')
wenzelm@60119
   721
              end;
wenzelm@60119
   722
wenzelm@60119
   723
            fun apply_text (text, ctxt') =
wenzelm@63527
   724
                Method.evaluate_runtime text ctxt' using (ctxt', focused_goal)
daniel@62133
   725
              |> Seq.filter_results
daniel@62133
   726
              |> Seq.maps (Seq.DETERM do_retrofit)             
daniel@62133
   727
wenzelm@61839
   728
          in Seq.map apply_text texts end)
wenzelm@60119
   729
  end;
wenzelm@60119
   730
wenzelm@60119
   731
val _ =
wenzelm@60119
   732
  Theory.setup
wenzelm@60119
   733
    (Method.setup @{binding match}
wenzelm@61837
   734
      (parse_match_kind :--
wenzelm@61837
   735
        (fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
wenzelm@61837
   736
        (fn (matches, bodies) => fn ctxt =>
wenzelm@61841
   737
          CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
wenzelm@61837
   738
            let
daniel@62133
   739
              val ctxt' = transfer_focus_prems goal_ctxt ctxt;
wenzelm@61841
   740
              fun exec (pats, fixes, text) st' =
daniel@62133
   741
                real_match using ctxt' fixes matches text pats st';
wenzelm@61841
   742
            in
wenzelm@61841
   743
              Seq.flat (Seq.FIRST (map exec bodies) st)
daniel@62133
   744
              |> Seq.map (apfst (fn ctxt' => transfer_focus_prems ctxt' goal_ctxt))
daniel@62133
   745
              |> Seq.make_results
wenzelm@61841
   746
            end))))
wenzelm@60119
   747
      "structural analysis/matching on goals");
wenzelm@60119
   748
wenzelm@60119
   749
end;