--- a/src/CCL/CCL.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/CCL/CCL.thy Thu Mar 19 22:31:23 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}))
*}
--- a/src/CCL/Wfd.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/CCL/Wfd.thy Thu Mar 19 22:31:23 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: "\<lbrakk>Wfd(r); <a,x>:r; <x,a>:r\<rbrakk> \<Longrightarrow> 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 =
--- a/src/CTT/CTT.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/CTT/CTT.thy Thu Mar 19 22:31:23 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. **)
--- a/src/Doc/Implementation/Tactic.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Doc/Implementation/Tactic.thy Thu Mar 19 22:31:23 2015 +0100
@@ -394,10 +394,14 @@
text %mlref \<open>
\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"} \\
--- a/src/Doc/Tutorial/Protocol/Message.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Mar 19 22:31:23 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])),
--- a/src/FOL/FOL.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/FOL/FOL.thy Thu Mar 19 22:31:23 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 = {*
--- a/src/HOL/Auth/Message.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Auth/Message.thy Thu Mar 19 22:31:23 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])),
--- a/src/HOL/Bali/AxExample.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Bali/AxExample.thy Thu Mar 19 22:31:23 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 =
--- a/src/HOL/Bali/Basis.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Bali/Basis.thy Thu Mar 19 22:31:23 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] *)
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 22:31:23 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;
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Thu Mar 19 22:31:23 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)
--- a/src/HOL/Prolog/prolog.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Prolog/prolog.ML Thu Mar 19 22:31:23 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]
--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Mar 19 22:31:23 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])),
--- a/src/HOL/TLA/TLA.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/TLA/TLA.thy Thu Mar 19 22:31:23 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)) *}
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Mar 19 22:31:23 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 19 22:31:23 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) =
--- a/src/HOL/Tools/TFL/post.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Tools/TFL/post.ML Thu Mar 19 22:31:23 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;
--- a/src/HOL/Tools/etc/options Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/Tools/etc/options Thu Mar 19 22:31:23 2015 +0100
@@ -1,6 +1,6 @@
(* :mode=isabelle-options: *)
-section {* Automatically tried tools *}
+section "Automatically tried tools"
public option auto_time_start : real = 1.0
-- "initial delay for automatically tried tools (seconds)"
--- a/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 22:31:23 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,
--- a/src/LCF/LCF.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/LCF/LCF.thy Thu Mar 19 22:31:23 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)
*}
--- a/src/Pure/Tools/rule_insts.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Pure/Tools/rule_insts.ML Thu Mar 19 22:31:23 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,19 +43,22 @@
(** reading instantiations **)
+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) #>
@@ -82,18 +94,18 @@
let
val thy = Proof_Context.theory_of ctxt;
- val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
+ val (type_insts, term_insts) = partition_insts mixed_insts;
(* 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);
@@ -108,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 *)
@@ -138,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 @
@@ -165,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");
@@ -196,80 +208,84 @@
(** tactics **)
-(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
+(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
-(* FIXME cleanup this mess!!! *)
-
-fun bires_inst_tac bires_flag ctxt insts thm =
+fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) =>
let
val thy = Proof_Context.theory_of ctxt;
- (* Separate type and term insts *)
- fun has_type_var ((x, _), _) =
- (case Symbol.explode x of "'" :: _ => true | _ => false);
- val Tinsts = filter has_type_var insts;
- val tinsts = filter_out has_type_var insts;
+
+ val (Tinsts, tinsts) = partition_insts mixed_insts;
+ val goal = Thm.term_of cgoal;
- (* Tactic *)
- fun tac i st = CSUBGOAL (fn (cgoal, _) =>
+ val params =
+ Logic.strip_params goal
+ (*as they are printed: bound variables with the same name are renamed*)
+ |> Term.rename_wrt_term goal
+ |> rev;
+ val (param_names, ctxt') = ctxt
+ |> Variable.declare_thm thm
+ |> Thm.fold_terms Variable.declare_constraints st
+ |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+
+
+ (* process type insts: Tinsts_env *)
+
+ val (rtypes, rsorts) = Drule.types_sorts thm;
+ fun readT ((xi, pos), s) =
let
- val goal = Thm.term_of cgoal;
- val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*)
- val params = rev (Term.rename_wrt_term goal params)
- (*as they are printed: bound variables with*)
- (*the same name are renamed during printing*)
+ 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_var "Cannot instantiate: " (xi, pos)
+ end;
+ val Tinsts_env = map readT Tinsts;
- val (param_names, ctxt') = ctxt
- |> Variable.declare_thm thm
- |> Thm.fold_terms Variable.declare_constraints st
- |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+
+ (* preprocess rule: extract vars and their types, apply Tinsts *)
- (* 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) =
- let val S = case rsorts xi of SOME S => S | NONE => absent xi;
- 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")
- end;
- val Tinsts_env = map readT Tinsts;
- (* Preprocess rule: extract vars and their types, apply Tinsts *)
- fun get_typ xi =
- (case rtypes xi of
- SOME T => typ_subst_atomic Tinsts_env T
- | NONE => absent xi);
- val (xis, ss) = Library.split_list tinsts;
- val Ts = map get_typ xis;
+ fun get_typ (xi, pos) =
+ (case rtypes xi of
+ SOME T => typ_subst_atomic Tinsts_env T
+ | 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) =
+ read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts;
+ 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))
+ (distinct
+ (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
+ (xis ~~ ts));
+
- val (ts, envT) =
- read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts;
- val envT' = map (fn (ixn, T) =>
- (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
- val cenv =
- 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));
- (* Lift and instantiate rule *)
- val maxidx = Thm.maxidx_of st;
- val paramTs = map #2 params
- and inc = maxidx+1
- fun liftvar (Var ((a,j), T)) =
- Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
- | liftvar t = raise TERM("Variable expected", [t]);
- fun liftterm t =
- fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
- fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
- val lifttvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc);
- val rule = Drule.instantiate_normalize
- (map lifttvar envT', map liftpair cenv)
- (Thm.lift_rule cgoal thm)
- in
- compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i
- end) i st;
- in tac end;
+ (* lift and instantiate rule *)
+
+ val maxidx = Thm.maxidx_of st;
+ val paramTs = map #2 params;
+ val inc = maxidx + 1;
+
+ fun lift_var (Var ((a, j), T)) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T)
+ | lift_var t = raise TERM ("Variable expected", [t]);
+ fun lift_term t =
+ fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
+ fun lift_inst (cv, ct) = (cterm_fun lift_var cv, cterm_fun lift_term ct);
+ val lift_tvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc);
+
+ val rule =
+ Drule.instantiate_normalize
+ (map lift_tvar envT', map lift_inst cenv)
+ (Thm.lift_rule cgoal thm);
+ in
+ compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i
+ end) i st;
val res_inst_tac = bires_inst_tac false;
val eres_inst_tac = bires_inst_tac true;
@@ -306,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;
@@ -318,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)
--- a/src/Sequents/LK0.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Sequents/LK0.thy Thu Mar 19 22:31:23 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)
*}
--- a/src/Tools/induct_tacs.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Tools/induct_tacs.ML Thu Mar 19 22:31:23 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) =
--- a/src/Tools/jEdit/etc/options Thu Mar 19 14:25:32 2015 +0000
+++ b/src/Tools/jEdit/etc/options Thu Mar 19 22:31:23 2015 +0100
@@ -141,4 +141,3 @@
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
option process_passive_icon : string = "idea-icons/process/step_passive.png"
option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png"
-
--- a/src/ZF/Tools/induct_tacs.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/ZF/Tools/induct_tacs.ML Thu Mar 19 22:31:23 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*)
--- a/src/ZF/UNITY/SubstAx.thy Thu Mar 19 14:25:32 2015 +0000
+++ b/src/ZF/UNITY/SubstAx.thy Thu Mar 19 22:31:23 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 *)
--- a/src/ZF/ind_syntax.ML Thu Mar 19 14:25:32 2015 +0000
+++ b/src/ZF/ind_syntax.ML Thu Mar 19 22:31:23 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}));