# HG changeset patch
# User wenzelm
# Date 1124356667 -7200
# Node ID 736f4b7841a83de707141de336f0e60dff716a89
# Parent  d2ea9c974570acd6e5ca0b4305afe02a06300378
moved after method.ML;
moved FINDGOAL/HEADGOAL to method.ML;
moved type method to method.ML;
prepare attributes here;
tuned various interfaces (cf. isar_thy.ML);
tuned;

diff -r d2ea9c974570 -r 736f4b7841a8 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Aug 18 11:17:46 2005 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Aug 18 11:17:47 2005 +0200
@@ -5,21 +5,13 @@
 The Isar/VM proof language interpreter.
 *)
 
-signature BASIC_PROOF =
-sig
-  val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
-end;
-
 signature PROOF =
 sig
-  include BASIC_PROOF
   type context
+  type method
   type state
-  datatype mode = Forward | ForwardChain | Backward
   exception STATE of string * state
-  val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
-  val init_state: theory -> state
+  val init: theory -> state
   val context_of: state -> context
   val theory_of: state -> theory
   val sign_of: state -> theory    (*obsolete*)
@@ -32,64 +24,63 @@
   val thisN: string
   val get_goal: state -> context * (thm list * thm)
   val goal_facts: (state -> thm list) -> state -> state
-  val get_mode: state -> mode
   val is_chain: state -> bool
   val assert_forward: state -> state
   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
+  val level: state -> int
   val show_main_goal: bool ref
   val verbose: bool ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
-  val level: state -> int
-  type method
-  val method: (thm list -> tactic) -> method
-  val method_cases: (thm list -> RuleCases.tactic) -> method
-  val refine: (context -> method) -> state -> state Seq.seq
-  val refine_end: (context -> method) -> state -> state Seq.seq
+  val refine: Method.text -> state -> state Seq.seq
+  val refine_end: Method.text -> state -> state Seq.seq
   val match_bind: (string list * string) list -> state -> state
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
   val simple_note_thms: string -> thm list -> state -> state
-  val note_thmss: ((bstring * context attribute list) *
-    (thmref * context attribute list) list) list -> state -> state
+  val note_thmss: ((bstring * Attrib.src list) *
+    (thmref * Attrib.src list) list) list -> state -> state
   val note_thmss_i: ((bstring * context attribute list) *
     (thm list * context attribute list) list) list -> state -> state
-  val with_thmss: ((bstring * context attribute list) *
-    (thmref * context attribute list) list) list -> state -> state
-  val with_thmss_i: ((bstring * context attribute list) *
-    (thm list * context attribute list) list) list -> state -> state
-  val using_thmss: ((thmref * context attribute list) list) list -> state -> state
+  val from_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+  val from_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+  val with_thmss: ((thmref * Attrib.src list) list) list -> state -> state
+  val with_thmss_i: ((thm list * context attribute list) list) list -> state -> state
+  val using_thmss: ((thmref * Attrib.src list) list) list -> state -> state
   val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
   val fix: (string list * string option) list -> state -> state
   val fix_i: (string list * typ option) list -> state -> state
   val assm: ProofContext.exporter
-    -> ((string * context attribute list) * (string * (string list * string list)) list) list
+    -> ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> state -> state
   val assm_i: ProofContext.exporter
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val assume:
-    ((string * context attribute list) * (string * (string list * string list)) list) list
+    ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> state -> state
   val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val presume:
-    ((string * context attribute list) * (string * (string list * string list)) list) list
+    ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> state -> state
   val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val def: string -> context attribute list -> string *  (string * string list) -> state -> state
-  val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
-  val invoke_case: string * string option list * context attribute list -> state -> state
+  val def: string * Attrib.src list -> string *  (string * string list) -> state -> state
+  val def_i: string * context attribute list -> string * (term * term list) -> state -> state
+  val invoke_case: string * string option list * Attrib.src list -> state -> state
+  val invoke_case_i: string * string option list * context attribute list -> state -> state
+  val chain: state -> state
+  val from_facts: thm list -> state -> state
   val multi_theorem: string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> context -> context -> thm -> thm) ->
     (xstring * (Attrib.src list * Attrib.src list list)) option ->
-    bstring * theory attribute list -> Locale.element Locale.elem_expr list
-    -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
+    bstring * Attrib.src list -> Locale.element Locale.elem_expr list
+    -> ((bstring * Attrib.src list) * (string * (string list * string list)) list) list
     -> theory -> state
   val multi_theorem_i: string -> (thm list * thm list -> theory -> theory) ->
     (cterm list -> context -> context -> thm -> thm) ->
@@ -98,26 +89,46 @@
     -> Locale.element_i Locale.elem_expr list
     -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
     -> theory -> state
-  val chain: state -> state
-  val from_facts: thm list -> state -> state
   val show: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
-    -> ((string * context attribute list) * (string * (string list * string list)) list) list
+    -> ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> bool -> state -> state
   val show_i: (bool -> state -> state) -> (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> bool -> state -> state
   val have: (thm list -> state -> state Seq.seq) -> bool
-    -> ((string * context attribute list) * (string * (string list * string list)) list) list
+    -> ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> state -> state
   val have_i: (thm list -> state -> state Seq.seq) -> bool
     -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val at_bottom: state -> bool
-  val local_qed: (state -> state Seq.seq)
-    -> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
-    -> state -> state Seq.seq
-  val global_qed: (state -> state Seq.seq) -> state
-    -> (theory * ((string * string) * (string * thm list) list)) Seq.seq
+  val local_qed: bool -> Method.text option
+    -> (context -> string * (string * thm list) list -> unit) *
+      (context -> thm -> unit) -> state -> state Seq.seq
+  val global_qed: bool -> Method.text option
+    -> state -> (theory * context) * ((string * string) * (string * thm list) list)
+  val proof: Method.text option -> state -> state Seq.seq
+  val local_terminal_proof: Method.text * Method.text option
+    -> (context -> string * (string * thm list) list -> unit) *
+      (context -> thm -> unit) -> state -> state Seq.seq
+  val local_default_proof: (context -> string * (string * thm list) list -> unit) *
+    (context -> thm -> unit) -> state -> state Seq.seq
+  val local_immediate_proof: (context -> string * (string * thm list) list -> unit) *
+    (context -> thm -> unit) -> state -> state Seq.seq
+  val local_done_proof: (context -> string * (string * thm list) list -> unit) *
+    (context -> thm -> unit) -> state -> state Seq.seq
+  val global_terminal_proof: Method.text * Method.text option
+    -> state -> (theory * context) * ((string * string) * (string * thm list) list)
+  val global_default_proof: state ->
+    (theory * context) * ((string * string) * (string * thm list) list)
+  val global_immediate_proof: state ->
+    (theory * context) * ((string * string) * (string * thm list) list)
+  val global_done_proof: state ->
+    (theory * context) * ((string * string) * (string * thm list) list)
+  val defer: int option -> state -> state Seq.seq
+  val prefer: int -> state -> state Seq.seq
+  val apply: Method.text -> state -> state Seq.seq
+  val apply_end: Method.text -> state -> state Seq.seq
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state Seq.seq
@@ -127,6 +138,7 @@
 struct
 
 type context = ProofContext.context;
+type method = Method.method;
 
 
 (** proof state **)
@@ -161,8 +173,8 @@
 
 (* type mode *)
 
-datatype mode = Forward | ForwardChain | Backward;
-val mode_name = (fn Forward => "state" | ForwardChain => "chain" | Backward => "prove");
+datatype mode = Forward | Chain | Backward;
+val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
 
 
 (* datatype state *)
@@ -175,12 +187,12 @@
     goal: (goal * (after_qed * bool)) option}
 and state =
   State of
-    node *              (*current*)
-    node list           (*parents wrt. block structure*)
+    node *              (*current node*)
+    node list           (*parent nodes wrt. block structure*)
 and after_qed =
   AfterQed of
-   (thm list -> state -> state Seq.seq) *
-   (thm list * thm list -> theory -> theory);
+   (thm list -> state -> state Seq.seq) *      (*after local qed*)
+   (thm list * thm list -> theory -> theory);  (*after global qed*)
 
 fun make_node (context, facts, mode, goal) =
   Node {context = context, facts = facts, mode = mode, goal = goal};
@@ -191,16 +203,11 @@
 fun err_malformed name state =
   raise STATE (name ^ ": internal error -- malformed proof state", state);
 
-fun check_result msg state sq =
-  (case Seq.pull sq of
-    NONE => raise STATE (msg, state)
-  | SOME s_sq => Seq.cons s_sq);
-
 
 fun map_current f (State (Node {context, facts, mode, goal}, nodes)) =
   State (make_node (f (context, facts, mode, goal)), nodes);
 
-fun init_state thy =
+fun init thy =
   State (make_node (ProofContext.init thy, NONE, Forward, NONE), []);
 
 
@@ -253,16 +260,17 @@
 
 val reset_facts = put_facts NONE;
 
-fun these_factss (state, named_factss) =
-  state |> put_facts (SOME (List.concat (map snd named_factss)));
+fun these_factss more_facts (state, named_factss) =
+  state |> put_facts (SOME (List.concat (map snd named_factss) @ more_facts));
 
 
 (* goal *)
 
 local
   fun find i (state as State (Node {goal = SOME goal, ...}, _)) = (context_of state, (i, goal))
-    | find i (State (Node {goal = NONE, ...}, node :: nodes)) = find (i + 1) (State (node, nodes))
-    | find _ (state as State (_, [])) = err_malformed "find_goal" state;
+    | find i (State (Node {goal = NONE, ...}, node :: nodes)) =
+        find (i + 1) (State (node, nodes))
+    | find _ (state as State (_, [])) = raise STATE ("No goal present", state);
 in val find_goal = find 0 end;
 
 fun get_goal state =
@@ -294,7 +302,7 @@
 fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
 
 val enter_forward = put_mode Forward;
-val enter_forward_chain = put_mode ForwardChain;
+val enter_forward_chain = put_mode Chain;
 val enter_backward = put_mode Backward;
 
 fun assert_mode pred state =
@@ -304,11 +312,11 @@
       ^ quote (mode_name mode) ^ " mode", state)
   end;
 
-fun is_chain state = get_mode state = ForwardChain;
+fun is_chain state = get_mode state = Chain;
 val assert_forward = assert_mode (equal Forward);
-val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain);
+val assert_forward_or_chain = assert_mode (equal Forward orf equal Chain);
 val assert_backward = assert_mode (equal Backward);
-val assert_no_chain = assert_mode (not_equal ForwardChain);
+val assert_no_chain = assert_mode (not_equal Chain);
 
 
 (* blocks *)
@@ -332,7 +340,6 @@
 val show_main_goal = ref false;
 val verbose = ProofContext.verbose;
 
-
 val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp;
 
 fun pretty_facts _ _ NONE = []
@@ -375,7 +382,7 @@
      (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
      (if ! verbose orelse mode = Forward then
        (pretty_facts "" ctxt facts @ prt_goal (find_goal state))
-      else if mode = ForwardChain then pretty_facts "picking " ctxt facts
+      else if mode = Chain then pretty_facts "picking " ctxt facts
       else prt_goal (find_goal state))
   in prts end;
 
@@ -387,14 +394,6 @@
 
 (** proof steps **)
 
-(* datatype method *)
-
-datatype method = Method of thm list -> RuleCases.tactic;
-
-fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
-val method_cases = Method;
-
-
 (* refine goal *)
 
 local
@@ -411,12 +410,12 @@
   if subthy (thy, theory_of state) then state
   else raise STATE ("Bad theory of method result: " ^ Context.str_of_thy thy, state);
 
-fun gen_refine current_context meth_fun state =
+fun apply_method current_context meth_fun state =
   let
     val (goal_ctxt, (_, ((result, (facts, st)), x))) = find_goal state;
-    val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
+    val meth = meth_fun (if current_context then context_of state else goal_ctxt);
   in
-    meth facts st |> Seq.map (fn (st', meth_cases) =>
+    Method.apply meth facts st |> Seq.map (fn (st', meth_cases) =>
       state
       |> check_theory (Thm.theory_of_thm st')
       |> map_goal
@@ -424,23 +423,26 @@
           (K ((result, (facts, st')), x)))
   end;
 
+fun apply_text cc text state =
+  let
+    val thy = theory_of state;
+
+    fun eval (Method.Basic m) = apply_method cc m
+      | eval (Method.Source src) = apply_method cc (Method.method thy src)
+      | eval (Method.Then txts) = Seq.EVERY (map eval txts)
+      | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
+      | eval (Method.Try txt) = Seq.TRY (eval txt)
+      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt);
+  in eval text state end;
+
 in
 
-val refine = gen_refine true;
-val refine_end = gen_refine false;
+val refine = apply_text true;
+val refine_end = apply_text false;
 
 end;
 
 
-(* goal addressing *)
-
-fun FINDGOAL tac st =
-  let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n))
-  in find (1, Thm.nprems_of st) st end;
-
-fun HEADGOAL tac = tac 1;
-
-
 (* export results *)
 
 fun refine_tac rule =
@@ -507,9 +509,9 @@
 
 (*** structured proof commands ***)
 
-(** context **)
+(** context elements **)
 
-(* bind *)
+(* bindings *)
 
 local
 
@@ -529,70 +531,14 @@
 end;
 
 
-(* note_thmss *)
-
-local
-
-fun gen_note_thmss f args state =
-  state
-  |> assert_forward
-  |> map_context_result (f args)
-  |> these_factss;
-
-in
-
-val note_thmss = gen_note_thmss ProofContext.note_thmss;
-val note_thmss_i = gen_note_thmss ProofContext.note_thmss_i;
-
-fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
-
-end;
-
-
-(* with_thmss *)
+(* fixes *)
 
 local
 
-fun gen_with_thmss f args state =
-  let val state' = state |> f args
-  in state' |> simple_note_thms "" (the_facts state' @ the_facts state) end;
-
-in
-
-val with_thmss = gen_with_thmss note_thmss;
-val with_thmss_i = gen_with_thmss note_thmss_i;
-
-end;
-
-
-(* using_thmss *)
-
-local
-
-fun gen_using_thmss f args state =
-  state
-  |> assert_backward
-  |> map_context_result (f (map (pair ("", [])) args))
-  |> (fn (st, named_facts) =>
-    let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
-    in st |> map_goal I (K ((result, (facts @ List.concat (map snd named_facts), thm)), x)) end);
-
-in
-
-val using_thmss = gen_using_thmss ProofContext.note_thmss;
-val using_thmss_i = gen_using_thmss ProofContext.note_thmss_i;
-
-end;
-
-
-(* fix *)
-
-local
-
-fun gen_fix f args state =
+fun gen_fix fix_ctxt args state =
   state
   |> assert_forward
-  |> map_context (f args)
+  |> map_context (fix_ctxt args)
   |> reset_facts;
 
 in
@@ -603,46 +549,46 @@
 end;
 
 
-(* assume and presume *)
+(* assumptions *)
 
 local
 
-fun gen_assume f exp args state =
+fun gen_assume asm prep_att exp args state =
   state
   |> assert_forward
-  |> map_context_result (f exp args)
-  |> these_factss;
+  |> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args))
+  |> these_factss [];
 
 in
 
-val assm = gen_assume ProofContext.assume;
-val assm_i = gen_assume ProofContext.assume_i;
-val assume = assm ProofContext.export_assume;
-val assume_i = assm_i ProofContext.export_assume;
-val presume = assm ProofContext.export_presume;
+val assm      = gen_assume ProofContext.assume Attrib.local_attribute;
+val assm_i    = gen_assume ProofContext.assume_i (K I);
+val assume    = assm ProofContext.export_assume;
+val assume_i  = assm_i ProofContext.export_assume;
+val presume   = assm ProofContext.export_presume;
 val presume_i = assm_i ProofContext.export_presume;
 
 end;
 
 
-
-(** local definitions **)
+(* local definitions *)
 
 local
 
-fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
+fun gen_def fix prep_att prep_term prep_pats
+    (raw_name, raw_atts) (x, (raw_rhs, raw_pats)) state =
   let
     val _ = assert_forward state;
+    val thy = theory_of state;
     val ctxt = context_of state;
 
-    (*rhs*)
-    val name = if raw_name = "" then Thm.def_name x else raw_name;
     val rhs = prep_term ctxt raw_rhs;
     val T = Term.fastype_of rhs;
     val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats;
+    val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
 
-    (*lhs*)
-    val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
+    val name = if raw_name = "" then Thm.def_name x else raw_name;
+    val atts = map (prep_att thy) raw_atts;
   in
     state
     |> fix [([x], NONE)]
@@ -652,32 +598,14 @@
 
 in
 
-val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats;
-val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats;
+val def = gen_def fix Attrib.local_attribute ProofContext.read_term ProofContext.read_term_pats;
+val def_i = gen_def fix_i (K I) ProofContext.cert_term ProofContext.cert_term_pats;
 
 end;
 
 
-(* invoke_case *)
 
-fun invoke_case (name, xs, atts) state =
-  let
-    val (state', (lets, asms)) =
-      map_context_result (ProofContext.apply_case (get_case state name xs)) state;
-    val assumptions = asms |> map (fn (a, ts) =>
-      ((NameSpace.qualified name a, atts), map (rpair ([], [])) ts));
-  in
-    state'
-    |> add_binds_i lets
-    |> map_context (ProofContext.no_base_names o ProofContext.qualified_names)
-    |> assume_i assumptions
-    |> map_context (ProofContext.restore_naming (context_of state))
-    |> (fn st => simple_note_thms name (the_facts st) st)
-  end;
-
-
-
-(** goals **)
+(** facts **)
 
 (* forward chaining *)
 
@@ -693,6 +621,87 @@
   |> chain;
 
 
+(* note / from / with *)
+
+fun no_result args = map (pair ("", [])) args;
+
+local
+
+fun gen_thmss note_ctxt more_facts opt_chain prep_atts args state =
+  state
+  |> assert_forward
+  |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
+  |> these_factss (more_facts state)
+  |> opt_chain;
+
+in
+
+val note_thmss = gen_thmss ProofContext.note_thmss (K []) I Attrib.local_attribute;
+val note_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) I (K I);
+fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
+
+val from_thmss =
+  gen_thmss ProofContext.note_thmss (K []) chain Attrib.local_attribute o no_result;
+val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain (K I) o no_result;
+
+val with_thmss =
+  gen_thmss ProofContext.note_thmss the_facts chain Attrib.local_attribute o no_result;
+val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain (K I) o no_result;
+
+end;
+
+
+(* using *)
+
+local
+
+fun gen_using_thmss note prep_atts args state =
+  state
+  |> assert_backward
+  |> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_result args)))
+  |> (fn (st, named_facts) =>
+    let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
+    in st |> map_goal I (K ((result, (facts @ List.concat (map snd named_facts), thm)), x)) end);
+
+in
+
+val using_thmss = gen_using_thmss ProofContext.note_thmss Attrib.local_attribute;
+val using_thmss_i = gen_using_thmss ProofContext.note_thmss_i (K I);
+
+end;
+
+
+(* case *)
+
+local
+
+fun gen_invoke_case prep_att (name, xs, raw_atts) state =
+  let
+    val atts = map (prep_att (theory_of state)) raw_atts;
+    val (state', (lets, asms)) =
+      map_context_result (ProofContext.apply_case (get_case state name xs)) state;
+    val assumptions = asms |> map (fn (a, ts) =>
+      ((NameSpace.qualified name a, atts), map (rpair ([], [])) ts));
+  in
+    state'
+    |> add_binds_i lets
+    |> map_context (ProofContext.no_base_names o ProofContext.qualified_names)
+    |> assume_i assumptions
+    |> map_context (ProofContext.restore_naming (context_of state))
+    |> `the_facts |-> simple_note_thms name
+  end;
+
+in
+
+val invoke_case = gen_invoke_case Attrib.local_attribute;
+val invoke_case_i = gen_invoke_case (K I);
+
+end;
+
+
+
+(** goals **)
+
 (* setup goals *)
 
 local
@@ -710,7 +719,7 @@
     val thy' = theory_of state';
 
     val AfterQed (after_local, after_global) = after_qed;
-    val after_qed' = AfterQed (fn results => after_local results o map_context gen_binds, after_global);
+    val after_qed' = AfterQed (fn res => after_local res o map_context gen_binds, after_global);
 
     val props = List.concat propss;
     val cprop = Thm.cterm_of thy' (Logic.mk_conjunction_list props);
@@ -738,20 +747,21 @@
     |> enter_backward
   end;
 
-fun global_goal prep kind after_global export raw_locale a elems concl thy =
+fun global_goal prep_att prep kind after_global export raw_locale (name, atts) elems concl thy =
   let
-    val init = init_state thy;
+    val prep_atts = map (prep_att thy);
+    val init_state = init thy;
     val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
-      prep (Option.map fst raw_locale) elems (map snd concl) (context_of init);
+      prep (Option.map fst raw_locale) elems (map snd concl) (context_of init_state);
   in
-    init
+    init_state
     |> open_block
     |> map_context (K locale_ctxt)
     |> open_block
     |> map_context (K elems_ctxt)
     |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
       (Theorem {kind = kind,
-        theory_spec = (a, map (snd o fst) concl),
+        theory_spec = ((name, prep_atts atts), map (prep_atts o snd o fst) concl),
         locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (the opt_name, x)),
         view = view,
         export = export})
@@ -759,23 +769,27 @@
       true (map (fst o fst) concl) propp
   end;
 
-fun local_goal' prepp kind (check: bool -> state -> state) after_local pr args int state =
-  state
-  |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
-    (AfterQed (after_local, K I)) pr (map (fst o fst) args) (map snd args)
-  |> warn_extra_tfrees state
-  |> check int;
+fun local_goal' prep_att prepp kind (check: bool -> state -> state)
+    after_local pr raw_args int state =
+  let val args = Attrib.map_specs (prep_att (theory_of state)) raw_args in
+    state
+    |> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
+      (AfterQed (after_local, K I)) pr (map (fst o fst) args) (map snd args)
+    |> warn_extra_tfrees state
+    |> check int
+  end;
 
-fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false;
+fun local_goal prep_att prepp kind f pr args =
+  local_goal' prep_att prepp kind (K I) f pr args false;
 
 in
 
-val multi_theorem = global_goal Locale.read_context_statement;
-val multi_theorem_i = global_goal Locale.cert_context_statement;
-val show = local_goal' ProofContext.bind_propp Show;
-val show_i = local_goal' ProofContext.bind_propp_i Show;
-val have = local_goal ProofContext.bind_propp Have;
-val have_i = local_goal ProofContext.bind_propp_i Have;
+val multi_theorem = global_goal Attrib.global_attribute Locale.read_context_statement;
+val multi_theorem_i = global_goal (K I) Locale.cert_context_statement;
+val show = local_goal' Attrib.local_attribute ProofContext.bind_propp Show;
+val show_i = local_goal' (K I) ProofContext.bind_propp_i Show;
+val have = local_goal Attrib.local_attribute ProofContext.bind_propp Have;
+val have_i = local_goal (K I) ProofContext.bind_propp_i Have;
 
 end;
 
@@ -844,15 +858,20 @@
     |> (Seq.flat o Seq.map (after_local results))
   end;
 
-fun local_qed finalize print state =
+fun local_qed asm opt_text print state =
   state
   |> end_proof false
-  |> finalize
+  |> refine (Method.finish_text asm opt_text)
   |> (Seq.flat o Seq.map (finish_local print));
 
 
 (* global_qed *)
 
+fun check_result msg state sq =
+  (case Seq.pull sq of
+    NONE => raise STATE (msg, state)
+  | SOME res => Seq.cons res);
+
 fun finish_global state =
   let
     val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (AfterQed (_, after_global), _))) =
@@ -888,15 +907,64 @@
       |> (fn (thy, res) => (thy, res)
           |>> (#1 o Locale.smart_note_thmss k locale_name
             [((name, atts), [(List.concat (map #2 res), [])])]));
-  in (after_global (locale_results, results) theory', ((k, name), results')) end;
+  in ((after_global (locale_results, results) theory', locale_ctxt), ((k, name), results')) end;
+
+fun global_qeds asm opt_text =
+  end_proof true
+  #> refine (Method.finish_text asm opt_text)
+  #> Seq.map finish_global
+  |> Seq.DETERM;   (*backtracking may destroy theory!*)
+
+fun global_qed asm opt_text state =
+  state
+  |> global_qeds asm opt_text
+  |> check_result "Failed to finish proof" state
+  |> Seq.hd;
 
 
-(*note: clients should inspect first result only, as backtracking may destroy theory*)
-fun global_qed finalize state =
+(* structured proof steps *)
+
+fun proof opt_text state =
+  state
+  |> assert_backward
+  |> refine (if_none opt_text Method.default_text)
+  |> Seq.map (goal_facts (K []))
+  |> Seq.map enter_forward;
+
+fun local_terminal_proof (text, opt_text) pr =
+  Seq.THEN (proof (SOME text), local_qed true opt_text pr);
+
+val local_default_proof = local_terminal_proof (Method.default_text, NONE);
+val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
+fun local_done_proof pr = Seq.THEN (proof (SOME Method.done_text), local_qed false NONE pr);
+
+fun global_term_proof asm (text, opt_text) state =
   state
-  |> end_proof true
-  |> finalize
-  |> Seq.map finish_global;
+  |> proof (SOME text)
+  |> check_result "Terminal proof method failed" state
+  |> (Seq.flat o Seq.map (global_qeds asm opt_text))
+  |> check_result "Failed to finish proof (after successful terminal method)" state
+  |> Seq.hd;
+
+val global_terminal_proof = global_term_proof true;
+val global_default_proof = global_terminal_proof (Method.default_text, NONE);
+val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
+val global_done_proof = global_term_proof false (Method.done_text, NONE);
+
+
+(* unstructured proof steps *)
+
+fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
+fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
+
+fun apply text =
+  assert_backward
+  #> refine text
+  #> Seq.map (goal_facts (K []));
+
+fun apply_end text =
+  assert_forward
+  #> refine_end text;
 
 
 
@@ -924,6 +992,3 @@
   |> transfer_facts state;
 
 end;
-
-structure BasicProof: BASIC_PROOF = Proof;
-open BasicProof;