src/Pure/Isar/method.ML

 (*  Title:      Pure/Isar/method.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Proof methods.
+Isar proof methods.
 *)
 
 signature BASIC_METHOD =
 sig
+  val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
+  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
+  type method
   val trace_rules: bool ref
   val print_methods: theory -> unit
-  val Method: bstring -> (Args.src -> Proof.context -> Proof.method) -> string -> unit
+  val Method: bstring -> (Args.src -> ProofContext.context -> method) -> string -> unit
 end;
 
 signature METHOD =
 sig
   include BASIC_METHOD
-  type src
-  val trace: Proof.context -> thm list -> unit
-  val RAW_METHOD: (thm list -> tactic) -> Proof.method
-  val RAW_METHOD_CASES: (thm list -> RuleCases.tactic) -> Proof.method
-  val METHOD: (thm list -> tactic) -> Proof.method
-  val METHOD_CASES: (thm list -> RuleCases.tactic) -> Proof.method
-  val SIMPLE_METHOD: tactic -> Proof.method
-  val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> Proof.method
-  val fail: Proof.method
-  val succeed: Proof.method
-  val defer: int option -> Proof.method
-  val prefer: int -> Proof.method
-  val insert_tac: thm list -> int -> tactic
-  val insert: thm list -> Proof.method
-  val insert_facts: Proof.method
-  val unfold: thm list -> Proof.method
-  val fold: thm list -> Proof.method
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
-  val rules_tac: Proof.context -> int option -> int -> tactic
+  val apply: method -> thm list -> RuleCases.tactic;
+  val RAW_METHOD_CASES: (thm list -> RuleCases.tactic) -> method
+  val RAW_METHOD: (thm list -> tactic) -> method
+  val METHOD_CASES: (thm list -> RuleCases.tactic) -> method
+  val METHOD: (thm list -> tactic) -> method
+  val fail: method
+  val succeed: method
+  val insert_tac: thm list -> int -> tactic
+  val insert: thm list -> method
+  val insert_facts: method
+  val SIMPLE_METHOD: tactic -> method
+  val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
+  val defer: int option -> method
+  val prefer: int -> method
+  val intro: thm list -> method
+  val elim: thm list -> method
+  val unfold: thm list -> method
+  val fold: thm list -> method
+  val atomize: bool -> method
+  val this: method
+  val assumption: ProofContext.context -> method
+  val close: bool -> ProofContext.context -> method
+  val trace: ProofContext.context -> thm list -> unit
   val rule_tac: thm list -> thm list -> int -> tactic
-  val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
-  val rule: thm list -> Proof.method
-  val erule: int -> thm list -> Proof.method
-  val drule: int -> thm list -> Proof.method
-  val frule: int -> thm list -> Proof.method
-  val this: Proof.method
-  val assumption: Proof.context -> Proof.method
-  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list -> thm -> int -> tactic
-  val set_tactic: (Proof.context -> thm list -> tactic) -> unit
-  val tactic: string -> Proof.context -> Proof.method
-  exception METHOD_FAIL of (string * Position.T) * exn
-  val method: theory -> src -> Proof.context -> Proof.method
-  val add_method: bstring * (src -> Proof.context -> Proof.method) * string
-    -> theory -> theory
-  val add_methods: (bstring * (src -> Proof.context -> Proof.method) * string) list
-    -> theory -> theory
-  val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    src -> Proof.context -> Proof.context * 'a
-  val simple_args: (Args.T list -> 'a * Args.T list)
-    -> ('a -> Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
-  val ctxt_args: (Proof.context -> Proof.method) -> src -> Proof.context -> Proof.method
-  val no_args: Proof.method -> src -> Proof.context -> Proof.method
-  type modifier
-  val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    (Args.T list -> modifier * Args.T list) list ->
-    ('a -> Proof.context -> 'b) -> src -> Proof.context -> 'b
-  val bang_sectioned_args:
-    (Args.T list -> modifier * Args.T list) list ->
-    (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
-  val bang_sectioned_args':
-    (Args.T list -> modifier * Args.T list) list ->
-    (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    ('a -> thm list -> Proof.context -> 'b) -> src -> Proof.context -> 'b
-  val only_sectioned_args:
-    (Args.T list -> modifier * Args.T list) list ->
-    (Proof.context -> 'a) -> src -> Proof.context -> 'a
-  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
-  val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
-  val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
+  val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic
+  val rule: thm list -> method
+  val erule: int -> thm list -> method
+  val drule: int -> thm list -> method
+  val frule: int -> thm list -> method
+  val rules_tac: ProofContext.context -> int option -> int -> tactic
+  val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list ->
+    thm -> int -> tactic
+  val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit
+  val tactic: string -> ProofContext.context -> method
+  type src
   datatype text =
-    Basic of (Proof.context -> Proof.method) |
+    Basic of (ProofContext.context -> method) |
     Source of src |
     Then of text list |
     Orelse of text list |
     Try of text |
     Repeat1 of text
-  val refine: text -> Proof.state -> Proof.state Seq.seq
-  val refine_end: text -> Proof.state -> Proof.state Seq.seq
-  val proof: text option -> Proof.state -> Proof.state Seq.seq
-  val local_qed: bool -> text option
-    -> (Proof.context -> string * (string * thm list) list -> unit) *
-      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val local_terminal_proof: text * text option
-    -> (Proof.context -> string * (string * thm list) list -> unit) *
-      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val local_default_proof: (Proof.context -> string * (string * thm list) list -> unit) *
-    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val local_immediate_proof: (Proof.context -> string * (string * thm list) list -> unit) *
-    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val local_done_proof: (Proof.context -> string * (string * thm list) list -> unit) *
-    (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
-  val global_qed: bool -> text option
-    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
-  val global_terminal_proof: text * text option
-    -> Proof.state -> theory * ((string * string) * (string * thm list) list)
-  val global_default_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
-  val global_immediate_proof: Proof.state ->
-    theory * ((string * string) * (string * thm list) list)
-  val global_done_proof: Proof.state -> theory * ((string * string) * (string * thm list) list)
+  val default_text: text
+  val this_text: text
+  val done_text: text
+  val finish_text: bool -> text option -> text
+  exception METHOD_FAIL of (string * Position.T) * exn
+  val method: theory -> src -> ProofContext.context -> method
+  val add_methods: (bstring * (src -> ProofContext.context -> method) * string) list
+    -> theory -> theory
+  val add_method: bstring * (src -> ProofContext.context -> method) * string
+    -> theory -> theory
+  val syntax: (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list))
+    -> src -> ProofContext.context -> ProofContext.context * 'a
+  val simple_args: (Args.T list -> 'a * Args.T list)
+    -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method
+  val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method
+  val no_args: method -> src -> ProofContext.context -> method
+  type modifier
+  val sectioned_args: (ProofContext.context * Args.T list ->
+      'a * (ProofContext.context * Args.T list)) ->
+    (Args.T list -> modifier * Args.T list) list ->
+    ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
+  val bang_sectioned_args:
+    (Args.T list -> modifier * Args.T list) list ->
+    (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
+  val bang_sectioned_args':
+    (Args.T list -> modifier * Args.T list) list ->
+    (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list)) ->
+    ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b
+  val only_sectioned_args:
+    (Args.T list -> modifier * Args.T list) list ->
+    (ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a
+  val thms_ctxt_args: (thm list -> ProofContext.context -> 'a) -> src ->
+    ProofContext.context -> 'a
+  val thms_args: (thm list -> 'a) -> src -> ProofContext.context -> 'a
+  val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a
   val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic)
-    -> src -> Proof.context -> Proof.method
-  val goal_args': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
-    -> ('a -> int -> tactic) -> src -> Proof.context -> Proof.method
-  val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> (Proof.context -> 'a -> int -> tactic)
-    -> src -> Proof.context -> Proof.method
-  val goal_args_ctxt': (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))
-    -> (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> Proof.method
+    -> src -> ProofContext.context -> method
+  val goal_args': (ProofContext.context * Args.T list ->
+      'a * (ProofContext.context * Args.T list))
+    -> ('a -> int -> tactic) -> src -> ProofContext.context -> method
+  val goal_args_ctxt: (Args.T list -> 'a * Args.T list) ->
+    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
+  val goal_args_ctxt': (ProofContext.context * Args.T list ->
+    'a * (ProofContext.context * Args.T list)) ->
+    (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method
 end;
 
 structure Method: METHOD =
 struct
 
-type src = Args.src;
+(** generic tools **)
+
+(* 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;
+
+
+(* multi_resolve *)
+
+local
+
+fun res th i rule =
+  Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
+
+fun multi_res _ [] rule = Seq.single rule
+  | multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule));
+
+in
+
+val multi_resolve = multi_res 1;
+fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
+
+end;
+
 
 
 (** proof methods **)
 
-(* tracing *)
-
-val trace_rules = ref false;
-
-fun trace ctxt rules =
-  conditional (! trace_rules andalso not (null rules)) (fn () =>
-    Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
-    |> Pretty.string_of |> tracing);
-
-
-(* make methods *)
-
-val RAW_METHOD = Proof.method;
-val RAW_METHOD_CASES = Proof.method_cases;
-
-fun METHOD m = Proof.method (fn facts => TRY Tactic.conjunction_tac THEN m facts);
-fun METHOD_CASES m =
-  Proof.method_cases (fn facts => Seq.THEN (TRY Tactic.conjunction_tac, m facts));
-
-
-(* primitive *)
+(* datatype method *)
+
+datatype method = Method of thm list -> RuleCases.tactic;
+
+fun apply (Method m) = m;
+
+val RAW_METHOD_CASES = Method;
+
+fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
+
+fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
+  Seq.THEN (TRY Tactic.conjunction_tac, tac facts));
+
+fun METHOD tac = RAW_METHOD (fn facts =>
+  TRY Tactic.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);
 
 
-(* shuffle *)
-
-fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
-
-
-(* insert *)
+(* insert facts *)
 
 local
 
 fun cut_rule_tac raw_rule =
   let

 fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
 
 end;
 
 
+(* shuffle subgoals *)
+
+fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
+fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
+
+
+(* unfold intro/elim rules *)
+
+fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
+fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
+
+
 (* unfold/fold definitions *)
 
 fun unfold_meth ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths));
 fun fold_meth ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
 

 
 fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
   | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
 
 
-(* unfold intro/elim rules *)
-
-fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
-fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
-
-
-(* multi_resolve *)
+(* this -- apply facts directly *)
+
+val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
+
+
+(* assumption *)
 
 local
 
-fun res th i rule =
-  Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
-
-fun multi_res _ [] rule = Seq.single rule
-  | multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule));
+fun asm_tac ths =
+  foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
+
+val refl_tac = SUBGOAL (fn (prop, i) =>
+  if can Logic.dest_equals (Logic.strip_assums_concl prop)
+  then Tactic.rtac Drule.reflexive_thm i else no_tac);
+
+fun assm_tac ctxt =
+  assume_tac APPEND'
+  asm_tac (ProofContext.prems_of ctxt) APPEND'
+  refl_tac;
+
+fun assumption_tac ctxt [] = assm_tac ctxt
+  | assumption_tac _ [fact] = asm_tac [fact]
+  | assumption_tac _ _ = K no_tac;
 
 in
 
-val multi_resolve = multi_res 1;
-fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
-
-end;
-
-
-(* rules_tac *)
+fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);
+fun close asm ctxt = METHOD (K
+  (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
+
+end;
+
+
+(* rule etc. -- single-step refinements *)
+
+val trace_rules = ref false;
+
+fun trace ctxt rules =
+  conditional (! trace_rules andalso not (null rules)) (fn () =>
+    Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
+    |> Pretty.string_of |> tracing);
+
+local
+
+fun gen_rule_tac tac rules [] i st = tac rules i st
+  | gen_rule_tac tac rules facts i st =
+      Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts rules));
+
+fun gen_arule_tac tac j rules facts =
+  EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
+
+fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
+  let
+    val rules =
+      if not (null arg_rules) then arg_rules
+      else List.concat (ContextRules.find_rules false facts goal ctxt)
+  in trace ctxt rules; tac rules facts i end);
+
+fun meth tac x = METHOD (HEADGOAL o tac x);
+fun meth' tac x y = METHOD (HEADGOAL o tac x y);
+
+in
+
+val rule_tac = gen_rule_tac Tactic.resolve_tac;
+val rule = meth rule_tac;
+val some_rule_tac = gen_some_rule_tac rule_tac;
+val some_rule = meth' some_rule_tac;
+
+val erule = meth' (gen_arule_tac Tactic.eresolve_tac);
+val drule = meth' (gen_arule_tac Tactic.dresolve_tac);
+val frule = meth' (gen_arule_tac Tactic.forward_tac);
+
+end;
+
+
+(* rules -- intuitionistic proof search *)
 
 local
 
 val remdups_tac = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in

 
 fun step_tac ctxt i =
   REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
   REMDUPS (unsafe_step_tac ctxt) i;
 
-fun intpr_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
+fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
   let
     val ps = Logic.strip_assums_hyp g;
     val c = Logic.strip_assums_concl g;
   in
     if gen_mem (fn ((ps1, c1), (ps2, c2)) =>
       c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac
-    else (step_tac ctxt THEN_ALL_NEW intpr_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
+    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
   end);
 
 in
 
 fun rules_tac ctxt opt_lim =
-  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4 1);
-
-end;
-
-
-(* rule_tac etc. *)
-
-local
-
-fun gen_rule_tac tac rules [] i st = tac rules i st
-  | gen_rule_tac tac rules facts i st =
-      Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts rules));
-
-fun gen_arule_tac tac j rules facts =
-  EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac);
-
-fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
-  let
-    val rules =
-      if not (null arg_rules) then arg_rules
-      else List.concat (ContextRules.find_rules false facts goal ctxt)
-  in trace ctxt rules; tac rules facts i end);
-
-fun meth tac x = METHOD (HEADGOAL o tac x);
-fun meth' tac x y = METHOD (HEADGOAL o tac x y);
-
-in
-
-val rule_tac = gen_rule_tac Tactic.resolve_tac;
-val rule = meth rule_tac;
-val some_rule_tac = gen_some_rule_tac rule_tac;
-val some_rule = meth' some_rule_tac;
-
-val erule = meth' (gen_arule_tac Tactic.eresolve_tac);
-val drule = meth' (gen_arule_tac Tactic.dresolve_tac);
-val frule = meth' (gen_arule_tac Tactic.forward_tac);
-
-end;
-
-
-(* this *)
-
-val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac));
-
-
-(* assumption *)
-
-fun asm_tac ths =
-  foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
-
-val refl_tac = SUBGOAL (fn (prop, i) =>
-  if can Logic.dest_equals (Logic.strip_assums_concl prop)
-  then Tactic.rtac Drule.reflexive_thm i else no_tac);
-
-fun assm_tac ctxt =
-  assume_tac APPEND'
-  asm_tac (ProofContext.prems_of ctxt) APPEND'
-  refl_tac;
-
-fun assumption_tac ctxt [] = assm_tac ctxt
-  | assumption_tac _ [fact] = asm_tac [fact]
-  | assumption_tac _ _ = K no_tac;
-
-fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);
-
-
-(* res_inst_tac etc. *)
-
-(*Reimplemented to support both static (Isar) and dynamic (proof state)
-  context.  By Clemens Ballarin.*)
+  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1);
+
+end;
+
+
+(* rule_tac etc. -- refer to dynamic goal state!! *)
 
 fun bires_inst_tac bires_flag ctxt insts thm =
   let
-    val sign = ProofContext.sign_of ctxt;
+    val thy = ProofContext.theory_of ctxt;
     (* Separate type and term insts *)
     fun has_type_var ((x, _), _) = (case Symbol.explode x of
           "'"::cs => true | cs => false);
     val Tinsts = List.filter has_type_var insts;
     val tinsts = filter_out has_type_var insts;

     fun absent xi = error
           ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
     val (rtypes, rsorts) = types_sorts thm;
     fun readT (xi, s) =
         let val S = case rsorts xi of SOME S => S | NONE => absent xi;
-            val T = Sign.read_typ (sign, sorts) s;
+            val T = Sign.read_typ (thy, sorts) s;
             val U = TVar (xi, S);
-        in if Sign.typ_instance sign (T, U) then (U, T)
+        in if Sign.typ_instance thy (T, U) then (U, T)
            else error
              ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
         end;
     val Tinsts_env = map readT Tinsts;
     (* Preprocess rule: extract vars and their types, apply Tinsts *)

         val envT' = map (fn (ixn, T) =>
           (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =
           map
             (fn (xi, t) =>
-              pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
+              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
             (gen_distinct
               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
               (xis ~~ ts));
         (* Lift and instantiate rule *)
         val {maxidx, ...} = rep_thm st;

           | liftvar t = raise TERM("Variable expected", [t]);
         fun liftterm t = list_abs_free
               (params, Logic.incr_indexes(paramTs,inc) t)
         fun liftpair (cv,ct) =
               (cterm_fun liftvar cv, cterm_fun liftterm ct)
-        val lifttvar = pairself (ctyp_of sign o Logic.incr_tvar inc);
+        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate
               (map lifttvar envT', map liftpair cenv)
               (lift_rule (st, i) thm)
       in
         if i > nprems_of st then no_tac st

                 | THM  (msg,_,_) => (warning msg; no_tac st);
   in
     tac
   end;
 
+local
+
 fun gen_inst _ tac _ (quant, ([], thms)) =
       METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
   | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
       METHOD (fn facts =>
         quant (insert_tac facts THEN' inst_tac ctxt insts thm))
   | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
 
-val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
-
-val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
-
 (* Preserve Var indexes of rl; increment revcut_rl instead.
    Copied from tactic.ML *)
 fun make_elim_preserve rl =
   let val {maxidx,...} = rep_thm rl
-      fun cvar xi = cterm_of (Theory.sign_of ProtoPure.thy) (Var(xi,propT));
+      fun cvar xi = cterm_of ProtoPure.thy (Var(xi,propT));
       val revcut_rl' =
           instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
                              (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
       val arg = (false, rl, nprems_of rl)
       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   in  th  end
   handle Bind => raise THM("make_elim_preserve", 1, [rl]);
 
+in
+
+val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
+
+val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
+
 val cut_inst_meth =
   gen_inst
-    (fn ctxt => fn insts => fn thm =>
-       bires_inst_tac false ctxt insts (make_elim_preserve thm))
+    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o make_elim_preserve)
     Tactic.cut_rules_tac;
 
 val dres_inst_meth =
   gen_inst
-    (fn ctxt => fn insts => fn rule =>
-       bires_inst_tac true ctxt insts (make_elim_preserve rule))
+    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o make_elim_preserve)
     Tactic.dresolve_tac;
 
 val forw_inst_meth =
   gen_inst
     (fn ctxt => fn insts => fn rule =>
        bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN'
        assume_tac)
     Tactic.forward_tac;
 
 fun subgoal_tac ctxt sprop =
-  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl THEN'
-  SUBGOAL (fn (prop, _) =>
-    let val concl' = Logic.strip_assums_concl prop in
-      if null (term_tvars concl') then ()
-      else warning "Type variables in new subgoal: add a type constraint?";
-      all_tac
-  end);
+  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl;
 
 fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
 
 fun thin_tac ctxt s =
   bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
 
-
-(* simple Prolog interpreter *)
-
-fun prolog_tac rules facts =
-  DEPTH_SOLVE_1 (HEADGOAL (Tactic.assume_tac APPEND' Tactic.resolve_tac (facts @ rules)));
-
-val prolog = METHOD o prolog_tac;
+end;
 
 
 (* ML tactics *)
 
-val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
+val tactic_ref = ref ((fn _ => raise Match): ProofContext.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
 fun tactic txt ctxt = METHOD (fn facts =>
   (Context.use_mltext
-    ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic = \
+    ("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \
        \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\
        \  and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n"
        ^ txt ^
        "\nend in Method.set_tactic tactic end")
     false NONE;
     Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
 
 
 
-(** methods theory data **)
-
-(* data kind 'Isar/methods' *)
+(** method syntax **)
+
+(* method text *)
+
+type src = Args.src;
+
+datatype text =
+  Basic of (ProofContext.context -> method) |
+  Source of src |
+  Then of text list |
+  Orelse of text list |
+  Try of text |
+  Repeat1 of text;
+
+val default_text = Source (Args.src (("default", []), Position.none));
+val this_text = Basic (K this);
+val done_text = Basic (K (SIMPLE_METHOD all_tac));
+
+fun finish_text asm NONE = Basic (close asm)
+  | finish_text asm (SOME txt) = Then [txt, Basic (close asm)];
+
+
+(* method definitions *)
 
 structure MethodsData = TheoryDataFun
 (struct
   val name = "Isar/methods";
-  type T = (((src -> Proof.context -> Proof.method) * string) * stamp) NameSpace.table;
+  type T = (((src -> ProofContext.context -> method) * string) * stamp) NameSpace.table;
 
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
   fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>

         | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
       end;
   in meth end;
 
 
-(* add_method(s) *)
+(* add method *)
 
 fun add_methods raw_meths thy =
   let
-    val sg = Theory.sign_of thy;
     val new_meths = raw_meths |> map (fn (name, f, comment) =>
       (name, ((f, comment), stamp ())));
 
-    fun add meths = NameSpace.extend_table (Sign.naming_of sg) (meths, new_meths)
+    fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths)
       handle Symtab.DUPS dups =>
         error ("Duplicate declaration of method(s) " ^ commas_quote dups);
   in MethodsData.map add thy end;
 
 val add_method = add_methods o Library.single;
 
-(*implicit version*)
 fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
 
 
 
-(** method syntax **)
+(** concrete syntax **)
 
 (* basic *)
 
-fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
+fun syntax (scan:
+    (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list))) =
   Args.syntax "method" scan;
 
-fun simple_args scan f src ctxt : Proof.method =
+fun simple_args scan f src ctxt : method =
   #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
 
-fun ctxt_args (f: Proof.context -> Proof.method) src ctxt =
+fun ctxt_args (f: ProofContext.context -> method) src ctxt =
   #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
 
 fun no_args m = ctxt_args (K m);
 
 
 (* sections *)
 
-type modifier = (Proof.context -> Proof.context) * Proof.context attribute;
+type modifier = (ProofContext.context -> ProofContext.context) * ProofContext.context attribute;
 
 local
 
 fun sect ss = Scan.first (map Scan.lift ss);
 fun thms ss = Scan.unless (sect ss) Attrib.local_thms;

 val destN = "dest";
 val ruleN = "rule";
 
 fun modifier name kind kind' att =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
-    >> (pair (I: Proof.context -> Proof.context) o att);
+    >> (pair (I: ProofContext.context -> ProofContext.context) o att);
 
 val rules_modifiers =
  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local,
   modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local,

 val insts_var =
   Scan.optional
     (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
       Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
 
-fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
+fun inst_args_var f src ctxt =
+  f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
 
 fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;

 fun goal_args_ctxt' args tac src ctxt =
   #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
-
-
-(** method text **)
-
-(* datatype text *)
-
-datatype text =
-  Basic of (Proof.context -> Proof.method) |
-  Source of src |
-  Then of text list |
-  Orelse of text list |
-  Try of text |
-  Repeat1 of text;
-
-
-(* refine *)
-
-fun gen_refine f text state =
-  let
-    val thy = Proof.theory_of state;
-
-    fun eval (Basic mth) = f mth
-      | eval (Source src) = f (method thy src)
-      | eval (Then txts) = Seq.EVERY (map eval txts)
-      | eval (Orelse txts) = Seq.FIRST (map eval txts)
-      | eval (Try txt) = Seq.TRY (eval txt)
-      | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
-  in eval text state end;
-
-val refine = gen_refine Proof.refine;
-val refine_end = gen_refine Proof.refine_end;
-
-
-(* structured proof steps *)
-
-val default_text = Source (Args.src (("default", []), Position.none));
-val this_text = Basic (K this);
-val done_text = Basic (K (SIMPLE_METHOD all_tac));
-
-fun close_text asm = Basic (fn ctxt => METHOD (K
-  (FILTER Thm.no_prems ((if asm then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))));
-
-fun finish_text asm NONE = close_text asm
-  | finish_text asm (SOME txt) = Then [txt, close_text asm];
-
-fun proof opt_text state =
-  state
-  |> Proof.assert_backward
-  |> refine (if_none opt_text default_text)
-  |> Seq.map (Proof.goal_facts (K []))
-  |> Seq.map Proof.enter_forward;
-
-fun local_qed asm opt_text = Proof.local_qed (refine (finish_text asm opt_text));
-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 (default_text, NONE);
-val local_immediate_proof = local_terminal_proof (this_text, NONE);
-fun local_done_proof pr = Seq.THEN (proof (SOME done_text), local_qed false NONE pr);
-
-
-fun global_qeds asm opt_text = Proof.global_qed (refine (finish_text asm opt_text));
-
-fun global_qed asm opt_text state =
-  state
-  |> global_qeds asm opt_text
-  |> Proof.check_result "Failed to finish proof" state
-  |> Seq.hd;
-
-fun global_term_proof asm (text, opt_text) state =
-  state
-  |> proof (SOME text)
-  |> Proof.check_result "Terminal proof method failed" state
-  |> (Seq.flat o Seq.map (global_qeds asm opt_text))
-  |> Proof.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 (default_text, NONE);
-val global_immediate_proof = global_terminal_proof (this_text, NONE);
-val global_done_proof = global_term_proof false (done_text, NONE);
 
 
 (* misc tactic emulations *)
 
 val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;

   ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
   ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
   ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
   ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
   ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
-  ("prolog", thms_args prolog, "simple prolog interpreter"),
   ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
 
 val _ = Context.add_setup [add_methods pure_methods];