src/Pure/Isar/method.ML
changeset 9539 7ff8f3516d54
parent 9485 e56577a63005
child 9565 3eb2ea15cc69
     1.1 --- a/src/Pure/Isar/method.ML	Fri Aug 04 23:00:15 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 04 23:01:39 2000 +0200
     1.3 @@ -56,7 +56,8 @@
     1.4    val tactic: string -> Proof.context -> Proof.method
     1.5    exception METHOD_FAIL of (string * Position.T) * exn
     1.6    val method: theory -> Args.src -> Proof.context -> Proof.method
     1.7 -  val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string -> theory -> theory
     1.8 +  val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string
     1.9 +    -> theory -> theory
    1.10    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    1.11      -> theory -> theory
    1.12    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.13 @@ -107,6 +108,10 @@
    1.14    val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.15    val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.16    val global_done_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.17 +  val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
    1.18 +    -> Args.src -> Proof.context -> Proof.method
    1.19 +  val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
    1.20 +    -> ('a -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    1.21    val setup: (theory -> theory) list
    1.22  end;
    1.23  
    1.24 @@ -340,9 +345,9 @@
    1.25  fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);
    1.26  
    1.27  
    1.28 -(* res_inst_tac emulations *)
    1.29 +(* res_inst_tac etc. *)
    1.30  
    1.31 -(*Note: insts refer to the implicit (!) goal context; use at your own risk*)
    1.32 +(*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
    1.33  fun gen_res_inst tac (quant, (insts, thm)) =
    1.34    METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm)));
    1.35  
    1.36 @@ -350,6 +355,7 @@
    1.37  val eres_inst = gen_res_inst Tactic.eres_inst_tac;
    1.38  val dres_inst = gen_res_inst Tactic.dres_inst_tac;
    1.39  val forw_inst = gen_res_inst Tactic.forw_inst_tac;
    1.40 +val cut_inst = gen_res_inst Tactic.cut_inst_tac;
    1.41  
    1.42  
    1.43  (* simple Prolog interpreter *)
    1.44 @@ -500,21 +506,20 @@
    1.45  end;
    1.46  
    1.47  
    1.48 -(* insts *)
    1.49 +(* tactic syntax *)
    1.50  
    1.51  val insts =
    1.52 -  Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --
    1.53 -    (Scan.lift (Args.$$$ "in") |-- Attrib.local_thm);
    1.54 +  Scan.optional
    1.55 +    (Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --|
    1.56 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thm;
    1.57  
    1.58  fun inst_args f = f oo (#2 oo syntax (Args.goal_spec HEADGOAL -- insts));
    1.59  
    1.60  
    1.61 -(* subgoal *)
    1.62 +fun goal_args' args tac = #2 oo syntax (Args.goal_spec HEADGOAL -- args >>
    1.63 +  (fn (quant, s) => METHOD (fn facts => quant (insert_tac facts THEN' tac s))));
    1.64  
    1.65 -fun subgoal x = (Args.goal_spec HEADGOAL -- Scan.lift Args.name >>
    1.66 -  (fn (quant, s) => METHOD (fn facts => quant (insert_tac facts THEN' Tactic.subgoal_tac s)))) x;
    1.67 -
    1.68 -val subgoal_meth = #2 oo syntax subgoal;
    1.69 +fun goal_args args tac = goal_args' (Scan.lift args) tac;
    1.70  
    1.71  
    1.72  
    1.73 @@ -600,27 +605,37 @@
    1.74  
    1.75  (** theory setup **)
    1.76  
    1.77 +(* misc tactic emulations *)
    1.78 +
    1.79 +val subgoal_meth = goal_args (Scan.repeat1 Args.name) Tactic.subgoals_tac;
    1.80 +val thin_meth = goal_args Args.name Tactic.thin_tac;
    1.81 +val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
    1.82 +
    1.83 +
    1.84  (* pure_methods *)
    1.85  
    1.86  val pure_methods =
    1.87   [("fail", no_args fail, "force failure"),
    1.88    ("succeed", no_args succeed, "succeed"),
    1.89    ("-", no_args insert_facts, "do nothing, inserting current facts only"),
    1.90 -  ("insert", thms_args insert, "insert theorems, ignoring facts (improper!)"),
    1.91 +  ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
    1.92    ("unfold", thms_args unfold, "unfold definitions"),
    1.93    ("fold", thms_args fold, "fold definitions"),
    1.94    ("default", thms_ctxt_args some_rule, "apply some rule"),
    1.95    ("rule", thms_ctxt_args some_rule, "apply some rule"),
    1.96 -  ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper!)"),
    1.97 -  ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper!)"),
    1.98 -  ("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper!)"),
    1.99 +  ("erule", thms_ctxt_args some_erule, "apply some rule in elimination manner (improper)"),
   1.100 +  ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper)"),
   1.101 +  ("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper)"),
   1.102    ("this", no_args this, "apply current facts as rules"),
   1.103    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
   1.104 -  ("res_inst_tac", inst_args res_inst, "res_inst_tac emulation (dynamic instantiation!)"),
   1.105 -  ("eres_inst_tac", inst_args eres_inst, "eres_inst_tac emulation (dynamic instantiation!)"),
   1.106 -  ("dres_inst_tac", inst_args dres_inst, "dres_inst_tac emulation (dynamic instantiation!)"),
   1.107 -  ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (dynamic instantiation!)"),
   1.108 +  ("rule_tac", inst_args res_inst, "apply rule (dynamic instantiation!)"),
   1.109 +  ("erule_tac", inst_args eres_inst, "apply rule in elimination manner (dynamic instantiation!)"),
   1.110 +  ("drule_tac", inst_args dres_inst, "apply rule in destruct manner (dynamic instantiation!)"),
   1.111 +  ("frule_tac", inst_args forw_inst, "apply rule in forward manner (dynamic instantiation!)"),
   1.112 +  ("cut_tac", inst_args cut_inst, "cut rule (dynamic instantiation!)"),
   1.113    ("subgoal_tac", subgoal_meth, "subgoal_tac emulation (dynamic instantiation!)"),
   1.114 +  ("thin_tac", thin_meth, "thin_tac emulation (dynamic instantiation!)"),
   1.115 +  ("rename_tac", rename_meth, "rename_tac emulation (dynamic instantiation!)"),
   1.116    ("prolog", thms_args prolog, "simple prolog interpreter"),
   1.117    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
   1.118