src/Pure/Isar/method.ML
changeset 12119 fab22bdb1496
parent 12055 a9c44895cc8c
child 12144 f84eb7334d04
     1.1 --- a/src/Pure/Isar/method.ML	Fri Nov 09 00:16:07 2001 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Nov 09 00:16:52 2001 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4    val frule: int -> thm list -> Proof.method
     1.5    val this: Proof.method
     1.6    val assumption: Proof.context -> Proof.method
     1.7 +  val impose_hyps_tac: Proof.context -> tactic
     1.8    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
     1.9    val tactic: string -> Proof.context -> Proof.method
    1.10    exception METHOD_FAIL of (string * Position.T) * exn
    1.11 @@ -170,6 +171,7 @@
    1.12  
    1.13    val empty = [NetRules.intro, NetRules.elim, NetRules.intro, NetRules.elim];
    1.14    val copy = I;
    1.15 +  val finish = I;
    1.16    val prep_ext = I;
    1.17    fun merge x = map2 NetRules.merge x;
    1.18    val print = print_rules Display.pretty_thm_sg;
    1.19 @@ -394,12 +396,16 @@
    1.20  
    1.21  (* res_inst_tac etc. *)
    1.22  
    1.23 +(*robustify instantiation by imposing (part of) the present static context*)
    1.24 +val impose_hyps_tac =
    1.25 +  PRIMITIVE o Drule.impose_hyps o flat o map #1 o ProofContext.assumptions_of;
    1.26 +
    1.27  (*Note: insts refer to the implicit (!!) goal context; use at your own risk*)
    1.28 -fun gen_res_inst _ tac (quant, ([], thms)) =
    1.29 +fun gen_res_inst _ tac _ (quant, ([], thms)) =
    1.30        METHOD (fn facts => (quant (insert_tac facts THEN' tac thms)))
    1.31 -  | gen_res_inst tac _ (quant, (insts, [thm])) =
    1.32 -      METHOD (fn facts => (quant (insert_tac facts THEN' tac insts thm)))
    1.33 -  | gen_res_inst _ _ _ = error "Cannot have instantiations with multiple rules";
    1.34 +  | gen_res_inst tac _ ctxt (quant, (insts, [thm])) =
    1.35 +      METHOD (fn facts => (impose_hyps_tac ctxt THEN quant (insert_tac facts THEN' tac insts thm)))
    1.36 +  | gen_res_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
    1.37  
    1.38  val res_inst = gen_res_inst Tactic.res_inst_tac Tactic.resolve_tac;
    1.39  val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
    1.40 @@ -446,6 +452,7 @@
    1.41  
    1.42    val empty = {space = NameSpace.empty, meths = Symtab.empty};
    1.43    val copy = I;
    1.44 +  val finish = I;
    1.45    val prep_ext = I;
    1.46    fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
    1.47      {space = NameSpace.merge (space1, space2),
    1.48 @@ -570,11 +577,11 @@
    1.49      (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
    1.50        Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss;
    1.51  
    1.52 -fun inst_args f = f oo (#2 oo syntax (Args.goal_spec HEADGOAL -- insts));
    1.53 +fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    1.54  
    1.55  
    1.56 -fun goal_args' args tac = #2 oo syntax (Args.goal_spec HEADGOAL -- args >>
    1.57 -  (fn (quant, s) => SIMPLE_METHOD' quant (tac s)));
    1.58 +fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
    1.59 +  (fn (quant, s) => SIMPLE_METHOD' quant (K (impose_hyps_tac ctxt) THEN' tac s))) src ctxt);
    1.60  
    1.61  fun goal_args args tac = goal_args' (Scan.lift args) tac;
    1.62