1(* Title: Pure/Isar/method.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Isar proof methods. 5*) 6 7signature METHOD = 8sig 9 type method = thm list -> context_tactic 10 val CONTEXT_METHOD: (thm list -> context_tactic) -> method 11 val METHOD: (thm list -> tactic) -> method 12 val fail: method 13 val succeed: method 14 val insert_tac: Proof.context -> thm list -> int -> tactic 15 val insert: thm list -> method 16 val SIMPLE_METHOD: tactic -> method 17 val SIMPLE_METHOD': (int -> tactic) -> method 18 val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method 19 val goal_cases_tac: string list -> context_tactic 20 val cheating: 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: Proof.context -> 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: Proof.context -> thm list -> thm list -> tactic 36 val try_intros_tac: Proof.context -> 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 val clean_facts: thm list -> thm list 43 val set_facts: thm list -> Proof.context -> Proof.context 44 val get_facts: Proof.context -> thm list 45 type combinator_info 46 val no_combinator_info: combinator_info 47 datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int 48 datatype text = 49 Source of Token.src | 50 Basic of Proof.context -> method | 51 Combinator of combinator_info * combinator * text list 52 val map_source: (Token.src -> Token.src) -> text -> text 53 val primitive_text: (Proof.context -> thm -> thm) -> text 54 val succeed_text: text 55 val standard_text: text 56 val this_text: text 57 val done_text: text 58 val sorry_text: bool -> text 59 val finish_text: text option * bool -> text 60 val print_methods: bool -> Proof.context -> unit 61 val check_name: Proof.context -> xstring * Position.T -> string 62 val check_src: Proof.context -> Token.src -> Token.src 63 val check_text: Proof.context -> text -> text 64 val checked_text: text -> bool 65 val method_syntax: (Proof.context -> method) context_parser -> 66 Token.src -> Proof.context -> method 67 val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory 68 val local_setup: binding -> (Proof.context -> method) context_parser -> string -> 69 local_theory -> local_theory 70 val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory 71 val method: Proof.context -> Token.src -> Proof.context -> method 72 val method_closure: Proof.context -> Token.src -> Token.src 73 val closure: bool Config.T 74 val method_cmd: Proof.context -> Token.src -> Proof.context -> method 75 val detect_closure_state: thm -> bool 76 val STATIC: (unit -> unit) -> context_tactic 77 val RUNTIME: context_tactic -> context_tactic 78 val sleep: Time.time -> context_tactic 79 val evaluate: text -> Proof.context -> method 80 val evaluate_runtime: text -> Proof.context -> method 81 type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T} 82 val modifier: attribute -> Position.T -> modifier 83 val old_section_parser: bool Config.T 84 val sections: modifier parser list -> unit context_parser 85 type text_range = text * Position.range 86 val text: text_range option -> text option 87 val position: text_range option -> Position.T 88 val reports_of: text_range -> Position.report list 89 val report: text_range -> unit 90 val parser: int -> text_range parser 91 val parse: text_range parser 92 val read: Proof.context -> Token.src -> text 93 val read_closure: Proof.context -> Token.src -> text * Token.src 94 val read_closure_input: Proof.context -> Input.source -> text * Token.src 95 val text_closure: text context_parser 96end; 97 98structure Method: METHOD = 99struct 100 101(** proof methods **) 102 103(* type method *) 104 105type method = thm list -> context_tactic; 106 107fun CONTEXT_METHOD tac : method = 108 fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac) #> Seq.maps_results (tac facts); 109 110fun METHOD tac : method = 111 fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac THEN tac facts); 112 113val fail = METHOD (K no_tac); 114val succeed = METHOD (K all_tac); 115 116 117(* insert facts *) 118 119fun insert_tac _ [] _ = all_tac 120 | insert_tac ctxt facts i = 121 EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts); 122 123fun insert thms = 124 CONTEXT_METHOD (fn _ => fn (ctxt, st) => 125 st |> ALLGOALS (insert_tac ctxt thms) |> TACTIC_CONTEXT ctxt); 126 127 128fun SIMPLE_METHOD tac = 129 CONTEXT_METHOD (fn facts => fn (ctxt, st) => 130 st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> TACTIC_CONTEXT ctxt); 131 132fun SIMPLE_METHOD'' quant tac = 133 CONTEXT_METHOD (fn facts => fn (ctxt, st) => 134 st |> quant (insert_tac ctxt facts THEN' tac) |> TACTIC_CONTEXT ctxt); 135 136val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; 137 138 139(* goals as cases *) 140 141fun goal_cases_tac case_names : context_tactic = 142 fn (ctxt, st) => 143 let 144 val cases = 145 (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names) 146 |> map (rpair [] o rpair []) 147 |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st)); 148 in CONTEXT_CASES cases all_tac (ctxt, st) end; 149 150 151(* cheating *) 152 153fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) => 154 if int orelse Config.get ctxt quick_and_dirty then 155 TACTIC_CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st) 156 else error "Cheating requires quick_and_dirty mode!"); 157 158 159(* unfold intro/elim rules *) 160 161fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths)); 162fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths)); 163 164 165(* unfold/fold definitions *) 166 167fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); 168fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); 169 170 171(* atomize rule statements *) 172 173fun atomize false ctxt = 174 SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt) 175 | atomize true ctxt = 176 Context_Tactic.CONTEXT_TACTIC o 177 K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); 178 179 180(* this -- resolve facts directly *) 181 182fun this ctxt = METHOD (EVERY o map (HEADGOAL o resolve_tac ctxt o single)); 183 184 185(* fact -- composition by facts from context *) 186 187fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt) 188 | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); 189 190 191(* assumption *) 192 193local 194 195fun cond_rtac ctxt cond rule = SUBGOAL (fn (prop, i) => 196 if cond (Logic.strip_assums_concl prop) 197 then resolve_tac ctxt [rule] i else no_tac); 198 199in 200 201fun assm_tac ctxt = 202 assume_tac ctxt APPEND' 203 Goal.assume_rule_tac ctxt APPEND' 204 cond_rtac ctxt (can Logic.dest_equals) Drule.reflexive_thm APPEND' 205 cond_rtac ctxt (can Logic.dest_term) Drule.termI; 206 207fun all_assm_tac ctxt = 208 let 209 fun tac i st = 210 if i > Thm.nprems_of st then all_tac st 211 else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st; 212 in tac 1 end; 213 214fun assumption ctxt = METHOD (HEADGOAL o 215 (fn [] => assm_tac ctxt 216 | [fact] => solve_tac ctxt [fact] 217 | _ => K no_tac)); 218 219fun finish immed ctxt = 220 METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); 221 222end; 223 224 225(* rule etc. -- single-step refinements *) 226 227val rule_trace = Attrib.setup_config_bool \<^binding>\<open>rule_trace\<close> (fn _ => false); 228 229fun trace ctxt rules = 230 if Config.get ctxt rule_trace andalso not (null rules) then 231 Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) 232 |> Pretty.string_of |> tracing 233 else (); 234 235local 236 237fun gen_rule_tac tac ctxt rules facts = 238 (fn i => fn st => 239 if null facts then tac ctxt rules i st 240 else 241 Seq.maps (fn rule => (tac ctxt o single) rule i st) 242 (Drule.multi_resolves (SOME ctxt) facts rules)) 243 THEN_ALL_NEW Goal.norm_hhf_tac ctxt; 244 245fun gen_arule_tac tac ctxt j rules facts = 246 EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); 247 248fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => 249 let 250 val rules = 251 if not (null arg_rules) then arg_rules 252 else flat (Context_Rules.find_rules ctxt false facts goal); 253 in trace ctxt rules; tac ctxt rules facts i end); 254 255fun meth tac x y = METHOD (HEADGOAL o tac x y); 256fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); 257 258in 259 260val rule_tac = gen_rule_tac resolve_tac; 261val rule = meth rule_tac; 262val some_rule_tac = gen_some_rule_tac rule_tac; 263val some_rule = meth some_rule_tac; 264 265val erule = meth' (gen_arule_tac eresolve_tac); 266val drule = meth' (gen_arule_tac dresolve_tac); 267val frule = meth' (gen_arule_tac forward_tac); 268 269end; 270 271 272(* intros_tac -- pervasive search spanned by intro rules *) 273 274fun gen_intros_tac goals ctxt intros facts = 275 goals (insert_tac ctxt facts THEN' 276 REPEAT_ALL_NEW (resolve_tac ctxt intros)) 277 THEN Tactic.distinct_subgoals_tac; 278 279val intros_tac = gen_intros_tac ALLGOALS; 280val try_intros_tac = gen_intros_tac TRYALL; 281 282 283 284(** method syntax **) 285 286(* context data *) 287 288structure Data = Generic_Data 289( 290 type T = 291 {methods: ((Token.src -> Proof.context -> method) * string) Name_Space.table, 292 ml_tactic: (morphism -> thm list -> tactic) option, 293 facts: thm list option}; 294 val empty : T = 295 {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE}; 296 val extend = I; 297 fun merge 298 ({methods = methods1, ml_tactic = ml_tactic1, facts = facts1}, 299 {methods = methods2, ml_tactic = ml_tactic2, facts = facts2}) : T = 300 {methods = Name_Space.merge_tables (methods1, methods2), 301 ml_tactic = merge_options (ml_tactic1, ml_tactic2), 302 facts = merge_options (facts1, facts2)}; 303); 304 305fun map_data f = Data.map (fn {methods, ml_tactic, facts} => 306 let val (methods', ml_tactic', facts') = f (methods, ml_tactic, facts) 307 in {methods = methods', ml_tactic = ml_tactic', facts = facts'} end); 308 309val get_methods = #methods o Data.get; 310 311val ops_methods = 312 {get_data = get_methods, 313 put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))}; 314 315 316(* ML tactic *) 317 318fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts)); 319 320fun the_tactic context = 321 (case #ml_tactic (Data.get context) of 322 SOME tac => tac 323 | NONE => raise Fail "Undefined ML tactic"); 324 325val parse_tactic = 326 Scan.state :|-- (fn context => 327 Scan.lift (Args.text_declaration (fn source => 328 let 329 val tac = 330 context 331 |> ML_Context.expression (Input.pos_of source) 332 (ML_Lex.read "Context.>> (Method.set_tactic (fn morphism: Morphism.morphism => fn facts: thm list => (" @ 333 ML_Lex.read_source source @ ML_Lex.read ")))") 334 |> the_tactic; 335 in 336 fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi)) 337 end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); 338 339 340(* method facts *) 341 342val clean_facts = filter_out Thm.is_dummy; 343 344fun set_facts facts = 345 (Context.proof_map o map_data) 346 (fn (methods, ml_tactic, _) => (methods, ml_tactic, SOME (clean_facts facts))); 347 348val get_facts_generic = these o #facts o Data.get; 349val get_facts = get_facts_generic o Context.Proof; 350 351val _ = 352 Theory.setup 353 (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", \<^here>), get_facts_generic)); 354 355 356(* method text *) 357 358datatype combinator_info = Combinator_Info of {keywords: Position.T list}; 359fun combinator_info keywords = Combinator_Info {keywords = keywords}; 360val no_combinator_info = combinator_info []; 361 362datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int; 363 364datatype text = 365 Source of Token.src | 366 Basic of Proof.context -> method | 367 Combinator of combinator_info * combinator * text list; 368 369fun map_source f (Source src) = Source (f src) 370 | map_source _ (Basic meth) = Basic meth 371 | map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); 372 373fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r); 374val succeed_text = Basic (K succeed); 375val standard_text = Source (Token.make_src ("standard", Position.none) []); 376val this_text = Basic this; 377val done_text = Basic (K (SIMPLE_METHOD all_tac)); 378fun sorry_text int = Basic (fn _ => cheating int); 379 380fun finish_text (NONE, immed) = Basic (finish immed) 381 | finish_text (SOME txt, immed) = 382 Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); 383 384 385(* method definitions *) 386 387fun print_methods verbose ctxt = 388 let 389 val meths = get_methods (Context.Proof ctxt); 390 fun prt_meth (name, (_, "")) = Pretty.mark_str name 391 | prt_meth (name, (_, comment)) = 392 Pretty.block 393 (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); 394 in 395 [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))] 396 |> Pretty.writeln_chunks 397 end; 398 399 400(* define *) 401 402fun define_global binding meth comment = 403 Entity.define_global ops_methods binding (meth, comment); 404 405fun define binding meth comment = 406 Entity.define ops_methods binding (meth, comment); 407 408 409(* check *) 410 411fun check_name ctxt = 412 let val context = Context.Proof ctxt 413 in #1 o Name_Space.check context (get_methods context) end; 414 415fun check_src ctxt = 416 #1 o Token.check_src ctxt (get_methods o Context.Proof); 417 418fun check_text ctxt (Source src) = Source (check_src ctxt src) 419 | check_text _ (Basic m) = Basic m 420 | check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body); 421 422fun checked_text (Source src) = Token.checked_src src 423 | checked_text (Basic _) = true 424 | checked_text (Combinator (_, _, body)) = forall checked_text body; 425 426 427(* method setup *) 428 429fun method_syntax scan src ctxt : method = 430 let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end; 431 432fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd; 433fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd; 434 435fun method_setup binding source comment = 436 ML_Context.expression (Input.pos_of source) 437 (ML_Lex.read 438 ("Theory.local_setup (Method.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @ 439 ML_Lex.read_source source @ ML_Lex.read (")" ^ ML_Syntax.print_string comment ^ ")")) 440 |> Context.proof_map; 441 442 443(* prepare methods *) 444 445fun method ctxt = 446 let val table = get_methods (Context.Proof ctxt) 447 in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; 448 449fun method_closure ctxt src = 450 let 451 val src' = map Token.init_assignable src; 452 val ctxt' = Context_Position.not_really ctxt; 453 val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm)); 454 in map Token.closure src' end; 455 456val closure = Config.declare_bool ("Method.closure", \<^here>) (K true); 457 458fun method_cmd ctxt = 459 check_src ctxt #> 460 Config.get ctxt closure ? method_closure ctxt #> 461 method ctxt; 462 463 464(* static vs. runtime state *) 465 466fun detect_closure_state st = 467 (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) st)) of 468 NONE => false 469 | SOME t => Term.is_dummy_pattern t); 470 471fun STATIC test : context_tactic = 472 fn (ctxt, st) => 473 if detect_closure_state st then (test (); Seq.single (Seq.Result (ctxt, st))) else Seq.empty; 474 475fun RUNTIME (tac: context_tactic) (ctxt, st) = 476 if detect_closure_state st then Seq.empty else tac (ctxt, st); 477 478fun sleep t = RUNTIME (fn ctxt_st => (OS.Process.sleep t; Seq.single (Seq.Result ctxt_st))); 479 480 481(* evaluate method text *) 482 483local 484 485val op THEN = Seq.THEN; 486 487fun BYPASS_CONTEXT (tac: tactic) = 488 fn result => 489 (case result of 490 Seq.Error _ => Seq.single result 491 | Seq.Result (ctxt, st) => tac st |> TACTIC_CONTEXT ctxt); 492 493val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac); 494 495fun RESTRICT_GOAL i n method = 496 BYPASS_CONTEXT (PRIMITIVE (Goal.restrict i n)) THEN 497 method THEN 498 BYPASS_CONTEXT (PRIMITIVE (Goal.unrestrict i)); 499 500fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method; 501 502fun (method1 THEN_ALL_NEW method2) i (result : context_state Seq.result) = 503 (case result of 504 Seq.Error _ => Seq.single result 505 | Seq.Result (_, st) => 506 result |> method1 i 507 |> Seq.maps (fn result' => 508 (case result' of 509 Seq.Error _ => Seq.single result' 510 | Seq.Result (_, st') => 511 result' |> Seq.INTERVAL method2 i (i + Thm.nprems_of st' - Thm.nprems_of st)))) 512 513fun COMBINATOR1 comb [meth] = comb meth 514 | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; 515 516fun combinator Then = Seq.EVERY 517 | combinator Then_All_New = 518 (fn [] => Seq.single 519 | methods => 520 preparation THEN (foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)) 521 | combinator Orelse = Seq.FIRST 522 | combinator Try = COMBINATOR1 Seq.TRY 523 | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 524 | combinator (Select_Goals n) = 525 COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method); 526 527in 528 529fun evaluate text ctxt0 facts = 530 let 531 val ctxt = set_facts facts ctxt0; 532 fun eval0 m = Seq.single #> Seq.maps_results (m facts); 533 fun eval (Basic m) = eval0 (m ctxt) 534 | eval (Source src) = eval0 (method_cmd ctxt src ctxt) 535 | eval (Combinator (_, c, txts)) = combinator c (map eval txts); 536 in eval text o Seq.Result end; 537 538end; 539 540fun evaluate_runtime text ctxt = 541 let 542 val text' = 543 text |> (map_source o map o Token.map_facts) 544 (fn SOME name => 545 (case Proof_Context.lookup_fact ctxt name of 546 SOME {dynamic = true, thms} => K thms 547 | _ => I) 548 | NONE => I); 549 val ctxt' = Config.put closure false ctxt; 550 in fn facts => RUNTIME (fn st => evaluate text' ctxt' facts st) end; 551 552 553 554(** concrete syntax **) 555 556(* type modifier *) 557 558type modifier = 559 {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}; 560 561fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos}; 562 563 564(* sections *) 565 566val old_section_parser = Config.declare_bool ("Method.old_section_parser", \<^here>) (K false); 567 568local 569 570fun thms ss = 571 Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm); 572 573fun app {init, attribute, pos = _} ths context = 574 fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context); 575 576fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- 577 (fn (m, ths) => Scan.succeed (swap (app m ths context)))); 578 579in 580 581fun old_sections ss = Scan.repeat (section ss) >> K (); 582 583end; 584 585local 586 587fun sect (modifier : modifier parser) = Scan.depend (fn context => 588 Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.thm) 589 >> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) => 590 let 591 val decl = 592 (case Token.get_value tok0 of 593 SOME (Token.Declaration decl) => decl 594 | _ => 595 let 596 val ctxt = Context.proof_of context; 597 val prep_att = Attrib.check_src ctxt #> map (Token.assign NONE); 598 val thms = 599 map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms; 600 val facts = 601 Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)] 602 |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs)); 603 604 fun decl phi = 605 Context.mapping I init #> 606 Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; 607 608 val modifier_report = 609 (#1 (Token.range_of modifier_toks), 610 Markup.properties (Position.def_properties_of pos) 611 (Markup.entity Markup.method_modifierN "")); 612 val _ = 613 Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0); 614 val _ = Token.assign (SOME (Token.Declaration decl)) tok0; 615 in decl end); 616 in (Morphism.form decl context, decl) end)); 617 618in 619 620fun sections ss = 621 Args.context :|-- (fn ctxt => 622 if Config.get ctxt old_section_parser then old_sections ss 623 else Scan.repeat (sect (Scan.first ss)) >> K ()); 624 625end; 626 627 628(* extra rule methods *) 629 630fun xrule_meth meth = 631 Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >> 632 (fn (n, ths) => fn ctxt => meth ctxt n ths); 633 634 635(* text range *) 636 637type text_range = text * Position.range; 638 639fun text NONE = NONE 640 | text (SOME (txt, _)) = SOME txt; 641 642fun position NONE = Position.none 643 | position (SOME (_, (pos, _))) = pos; 644 645 646(* reports *) 647 648local 649 650fun keyword_positions (Source _) = [] 651 | keyword_positions (Basic _) = [] 652 | keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = 653 keywords @ maps keyword_positions texts; 654 655in 656 657fun reports_of ((text, (pos, _)): text_range) = 658 (pos, Markup.language_method) :: 659 maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs "")) 660 (keyword_positions text); 661 662val report = Position.reports o reports_of; 663 664end; 665 666 667(* parser *) 668 669local 670 671fun is_symid_meth s = 672 s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s; 673 674in 675 676fun parser pri = 677 let 678 val meth_name = Parse.token Parse.name; 679 680 fun meth5 x = 681 (meth_name >> (Source o single) || 682 Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => 683 Source (Token.make_src ("cartouche", Position.none) [tok])) || 684 Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x 685 and meth4 x = 686 (meth5 -- Parse.position (Parse.$$$ "?") 687 >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || 688 meth5 -- Parse.position (Parse.$$$ "+") 689 >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || 690 meth5 -- (Parse.position (Parse.$$$ "[") -- 691 Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) 692 >> (fn (m, (((_, pos1), n), (_, pos2))) => 693 Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || 694 meth5) x 695 and meth3 x = 696 (meth_name ::: Parse.args1 is_symid_meth >> Source || 697 meth4) x 698 and meth2 x = 699 (Parse.enum1_positions "," meth3 700 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x 701 and meth1 x = 702 (Parse.enum1_positions ";" meth2 703 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x 704 and meth0 x = 705 (Parse.enum1_positions "|" meth1 706 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; 707 708 val meth = 709 nth [meth0, meth1, meth2, meth3, meth4, meth5] pri 710 handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri); 711 in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end; 712 713val parse = parser 4; 714 715end; 716 717 718(* read method text *) 719 720fun read ctxt src = 721 (case Scan.read Token.stopper (Parse.!!! (parser 0 --| Scan.ahead Parse.eof)) src of 722 SOME (text, range) => 723 if checked_text text then text 724 else (report (text, range); check_text ctxt text) 725 | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src)))); 726 727fun read_closure ctxt src0 = 728 let 729 val src1 = map Token.init_assignable src0; 730 val text = read ctxt src1 |> map_source (method_closure ctxt); 731 val src2 = map Token.closure src1; 732 in (text, src2) end; 733 734fun read_closure_input ctxt input = 735 let val syms = Input.source_explode input in 736 (case Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.many Token.not_eof) syms of 737 SOME res => read_closure ctxt res 738 | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) 739 end; 740 741val text_closure = 742 Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) => 743 (case Token.get_value tok of 744 SOME (Token.Source src) => read ctxt src 745 | _ => 746 let 747 val (text, src) = read_closure_input ctxt (Token.input_of tok); 748 val _ = Token.assign (SOME (Token.Source src)) tok; 749 in text end)); 750 751 752(* theory setup *) 753 754val _ = Theory.setup 755 (setup \<^binding>\<open>fail\<close> (Scan.succeed (K fail)) "force failure" #> 756 setup \<^binding>\<open>succeed\<close> (Scan.succeed (K succeed)) "succeed" #> 757 setup \<^binding>\<open>sleep\<close> (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s))) 758 "succeed after delay (in seconds)" #> 759 setup \<^binding>\<open>-\<close> (Scan.succeed (K (SIMPLE_METHOD all_tac))) 760 "insert current facts, nothing else" #> 761 setup \<^binding>\<open>goal_cases\<close> (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ => 762 CONTEXT_METHOD (fn _ => fn (ctxt, st) => 763 (case drop (Thm.nprems_of st) names of 764 [] => NONE 765 | bad => 766 if detect_closure_state st then NONE 767 else 768 SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^ 769 Position.here (#1 (Token.range_of bad))))) 770 |> (fn SOME msg => Seq.single (Seq.Error msg) 771 | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st))))) 772 "bind cases for goals" #> 773 setup \<^binding>\<open>subproofs\<close> (text_closure >> (Context_Tactic.SUBPROOFS ooo evaluate_runtime)) 774 "apply proof method to subproofs with closed derivation" #> 775 setup \<^binding>\<open>insert\<close> (Attrib.thms >> (K o insert)) 776 "insert theorems, ignoring facts" #> 777 setup \<^binding>\<open>intro\<close> (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) 778 "repeatedly apply introduction rules" #> 779 setup \<^binding>\<open>elim\<close> (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) 780 "repeatedly apply elimination rules" #> 781 setup \<^binding>\<open>unfold\<close> (Attrib.thms >> unfold_meth) "unfold definitions" #> 782 setup \<^binding>\<open>fold\<close> (Attrib.thms >> fold_meth) "fold definitions" #> 783 setup \<^binding>\<open>atomize\<close> (Scan.lift (Args.mode "full") >> atomize) 784 "present local premises as object-level statements" #> 785 setup \<^binding>\<open>rule\<close> (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths)) 786 "apply some intro/elim rule" #> 787 setup \<^binding>\<open>erule\<close> (xrule_meth erule) "apply rule in elimination manner (improper)" #> 788 setup \<^binding>\<open>drule\<close> (xrule_meth drule) "apply rule in destruct manner (improper)" #> 789 setup \<^binding>\<open>frule\<close> (xrule_meth frule) "apply rule in forward manner (improper)" #> 790 setup \<^binding>\<open>this\<close> (Scan.succeed this) "apply current facts as rules" #> 791 setup \<^binding>\<open>fact\<close> (Attrib.thms >> fact) "composition by facts from context" #> 792 setup \<^binding>\<open>assumption\<close> (Scan.succeed assumption) 793 "proof by assumption, preferring facts" #> 794 setup \<^binding>\<open>rename_tac\<close> (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> 795 (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) 796 "rename parameters of goal" #> 797 setup \<^binding>\<open>rotate_tac\<close> (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> 798 (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) 799 "rotate assumptions of goal" #> 800 setup \<^binding>\<open>tactic\<close> (parse_tactic >> (K o METHOD)) 801 "ML tactic as proof method" #> 802 setup \<^binding>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => Context_Tactic.CONTEXT_TACTIC o tac)) 803 "ML tactic as raw proof method" #> 804 setup \<^binding>\<open>use\<close> 805 (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >> 806 (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms)) 807 "indicate method facts and context for method expression"); 808 809 810(*final declarations of this structure!*) 811val unfold = unfold_meth; 812val fold = fold_meth; 813 814end; 815 816val CONTEXT_METHOD = Method.CONTEXT_METHOD; 817val METHOD = Method.METHOD; 818val SIMPLE_METHOD = Method.SIMPLE_METHOD; 819val SIMPLE_METHOD' = Method.SIMPLE_METHOD'; 820val SIMPLE_METHOD'' = Method.SIMPLE_METHOD''; 821