src/Pure/Isar/method.ML
changeset 8372 7b2cec1e789c
parent 8351 1b8ac0f48233
child 8381 4fc7e63781f6
     1.1 --- a/src/Pure/Isar/method.ML	Wed Mar 08 17:56:43 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 08 17:58:37 2000 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4    val intro_local: Proof.context attribute
     1.5    val delrule_local: Proof.context attribute
     1.6    val METHOD: (thm list -> tactic) -> Proof.method
     1.7 +  val METHOD_CASES:
     1.8 +    (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method
     1.9    val METHOD0: tactic -> Proof.method
    1.10    val fail: Proof.method
    1.11    val succeed: Proof.method
    1.12 @@ -37,8 +39,9 @@
    1.13    val fold: thm list -> Proof.method
    1.14    val multi_resolve: thm list -> thm -> thm Seq.seq
    1.15    val multi_resolves: thm list -> thm list -> thm Seq.seq
    1.16 -  val multi_resolveq: thm list -> thm Seq.seq -> thm Seq.seq
    1.17    val resolveq_tac: thm Seq.seq -> int -> tactic
    1.18 +  val resolveq_cases_tac: (thm * string list) Seq.seq
    1.19 +    -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
    1.20    val rule_tac: thm list -> thm list -> int -> tactic
    1.21    val rule: thm list -> Proof.method
    1.22    val erule: thm list -> Proof.method
    1.23 @@ -193,9 +196,11 @@
    1.24  
    1.25  (** proof methods **)
    1.26  
    1.27 -(* method from tactic *)
    1.28 +(* make methods *)
    1.29  
    1.30  val METHOD = Proof.method;
    1.31 +val METHOD_CASES = Proof.method_cases;
    1.32 +
    1.33  fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts");
    1.34  
    1.35  
    1.36 @@ -251,24 +256,28 @@
    1.37  in
    1.38  
    1.39  val multi_resolve = multi_res 1;
    1.40 -fun multi_resolveq facts rules = Seq.flat (Seq.map (multi_resolve facts) rules);
    1.41 -fun multi_resolves facts = multi_resolveq facts o Seq.of_list;
    1.42 +fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
    1.43  
    1.44  end;
    1.45  
    1.46  
    1.47 -(* rule *)
    1.48 +(* general rule *)
    1.49  
    1.50  fun gen_resolveq_tac tac rules i st =
    1.51 -  Seq.flat (Seq.map (fn rule => tac [rule] i st) rules);
    1.52 +  Seq.flat (Seq.map (fn rule => tac rule i st) rules);
    1.53 +
    1.54 +val resolveq_tac = gen_resolveq_tac Tactic.rtac;
    1.55  
    1.56 -val resolveq_tac = gen_resolveq_tac Tactic.resolve_tac;
    1.57 +val resolveq_cases_tac = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
    1.58 +  Seq.map (rpair (RuleCases.make rule cases)) (Tactic.rtac rule i st));
    1.59  
    1.60  
    1.61 +(* simple rule *)
    1.62 +
    1.63  local
    1.64  
    1.65  fun gen_rule_tac tac rules [] = tac rules
    1.66 -  | gen_rule_tac tac erules facts = gen_resolveq_tac tac (multi_resolves facts erules);
    1.67 +  | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
    1.68  
    1.69  fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);
    1.70  
    1.71 @@ -336,10 +345,12 @@
    1.72  fun set_tactic f = tactic_ref := f;
    1.73  
    1.74  fun tactic txt ctxt = METHOD (fn facts =>
    1.75 -  (Context.use_mltext
    1.76 -    ("let fun (tactic: Proof.context -> thm list -> tactic) ctxt facts = " ^ txt ^
    1.77 -     "in Method.set_tactic tactic end")
    1.78 -    false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));
    1.79 + (Context.use_mltext
    1.80 +   ("let fun (tactic: Proof.context -> thm list -> tactic) ctxt facts = \
    1.81 +    \let val thm = ProofContext.get_thm ctxt and thms = ProofContext.get_thms ctxt in\n"
    1.82 +    ^ txt ^
    1.83 +    "\nend in Method.set_tactic tactic end")
    1.84 +  false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));
    1.85  
    1.86  
    1.87