50 val erule: int -> thm list -> method |
50 val erule: int -> thm list -> method |
51 val drule: int -> thm list -> method |
51 val drule: int -> thm list -> method |
52 val frule: int -> thm list -> method |
52 val frule: int -> thm list -> method |
53 val iprover_tac: Proof.context -> int option -> int -> tactic |
53 val iprover_tac: Proof.context -> int option -> int -> tactic |
54 val set_tactic: (Proof.context -> thm list -> tactic) -> unit |
54 val set_tactic: (Proof.context -> thm list -> tactic) -> unit |
55 val tactic: string -> Proof.context -> method |
55 val tactic: string * Position.T -> Proof.context -> method |
56 type src |
56 type src |
57 datatype text = |
57 datatype text = |
58 Basic of (Proof.context -> method) * Position.T | |
58 Basic of (Proof.context -> method) * Position.T | |
59 Source of src | |
59 Source of src | |
60 Source_i of src | |
60 Source_i of src | |
74 val method_i: theory -> src -> Proof.context -> method |
74 val method_i: theory -> src -> Proof.context -> method |
75 val add_methods: (bstring * (src -> Proof.context -> method) * string) list |
75 val add_methods: (bstring * (src -> Proof.context -> method) * string) list |
76 -> theory -> theory |
76 -> theory -> theory |
77 val add_method: bstring * (src -> Proof.context -> method) * string |
77 val add_method: bstring * (src -> Proof.context -> method) * string |
78 -> theory -> theory |
78 -> theory -> theory |
79 val method_setup: bstring * string * string -> theory -> theory |
79 val method_setup: bstring -> string * Position.T -> string -> theory -> theory |
80 val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) |
80 val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) |
81 -> src -> Proof.context -> 'a * Proof.context |
81 -> src -> Proof.context -> 'a * Proof.context |
82 val simple_args: (Args.T list -> 'a * Args.T list) |
82 val simple_args: (Args.T list -> 'a * Args.T list) |
83 -> ('a -> Proof.context -> method) -> src -> Proof.context -> method |
83 -> ('a -> Proof.context -> method) -> src -> Proof.context -> method |
84 val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method |
84 val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method |
351 (* ML tactics *) |
351 (* ML tactics *) |
352 |
352 |
353 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic); |
353 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic); |
354 fun set_tactic f = tactic_ref := f; |
354 fun set_tactic f = tactic_ref := f; |
355 |
355 |
356 fun ml_tactic txt ctxt = NAMED_CRITICAL "ML" (fn () => |
356 fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () => |
357 (ML_Context.use_mltext |
357 (ML_Context.use_mltext false pos |
358 ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n" |
358 ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n" |
359 ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt)); |
359 ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt)); |
360 ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt))); |
360 ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt))); |
361 |
361 |
362 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
362 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
363 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
363 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
364 |
364 |
444 val add_method = add_methods o Library.single; |
444 val add_method = add_methods o Library.single; |
445 |
445 |
446 |
446 |
447 (* method_setup *) |
447 (* method_setup *) |
448 |
448 |
449 fun method_setup (name, txt, cmt) = |
449 fun method_setup name (txt, pos) cmt = |
450 ML_Context.use_let |
450 ML_Context.use_let pos |
451 "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string" |
451 "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string" |
452 "Context.map_theory (Method.add_method method)" |
452 "Context.map_theory (Method.add_method method)" |
453 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")") |
453 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")") |
454 |> Context.theory_map; |
454 |> Context.theory_map; |
455 |
455 |
575 ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), |
575 ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), |
576 ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac, |
576 ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac, |
577 "rename parameters of goal"), |
577 "rename parameters of goal"), |
578 ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac, |
578 ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac, |
579 "rotate assumptions of goal"), |
579 "rotate assumptions of goal"), |
580 ("tactic", simple_args Args.name tactic, "ML tactic as proof method"), |
580 ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"), |
581 ("raw_tactic", simple_args Args.name raw_tactic, "ML tactic as raw proof method")]); |
581 ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]); |
582 |
582 |
583 |
583 |
584 (* outer parser *) |
584 (* outer parser *) |
585 |
585 |
586 local |
586 local |