src/Pure/Isar/method.ML
changeset 6981 eaade7e398a7
parent 6951 13399b560e4e
child 7130 a17f7b5ac40f
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jul 12 22:25:39 1999 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jul 12 22:27:20 1999 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val succeed: Proof.method
     1.5    val same_tac: thm list -> int -> tactic
     1.6    val same: Proof.method
     1.7 +  val assumption_tac: thm list -> int -> tactic
     1.8    val assumption: Proof.method
     1.9    val forward_chain: thm list -> thm list -> thm Seq.seq
    1.10    val rule_tac: thm list -> thm list -> int -> tactic
    1.11 @@ -55,13 +56,15 @@
    1.12    val tac: text -> Proof.state -> Proof.state Seq.seq
    1.13    val then_tac: text -> Proof.state -> Proof.state Seq.seq
    1.14    val proof: text option -> Proof.state -> Proof.state Seq.seq
    1.15 -  val local_qed: text option -> ({kind: string, name: string, thm: thm} -> unit)
    1.16 -    -> Proof.state -> Proof.state Seq.seq
    1.17 -  val local_terminal_proof: text * text option -> ({kind: string, name: string, thm: thm} -> unit)
    1.18 +  val local_qed: text option
    1.19 +    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.20      -> Proof.state -> Proof.state Seq.seq
    1.21 -  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit)
    1.22 +  val local_terminal_proof: text * text option
    1.23 +    -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.24      -> Proof.state -> Proof.state Seq.seq
    1.25 -  val local_default_proof: ({kind: string, name: string, thm: thm} -> unit)
    1.26 +  val local_immediate_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.27 +    -> Proof.state -> Proof.state Seq.seq
    1.28 +  val local_default_proof: ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.29      -> Proof.state -> Proof.state Seq.seq
    1.30    val global_qed: text option -> Proof.state -> theory * {kind: string, name: string, thm: thm}
    1.31    val global_terminal_proof: text * text option
    1.32 @@ -95,16 +98,24 @@
    1.33  val succeed = METHOD (K all_tac);
    1.34  
    1.35  
    1.36 -(* same, assumption *)
    1.37 +(* same *)
    1.38  
    1.39 -fun same_tac [] = K all_tac
    1.40 -  | same_tac facts =
    1.41 -      let val r = ~ (length facts);
    1.42 -      in metacuts_tac facts THEN' rotate_tac r end;
    1.43 +fun cut_rule_tac raw_rule =
    1.44 +  let
    1.45 +    val rule = Drule.forall_intr_vars raw_rule;
    1.46 +    val revcut_rl = Drule.incr_indexes_wrt [] [] [] [rule] Drule.revcut_rl;
    1.47 +  in Tactic.rtac (rule COMP revcut_rl) THEN' Tactic.rotate_tac ~1 end;
    1.48 +
    1.49 +fun same_tac [] i = all_tac
    1.50 +  | same_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
    1.51  
    1.52  val same = METHOD (ALLGOALS o same_tac);
    1.53 -val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));
    1.54 +
    1.55  
    1.56 +(* assumption *)
    1.57 +
    1.58 +fun assumption_tac facts = same_tac facts THEN' assume_tac;
    1.59 +val assumption = METHOD (FIRSTGOAL o assumption_tac);
    1.60  val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));
    1.61  
    1.62