--- a/.hgignore Sat Jan 25 19:07:07 2014 +0100
+++ b/.hgignore Sat Jan 25 22:18:20 2014 +0100
@@ -5,7 +5,6 @@
*.jar
*.orig
*.rej
-*.pyc
.DS_Store
.swp
--- a/Admin/user-aliases Sat Jan 25 19:07:07 2014 +0100
+++ b/Admin/user-aliases Sat Jan 25 22:18:20 2014 +0100
@@ -1,4 +1,5 @@
lcp paulson
+lp15@cam.ac.uk paulson
norbert.schirmer@web.de schirmer
schirmer@in.tum.de schirmer
urbanc@in.tum.de urbanc
--- a/NEWS Sat Jan 25 19:07:07 2014 +0100
+++ b/NEWS Sat Jan 25 22:18:20 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
@@ -53,6 +57,9 @@
*** HOL ***
+* Simproc "finite_Collect" is no longer enabled by default, due to
+spurious crashes and other surprises. Potential INCOMPATIBILITY.
+
* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
"primrec_new", "primcorec", and "primcorecursive" command are now part of
@@ -266,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 19:07:07 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Sat Jan 25 22:18:20 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/Tutorial/Protocol/Event.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Sat Jan 25 22:18:20 2014 +0100
@@ -93,7 +93,7 @@
(*Simplifying
parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
lemma knows_Spy_Says [simp]:
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -256,7 +256,7 @@
knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
ML
{*
@@ -290,7 +290,7 @@
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
ML
{*
--- a/src/Doc/Tutorial/Protocol/Message.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sat Jan 25 22:18:20 2014 +0100
@@ -190,7 +190,7 @@
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
@@ -388,9 +388,9 @@
apply (erule analz.induct, blast+)
done
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -404,7 +404,7 @@
apply (erule analz.induct, auto)
done
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection{*General equational properties *}
@@ -786,21 +786,23 @@
text{*Rewrites to push in Key and Crypt messages, so that other messages can
be pulled out using the @{text analz_insert} rules*}
-lemmas pushKeys [standard] =
+lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
insert_commute [of "Key K" "Nonce N"]
insert_commute [of "Key K" "Number N"]
insert_commute [of "Key K" "Hash X"]
insert_commute [of "Key K" "MPair X Y"]
insert_commute [of "Key K" "Crypt X K'"]
+ for K C N X Y K'
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Nonce N"]
insert_commute [of "Crypt X K" "Number N"]
insert_commute [of "Crypt X K" "Hash X'"]
insert_commute [of "Crypt X K" "MPair X' Y"]
+ for X K C N X' Y
text{*Cannot be added with @{text "[simp]"} -- messages should not always be
re-ordered. *}
--- a/src/Doc/isar.sty Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Doc/isar.sty Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Library/Binomial.thy Sat Jan 25 22:18:20 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/Library/Numeral_Type.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sat Jan 25 22:18:20 2014 +0100
@@ -284,8 +284,8 @@
lemmas bit0_iszero_numeral [simp] = bit0.iszero_numeral
lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
-declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
+lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
subsection {* Order instances *}
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Jan 25 22:18:20 2014 +0100
@@ -1514,8 +1514,7 @@
assume i: "i \<in> Basis"
have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
- by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf uminus_add_conv_diff
- norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
+ by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
also have "\<dots> \<le> e + e"
unfolding real_norm_def
by (intro add_mono norm_bound_Basis_le i fPs) auto
--- a/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Prolog/prolog.ML Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Rat.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Set.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Set_Interval.thy Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 22:18:20 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 19:07:07 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sat Jan 25 22:18:20 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/HOL/ex/Cartouche_Examples.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Sat Jan 25 22:18:20 2014 +0100
@@ -52,35 +52,35 @@
end;
*}
-syntax "_STR_cartouche" :: "cartouche_position \<Rightarrow> string" ("STR _")
+syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_")
parse_translation {*
- [(@{syntax_const "_STR_cartouche"},
+ [(@{syntax_const "_cartouche_string"},
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
*}
-term "STR \<open>\<close>"
-term "STR \<open>abc\<close>"
-term "STR \<open>abc\<close> @ STR \<open>xyz\<close>"
-term "STR \<open>\<newline>\<close>"
-term "STR \<open>\001\010\100\<close>"
+term "\<open>\<close>"
+term "\<open>abc\<close>"
+term "\<open>abc\<close> @ \<open>xyz\<close>"
+term "\<open>\<newline>\<close>"
+term "\<open>\001\010\100\<close>"
subsection {* Alternate outer and inner syntax: string literals *}
subsubsection {* Nested quotes *}
-syntax "_STR_string" :: "string_position \<Rightarrow> string" ("STR _")
+syntax "_string_string" :: "string_position \<Rightarrow> string" ("_")
parse_translation {*
- [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))]
+ [(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
*}
-term "STR \"\""
-term "STR \"abc\""
-term "STR \"abc\" @ STR \"xyz\""
-term "STR \"\<newline>\""
-term "STR \"\001\010\100\""
+term "\"\""
+term "\"abc\""
+term "\"abc\" @ \"xyz\""
+term "\"\<newline>\""
+term "\"\001\010\100\""
subsubsection {* Term cartouche and regular quotes *}
@@ -95,11 +95,11 @@
in writeln (Syntax.string_of_term ctxt t) end)))
*}
-term_cartouche \<open>STR ""\<close>
-term_cartouche \<open>STR "abc"\<close>
-term_cartouche \<open>STR "abc" @ STR "xyz"\<close>
-term_cartouche \<open>STR "\<newline>"\<close>
-term_cartouche \<open>STR "\001\010\100"\<close>
+term_cartouche \<open>""\<close>
+term_cartouche \<open>"abc"\<close>
+term_cartouche \<open>"abc" @ "xyz"\<close>
+term_cartouche \<open>"\<newline>"\<close>
+term_cartouche \<open>"\001\010\100"\<close>
subsubsection {* Further nesting: antiquotations *}
@@ -125,22 +125,22 @@
*}
ML {*
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>};
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>};
*}
text {*
@{ML_cartouche
\<open>
(
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>}
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -160,11 +160,11 @@
@{ML_cartouche
\<open>
(
- @{term_cartouche \<open>STR ""\<close>};
- @{term_cartouche \<open>STR "abc"\<close>};
- @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
- @{term_cartouche \<open>STR "\<newline>"\<close>};
- @{term_cartouche \<open>STR "\001\010\100"\<close>}
+ @{term_cartouche \<open>""\<close>};
+ @{term_cartouche \<open>"abc"\<close>};
+ @{term_cartouche \<open>"abc" @ "xyz"\<close>};
+ @{term_cartouche \<open>"\<newline>"\<close>};
+ @{term_cartouche \<open>"\001\010\100"\<close>}
)
\<close>
}
--- a/src/Pure/Isar/attrib.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Jan 25 22:18:20 2014 +0100
@@ -37,6 +37,7 @@
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
theory -> theory
+ val internal: (morphism -> attribute) -> src
val add_del: attribute -> attribute -> attribute context_parser
val thm_sel: Facts.interval list parser
val thm: thm context_parser
@@ -45,7 +46,6 @@
val partial_evaluation: Proof.context ->
(binding * (thm list * Args.src list) list) list ->
(binding * (thm list * Args.src list) list) list
- val internal: (morphism -> attribute) -> src
val print_options: Proof.context -> unit
val config_bool: Binding.binding ->
(Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -194,6 +194,15 @@
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
+(* internal attribute *)
+
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
+
+val _ = Theory.setup
+ (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+ "internal attribute");
+
+
(* add/del syntax *)
fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
@@ -318,119 +327,6 @@
-(** basic attributes **)
-
-(* internal *)
-
-fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
-
-
-(* rule composition *)
-
-val THEN_att =
- Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
-
-val OF_att =
- thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
-
-
-(* rename_abs *)
-
-val rename_abs =
- Scan.repeat (Args.maybe Args.name)
- >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
-
-
-(* unfold / fold definitions *)
-
-fun unfolded_syntax rule =
- thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
-
-val unfolded = unfolded_syntax Local_Defs.unfold;
-val folded = unfolded_syntax Local_Defs.fold;
-
-
-(* rule format *)
-
-fun rule_format true = Object_Logic.rule_format_no_asm
- | rule_format false = Object_Logic.rule_format;
-
-val elim_format = Thm.rule_attribute (K Tactic.make_elim);
-
-
-(* case names *)
-
-val case_names =
- Scan.repeat1 (Args.name --
- Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
- (fn cs =>
- Rule_Cases.cases_hyp_names (map fst cs)
- (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
-
-
-(* misc rules *)
-
-val no_vars = Thm.rule_attribute (fn context => fn th =>
- let
- val ctxt = Variable.set_body false (Context.proof_of context);
- val ((_, [th']), _) = Variable.import true [th] ctxt;
- in th' end);
-
-val eta_long =
- Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
-
-val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
-
-
-(* theory setup *)
-
-val _ = Theory.setup
- (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
- "internal attribute" #>
- setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
- setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
- setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
- setup (Binding.name "THEN") THEN_att "resolution with rule" #>
- setup (Binding.name "OF") OF_att "rule applied to facts" #>
- setup (Binding.name "rename_abs") (Scan.lift rename_abs)
- "rename bound variables in abstractions" #>
- setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
- setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
- "number of consumed facts" #>
- setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
- "number of equality constraints" #>
- setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
- setup (Binding.name "case_conclusion")
- (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
- "named conclusion of rule cases" #>
- setup (Binding.name "params")
- (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
- "named rule parameters" #>
- setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
- "result put into standard form (legacy)" #>
- setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
- "result put into canonical rule format" #>
- setup (Binding.name "elim_format") (Scan.succeed elim_format)
- "destruct rule turned into elimination rule format" #>
- setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
- setup (Binding.name "eta_long") (Scan.succeed eta_long)
- "put theorem into eta long beta normal form" #>
- setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
- "declaration of atomize rule" #>
- setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
- "declaration of rulify rule" #>
- setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
- setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
- "declaration of definitional transformations" #>
- setup (Binding.name "abs_def")
- (Scan.succeed (Thm.rule_attribute (fn context =>
- Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
- "abstract over free variables of definitional theorem");
-
-
-
(** configuration options **)
(* naming *)
--- a/src/Pure/Isar/calculation.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Sat Jan 25 22:18:20 2014 +0100
@@ -95,11 +95,11 @@
(* concrete syntax *)
val _ = Theory.setup
- (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del)
"declaration of transitivity rule" #>
- Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+ Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del)
"declaration of symmetry rule" #>
- Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+ Attrib.setup @{binding symmetric} (Scan.succeed symmetric)
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
@@ -197,4 +197,32 @@
val moreover = collect false;
val ultimately = collect true;
+
+(* outer syntax *)
+
+val calc_args =
+ Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
+
+val _ =
+ Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
+ (calc_args >> (Toplevel.proofs' o also_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "finally"}
+ "combine calculation and current facts, exhibit result"
+ (calc_args >> (Toplevel.proofs' o finally_cmd));
+
+val _ =
+ Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
+ (Scan.succeed (Toplevel.proof' moreover));
+
+val _ =
+ Outer_Syntax.command @{command_spec "ultimately"}
+ "augment calculation by current facts, exhibit result"
+ (Scan.succeed (Toplevel.proof' ultimately));
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+ (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+
end;
--- a/src/Pure/Isar/isar_syn.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Jan 25 22:18:20 2014 +0100
@@ -688,30 +688,6 @@
Toplevel.skip_proof (fn i => i + 1)));
-(* calculational proof commands *)
-
-val calc_args =
- Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
-
-val _ =
- Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
- (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "finally"}
- "combine calculation and current facts, exhibit result"
- (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
- (Scan.succeed (Toplevel.proof' Calculation.moreover));
-
-val _ =
- Outer_Syntax.command @{command_spec "ultimately"}
- "augment calculation by current facts, exhibit result"
- (Scan.succeed (Toplevel.proof' Calculation.ultimately));
-
-
(* proof navigation *)
val _ =
@@ -847,11 +823,6 @@
Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
--- a/src/Pure/Isar/token.scala Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Isar/token.scala Sat Jan 25 22:18:20 2014 +0100
@@ -108,7 +108,7 @@
else source
def text: (String, String) =
- if (is_command && source == ";") ("terminator", "")
+ if (is_keyword && source == ";") ("terminator", "")
else (kind.toString, source)
}
--- a/src/Pure/Pure.thy Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Pure.thy Sat Jan 25 22:18:20 2014 +0100
@@ -103,6 +103,7 @@
begin
ML_file "Isar/isar_syn.ML"
+ML_file "Isar/calculation.ML"
ML_file "Tools/rail.ML"
ML_file "Tools/rule_insts.ML";
ML_file "Tools/find_theorems.ML"
@@ -111,6 +112,117 @@
ML_file "Tools/simplifier_trace.ML"
+section {* Basic attributes *}
+
+attribute_setup tagged =
+ "Scan.lift (Args.name -- Args.name) >> Thm.tag"
+ "tagged theorem"
+
+attribute_setup untagged =
+ "Scan.lift Args.name >> Thm.untag"
+ "untagged theorem"
+
+attribute_setup kind =
+ "Scan.lift Args.name >> Thm.kind"
+ "theorem kind"
+
+attribute_setup THEN =
+ "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
+ >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
+ "resolution with rule"
+
+attribute_setup OF =
+ "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
+ "rule resolved with facts"
+
+attribute_setup rename_abs =
+ "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
+ Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
+ "rename bound variables in abstractions"
+
+attribute_setup unfolded =
+ "Attrib.thms >> (fn ths =>
+ Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
+ "unfolded definitions"
+
+attribute_setup folded =
+ "Attrib.thms >> (fn ths =>
+ Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
+ "folded definitions"
+
+attribute_setup consumes =
+ "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
+ "number of consumed facts"
+
+attribute_setup constraints =
+ "Scan.lift Parse.nat >> Rule_Cases.constraints"
+ "number of equality constraints"
+
+attribute_setup case_names = {*
+ Scan.lift (Scan.repeat1 (Args.name --
+ Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
+ >> (fn cs =>
+ Rule_Cases.cases_hyp_names
+ (map #1 cs)
+ (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
+*} "named rule cases"
+
+attribute_setup case_conclusion =
+ "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
+ "named conclusion of rule cases"
+
+attribute_setup params =
+ "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
+ "named rule parameters"
+
+attribute_setup standard =
+ "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
+ "result put into standard form (legacy)"
+
+attribute_setup rule_format = {*
+ Scan.lift (Args.mode "no_asm")
+ >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
+*} "result put into canonical rule format"
+
+attribute_setup elim_format =
+ "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
+ "destruct rule turned into elimination rule format"
+
+attribute_setup no_vars = {*
+ Scan.succeed (Thm.rule_attribute (fn context => fn th =>
+ let
+ val ctxt = Variable.set_body false (Context.proof_of context);
+ val ((_, [th']), _) = Variable.import true [th] ctxt;
+ in th' end))
+*} "imported schematic variables"
+
+attribute_setup eta_long =
+ "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
+ "put theorem into eta long beta normal form"
+
+attribute_setup atomize =
+ "Scan.succeed Object_Logic.declare_atomize"
+ "declaration of atomize rule"
+
+attribute_setup rulify =
+ "Scan.succeed Object_Logic.declare_rulify"
+ "declaration of rulify rule"
+
+attribute_setup rotated =
+ "Scan.lift (Scan.optional Parse.int 1
+ >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
+ "rotated theorem premises"
+
+attribute_setup defn =
+ "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
+ "declaration of definitional transformations"
+
+attribute_setup abs_def =
+ "Scan.succeed (Thm.rule_attribute (fn context =>
+ Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
+ "abstract over free variables of definitional theorem"
+
+
section {* Further content for the Pure theory *}
subsection {* Meta-level connectives in assumptions *}
--- a/src/Pure/ROOT Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/ROOT Sat Jan 25 22:18:20 2014 +0100
@@ -106,7 +106,6 @@
"Isar/attrib.ML"
"Isar/auto_bind.ML"
"Isar/bundle.ML"
- "Isar/calculation.ML"
"Isar/class.ML"
"Isar/class_declaration.ML"
"Isar/code.ML"
--- a/src/Pure/ROOT.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/ROOT.ML Sat Jan 25 22:18:20 2014 +0100
@@ -236,9 +236,6 @@
use "Isar/method.ML";
use "Isar/proof.ML";
use "Isar/element.ML";
-
-(*derived theory and proof elements*)
-use "Isar/calculation.ML";
use "Isar/obtain.ML";
(*local theories and targets*)
--- a/src/Pure/System/session.scala Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/System/session.scala Sat Jan 25 22:18:20 2014 +0100
@@ -180,12 +180,12 @@
case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
val prev = previous.get_finished
- val (doc_edits, version) =
+ val (syntax_changed, doc_edits, version) =
Timing.timeit("Thy_Load.text_edits", timing) {
thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
}
version_result.fulfill(version)
- sender ! Change(doc_blobs, doc_edits, prev, version)
+ sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
case bad => System.err.println("change_parser: ignoring bad message " + bad)
}
@@ -252,6 +252,7 @@
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Change(
doc_blobs: Document.Blobs,
+ syntax_changed: Boolean,
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
version: Document.Version)
@@ -370,9 +371,7 @@
def handle_change(change: Change)
//{{{
{
- val previous = change.previous
- val version = change.version
- val doc_edits = change.doc_edits
+ val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
def id_command(command: Command)
{
@@ -380,7 +379,7 @@
digest <- command.blobs_digests
if !global_state().defined_blob(digest)
} {
- change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+ doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
case Some(blob) =>
global_state >> (_.define_blob(digest))
prover.get.define_blob(blob)
@@ -401,6 +400,8 @@
val assignment = global_state().the_assignment(previous).check_finished
global_state >> (_.define_version(version, assignment))
prover.get.update(previous.id, version.id, doc_edits)
+
+ if (syntax_changed) thy_load.syntax_changed()
}
//}}}
--- a/src/Pure/Thy/thy_load.scala Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Thy/thy_load.scala Sat Jan 25 22:18:20 2014 +0100
@@ -103,7 +103,9 @@
reparse_limit: Int,
previous: Document.Version,
doc_blobs: Document.Blobs,
- edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+ edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+
+ def syntax_changed() { }
}
--- a/src/Pure/Thy/thy_syntax.scala Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sat Jan 25 22:18:20 2014 +0100
@@ -155,8 +155,8 @@
private def header_edits(
base_syntax: Outer_Syntax,
previous: Document.Version,
- edits: List[Document.Edit_Text])
- : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
+ edits: List[Document.Edit_Text]):
+ ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
{
var updated_imports = false
var updated_keywords = false
@@ -179,11 +179,14 @@
}
val syntax =
- if (previous.is_init || updated_keywords)
- (base_syntax /: nodes.entries) {
- case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
- }
- else previous.syntax
+ if (previous.is_init || updated_keywords) {
+ val syntax =
+ (base_syntax /: nodes.entries) {
+ case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+ }
+ (syntax, true)
+ }
+ else (previous.syntax, false)
val reparse =
if (updated_imports || updated_keywords)
@@ -428,13 +431,13 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text])
- : (List[Document.Edit_Command], Document.Version) =
+ : (Boolean, List[Document.Edit_Command], Document.Version) =
{
- val (syntax, reparse0, nodes0, doc_edits0) =
+ val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
header_edits(thy_load.base_syntax, previous, edits)
if (edits.isEmpty)
- (Nil, Document.Version.make(syntax, previous.nodes))
+ (false, Nil, Document.Version.make(syntax, previous.nodes))
else {
val reparse =
(reparse0 /: nodes0.entries)({
@@ -472,7 +475,7 @@
nodes += (name -> node2)
}
- (doc_edits.toList, Document.Version.make(syntax, nodes))
+ (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
}
}
}
--- a/src/Pure/Tools/rule_insts.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sat Jan 25 22:18:20 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/Tools/jEdit/src/jedit_thy_load.scala Sat Jan 25 19:07:07 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Sat Jan 25 22:18:20 2014 +0100
@@ -14,7 +14,7 @@
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
-import org.gjt.sp.jedit.{View, Buffer}
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.bufferio.BufferIORequest
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
@@ -111,5 +111,11 @@
}
content()
}
+
+
+ /* theory text edits */
+
+ override def syntax_changed(): Unit =
+ Swing_Thread.later { jEdit.propertiesChanged() }
}
--- a/src/ZF/ind_syntax.ML Sat Jan 25 19:07:07 2014 +0100
+++ b/src/ZF/ind_syntax.ML Sat Jan 25 22:18:20 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}));