src/Pure/Isar/method.ML
changeset 6404 2daaf2943c79
parent 6108 2c9ed58c30ba
child 6500 68ba555ac59a
     1.1 --- a/src/Pure/Isar/method.ML	Thu Mar 18 16:44:53 1999 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 19 11:24:00 1999 +0100
     1.3 @@ -49,17 +49,19 @@
     1.4      Try of text |
     1.5      Repeat of text |
     1.6      Repeat1 of text
     1.7 -  val dynamic_method: string -> (Proof.context -> Proof.method)
     1.8    val refine: text -> Proof.state -> Proof.state Seq.seq
     1.9    val tac: text -> Proof.state -> Proof.state Seq.seq
    1.10    val then_tac: text -> Proof.state -> Proof.state Seq.seq
    1.11    val proof: text option -> Proof.state -> Proof.state Seq.seq
    1.12 -  val end_block: Proof.state -> Proof.state Seq.seq
    1.13 -  val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    1.14 -  val immediate_proof: Proof.state -> Proof.state Seq.seq
    1.15 -  val default_proof: Proof.state -> Proof.state Seq.seq
    1.16 -  val qed: bstring option -> theory attribute list option -> Proof.state
    1.17 -    -> theory * (string * string * thm)
    1.18 +  val local_qed: text option -> Proof.state -> Proof.state Seq.seq
    1.19 +  val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    1.20 +  val local_immediate_proof: Proof.state -> Proof.state Seq.seq
    1.21 +  val local_default_proof: Proof.state -> Proof.state Seq.seq
    1.22 +  val global_qed: bstring option -> theory attribute list option -> text option
    1.23 +    -> Proof.state -> theory * (string * string * thm)
    1.24 +  val global_terminal_proof: text -> Proof.state -> theory * (string * string * thm)
    1.25 +  val global_immediate_proof: Proof.state -> theory * (string * string * thm)
    1.26 +  val global_default_proof: Proof.state -> theory * (string * string * thm)
    1.27    val setup: (theory -> theory) list
    1.28  end;
    1.29  
    1.30 @@ -241,12 +243,6 @@
    1.31    Repeat1 of text;
    1.32  
    1.33  
    1.34 -(* dynamic methods *)
    1.35 -
    1.36 -fun dynamic_method name = (fn ctxt =>
    1.37 -  method (ProofContext.theory_of ctxt) (Args.src ((name, []), Position.none)) ctxt);
    1.38 -
    1.39 -
    1.40  (* refine *)
    1.41  
    1.42  fun refine text state =
    1.43 @@ -262,6 +258,8 @@
    1.44        | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
    1.45    in eval text state end;
    1.46  
    1.47 +fun named_method name = Source (Args.src ((name, []), Position.none));
    1.48 +
    1.49  
    1.50  (* unstructured steps *)
    1.51  
    1.52 @@ -276,27 +274,28 @@
    1.53    |> refine text;
    1.54  
    1.55  
    1.56 -(* proof steps *)
    1.57 +(* structured proof steps *)
    1.58  
    1.59 -val default_txt = Source (Args.src (("default", []), Position.none));
    1.60 -val finishN = "finish";
    1.61 +val default_text = named_method "default";
    1.62 +val finish_text = named_method "finish";
    1.63  
    1.64  fun proof opt_text state =
    1.65    state
    1.66    |> Proof.assert_backward
    1.67 -  |> refine (if_none opt_text default_txt)
    1.68 +  |> refine (if_none opt_text default_text)
    1.69    |> Seq.map Proof.enter_forward;
    1.70  
    1.71 -
    1.72 -(* conclusions *)
    1.73 -
    1.74 -val end_block = Proof.end_block (dynamic_method finishN);
    1.75 +fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
    1.76 +fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None);
    1.77 +val local_immediate_proof = local_terminal_proof (Basic (K same));
    1.78 +val local_default_proof = local_terminal_proof default_text;
    1.79  
    1.80 -fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
    1.81 -val immediate_proof = terminal_proof (Basic (K same));
    1.82 -val default_proof = terminal_proof default_txt;
    1.83 +fun global_qed alt_name alt_atts opt_text =
    1.84 +  Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
    1.85  
    1.86 -val qed = Proof.qed (dynamic_method finishN);
    1.87 +fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
    1.88 +val global_immediate_proof = global_terminal_proof (Basic (K same));
    1.89 +val global_default_proof = global_terminal_proof default_text;
    1.90  
    1.91  
    1.92