# HG changeset patch # User paulson # Date 1426860375 0 # Node ID 66fc7122f51a865a0657e9fe6b88b5d54d96c4ab # Parent 93d4169e07dc78f96c66654e8ceef2a619d89d4a# Parent 96abba46955f65a5fd1d6ff656a46b0a43f6e8b7 Merge diff -r 93d4169e07dc -r 66fc7122f51a src/CCL/CCL.thy --- a/src/CCL/CCL.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/CCL/CCL.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/CCL/Wfd.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/CTT/CTT.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Doc/Implementation/Tactic.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/FOL/FOL.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Auth/Message.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Bali/AxExample.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Bali/Basis.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Prolog/prolog.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/TLA/TLA.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Tools/TFL/post.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/Tools/etc/options Fri Mar 20 14:06:15 2015 +0000 @@ -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)" diff -r 93d4169e07dc -r 66fc7122f51a src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/LCF/LCF.thy --- a/src/LCF/LCF.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/LCF/LCF.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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) diff -r 93d4169e07dc -r 66fc7122f51a src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Sequents/LK0.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Tools/induct_tacs.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Mar 20 14:00:22 2015 +0000 +++ b/src/Tools/jEdit/etc/options Fri Mar 20 14:06:15 2015 +0000 @@ -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" - diff -r 93d4169e07dc -r 66fc7122f51a src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Fri Mar 20 14:00:22 2015 +0000 +++ b/src/ZF/UNITY/SubstAx.thy Fri Mar 20 14:06:15 2015 +0000 @@ -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 93d4169e07dc -r 66fc7122f51a src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Fri Mar 20 14:00:22 2015 +0000 +++ b/src/ZF/ind_syntax.ML Fri Mar 20 14:06:15 2015 +0000 @@ -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}));