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