explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
--- a/NEWS Sat Jan 25 21:52:04 2014 +0100
+++ b/NEWS Sat Jan 25 22:06:07 2014 +0100
@@ -40,6 +40,10 @@
*** Pure ***
+* Attributes "where" and "of" allow an optional context of local
+variables ('for' declaration): these variables become schematic in the
+instantiated theorem.
+
* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps). Potential INCOMPATIBILITY, tools need to observe standard
@@ -269,6 +273,13 @@
*** ML ***
+* Proper context discipline for read_instantiate and instantiate_tac:
+variables that are meant to become schematic need to be given as
+fixed, and are generalized by the explicit context of local variables.
+This corresponds to Isar attributes "where" and "of" with 'for'
+declaration. INCOMPATIBILITY, also due to potential change of indices
+of schematic variables.
+
* Toplevel function "use" refers to raw ML bootstrap environment,
without Isar context nor antiquotations. Potential INCOMPATIBILITY.
Note that 'ML_file' is the canonical command to load ML files into the
--- a/src/Doc/IsarRef/Proof.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Sat Jan 25 22:06:07 2014 +0100
@@ -721,11 +721,13 @@
;
@@{attribute OF} @{syntax thmrefs}
;
- @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
+ @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
+ (@'for' (@{syntax vars} + @'and'))?
;
@@{attribute "where"}
((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
- (@{syntax type} | @{syntax term}) * @'and')
+ (@{syntax type} | @{syntax term}) * @'and') \<newline>
+ (@'for' (@{syntax vars} + @'and'))?
\<close>}
\begin{description}
@@ -812,6 +814,10 @@
left to right; ``@{text _}'' (underscore) indicates to skip a
position. Arguments following a ``@{text "concl:"}'' specification
refer to positions of the conclusion of a rule.
+
+ An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ be specified: the instantiated theorem is exported, and these
+ variables become schematic (usually with some shifting of indices).
\item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
performs named instantiation of schematic type and term variables
@@ -821,6 +827,9 @@
As type instantiations are inferred from term instantiations,
explicit type instantiations are seldom necessary.
+ An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ be specified as for @{attribute "of"} above.
+
\end{description}
*}
--- a/src/Doc/isar.sty Sat Jan 25 21:52:04 2014 +0100
+++ b/src/Doc/isar.sty Sat Jan 25 22:06:07 2014 +0100
@@ -11,6 +11,7 @@
\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
+\newcommand{\isasymFOR}{\isakeyword{for}}
\newcommand{\isasymAND}{\isakeyword{and}}
\newcommand{\isasymIS}{\isakeyword{is}}
\newcommand{\isasymWHERE}{\isakeyword{where}}
--- a/src/HOL/Bali/AxExample.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sat Jan 25 22:06:07 2014 +0100
@@ -41,9 +41,9 @@
declare lvar_def [simp]
ML {*
-fun inst1_tac ctxt s t st =
+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 => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
+ SOME i => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty;
val ax_tac =
REPEAT o rtac allI THEN'
@@ -64,7 +64,7 @@
apply (tactic "ax_tac 1" (* Try *))
defer
apply (tactic {* inst1_tac @{context} "Q"
- "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
+ "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
prefer 2
apply simp
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
@@ -83,7 +83,7 @@
apply (tactic "ax_tac 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply (simp del: avar_def2 peek_and_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -124,7 +124,7 @@
apply (tactic "ax_tac 1") (* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *})
apply (rule allI)
apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
apply (rule ax_derivs.Abrupt)
@@ -132,17 +132,17 @@
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
apply (tactic "ax_tac 1")
-apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
+apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" [] *})
apply fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *})
apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -161,7 +161,7 @@
apply (tactic "ax_tac 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
@@ -189,18 +189,18 @@
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *})
apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
+apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *})
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
apply (tactic "ax_tac 2")
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
-apply (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
+apply (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" [] *})
apply (clarsimp split del: split_if)
apply (frule atleast_free_weaken [THEN atleast_free_weaken])
apply (drule initedD)
@@ -210,9 +210,9 @@
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *})
apply clarsimp
-apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
+apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *})
apply clarsimp
(* end init *)
apply (rule conseq1)
@@ -244,7 +244,7 @@
apply clarsimp
apply (tactic "ax_tac 1" (* If *))
apply (tactic
- {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+ {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *})
apply (tactic "ax_tac 1")
apply (rule conseq1)
apply (tactic "ax_tac 1")
@@ -265,7 +265,7 @@
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
apply (rule allI)
apply (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
--- a/src/HOL/Bali/Basis.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sat Jan 25 22:06:07 2014 +0100
@@ -181,7 +181,7 @@
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
simplify (ctxt delsimps [@{thm not_None_eq}])
- (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+ (read_instantiate ctxt [(("t", 0), "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/Library/Binomial.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Library/Binomial.thy Sat Jan 25 22:06:07 2014 +0100
@@ -131,7 +131,7 @@
prefer 4 apply (force simp add: constr_bij)
prefer 3 apply force
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
- finite_subset [of _ "Pow (insert x F)", standard])
+ finite_subset [of _ "Pow (insert x F)" for F])
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
qed
--- a/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 22:06:07 2014 +0100
@@ -133,7 +133,7 @@
prefer 4 apply (force simp add: constr_bij)
prefer 3 apply force
prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
- finite_subset [of _ "Pow (insert x F)", standard])
+ finite_subset [of _ "Pow (insert x F)" for F])
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
qed
@@ -669,7 +669,9 @@
have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
using assms by(auto intro!: inj_onI)
moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
- using assms by(auto intro!: rev_image_eqI[where x="(card a, a)", standard] simp add: card_gt_0_iff[folded Suc_le_eq] dest: finite_subset intro: card_mono)
+ using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
+ simp add: card_gt_0_iff[folded Suc_le_eq]
+ dest: finite_subset intro: card_mono)
ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
by(rule setsum_reindex_cong[where f=snd]) fastforce
also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
--- a/src/HOL/Prolog/prolog.ML Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Prolog/prolog.ML Sat Jan 25 22:06:07 2014 +0100
@@ -49,14 +49,16 @@
fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm)
then thm else raise not_HOHH);
-fun atomizeD ctxt thm = let
+fun atomizeD ctxt thm =
+ let
fun at thm = case concl_of thm of
- _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
- (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
+ _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
+ let val s' = if s="P" then "PP" else s
+ in at(thm RS (read_instantiate ctxt [(("x", 0), 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]
-in map zero_var_indexes (at thm) end;
+ in map zero_var_indexes (at thm) end;
val atomize_ss =
(empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs))
--- a/src/HOL/Rat.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Rat.thy Sat Jan 25 22:06:07 2014 +0100
@@ -622,8 +622,8 @@
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
#> Lin_Arith.add_simps [@{thm neg_less_iff_less},
@{thm True_implies_equals},
- read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
- read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
+ @{thm distrib_left [where a = "numeral v" for v]},
+ @{thm distrib_left [where a = "- numeral v" for v]},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
--- a/src/HOL/Set.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Set.thy Sat Jan 25 22:06:07 2014 +0100
@@ -1577,10 +1577,10 @@
by (auto simp add: Pow_def)
lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
- by (blast intro: image_eqI [where ?x = "u - {a}", standard])
+ by (blast intro: image_eqI [where ?x = "u - {a}" for u])
lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
- by (blast intro: exI [where ?x = "- u", standard])
+ by (blast intro: exI [where ?x = "- u" for u])
lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
by blast
--- a/src/HOL/Set_Interval.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Set_Interval.thy Sat Jan 25 22:06:07 2014 +0100
@@ -728,7 +728,7 @@
qed auto
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
-by(auto intro!: image_eqI[where x="nat x", standard])
+ by (auto intro!: image_eqI [where x = "nat x" for x])
context ordered_ab_group_add
begin
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 22:06:07 2014 +0100
@@ -416,7 +416,7 @@
|> hackish_string_of_term ctxt
in
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
- stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
+ stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)] [])
end
fun type_match thy (T1, T2) =
--- a/src/HOL/Tools/TFL/post.ML Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sat Jan 25 22:06:07 2014 +0100
@@ -130,7 +130,7 @@
rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
-val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
+val spec'= read_instantiate @{context} [(("x", 0), "P::'b=>bool")] [] spec;
fun tracing true _ = ()
| tracing false msg = writeln msg;
--- a/src/Pure/Tools/rule_insts.ML Sat Jan 25 21:52:04 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sat Jan 25 22:06:07 2014 +0100
@@ -6,8 +6,8 @@
signature BASIC_RULE_INSTS =
sig
- val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
- val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
+ val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
+ val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
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
@@ -20,6 +20,10 @@
signature RULE_INSTS =
sig
include BASIC_RULE_INSTS
+ val where_rule: Proof.context -> (indexname * 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 make_elim_preserve: thm -> thm
val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
@@ -123,9 +127,10 @@
(map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
end;
-fun read_instantiate_mixed ctxt mixed_insts thm =
+fun where_rule ctxt mixed_insts fixes thm =
let
val ctxt' = ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
|> Variable.declare_thm thm
|> fold (fn a => Variable.declare_names (Logic.mk_type (TFree (a, dummyS)))) (add_used thm []); (* FIXME !? *)
val tvars = Thm.fold_terms Term.add_tvars thm [];
@@ -133,10 +138,11 @@
val insts = read_insts ctxt' mixed_insts (tvars, vars);
in
Drule.instantiate_normalize insts thm
+ |> singleton (Proof_Context.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+fun of_rule ctxt (args, concl_args) fixes thm =
let
fun zip_vars _ [] = []
| zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
@@ -145,17 +151,18 @@
val insts =
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
- in read_instantiate_mixed ctxt insts thm end;
+ in where_rule ctxt insts fixes thm end;
end;
(* instantiation of rule or goal state *)
-fun read_instantiate ctxt =
- read_instantiate_mixed (ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic); (* FIXME !? *)
+fun read_instantiate ctxt insts xs =
+ where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
-fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+fun instantiate_tac ctxt insts fixes =
+ PRIMITIVE (read_instantiate ctxt insts fixes);
@@ -165,9 +172,10 @@
val _ = Theory.setup
(Attrib.setup @{binding "where"}
- (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
- (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+ (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)))
"named instantiation of theorem");
@@ -186,8 +194,8 @@
val _ = Theory.setup
(Attrib.setup @{binding "of"}
- (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
+ (Scan.lift (insts -- Parse.for_fixes) >> (fn (args, fixes) =>
+ Thm.rule_attribute (fn context => of_rule (Context.proof_of context) args fixes)))
"positional instantiation of theorem");
end;
--- a/src/ZF/ind_syntax.ML Sat Jan 25 21:52:04 2014 +0100
+++ b/src/ZF/ind_syntax.ML Sat Jan 25 22:06:07 2014 +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 =
- read_instantiate @{context} [(("W", 0), "?Q")]
+ read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));