# HG changeset patch # User wenzelm # Date 1426800657 -3600 # Node ID f8d164ab0dc18cd594114999fcdcfbd20e8acabe # Parent 696d87036f0496b04b9e8bb6ea66d400e5b3a3f3 more position information; diff -r 696d87036f04 -r f8d164ab0dc1 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/CCL/CCL.thy Thu Mar 19 22:30:57 2015 +0100 @@ -475,7 +475,7 @@ method_setup eq_coinduct3 = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => - SIMPLE_METHOD' (res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3})) + SIMPLE_METHOD' (res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) *} diff -r 696d87036f04 -r f8d164ab0dc1 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/CCL/Wfd.thy Thu Mar 19 22:30:57 2015 +0100 @@ -49,7 +49,8 @@ method_setup wfd_strengthen = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (fn i => - res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1))) + res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i + THEN assume_tac ctxt (i + 1))) *} lemma wf_anti_sym: "\Wfd(r); :r; :r\ \ P" @@ -430,11 +431,12 @@ fun IHinst tac rls = SUBGOAL (fn (Bi,i) => let val bvs = bvars Bi [] val ihs = filter could_IH (Logic.strip_assums_hyp Bi) - val rnames = map (fn x=> + val rnames = map (fn x => let val (a,b) = get_bno [] 0 x in (nth bvs a, b) end) ihs fun try_IHs [] = no_tac - | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs) + | try_IHs ((x,y)::xs) = + tac [((("g", 0), Position.none), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs) in try_IHs rnames end) fun is_rigid_prog t = diff -r 696d87036f04 -r f8d164ab0dc1 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/CTT/CTT.thy Thu Mar 19 22:30:57 2015 +0100 @@ -421,13 +421,13 @@ The (rtac EqE i) lets them apply to equality judgements. **) fun NE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i fun SumE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i fun PlusE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) diff -r 696d87036f04 -r f8d164ab0dc1 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/Doc/Implementation/Tactic.thy Thu Mar 19 22:30:57 2015 +0100 @@ -394,10 +394,14 @@ text %mlref \ \begin{mldecls} - @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ - @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ - @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ - @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ + @{index_ML res_inst_tac: "Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ + @{index_ML eres_inst_tac: "Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ + @{index_ML dres_inst_tac: "Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ + @{index_ML forw_inst_tac: "Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\ @{index_ML rename_tac: "string list -> int -> tactic"} \\ diff -r 696d87036f04 -r f8d164ab0dc1 src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Mar 19 22:30:57 2015 +0100 @@ -856,7 +856,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 696d87036f04 -r f8d164ab0dc1 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/FOL/FOL.thy Thu Mar 19 22:30:57 2015 +0100 @@ -66,7 +66,8 @@ done ML {* - fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} + fun case_tac ctxt a = + res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split} *} method_setup case_tac = {* diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Auth/Message.thy Thu Mar 19 22:30:57 2015 +0100 @@ -866,7 +866,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Bali/AxExample.thy Thu Mar 19 22:30:57 2015 +0100 @@ -43,7 +43,7 @@ ML {* fun inst1_tac ctxt s t xs st = (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of - SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st + SOME i => Rule_Insts.instantiate_tac ctxt [(((s, i), Position.none), t)] xs st | NONE => Seq.empty); fun ax_tac ctxt = diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Bali/Basis.thy Thu Mar 19 22:30:57 2015 +0100 @@ -180,7 +180,7 @@ fun sum3_instantiate ctxt thm = map (fn s => simplify (ctxt delsimps @{thms not_None_eq}) - (Rule_Insts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " x")] ["x"] thm)) + (Rule_Insts.read_instantiate ctxt [((("t", 0), Position.none), "In" ^ s ^ " x")] ["x"] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 22:30:57 2015 +0100 @@ -1081,7 +1081,7 @@ ML {* fun Seq_case_tac ctxt s i = - res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i + res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2); (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) @@ -1093,7 +1093,7 @@ (* rws are definitions to be unfolded for admissibility check *) fun Seq_induct_tac ctxt s rws i = - res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i + res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1)))) THEN simp_tac (ctxt addsimps rws) i; @@ -1102,12 +1102,12 @@ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); fun pair_tac ctxt s = - res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} + res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE} THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt; (* induction on a sequence of pairs with pairsplitting and simplification *) fun pair_induct_tac ctxt s rws i = - res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i + res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i THEN pair_tac ctxt "a" (i+3) THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1)))) THEN simp_tac (ctxt addsimps rws) i; diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Thu Mar 19 22:30:57 2015 +0100 @@ -135,7 +135,7 @@ val take_ss = simpset_of (put_simpset HOL_ss @{context} addsimps (@{thm Rep_cfun_strict1} :: take_rews)) fun quant_tac ctxt i = EVERY - (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names) + (map (fn name => res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names) (* FIXME: move this message to domain_take_proofs.ML *) val is_finite = #is_finite take_info @@ -182,7 +182,7 @@ asm_simp_tac (put_simpset take_ss ctxt) 1 THEN (resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1 fun cases_tacs (cons, exhaust) = - res_inst_tac ctxt [(("y", 0), "x")] exhaust 1 :: + res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 :: asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 :: map con_tac cons val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Prolog/prolog.ML Thu Mar 19 22:30:57 2015 +0100 @@ -53,8 +53,9 @@ let fun at thm = case Thm.concl_of thm of _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> - let val s' = if s="P" then "PP" else s - in at(thm RS (Rule_Insts.read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end + let val s' = if s="P" then "PP" else s in + at(thm RS (Rule_Insts.read_instantiate ctxt [((("x", 0), Position.none), s')] [s'] spec)) + end | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp) | _ => [thm] diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 19 22:30:57 2015 +0100 @@ -871,7 +871,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/TLA/TLA.thy Thu Mar 19 22:30:57 2015 +0100 @@ -299,16 +299,16 @@ REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i]) fun merge_temp_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, - eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i]) + REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, + eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i]) fun merge_stp_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, - eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i]) + REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, + eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i]) fun merge_act_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, - eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i]) + REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, + eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i]) *} method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Mar 19 22:30:57 2015 +0100 @@ -185,7 +185,7 @@ else let fun instantiate param = - (map (eres_inst_tac ctxt [(("x", 0), param)]) thms + (map (eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms |> FIRST') val attempts = map instantiate parameters in @@ -221,7 +221,7 @@ else let fun instantiates param = - eres_inst_tac ctxt [(("x", 0), param)] thm + eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm val quantified_var = head_quantified_variable ctxt i st in @@ -427,7 +427,7 @@ fun instantiate_vars ctxt vars : tactic = map (fn var => Rule_Insts.eres_inst_tac ctxt - [(("x", 0), var)] @{thm allE} 1) + [((("x", 0), Position.none), var)] @{thm allE} 1) vars |> EVERY @@ -673,7 +673,8 @@ else let fun instantiate const_name = - dres_inst_tac ctxt [(("sk", 0), const_name ^ parameters)] @{thm leo2_skolemise} + dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] + @{thm leo2_skolemise} val attempts = map instantiate candidate_consts in (fold (curry (op APPEND')) attempts (K no_tac)) i st @@ -1556,7 +1557,7 @@ val tecs = map (fn t_s => - eres_inst_tac @{context} [(("x", 0), t_s)] @{thm allE} + eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE} THEN' atac) in (TRY o etac @{thm forall_pos_lift}) @@ -1735,7 +1736,8 @@ member (op =) (Term.add_frees hyp_body []) (hd hyp_prefix) then no_tac st else - eres_inst_tac ctxt [(("x", 0), "(@X. False)")] @{thm allE} i st + eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] + @{thm allE} i st end end end diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 19 22:30:57 2015 +0100 @@ -404,7 +404,7 @@ |> hackish_string_of_term ctxt in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), - th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] []) + th |> Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] []) end fun type_match thy (T1, T2) = diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Tools/TFL/post.ML Thu Mar 19 22:30:57 2015 +0100 @@ -128,7 +128,8 @@ rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' etac conjE))); (*Strip off the outer !P*) -val spec'= Rule_Insts.read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec; +val spec'= + Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec; fun tracing true _ = () | tracing false msg = writeln msg; diff -r 696d87036f04 -r f8d164ab0dc1 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 22:30:57 2015 +0100 @@ -44,9 +44,9 @@ (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2, res_inst_tac ctxt - [(("act", 0), sact)] @{thm totalize_transientI} 2 + [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2 ORELSE res_inst_tac ctxt - [(("act", 0), sact)] @{thm transientI} 2, + [((("act", 0), Position.none), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ctxt addsimps @{thms Domain_unfold}) 3, constrains_tac ctxt 1, diff -r 696d87036f04 -r f8d164ab0dc1 src/LCF/LCF.thy --- a/src/LCF/LCF.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/LCF/LCF.thy Thu Mar 19 22:30:57 2015 +0100 @@ -321,7 +321,7 @@ method_setup induct = {* Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => SIMPLE_METHOD' (fn i => - res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN + res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) *} @@ -380,7 +380,8 @@ ML {* fun induct2_tac ctxt (f, g) i = - res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN + res_inst_tac ctxt + [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN REPEAT(resolve_tac ctxt @{thms adm_lemmas} i) *} diff -r 696d87036f04 -r f8d164ab0dc1 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Thu Mar 19 22:30:57 2015 +0100 @@ -6,11 +6,16 @@ signature BASIC_RULE_INSTS = sig - val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic - val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic - val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic - val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic - val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic + val res_inst_tac: Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic + val eres_inst_tac: Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic + val cut_inst_tac: Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic + val forw_inst_tac: Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic + val dres_inst_tac: Proof.context -> + ((indexname * Position.T) * string) list -> thm -> int -> tactic val thin_tac: Proof.context -> string -> int -> tactic val subgoal_tac: Proof.context -> string -> int -> tactic end; @@ -18,14 +23,18 @@ signature RULE_INSTS = sig include BASIC_RULE_INSTS - val where_rule: Proof.context -> (indexname * string) list -> + val where_rule: Proof.context -> + ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> thm val of_rule: Proof.context -> string option list * string option list -> (binding * string option * mixfix) list -> thm -> thm - val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm - val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic + val read_instantiate: Proof.context -> + ((indexname * Position.T) * string) list -> string list -> thm -> thm + val instantiate_tac: Proof.context -> + ((indexname * Position.T) * string) list -> string list -> tactic val make_elim_preserve: Proof.context -> thm -> thm - val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) -> + val method: + (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) -> (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser end; @@ -34,21 +43,22 @@ (** reading instantiations **) -val partition_insts = List.partition (fn ((x, _), _) => String.isPrefix "'" x); +val partition_insts = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x); + +fun error_var msg (xi, pos) = + error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); local -fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi)); - -fun the_sort tvars (xi: indexname) = +fun the_sort tvars (xi, pos) : sort = (case AList.lookup (op =) tvars xi of SOME S => S - | NONE => error_var "No such type variable in theorem: " xi); + | NONE => error_var "No such type variable in theorem: " (xi, pos)); -fun the_type vars (xi: indexname) = +fun the_type vars (xi, pos) : typ = (case AList.lookup (op =) vars xi of SOME T => T - | NONE => error_var "No such variable in theorem: " xi); + | NONE => error_var "No such variable in theorem: " (xi, pos)); fun instantiate inst = Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #> @@ -89,13 +99,13 @@ (* type instantiations *) - fun readT (xi, s) = + fun readT ((xi, pos), s) = let - val S = the_sort tvars xi; + val S = the_sort tvars (xi, pos); val T = Syntax.read_typ ctxt s; in if Sign.of_sort thy (T, S) then ((xi, S), T) - else error_var "Incompatible sort for typ instantiation of " xi + else error_var "Incompatible sort for typ instantiation of " (xi, pos) end; val instT1 = Term_Subst.instantiateT (map readT type_insts); @@ -110,7 +120,7 @@ val instT2 = Term.typ_subst_TVars inferred; val vars2 = map (apsnd instT2) vars1; - val inst2 = instantiate (xs ~~ ts); + val inst2 = instantiate (map #1 xs ~~ ts); (* result *) @@ -140,7 +150,7 @@ let fun zip_vars _ [] = [] | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest - | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest + | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest | zip_vars [] _ = error "More instantiations than variables in theorem"; val insts = zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @ @@ -167,9 +177,9 @@ val _ = Theory.setup (Attrib.setup @{binding "where"} (Scan.lift - (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >> - (fn (insts, fixes) => - Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes))) + (Parse.and_list (Parse.position Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) + -- Parse.for_fixes) >> (fn (insts, fixes) => + Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes))) "named instantiation of theorem"); @@ -220,29 +230,29 @@ (* process type insts: Tinsts_env *) - fun absent xi = - error ("No such variable in theorem: " ^ Term.string_of_vname xi); - val (rtypes, rsorts) = Drule.types_sorts thm; - fun readT (xi, s) = + fun readT ((xi, pos), s) = let - val S = (case rsorts xi of SOME S => S | NONE => absent xi); + val S = + (case rsorts xi of + SOME S => S + | NONE => error_var "No such type variable in theorem: " (xi, pos)); val T = Syntax.read_typ ctxt' s; val U = TVar (xi, S); in if Sign.typ_instance thy (T, U) then (U, T) - else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails") + else error_var "Cannot instantiate: " (xi, pos) end; val Tinsts_env = map readT Tinsts; (* preprocess rule: extract vars and their types, apply Tinsts *) - fun get_typ xi = + fun get_typ (xi, pos) = (case rtypes xi of SOME T => typ_subst_atomic Tinsts_env T - | NONE => absent xi); - val (xis, ss) = Library.split_list tinsts; + | NONE => error_var "No such variable in theorem: " (xi, pos) xi); + val (xis, ss) = split_list tinsts; val Ts = map get_typ xis; val (ts, envT) = @@ -250,7 +260,7 @@ val envT' = map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env; val cenv = - map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) + map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) (distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xis ~~ ts)); @@ -312,10 +322,12 @@ (* derived tactics *) (*deletion of an assumption*) -fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl; +fun thin_tac ctxt s = + eres_inst_tac ctxt [((("V", 0), Position.none), s)] Drule.thin_rl; (*Introduce the given proposition as lemma and subgoal*) -fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl; +fun subgoal_tac ctxt A = + DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] cut_rl; @@ -324,8 +336,8 @@ fun method inst_tac tac = Args.goal_spec -- Scan.optional (Scan.lift - (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --| - Args.$$$ "in")) [] -- + (Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) + --| Args.$$$ "in")) [] -- Attrib.thms >> (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts => if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms) diff -r 696d87036f04 -r f8d164ab0dc1 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/Sequents/LK0.thy Thu Mar 19 22:30:57 2015 +0100 @@ -153,11 +153,11 @@ ML {* (*Cut and thin, replacing the right-side formula*) fun cutR_tac ctxt s i = - res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i + res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN rtac @{thm thinR} i (*Cut and thin, replacing the left-side formula*) fun cutL_tac ctxt s i = - res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) + res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) *} diff -r 696d87036f04 -r f8d164ab0dc1 src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/Tools/induct_tacs.ML Thu Mar 19 22:30:57 2015 +0100 @@ -44,7 +44,7 @@ (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of Var (xi, _) :: _ => xi | _ => raise THM ("Malformed cases rule", 0, [rule])); - in res_inst_tac ctxt [(xi, s)] rule i st end + in res_inst_tac ctxt [((xi, Position.none), s)] rule i st end handle THM _ => Seq.empty; fun case_tac ctxt s = gen_case_tac ctxt s NONE; @@ -55,7 +55,7 @@ local -fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) +fun prep_var (Var (xi, _), SOME x) = SOME ((xi, Position.none), x) | prep_var _ = NONE; fun prep_inst (concl, xs) = diff -r 696d87036f04 -r f8d164ab0dc1 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Thu Mar 19 22:30:57 2015 +0100 @@ -101,7 +101,7 @@ [] => error "induction is not available for this datatype" | major::_ => FOLogic.dest_Trueprop major) in - eres_inst_tac ctxt [(ixn, var)] rule i + eres_inst_tac ctxt [((ixn, Position.none), var)] rule i end handle Find_tname msg => if exh then (*try boolean case analysis instead*) diff -r 696d87036f04 -r f8d164ab0dc1 src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/ZF/UNITY/SubstAx.thy Thu Mar 19 22:30:57 2015 +0100 @@ -359,7 +359,7 @@ @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2, - res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, + res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ctxt addsimps [@{thm domain_def}]) 3, (* proving the domain part *) diff -r 696d87036f04 -r f8d164ab0dc1 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Thu Mar 19 17:25:57 2015 +0100 +++ b/src/ZF/ind_syntax.ML Thu Mar 19 22:30:57 2015 +0100 @@ -50,7 +50,7 @@ (*For deriving cases rules. CollectD2 discards the domain, which is redundant; read_instantiate replaces a propositional variable by a formula variable*) val equals_CollectD = - Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"] + Rule_Insts.read_instantiate @{context} [((("W", 0), Position.none), "Q")] ["Q"] (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));