src/Pure/Isar/method.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@5824
     1
(*  Title:      Pure/Isar/method.ML
wenzelm@5824
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5824
     3
wenzelm@17110
     4
Isar proof methods.
wenzelm@5824
     5
*)
wenzelm@5824
     6
wenzelm@5824
     7
signature METHOD =
wenzelm@5824
     8
sig
wenzelm@58002
     9
  type method = thm list -> cases_tactic
wenzelm@18227
    10
  val METHOD_CASES: (thm list -> cases_tactic) -> method
wenzelm@17110
    11
  val METHOD: (thm list -> tactic) -> method
wenzelm@17110
    12
  val fail: method
wenzelm@17110
    13
  val succeed: method
wenzelm@17110
    14
  val insert_tac: thm list -> int -> tactic
wenzelm@17110
    15
  val insert: thm list -> method
wenzelm@17110
    16
  val insert_facts: method
wenzelm@17110
    17
  val SIMPLE_METHOD: tactic -> method
wenzelm@21592
    18
  val SIMPLE_METHOD': (int -> tactic) -> method
wenzelm@21592
    19
  val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
wenzelm@52059
    20
  val cheating: Proof.context -> bool -> method
wenzelm@58957
    21
  val intro: Proof.context -> thm list -> method
wenzelm@58957
    22
  val elim: Proof.context -> thm list -> method
wenzelm@20289
    23
  val unfold: thm list -> Proof.context -> method
wenzelm@20289
    24
  val fold: thm list -> Proof.context -> method
wenzelm@54742
    25
  val atomize: bool -> Proof.context -> method
wenzelm@17110
    26
  val this: method
wenzelm@20289
    27
  val fact: thm list -> Proof.context -> method
wenzelm@30234
    28
  val assm_tac: Proof.context -> int -> tactic
wenzelm@30567
    29
  val all_assm_tac: Proof.context -> tactic
wenzelm@20289
    30
  val assumption: Proof.context -> method
wenzelm@46466
    31
  val rule_trace: bool Config.T
wenzelm@20289
    32
  val trace: Proof.context -> thm list -> unit
wenzelm@54742
    33
  val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
wenzelm@54742
    34
  val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
haftmann@25270
    35
  val intros_tac: thm list -> thm list -> tactic
ballarin@36093
    36
  val try_intros_tac: thm list -> thm list -> tactic
wenzelm@54742
    37
  val rule: Proof.context -> thm list -> method
wenzelm@54742
    38
  val erule: Proof.context -> int -> thm list -> method
wenzelm@54742
    39
  val drule: Proof.context -> int -> thm list -> method
wenzelm@54742
    40
  val frule: Proof.context -> int -> thm list -> method
wenzelm@58018
    41
  val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
wenzelm@55765
    42
  type combinator_info
wenzelm@55765
    43
  val no_combinator_info: combinator_info
wenzelm@58005
    44
  datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int
wenzelm@5824
    45
  datatype text =
wenzelm@58011
    46
    Source of Token.src |
wenzelm@32193
    47
    Basic of Proof.context -> method |
wenzelm@58005
    48
    Combinator of combinator_info * combinator * text list
wenzelm@58011
    49
  val map_source: (Token.src -> Token.src) -> text -> text
wenzelm@54883
    50
  val primitive_text: (Proof.context -> thm -> thm) -> text
wenzelm@17857
    51
  val succeed_text: text
wenzelm@17110
    52
  val default_text: text
wenzelm@17110
    53
  val this_text: text
wenzelm@17110
    54
  val done_text: text
wenzelm@17356
    55
  val sorry_text: bool -> text
wenzelm@32193
    56
  val finish_text: text option * bool -> text
wenzelm@55742
    57
  val print_methods: Proof.context -> unit
wenzelm@55742
    58
  val check_name: Proof.context -> xstring * Position.T -> string
wenzelm@58011
    59
  val method_syntax: (Proof.context -> method) context_parser ->
wenzelm@58011
    60
    Token.src -> Proof.context -> method
wenzelm@30512
    61
  val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
wenzelm@57935
    62
  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
wenzelm@57935
    63
    local_theory -> local_theory
wenzelm@57941
    64
  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
wenzelm@57941
    65
    local_theory -> local_theory
wenzelm@58011
    66
  val method: Proof.context -> Token.src -> Proof.context -> method
wenzelm@58011
    67
  val method_closure: Proof.context -> Token.src -> Token.src
wenzelm@58011
    68
  val method_cmd: Proof.context -> Token.src -> Proof.context -> method
wenzelm@58007
    69
  val evaluate: text -> Proof.context -> method
wenzelm@58048
    70
  type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
wenzelm@58048
    71
  val modifier: attribute -> Position.T -> modifier
wenzelm@58029
    72
  val section: modifier parser list -> declaration context_parser
wenzelm@58029
    73
  val sections: modifier parser list -> declaration list context_parser
wenzelm@49889
    74
  type text_range = text * Position.range
wenzelm@49889
    75
  val text: text_range option -> text option
wenzelm@49889
    76
  val position: text_range option -> Position.T
wenzelm@55795
    77
  val reports_of: text_range -> Position.report list
wenzelm@55795
    78
  val report: text_range -> unit
wenzelm@55761
    79
  val parse: text_range parser
wenzelm@5824
    80
end;
wenzelm@5824
    81
wenzelm@5824
    82
structure Method: METHOD =
wenzelm@5824
    83
struct
wenzelm@5824
    84
wenzelm@12324
    85
(** proof methods **)
wenzelm@12324
    86
wenzelm@58006
    87
(* method *)
wenzelm@11731
    88
wenzelm@58002
    89
type method = thm list -> cases_tactic;
wenzelm@11731
    90
wenzelm@58030
    91
fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
wenzelm@58030
    92
fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
wenzelm@5824
    93
wenzelm@5824
    94
val fail = METHOD (K no_tac);
wenzelm@5824
    95
val succeed = METHOD (K all_tac);
wenzelm@5824
    96
wenzelm@5824
    97
wenzelm@17110
    98
(* insert facts *)
wenzelm@7419
    99
wenzelm@7419
   100
local
wenzelm@5824
   101
wenzelm@21579
   102
fun cut_rule_tac rule =
wenzelm@58837
   103
  resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
wenzelm@6981
   104
wenzelm@7419
   105
in
wenzelm@5824
   106
wenzelm@51552
   107
fun insert_tac [] _ = all_tac
wenzelm@7419
   108
  | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
wenzelm@6981
   109
wenzelm@7555
   110
val insert_facts = METHOD (ALLGOALS o insert_tac);
wenzelm@7664
   111
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
wenzelm@7419
   112
wenzelm@9706
   113
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
wenzelm@21592
   114
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
wenzelm@21592
   115
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
wenzelm@9706
   116
wenzelm@12324
   117
end;
wenzelm@12324
   118
wenzelm@9706
   119
wenzelm@17356
   120
(* cheating *)
wenzelm@17356
   121
wenzelm@52059
   122
fun cheating ctxt int = METHOD (fn _ => fn st =>
wenzelm@52059
   123
  if int orelse Config.get ctxt quick_and_dirty then
wenzelm@51552
   124
    ALLGOALS Skip_Proof.cheat_tac st
wenzelm@51552
   125
  else error "Cheating requires quick_and_dirty mode!");
wenzelm@17356
   126
wenzelm@17356
   127
wenzelm@17110
   128
(* unfold intro/elim rules *)
wenzelm@17110
   129
wenzelm@58957
   130
fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
wenzelm@58957
   131
fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
wenzelm@17110
   132
wenzelm@17110
   133
wenzelm@12384
   134
(* unfold/fold definitions *)
wenzelm@12384
   135
wenzelm@35624
   136
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
wenzelm@35624
   137
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
wenzelm@6532
   138
wenzelm@12384
   139
wenzelm@12829
   140
(* atomize rule statements *)
wenzelm@12829
   141
wenzelm@54742
   142
fun atomize false ctxt =
wenzelm@54742
   143
      SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
wenzelm@54742
   144
  | atomize true ctxt =
wenzelm@58002
   145
      NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
wenzelm@12829
   146
wenzelm@12829
   147
wenzelm@18039
   148
(* this -- resolve facts directly *)
wenzelm@12384
   149
wenzelm@58837
   150
val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single));
wenzelm@9484
   151
wenzelm@9484
   152
wenzelm@18039
   153
(* fact -- composition by facts from context *)
wenzelm@18039
   154
wenzelm@42360
   155
fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
wenzelm@54742
   156
  | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
wenzelm@18039
   157
wenzelm@18039
   158
wenzelm@17110
   159
(* assumption *)
wenzelm@7419
   160
wenzelm@7419
   161
local
wenzelm@7419
   162
wenzelm@19778
   163
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
wenzelm@19778
   164
  if cond (Logic.strip_assums_concl prop)
wenzelm@58837
   165
  then resolve_tac [rule] i else no_tac);
wenzelm@7419
   166
kleing@29857
   167
in
kleing@29857
   168
wenzelm@30234
   169
fun assm_tac ctxt =
wenzelm@17110
   170
  assume_tac APPEND'
wenzelm@23349
   171
  Goal.assume_rule_tac ctxt APPEND'
wenzelm@19778
   172
  cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
wenzelm@19778
   173
  cond_rtac (can Logic.dest_term) Drule.termI;
wenzelm@17110
   174
wenzelm@49846
   175
fun all_assm_tac ctxt =
wenzelm@49846
   176
  let
wenzelm@49846
   177
    fun tac i st =
wenzelm@49846
   178
      if i > Thm.nprems_of st then all_tac st
wenzelm@49846
   179
      else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st;
wenzelm@49846
   180
  in tac 1 end;
wenzelm@30567
   181
wenzelm@23349
   182
fun assumption ctxt = METHOD (HEADGOAL o
wenzelm@30234
   183
  (fn [] => assm_tac ctxt
wenzelm@23349
   184
    | [fact] => solve_tac [fact]
wenzelm@23349
   185
    | _ => K no_tac));
wenzelm@23349
   186
wenzelm@49846
   187
fun finish immed ctxt =
wenzelm@58950
   188
  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt));
wenzelm@7419
   189
wenzelm@7419
   190
end;
wenzelm@7419
   191
wenzelm@7419
   192
wenzelm@17110
   193
(* rule etc. -- single-step refinements *)
wenzelm@12347
   194
wenzelm@56204
   195
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
wenzelm@12347
   196
wenzelm@17110
   197
fun trace ctxt rules =
wenzelm@41379
   198
  if Config.get ctxt rule_trace andalso not (null rules) then
wenzelm@51584
   199
    Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
wenzelm@21962
   200
    |> Pretty.string_of |> tracing
wenzelm@21962
   201
  else ();
wenzelm@12347
   202
wenzelm@12347
   203
local
wenzelm@12347
   204
wenzelm@54742
   205
fun gen_rule_tac tac ctxt rules facts =
wenzelm@18841
   206
  (fn i => fn st =>
wenzelm@18841
   207
    if null facts then tac rules i st
wenzelm@58950
   208
    else
wenzelm@58950
   209
      Seq.maps (fn rule => (tac o single) rule i st)
wenzelm@58950
   210
        (Drule.multi_resolves (SOME ctxt) facts rules))
wenzelm@54742
   211
  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
wenzelm@7130
   212
wenzelm@54742
   213
fun gen_arule_tac tac ctxt j rules facts =
wenzelm@54742
   214
  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
wenzelm@10744
   215
wenzelm@54742
   216
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
wenzelm@11785
   217
  let
wenzelm@11785
   218
    val rules =
wenzelm@11785
   219
      if not (null arg_rules) then arg_rules
wenzelm@33369
   220
      else flat (Context_Rules.find_rules false facts goal ctxt)
wenzelm@54742
   221
  in trace ctxt rules; tac ctxt rules facts i end);
wenzelm@10309
   222
wenzelm@54742
   223
fun meth tac x y = METHOD (HEADGOAL o tac x y);
wenzelm@54742
   224
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
wenzelm@8220
   225
wenzelm@7419
   226
in
wenzelm@7419
   227
wenzelm@52732
   228
val rule_tac = gen_rule_tac resolve_tac;
wenzelm@10744
   229
val rule = meth rule_tac;
wenzelm@10744
   230
val some_rule_tac = gen_some_rule_tac rule_tac;
wenzelm@54742
   231
val some_rule = meth some_rule_tac;
wenzelm@10744
   232
wenzelm@52732
   233
val erule = meth' (gen_arule_tac eresolve_tac);
wenzelm@52732
   234
val drule = meth' (gen_arule_tac dresolve_tac);
wenzelm@52732
   235
val frule = meth' (gen_arule_tac forward_tac);
wenzelm@5824
   236
wenzelm@7419
   237
end;
wenzelm@7419
   238
wenzelm@7419
   239
haftmann@25270
   240
(* intros_tac -- pervasive search spanned by intro rules *)
haftmann@25270
   241
ballarin@36093
   242
fun gen_intros_tac goals intros facts =
ballarin@36093
   243
  goals (insert_tac facts THEN'
haftmann@25270
   244
      REPEAT_ALL_NEW (resolve_tac intros))
haftmann@25270
   245
    THEN Tactic.distinct_subgoals_tac;
haftmann@25270
   246
ballarin@36093
   247
val intros_tac = gen_intros_tac ALLGOALS;
ballarin@36093
   248
val try_intros_tac = gen_intros_tac TRYALL;
haftmann@25270
   249
wenzelm@37216
   250
wenzelm@58016
   251
wenzelm@58016
   252
(** method syntax **)
wenzelm@58016
   253
wenzelm@58016
   254
(* context data *)
wenzelm@8351
   255
wenzelm@58016
   256
structure Data = Generic_Data
wenzelm@26472
   257
(
wenzelm@58016
   258
  type T =
wenzelm@58016
   259
    ((Token.src -> Proof.context -> method) * string) Name_Space.table *  (*methods*)
wenzelm@58018
   260
    (morphism -> thm list -> tactic) option;  (*ML tactic*)
wenzelm@58016
   261
  val empty : T = (Name_Space.empty_table "method", NONE);
wenzelm@58016
   262
  val extend = I;
wenzelm@58016
   263
  fun merge ((tab, tac), (tab', tac')) : T =
wenzelm@58016
   264
    (Name_Space.merge_tables (tab, tab'), merge_options (tac, tac'));
wenzelm@26472
   265
);
wenzelm@26472
   266
wenzelm@58016
   267
val get_methods = fst o Data.get;
wenzelm@58016
   268
val map_methods = Data.map o apfst;
wenzelm@58016
   269
wenzelm@58016
   270
wenzelm@58016
   271
(* ML tactic *)
wenzelm@58016
   272
wenzelm@58016
   273
val set_tactic = Data.map o apsnd o K o SOME;
wenzelm@58016
   274
wenzelm@58016
   275
fun the_tactic context =
wenzelm@58016
   276
  (case snd (Data.get context) of
wenzelm@58016
   277
    SOME tac => tac
wenzelm@58016
   278
  | NONE => raise Fail "Undefined ML tactic");
wenzelm@8351
   279
wenzelm@58018
   280
val parse_tactic =
wenzelm@58018
   281
  Scan.state :|-- (fn context =>
wenzelm@58018
   282
    Scan.lift (Args.text_declaration (fn source =>
wenzelm@58018
   283
      let
wenzelm@58018
   284
        val context' = context |>
wenzelm@58018
   285
          ML_Context.expression (#pos source)
wenzelm@58024
   286
            "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
wenzelm@58018
   287
            "Method.set_tactic tactic" (ML_Lex.read_source false source);
wenzelm@58018
   288
        val tac = the_tactic context';
wenzelm@58018
   289
      in
wenzelm@58018
   290
        fn phi =>
wenzelm@58018
   291
          set_tactic (fn _ => Context.setmp_thread_data (SOME context) (tac phi))
wenzelm@58018
   292
      end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
wenzelm@8351
   293
wenzelm@8351
   294
wenzelm@17110
   295
(* method text *)
wenzelm@17110
   296
wenzelm@55765
   297
datatype combinator_info = Combinator_Info of {keywords: Position.T list};
wenzelm@55765
   298
fun combinator_info keywords = Combinator_Info {keywords = keywords};
wenzelm@55765
   299
val no_combinator_info = combinator_info [];
wenzelm@55765
   300
wenzelm@58005
   301
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int;
wenzelm@58005
   302
wenzelm@17110
   303
datatype text =
wenzelm@58011
   304
  Source of Token.src |
wenzelm@32193
   305
  Basic of Proof.context -> method |
wenzelm@58005
   306
  Combinator of combinator_info * combinator * text list;
wenzelm@55765
   307
wenzelm@58006
   308
fun map_source f (Source src) = Source (f src)
wenzelm@58006
   309
  | map_source _ (Basic meth) = Basic meth
wenzelm@58006
   310
  | map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts);
wenzelm@58006
   311
wenzelm@54883
   312
fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
wenzelm@32193
   313
val succeed_text = Basic (K succeed);
wenzelm@58011
   314
val default_text = Source (Token.src ("default", Position.none) []);
wenzelm@32193
   315
val this_text = Basic (K this);
wenzelm@32193
   316
val done_text = Basic (K (SIMPLE_METHOD all_tac));
wenzelm@52059
   317
fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
wenzelm@17110
   318
wenzelm@49846
   319
fun finish_text (NONE, immed) = Basic (finish immed)
wenzelm@58005
   320
  | finish_text (SOME txt, immed) =
wenzelm@58005
   321
      Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]);
wenzelm@17110
   322
wenzelm@17110
   323
wenzelm@17110
   324
(* method definitions *)
wenzelm@5824
   325
wenzelm@57937
   326
fun transfer_methods ctxt =
wenzelm@57935
   327
  let
wenzelm@58016
   328
    val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt));
wenzelm@58016
   329
    val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
wenzelm@58016
   330
  in Context.proof_map (map_methods (K meths')) ctxt end;
wenzelm@55742
   331
wenzelm@55742
   332
fun print_methods ctxt =
wenzelm@22846
   333
  let
wenzelm@58016
   334
    val meths = get_methods (Context.Proof ctxt);
wenzelm@50301
   335
    fun prt_meth (name, (_, "")) = Pretty.mark_str name
wenzelm@42813
   336
      | prt_meth (name, (_, comment)) =
wenzelm@50301
   337
          Pretty.block
wenzelm@50301
   338
            (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
wenzelm@22846
   339
  in
wenzelm@56052
   340
    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
wenzelm@56334
   341
    |> Pretty.writeln_chunks
wenzelm@22846
   342
  end;
wenzelm@7611
   343
wenzelm@57935
   344
wenzelm@57935
   345
(* define *)
wenzelm@57935
   346
wenzelm@57935
   347
fun define_global binding meth comment thy =
wenzelm@57935
   348
  let
wenzelm@57935
   349
    val context = Context.Theory thy;
wenzelm@57935
   350
    val (name, meths') =
wenzelm@58016
   351
      Name_Space.define context true (binding, (meth, comment)) (get_methods context);
wenzelm@58016
   352
  in (name, Context.the_theory (map_methods (K meths') context)) end;
wenzelm@57935
   353
wenzelm@57941
   354
fun define binding meth comment =
wenzelm@57941
   355
  Local_Theory.background_theory_result (define_global binding meth comment)
wenzelm@57941
   356
  #-> (fn name =>
wenzelm@57941
   357
    Local_Theory.map_contexts (K transfer_methods)
wenzelm@58016
   358
    #> Local_Theory.generic_alias map_methods binding name
wenzelm@57941
   359
    #> pair name);
wenzelm@31304
   360
wenzelm@55997
   361
wenzelm@55997
   362
(* check *)
wenzelm@55997
   363
wenzelm@58016
   364
fun check_name ctxt =
wenzelm@58016
   365
  let val context = Context.Proof ctxt
wenzelm@58016
   366
  in #1 o Name_Space.check context (get_methods context) end;
wenzelm@58016
   367
wenzelm@58016
   368
fun check_src ctxt src =
wenzelm@58016
   369
  Token.check_src ctxt (get_methods (Context.Proof ctxt)) src;
wenzelm@55997
   370
wenzelm@55997
   371
wenzelm@30512
   372
(* method setup *)
wenzelm@30512
   373
wenzelm@57935
   374
fun method_syntax scan src ctxt : method =
wenzelm@58011
   375
  let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
wenzelm@57935
   376
wenzelm@57935
   377
fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
wenzelm@57935
   378
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
wenzelm@17356
   379
wenzelm@55828
   380
fun method_setup name source cmt =
wenzelm@57941
   381
  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
wenzelm@57941
   382
    ML_Lex.read_source false source @
wenzelm@57941
   383
    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
wenzelm@57941
   384
  |> ML_Context.expression (#pos source)
wenzelm@30544
   385
    "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
wenzelm@57941
   386
    "Context.map_proof (Method.local_setup name scan comment)"
wenzelm@57941
   387
  |> Context.proof_map;
wenzelm@17356
   388
wenzelm@17356
   389
wenzelm@58006
   390
(* prepare methods *)
wenzelm@58006
   391
wenzelm@58006
   392
fun method ctxt =
wenzelm@58016
   393
  let val table = get_methods (Context.Proof ctxt)
wenzelm@58011
   394
  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
wenzelm@58006
   395
wenzelm@58006
   396
fun method_closure ctxt0 src0 =
wenzelm@58006
   397
  let
wenzelm@58026
   398
    val (src1, _) = check_src ctxt0 src0;
wenzelm@58011
   399
    val src2 = Token.init_assignable_src src1;
wenzelm@58006
   400
    val ctxt = Context_Position.not_really ctxt0;
wenzelm@58006
   401
    val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
wenzelm@58011
   402
  in Token.closure_src src2 end;
wenzelm@58006
   403
wenzelm@58006
   404
fun method_cmd ctxt = method ctxt o method_closure ctxt;
wenzelm@58006
   405
wenzelm@58006
   406
wenzelm@58003
   407
(* evaluate method text *)
wenzelm@58003
   408
wenzelm@58003
   409
local
wenzelm@58003
   410
wenzelm@58003
   411
fun APPEND_CASES (meth: cases_tactic) (cases, st) =
wenzelm@58003
   412
  meth st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
wenzelm@58003
   413
wenzelm@58003
   414
fun BYPASS_CASES (tac: tactic) (cases, st) =
wenzelm@58003
   415
  tac st |> Seq.map (pair cases);
wenzelm@58003
   416
wenzelm@58003
   417
val op THEN = Seq.THEN;
wenzelm@58003
   418
wenzelm@58003
   419
fun SELECT_GOALS n method =
wenzelm@58003
   420
  BYPASS_CASES
wenzelm@58003
   421
    (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1)
wenzelm@58003
   422
  THEN method
wenzelm@58003
   423
  THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1));
wenzelm@58003
   424
wenzelm@58005
   425
fun COMBINATOR1 comb [meth] = comb meth
wenzelm@58005
   426
  | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
wenzelm@58005
   427
wenzelm@58005
   428
fun combinator Then = Seq.EVERY
wenzelm@58005
   429
  | combinator Orelse = Seq.FIRST
wenzelm@58005
   430
  | combinator Try = COMBINATOR1 Seq.TRY
wenzelm@58005
   431
  | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
wenzelm@58005
   432
  | combinator (Select_Goals n) = COMBINATOR1 (SELECT_GOALS n);
wenzelm@58003
   433
wenzelm@58003
   434
in
wenzelm@58003
   435
wenzelm@58007
   436
fun evaluate text ctxt =
wenzelm@58003
   437
  let
wenzelm@58007
   438
    fun eval (Basic meth) = APPEND_CASES o meth ctxt
wenzelm@58007
   439
      | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
wenzelm@58005
   440
      | eval (Combinator (_, c, txts)) =
wenzelm@58005
   441
          let
wenzelm@58005
   442
            val comb = combinator c;
wenzelm@58007
   443
            val meths = map eval txts;
wenzelm@58007
   444
          in fn facts => comb (map (fn meth => meth facts) meths) end;
wenzelm@58003
   445
    val meth = eval text;
wenzelm@58007
   446
  in fn facts => fn st => meth facts ([], st) end;
wenzelm@58003
   447
wenzelm@58003
   448
end;
wenzelm@58003
   449
wenzelm@58003
   450
wenzelm@5884
   451
wenzelm@17110
   452
(** concrete syntax **)
wenzelm@5824
   453
wenzelm@58048
   454
(* type modifier *)
wenzelm@58048
   455
wenzelm@58048
   456
type modifier =
wenzelm@58048
   457
  {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T};
wenzelm@5824
   458
wenzelm@58048
   459
fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
wenzelm@58048
   460
wenzelm@58048
   461
wenzelm@58048
   462
(* sections *)
wenzelm@7268
   463
wenzelm@7268
   464
local
wenzelm@7268
   465
wenzelm@58048
   466
fun sect (modifier : modifier parser) = Scan.depend (fn context =>
wenzelm@58068
   467
  Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier Parse.xthm) >>
wenzelm@58068
   468
    (fn ((tok, {init, attribute, pos}), xthms) =>
wenzelm@58029
   469
      let
wenzelm@58068
   470
        val decl =
wenzelm@58068
   471
          (case Token.get_value tok of
wenzelm@58068
   472
            SOME (Token.Declaration decl) => decl
wenzelm@58068
   473
          | _ =>
wenzelm@58068
   474
              let
wenzelm@58068
   475
                val ctxt = Context.proof_of context;
wenzelm@58068
   476
                fun prep_att src =
wenzelm@58068
   477
                  let
wenzelm@58068
   478
                    val src' = Attrib.check_src ctxt src;
wenzelm@58068
   479
                    val _ = List.app (Token.assign NONE) (Token.args_of_src src');
wenzelm@58068
   480
                  in src' end;
wenzelm@58068
   481
                val thms =
wenzelm@58068
   482
                  map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms;
wenzelm@58068
   483
                val facts =
wenzelm@58068
   484
                  Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
wenzelm@58068
   485
                  |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
wenzelm@58068
   486
                val _ =
wenzelm@58068
   487
                  Context_Position.report ctxt (Token.pos_of tok)
wenzelm@58068
   488
                    (Markup.entity Markup.method_modifierN ""
wenzelm@58068
   489
                      |> Markup.properties (Position.def_properties_of pos));
wenzelm@58068
   490
                fun decl phi =
wenzelm@58068
   491
                  Context.mapping I init #>
wenzelm@58068
   492
                  Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
wenzelm@58068
   493
                val _ = Token.assign (SOME (Token.Declaration decl)) tok;
wenzelm@58068
   494
              in decl end);
wenzelm@58068
   495
      in (Morphism.form decl context, decl) end));
wenzelm@5824
   496
wenzelm@30540
   497
in
wenzelm@30540
   498
wenzelm@58029
   499
val section = sect o Scan.first;
wenzelm@58029
   500
val sections = Scan.repeat o section;
wenzelm@5824
   501
wenzelm@7268
   502
end;
wenzelm@7268
   503
wenzelm@5824
   504
wenzelm@30515
   505
(* extra rule methods *)
wenzelm@30515
   506
wenzelm@54742
   507
fun xrule_meth meth =
wenzelm@36950
   508
  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
wenzelm@54742
   509
  (fn (n, ths) => fn ctxt => meth ctxt n ths);
wenzelm@30515
   510
wenzelm@30515
   511
wenzelm@55761
   512
(* text range *)
wenzelm@55761
   513
wenzelm@55761
   514
type text_range = text * Position.range;
wenzelm@55761
   515
wenzelm@55761
   516
fun text NONE = NONE
wenzelm@55761
   517
  | text (SOME (txt, _)) = SOME txt;
wenzelm@55761
   518
wenzelm@55761
   519
fun position NONE = Position.none
wenzelm@55761
   520
  | position (SOME (_, (pos, _))) = pos;
wenzelm@55761
   521
wenzelm@55761
   522
wenzelm@55795
   523
(* reports *)
wenzelm@55795
   524
wenzelm@55795
   525
local
wenzelm@55795
   526
wenzelm@55795
   527
fun keyword_positions (Source _) = []
wenzelm@55795
   528
  | keyword_positions (Basic _) = []
wenzelm@58005
   529
  | keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) =
wenzelm@58005
   530
      keywords @ maps keyword_positions texts;
wenzelm@55795
   531
wenzelm@55795
   532
in
wenzelm@55795
   533
wenzelm@55795
   534
fun reports_of ((text, (pos, _)): text_range) =
wenzelm@55795
   535
  (pos, Markup.language_method) ::
wenzelm@55917
   536
    maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs ""))
wenzelm@55917
   537
      (keyword_positions text);
wenzelm@55795
   538
wenzelm@55795
   539
val report = Position.reports o reports_of;
wenzelm@55795
   540
wenzelm@55795
   541
end;
wenzelm@55795
   542
wenzelm@55795
   543
wenzelm@27813
   544
(* outer parser *)
wenzelm@27813
   545
wenzelm@27813
   546
fun is_symid_meth s =
wenzelm@36959
   547
  s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
wenzelm@27813
   548
wenzelm@27813
   549
local
wenzelm@27813
   550
wenzelm@27813
   551
fun meth4 x =
wenzelm@58011
   552
 (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) ||
wenzelm@55048
   553
  Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
wenzelm@58011
   554
    Source (Token.src ("cartouche", Token.pos_of tok) [tok])) ||
wenzelm@36950
   555
  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
wenzelm@27813
   556
and meth3 x =
wenzelm@55765
   557
 (meth4 -- Parse.position (Parse.$$$ "?")
wenzelm@58005
   558
    >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
wenzelm@55765
   559
  meth4 -- Parse.position (Parse.$$$ "+")
wenzelm@58005
   560
    >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
wenzelm@55765
   561
  meth4 --
wenzelm@55765
   562
    (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
wenzelm@55765
   563
    >> (fn (m, (((_, pos1), n), (_, pos2))) =>
wenzelm@58005
   564
        Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
wenzelm@27813
   565
  meth4) x
wenzelm@27813
   566
and meth2 x =
wenzelm@58011
   567
 (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) ||
wenzelm@27813
   568
  meth3) x
wenzelm@55765
   569
and meth1 x =
wenzelm@55765
   570
  (Parse.enum1_positions "," meth2
wenzelm@58005
   571
    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
wenzelm@55765
   572
and meth0 x =
wenzelm@55765
   573
  (Parse.enum1_positions "|" meth1
wenzelm@58005
   574
    >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
wenzelm@27813
   575
wenzelm@49866
   576
in
wenzelm@49866
   577
wenzelm@49866
   578
val parse =
wenzelm@55709
   579
  Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
wenzelm@49866
   580
wenzelm@55761
   581
end;
wenzelm@27813
   582
wenzelm@27813
   583
wenzelm@18708
   584
(* theory setup *)
wenzelm@5824
   585
wenzelm@53171
   586
val _ = Theory.setup
wenzelm@56204
   587
 (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
wenzelm@56204
   588
  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
wenzelm@56204
   589
  setup @{binding "-"} (Scan.succeed (K insert_facts))
wenzelm@30515
   590
    "do nothing (insert current facts only)" #>
wenzelm@56204
   591
  setup @{binding insert} (Attrib.thms >> (K o insert))
wenzelm@30515
   592
    "insert theorems, ignoring facts (improper)" #>
wenzelm@58957
   593
  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
wenzelm@30515
   594
    "repeatedly apply introduction rules" #>
wenzelm@58957
   595
  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
wenzelm@30515
   596
    "repeatedly apply elimination rules" #>
wenzelm@56204
   597
  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
wenzelm@56204
   598
  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
wenzelm@56204
   599
  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
wenzelm@30515
   600
    "present local premises as object-level statements" #>
wenzelm@56204
   601
  setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
wenzelm@54742
   602
    "apply some intro/elim rule" #>
wenzelm@56204
   603
  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
wenzelm@56204
   604
  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
wenzelm@56204
   605
  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
wenzelm@56204
   606
  setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
wenzelm@56204
   607
  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
wenzelm@56204
   608
  setup @{binding assumption} (Scan.succeed assumption)
wenzelm@30515
   609
    "proof by assumption, preferring facts" #>
wenzelm@56204
   610
  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
wenzelm@52732
   611
    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
wenzelm@30515
   612
    "rename parameters of goal" #>
wenzelm@56204
   613
  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
wenzelm@52732
   614
    (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
wenzelm@30515
   615
      "rotate assumptions of goal" #>
wenzelm@58018
   616
  setup @{binding tactic} (parse_tactic >> (K o METHOD))
wenzelm@30515
   617
    "ML tactic as proof method" #>
wenzelm@58018
   618
  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac))
wenzelm@53171
   619
    "ML tactic as raw proof method");
wenzelm@5824
   620
wenzelm@5824
   621
wenzelm@16145
   622
(*final declarations of this structure!*)
wenzelm@16145
   623
val unfold = unfold_meth;
wenzelm@16145
   624
val fold = fold_meth;
wenzelm@16145
   625
wenzelm@5824
   626
end;
wenzelm@5824
   627
wenzelm@30508
   628
val METHOD_CASES = Method.METHOD_CASES;
wenzelm@30508
   629
val METHOD = Method.METHOD;
wenzelm@30508
   630
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
wenzelm@30508
   631
val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
wenzelm@30508
   632
val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
wenzelm@30508
   633