--- a/NEWS Sat Mar 15 01:36:38 2014 +0100
+++ b/NEWS Sat Mar 15 03:37:22 2014 +0100
@@ -460,6 +460,12 @@
* ML antiquotation @{here} refers to its source position, which is
occasionally useful for experimentation and diagnostic purposes.
+* ML antiquotation @{path} produces a Path.T value, similarly to
+Path.explode, but with compile-time check against the file-system and
+some PIDE markup. Note that unlike theory source, ML does not have a
+well-defined master directory, so an absolute symbolic path
+specification is usually required, e.g. "~~/src/HOL".
+
*** System ***
--- a/etc/isar-keywords-ZF.el Sat Mar 15 01:36:38 2014 +0100
+++ b/etc/isar-keywords-ZF.el Sat Mar 15 03:37:22 2014 +0100
@@ -367,6 +367,7 @@
"hide_fact"
"hide_type"
"inductive"
+ "inductive_cases"
"instantiation"
"judgment"
"lemmas"
@@ -404,7 +405,7 @@
"typedecl"))
(defconst isar-keywords-theory-script
- '("inductive_cases"))
+ '())
(defconst isar-keywords-theory-goal
'("corollary"
--- a/etc/isar-keywords.el Sat Mar 15 01:36:38 2014 +0100
+++ b/etc/isar-keywords.el Sat Mar 15 03:37:22 2014 +0100
@@ -532,7 +532,9 @@
"import_tptp"
"import_type_map"
"inductive"
+ "inductive_cases"
"inductive_set"
+ "inductive_simps"
"instantiation"
"judgment"
"lemmas"
@@ -592,8 +594,7 @@
"typedecl"))
(defconst isar-keywords-theory-script
- '("inductive_cases"
- "inductive_simps"))
+ '())
(defconst isar-keywords-theory-goal
'("ax_specification"
--- a/src/Doc/antiquote_setup.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Sat Mar 15 03:37:22 2014 +0100
@@ -166,12 +166,12 @@
| parse_named _ _ = [];
val jedit_actions =
- (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
+ (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []);
val jedit_dockables =
- (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
+ (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []);
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Mar 15 03:37:22 2014 +0100
@@ -448,8 +448,8 @@
by unfold_locales (* subsumed, thm int2.assoc not generated *)
ML {* (Global_Theory.get_thms @{theory} "int2.assoc";
- error "thm int2.assoc was generated")
- handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
+ raise Fail "thm int2.assoc was generated")
+ handle ERROR _ => ([]:thm list); *}
thm int.lone int.right.rone
(* the latter comes through the sublocale relation *)
@@ -782,8 +782,8 @@
context container begin
ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
val _ = Proof_Context.get_thms context "private.true" in generic end);
- error "thm private.true was persisted")
- handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
+ raise Fail "thm private.true was persisted")
+ handle ERROR _ => ([]:thm list); *}
thm true_copy
end
--- a/src/HOL/Algebra/FiniteProduct.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Sat Mar 15 03:37:22 2014 +0100
@@ -456,7 +456,7 @@
text {*Usually, if this rule causes a failed congruence proof error,
the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.
- For this reason, @{thm [source] comm_monoid.finprod_cong}
+ For this reason, @{thm [source] finprod_cong}
is not added to the simpset by default.
*}
--- a/src/HOL/Inductive.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Inductive.thy Sat Mar 15 03:37:22 2014 +0100
@@ -7,8 +7,8 @@
theory Inductive
imports Complete_Lattices Ctr_Sugar
keywords
- "inductive" "coinductive" :: thy_decl and
- "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+ "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+ "monos" and
"print_inductives" :: diag and
"rep_datatype" :: thy_goal and
"primrec" :: thy_decl
--- a/src/HOL/Lattices_Big.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Lattices_Big.thy Sat Mar 15 03:37:22 2014 +0100
@@ -640,6 +640,11 @@
shows "Max M \<le> Max N"
using assms by (fact Max.antimono)
+end
+
+context linorder (* FIXME *)
+begin
+
lemma mono_Min_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
--- a/src/HOL/Library/refute.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Library/refute.ML Sat Mar 15 03:37:22 2014 +0100
@@ -1073,7 +1073,7 @@
handle Option.Option =>
error ("Unknown SAT solver: " ^ quote satsolver ^
". Available solvers: " ^
- commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
+ commas (map (quote o fst) (SatSolver.get_solvers ())) ^ ".")
in
Output.urgent_message "Invoking SAT solver...";
(case solver fm of
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sat Mar 15 03:37:22 2014 +0100
@@ -293,20 +293,6 @@
subsection {* Differentiability implies continuity *}
-lemma Lim_mul_norm_within:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- shows "(f ---> 0) (at a within s) \<Longrightarrow> ((\<lambda>x. norm(x - a) *\<^sub>R f x) ---> 0) (at a within s)"
- unfolding Lim_within
- apply (auto simp: )
- apply (erule_tac x=e in allE)
- apply (auto simp: )
- apply (rule_tac x="min d 1" in exI)
- apply (auto simp: )
- apply (erule_tac x=x in ballE)
- unfolding dist_norm diff_0_right
- apply (auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left])
- done
-
lemma differentiable_imp_continuous_within:
"f differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (auto simp: differentiable_def intro: FDERIV_continuous)
@@ -340,63 +326,30 @@
unfolding differentiable_on_def
by auto
+text {* Results about neighborhoods filter. *}
+
+lemma eventually_nhds_metric_le:
+ "eventually P (nhds a) = (\<exists>d>0. \<forall>x. dist x a \<le> d \<longrightarrow> P x)"
+ unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
+
+lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
+ unfolding le_filter_def eventually_nhds by (fast elim: eventually_elim1)
+
+lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
+ unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_elim1)
+
+lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
+ unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_elim1)
+
text {* Several results are easier using a "multiplied-out" variant.
(I got this idea from Dieudonne's proof of the chain rule). *}
lemma has_derivative_within_alt:
"(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
(\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?lhs
- then show ?rhs
- unfolding has_derivative_within Lim_within
- apply clarify
- apply (erule_tac x=e in allE)
- apply safe
- apply (rule_tac x=d in exI)
- apply clarify
- proof-
- fix x y e d
- assume as:
- "0 < e"
- "0 < d"
- "norm (y - x) < d"
- "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
- dist ((1 / norm (xa - x)) *\<^sub>R (f xa - (f x + f' (xa - x)))) 0 < e"
- "y \<in> s"
- "bounded_linear f'"
- then interpret bounded_linear f'
- by auto
- show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
- proof (cases "y = x")
- case True
- then show ?thesis
- using `bounded_linear f'` by (auto simp add: zero)
- next
- case False
- then have "norm (f y - (f x + f' (y - x))) < e * norm (y - x)"
- using as(4)[rule_format, OF `y \<in> s`]
- unfolding dist_norm diff_0_right
- using as(3)
- using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm]
- by (auto simp add: linear_0 linear_sub)
- then show ?thesis
- by (auto simp add: algebra_simps)
- qed
- qed
-next
- assume ?rhs
- then show ?lhs
- apply (auto simp: has_derivative_within Lim_within)
- apply (erule_tac x="e/2" in allE, auto)
- apply (rule_tac x=d in exI, auto)
- unfolding dist_norm diff_0_right norm_scaleR
- apply (erule_tac x=xa in ballE, auto)
- apply (rule_tac y="e/2" in le_less_trans)
- apply (auto intro!: mult_imp_div_pos_le simp add: algebra_simps)
- done
-qed
+ unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
+ eventually_at dist_norm diff_add_eq_diff_diff
+ by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq)
lemma has_derivative_at_alt:
"(f has_derivative f') (at x) \<longleftrightarrow>
@@ -617,110 +570,84 @@
unfolding euclidean_representation ..
qed
-text {* We do not introduce @{text jacobian}, which is defined on matrices, instead we use
- the unfolding of it. *}
+text {* Derivatives of local minima and maxima are zero. *}
-lemma jacobian_works:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f differentiable net \<longleftrightarrow>
- (f has_derivative (\<lambda>h. \<Sum>i\<in>Basis.
- (\<Sum>j\<in>Basis. frechet_derivative f net j \<bullet> i * (h \<bullet> j)) *\<^sub>R i)) net"
- (is "?differentiable \<longleftrightarrow> (f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net")
+lemma has_derivative_local_min:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> real"
+ assumes deriv: "(f has_derivative f') (at x)"
+ assumes min: "eventually (\<lambda>y. f x \<le> f y) (at x)"
+ shows "f' = (\<lambda>h. 0)"
proof
- assume *: ?differentiable
- {
- fix h i
- have "?SUM h i = frechet_derivative f net h \<bullet> i"
- using *
- by (auto intro!: setsum_cong simp: linear_componentwise[of _ h i] linear_frechet_derivative)
- }
- with * show "(f has_derivative (\<lambda>h. \<Sum>i\<in>Basis. ?SUM h i *\<^sub>R i)) net"
- by (simp add: frechet_derivative_works euclidean_representation)
-qed (auto intro!: differentiableI)
+ fix h :: 'a
+ interpret f': bounded_linear f'
+ using deriv by (rule FDERIV_bounded_linear)
+ show "f' h = 0"
+ proof (cases "h = 0")
+ assume "h \<noteq> 0"
+ from min obtain d where d1: "0 < d" and d2: "\<forall>y\<in>ball x d. f x \<le> f y"
+ unfolding eventually_at by (force simp: dist_commute)
+ have "FDERIV (\<lambda>r. x + r *\<^sub>R h) 0 :> (\<lambda>r. r *\<^sub>R h)"
+ by (intro FDERIV_eq_intros, auto)
+ then have "FDERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> (\<lambda>k. f' (k *\<^sub>R h))"
+ by (rule FDERIV_compose, simp add: deriv)
+ then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
+ unfolding deriv_fderiv by (simp add: f'.scaleR)
+ moreover have "0 < d / norm h"
+ using d1 and `h \<noteq> 0` by (simp add: divide_pos_pos)
+ moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
+ using `h \<noteq> 0` by (auto simp add: d2 dist_norm pos_less_divide_eq)
+ ultimately show "f' h = 0"
+ by (rule DERIV_local_min)
+ qed (simp add: f'.zero)
+qed
-lemma differential_zero_maxmin_component:
+lemma has_derivative_local_max:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> real"
+ assumes "(f has_derivative f') (at x)"
+ assumes "eventually (\<lambda>y. f y \<le> f x) (at x)"
+ shows "f' = (\<lambda>h. 0)"
+ using has_derivative_local_min [of "\<lambda>x. - f x" "\<lambda>h. - f' h" "x"]
+ using assms unfolding fun_eq_iff by simp
+
+lemma differential_zero_maxmin:
+ fixes f::"'a::real_normed_vector \<Rightarrow> real"
+ assumes "x \<in> s"
+ and "open s"
+ and deriv: "(f has_derivative f') (at x)"
+ and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
+ shows "f' = (\<lambda>v. 0)"
+ using mono
+proof
+ assume "\<forall>y\<in>s. f y \<le> f x"
+ with `x \<in> s` and `open s` have "eventually (\<lambda>y. f y \<le> f x) (at x)"
+ unfolding eventually_at_topological by auto
+ with deriv show ?thesis
+ by (rule has_derivative_local_max)
+next
+ assume "\<forall>y\<in>s. f x \<le> f y"
+ with `x \<in> s` and `open s` have "eventually (\<lambda>y. f x \<le> f y) (at x)"
+ unfolding eventually_at_topological by auto
+ with deriv show ?thesis
+ by (rule has_derivative_local_min)
+qed
+
+lemma differential_zero_maxmin_component: (* TODO: delete? *)
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes k: "k \<in> Basis"
and ball: "0 < e" "(\<forall>y \<in> ball x e. (f y)\<bullet>k \<le> (f x)\<bullet>k) \<or> (\<forall>y\<in>ball x e. (f x)\<bullet>k \<le> (f y)\<bullet>k)"
and diff: "f differentiable (at x)"
shows "(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) = (0::'a)" (is "?D k = 0")
-proof (rule ccontr)
- assume "\<not> ?thesis"
- then obtain j where j: "?D k \<bullet> j \<noteq> 0" "j \<in> Basis"
- unfolding euclidean_eq_iff[of _ "0::'a"] by auto
- then have *: "\<bar>?D k \<bullet> j\<bar> / 2 > 0"
- by auto
- note as = diff[unfolded jacobian_works has_derivative_at_alt]
- obtain e' where e':
- "0 < e'"
- "(\<And>y. norm (y - x) < e' \<Longrightarrow>
- norm (f y - f x -
- (\<Sum>i\<in>Basis. (\<Sum>j\<in>Basis. frechet_derivative f (at x) j \<bullet> i * ((y - x) \<bullet> j)) *\<^sub>R i))
- \<le> \<bar>(\<Sum>j\<in>Basis. (frechet_derivative f (at x) j \<bullet> k) *\<^sub>R j) \<bullet> j\<bar> / 2 * norm (y - x))"
- using as[THEN conjunct2] * by blast
- obtain d where d: "0 < d" "d < e" "d < e'"
- using real_lbound_gt_zero[OF ball(1) e'(1)] by blast
- {
- fix c
- assume "abs c \<le> d"
- then have *: "norm (x + c *\<^sub>R j - x) < e'"
- using norm_Basis[OF j(2)] d by auto
- let ?v = "(\<Sum>i\<in>Basis. (\<Sum>l\<in>Basis. ?D i \<bullet> l * ((c *\<^sub>R j :: 'a) \<bullet> l)) *\<^sub>R i)"
- have if_dist: "\<And> P a b c. a * (if P then b else c) = (if P then a * b else a * c)"
- by auto
- have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> norm (f (x + c *\<^sub>R j) - f x - ?v)"
- by (rule Basis_le_norm[OF k])
- also have "\<dots> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
- using e'(2)[OF *] and norm_Basis[OF j(2)] j
- by simp
- finally have "\<bar>(f (x + c *\<^sub>R j) - f x - ?v) \<bullet> k\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
- by simp
- then have "\<bar>f (x + c *\<^sub>R j) \<bullet> k - f x \<bullet> k - c * (?D k \<bullet> j)\<bar> \<le> \<bar>?D k \<bullet> j\<bar> / 2 * \<bar>c\<bar>"
- using j k
- by (simp add: inner_simps field_simps inner_Basis setsum_cases if_dist)
- }
- note * = this
- have "x + d *\<^sub>R j \<in> ball x e" "x - d *\<^sub>R j \<in> ball x e"
- unfolding mem_ball dist_norm
- using norm_Basis[OF j(2)] d
- by auto
- then have **: "((f (x - d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<le> (f x)\<bullet>k) \<or>
- ((f (x - d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k \<and> (f (x + d *\<^sub>R j))\<bullet>k \<ge> (f x)\<bullet>k)"
- using ball by auto
- have ***: "\<And>y y1 y2 d dx :: real. y1 \<le> y \<and> y2 \<le> y \<or> y \<le> y1 \<and> y \<le> y2 \<Longrightarrow>
- d < abs dx \<Longrightarrow> abs (y1 - y - - dx) \<le> d \<Longrightarrow> abs (y2 - y - dx) \<le> d \<Longrightarrow> False"
- by arith
- show False
- apply (rule ***[OF **, where dx="d * (?D k \<bullet> j)" and d="\<bar>?D k \<bullet> j\<bar> / 2 * \<bar>d\<bar>"])
- using *[of "-d"] and *[of d] and d(1) and j
- unfolding mult_minus_left
- unfolding abs_mult diff_minus_eq_add scaleR_minus_left
- unfolding algebra_simps
- apply (auto intro: mult_pos_pos)
- done
-qed
-
-text {* In particular if we have a mapping into @{typ "real"}. *}
-
-lemma differential_zero_maxmin:
- fixes f::"'a::euclidean_space \<Rightarrow> real"
- assumes "x \<in> s"
- and "open s"
- and deriv: "(f has_derivative f') (at x)"
- and mono: "(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
- shows "f' = (\<lambda>v. 0)"
proof -
- obtain e where e: "e > 0" "ball x e \<subseteq> s"
- using `open s`[unfolded open_contains_ball] and `x \<in> s` by auto
- with differential_zero_maxmin_component[where 'b=real, of 1 e x f] mono deriv
- have "(\<Sum>j\<in>Basis. frechet_derivative f (at x) j *\<^sub>R j) = (0::'a)"
- by (auto simp: Basis_real_def differentiable_def)
- with frechet_derivative_at[OF deriv, symmetric]
- have "\<forall>i\<in>Basis. f' i = 0"
- by (simp add: euclidean_eq_iff[of _ "0::'a"] inner_setsum_left_Basis)
- with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 1]
- show ?thesis
- by (simp add: fun_eq_iff)
+ let ?f' = "frechet_derivative f (at x)"
+ have "x \<in> ball x e" using `0 < e` by simp
+ moreover have "open (ball x e)" by simp
+ moreover have "((\<lambda>x. f x \<bullet> k) has_derivative (\<lambda>h. ?f' h \<bullet> k)) (at x)"
+ using bounded_linear_inner_left diff[unfolded frechet_derivative_works]
+ by (rule bounded_linear.FDERIV)
+ ultimately have "(\<lambda>h. frechet_derivative f (at x) h \<bullet> k) = (\<lambda>v. 0)"
+ using ball(2) by (rule differential_zero_maxmin)
+ then show ?thesis
+ unfolding fun_eq_iff by simp
qed
lemma rolle:
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Sat Mar 15 03:37:22 2014 +0100
@@ -37,7 +37,7 @@
ML {*
fun mutation_testing_of (name, thy) =
- (MutabelleExtra.random_seed := 1.0;
+ (MutabelleExtra.init_random 1.0;
MutabelleExtra.thms_of false thy
|> MutabelleExtra.take_random 200
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
@@ -50,7 +50,7 @@
(*
ML {*
- MutabelleExtra.random_seed := 1.0;
+ MutabelleExtra.init_random 1.0;
MutabelleExtra.thms_of true @{theory Complex_Main}
|> MutabelleExtra.take_random 1000000
|> (fn thms => List.drop (thms, 1000))
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Mar 15 03:37:22 2014 +0100
@@ -40,15 +40,12 @@
val mutate_theorems_and_write_report :
theory -> int * int -> mtd list -> thm list -> string -> unit
-val random_seed : real Unsynchronized.ref
+val init_random : real -> unit
end;
structure MutabelleExtra : MUTABELLE_EXTRA =
struct
-(* Own seed; can't rely on the Isabelle one to stay the same *)
-val random_seed = Unsynchronized.ref 1.0;
-
(* Another Random engine *)
exception RANDOM;
@@ -56,13 +53,20 @@
fun rmod x y = x - y * Real.realFloor (x / y);
local
+ (* Own seed; can't rely on the Isabelle one to stay the same *)
+ val random_seed = Synchronized.var "random_seed" 1.0;
+
val a = 16807.0;
val m = 2147483647.0;
in
-fun random () = CRITICAL (fn () =>
- let val r = rmod (a * ! random_seed) m
- in (random_seed := r; r) end);
+fun init_random r = Synchronized.change random_seed (K r);
+
+fun random () =
+ Synchronized.change_result random_seed
+ (fn s =>
+ let val r = rmod (a * s) m
+ in (r, r) end);
end;
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Mar 15 03:37:22 2014 +0100
@@ -573,7 +573,7 @@
let
(* use the first ML solver (to avoid startup overhead) *)
val (ml_solvers, nonml_solvers) =
- !SatSolver.solvers
+ SatSolver.get_solvers ()
|> List.partition (member (op =) ["dptsat", "dpll"] o fst)
val res =
if null nonml_solvers then
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Mar 15 03:37:22 2014 +0100
@@ -200,10 +200,10 @@
(** invocation of Haskell interpreter **)
val narrowing_engine =
- File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
+ File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
val pnf_narrowing_engine =
- File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+ File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
fun exec verbose code =
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 15 03:37:22 2014 +0100
@@ -459,7 +459,7 @@
else
is_too_complex
val local_facts = Proof_Context.facts_of ctxt
- val named_locals = local_facts |> Facts.dest_static []
+ val named_locals = local_facts |> Facts.dest_static [global_facts]
val assms = Assumption.all_assms_of ctxt
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
--- a/src/HOL/Tools/sat_solver.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/HOL/Tools/sat_solver.ML Sat Mar 15 03:37:22 2014 +0100
@@ -42,7 +42,7 @@
val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
(* generic solver interface *)
- val solvers : (string * solver) list Unsynchronized.ref
+ val get_solvers : unit -> (string * solver) list
val add_solver : string * solver -> unit
val invoke_solver : string -> solver (* exception Option *)
end;
@@ -348,22 +348,24 @@
end;
(* ------------------------------------------------------------------------- *)
-(* solvers: a (reference to a) table of all registered SAT solvers *)
+(* solvers: a table of all registered SAT solvers *)
(* ------------------------------------------------------------------------- *)
- val solvers = Unsynchronized.ref ([] : (string * solver) list);
+ val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
+
+ fun get_solvers () = Synchronized.value solvers;
(* ------------------------------------------------------------------------- *)
(* add_solver: updates 'solvers' by adding a new solver *)
(* ------------------------------------------------------------------------- *)
- fun add_solver (name, new_solver) = CRITICAL (fn () =>
+ fun add_solver (name, new_solver) =
+ Synchronized.change solvers (fn the_solvers =>
let
- val the_solvers = !solvers;
val _ = if AList.defined (op =) the_solvers name
then warning ("SAT solver " ^ quote name ^ " was defined before")
else ();
- in solvers := AList.update (op =) (name, new_solver) the_solvers end);
+ in AList.update (op =) (name, new_solver) the_solvers end);
(* ------------------------------------------------------------------------- *)
(* invoke_solver: returns the solver associated with the given 'name' *)
@@ -372,7 +374,7 @@
(* ------------------------------------------------------------------------- *)
fun invoke_solver name =
- (the o AList.lookup (op =) (!solvers)) name;
+ the (AList.lookup (op =) (get_solvers ()) name);
end; (* SatSolver *)
@@ -521,7 +523,7 @@
handle SatSolver.NOT_CONFIGURED => loop solvers
)
in
- loop (!SatSolver.solvers)
+ loop (SatSolver.get_solvers ())
end
in
SatSolver.add_solver ("auto", auto_solver)
--- a/src/Pure/General/change_table.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/General/change_table.ML Sat Mar 15 03:37:22 2014 +0100
@@ -17,6 +17,7 @@
val empty: 'a T
val is_empty: 'a T -> bool
val change_base: bool -> 'a T -> 'a T
+ val change_ignore: 'a T -> 'a T
val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*)
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*)
val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
@@ -43,35 +44,42 @@
(* optional change *)
-datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set};
+datatype change =
+ No_Change | Change of {base: serial, depth: int, changes: Table.set option};
fun make_change base depth changes =
Change {base = base, depth = depth, changes = changes};
+fun ignore_change (Change {base, depth, changes = SOME _}) =
+ make_change base depth NONE
+ | ignore_change change = change;
+
+fun update_change key (Change {base, depth, changes = SOME ch}) =
+ make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
+ | update_change _ change = change;
+
fun base_change true No_Change =
- make_change (serial ()) 0 Table.empty
+ make_change (serial ()) 0 (SOME Table.empty)
| base_change true (Change {base, depth, changes}) =
make_change base (depth + 1) changes
| base_change false (Change {base, depth, changes}) =
if depth = 0 then No_Change else make_change base (depth - 1) changes
- | base_change false No_Change = raise Fail "Unbalanced block structure of change table";
+ | base_change false No_Change = raise Fail "Unbalanced change structure";
-fun update_change _ No_Change = No_Change
- | update_change key (Change {base, depth, changes}) =
- make_change base depth (Table.insert (K true) (key, ()) changes);
-
-fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
+fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure";
fun merge_change (No_Change, No_Change) = NONE
| merge_change (Change change1, Change change2) =
let
val {base = base1, depth = depth1, changes = changes1} = change1;
val {base = base2, depth = depth2, changes = changes2} = change2;
- in
- if base1 = base2 andalso depth1 = depth2 then
- SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
- else cannot_merge ()
- end
+ val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge ();
+ val (swapped, ch2) =
+ (case (changes1, changes2) of
+ (_, SOME ch2) => (false, ch2)
+ | (SOME ch1, _) => (true, ch1)
+ | _ => cannot_merge ());
+ in SOME (swapped, ch2, make_change base1 depth1 NONE) end
| merge_change _ = cannot_merge ();
@@ -90,6 +98,7 @@
fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
fun change_base begin = (map_change_table o apfst) (base_change begin);
+fun change_ignore arg = (map_change_table o apfst) ignore_change arg;
(* join and merge *)
@@ -105,20 +114,21 @@
else
(case merge_change (change1, change2) of
NONE => make_change_table (No_Change, Table.join f (table1, table2))
- | SOME (changes2, change') =>
+ | SOME (swapped, ch2, change') =>
let
- fun update key table =
- (case Table.lookup table2 key of
- NONE => table
+ fun maybe_swap (x, y) = if swapped then (y, x) else (x, y);
+ val (tab1, tab2) = maybe_swap (table1, table2);
+ fun update key tab =
+ (case Table.lookup tab2 key of
+ NONE => tab
| SOME y =>
- (case Table.lookup table key of
- NONE => Table.update (key, y) table
+ (case Table.lookup tab key of
+ NONE => Table.update (key, y) tab
| SOME x =>
- (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
- NONE => table
- | SOME z => Table.update (key, z) table)));
- val table' = Table.fold (update o #1) changes2 table1;
- in make_change_table (change', table') end)
+ (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
+ NONE => tab
+ | SOME z => Table.update (key, z) tab)));
+ in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
end;
fun merge eq =
--- a/src/Pure/General/name_space.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/General/name_space.ML Sat Mar 15 03:37:22 2014 +0100
@@ -56,6 +56,7 @@
val declare: Context.generic -> bool -> binding -> T -> string * T
type 'a table
val change_base: bool -> 'a table -> 'a table
+ val change_ignore: 'a table -> 'a table
val space_of_table: 'a table -> T
val check_reports: Context.generic -> 'a table ->
xstring * Position.T list -> (string * Position.report list) * 'a
@@ -123,6 +124,9 @@
fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
(kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
+val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
+ (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
+
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
(kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
@@ -474,6 +478,9 @@
fun change_base begin (Table (space, tab)) =
Table (change_base_space begin space, Change_Table.change_base begin tab);
+fun change_ignore (Table (space, tab)) =
+ Table (change_ignore_space space, Change_Table.change_ignore tab);
+
fun space_of_table (Table (space, _)) = space;
fun check_reports context (Table (space, tab)) (xname, ps) =
--- a/src/Pure/General/path.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/General/path.ML Sat Mar 15 03:37:22 2014 +0100
@@ -30,6 +30,7 @@
val ext: string -> T -> T
val split_ext: T -> T * string
val expand: T -> T
+ val smart_implode: T -> string
val position: T -> Position.T
end;
@@ -194,21 +195,26 @@
val expand = rep #> maps eval #> norm #> Path;
-(* source position -- with smart replacement of ISABELLE_HOME *)
+(* smart implode *)
-val isabelle_home = explode_path "~~";
-
-fun position path =
+fun smart_implode path =
let
- val s = implode_path path;
- val prfx = implode_path (expand isabelle_home) ^ "/";
+ val full_name = implode_path (expand path);
+ fun fold_path a =
+ let val b = implode_path (expand (explode_path a)) in
+ if full_name = b then SOME a
+ else
+ (case try (unprefix (b ^ "/")) full_name of
+ SOME name => SOME (a ^ "/" ^ name)
+ | NONE => NONE)
+ end;
in
- Position.file
- (case try (unprefix prfx) s of
- NONE => s
- | SOME s' => "~~/" ^ s')
+ (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
+ SOME name => name
+ | NONE => implode_path path)
end;
+val position = Position.file o smart_implode;
(*final declarations of this structure!*)
val implode = implode_path;
--- a/src/Pure/Isar/attrib.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Mar 15 03:37:22 2014 +0100
@@ -213,7 +213,7 @@
fun gen_thm pick = Scan.depend (fn context =>
let
- val get = Context.cases (Global_Theory.get_fact context) Proof_Context.get_fact context;
+ val get = Proof_Context.get_fact_generic context;
val get_fact = get o Facts.Fact;
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
in
@@ -249,6 +249,8 @@
(** partial evaluation -- observing rule/declaration/mixed attributes **)
+(*NB: result length may change due to rearrangement of symbolic expression*)
+
local
fun apply_att src (context, th) =
--- a/src/Pure/Isar/keyword.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Isar/keyword.ML Sat Mar 15 03:37:22 2014 +0100
@@ -20,7 +20,6 @@
val thy_decl: T
val thy_load: T
val thy_load_files: string list -> T
- val thy_script: T
val thy_goal: T
val qed: T
val qed_script: T
@@ -101,7 +100,6 @@
val thy_decl = kind "thy_decl";
val thy_load = kind "thy_load";
fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
-val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
val qed = kind "qed";
val qed_script = kind "qed_script";
@@ -123,7 +121,7 @@
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
+ thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
@@ -249,7 +247,7 @@
val is_theory = command_category
[thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
- thy_load, thy_decl, thy_script, thy_goal];
+ thy_load, thy_decl, thy_goal];
val is_proof = command_category
[qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
--- a/src/Pure/Isar/keyword.scala Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Sat Mar 15 03:37:22 2014 +0100
@@ -22,7 +22,6 @@
val THY_HEADING4 = "thy_heading4"
val THY_DECL = "thy_decl"
val THY_LOAD = "thy_load"
- val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
val QED = "qed"
val QED_SCRIPT = "qed_script"
@@ -50,7 +49,7 @@
val diag = Set(DIAG)
val theory =
Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
- THY_DECL, THY_SCRIPT, THY_GOAL)
+ THY_DECL, THY_GOAL)
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
@@ -61,6 +60,5 @@
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
- val improper = Set(THY_SCRIPT, PRF_SCRIPT)
}
--- a/src/Pure/Isar/proof_context.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 15 03:37:22 2014 +0100
@@ -30,7 +30,6 @@
val consts_of: Proof.context -> Consts.T
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
- val facts_of: Proof.context -> Facts.T
val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
val naming_of: Proof.context -> Name_Space.naming
val restore_naming: Proof.context -> Proof.context -> Proof.context
@@ -53,9 +52,10 @@
val transfer: theory -> Proof.context -> Proof.context
val background_theory: (theory -> theory) -> Proof.context -> Proof.context
val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
- val extern_fact: Proof.context -> string -> xstring
+ val facts_of: Proof.context -> Facts.T
+ val facts_of_fact: Proof.context -> string -> Facts.T
+ val markup_extern_fact: Proof.context -> string -> Markup.T * xstring
val pretty_term_abbrev: Proof.context -> term -> Pretty.T
- val markup_fact: Proof.context -> string -> Markup.T
val pretty_fact: Proof.context -> string * thm list -> Pretty.T
val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
val read_class: Proof.context -> string -> class
@@ -120,6 +120,7 @@
(term list list * (Proof.context -> Proof.context)) * Proof.context
val fact_tac: Proof.context -> thm list -> int -> tactic
val some_fact_tac: Proof.context -> int -> tactic
+ val get_fact_generic: Context.generic -> Facts.ref -> thm list
val get_fact: Proof.context -> Facts.ref -> thm list
val get_fact_single: Proof.context -> Facts.ref -> thm
val get_thms: Proof.context -> xstring -> thm list
@@ -209,7 +210,7 @@
syntax: Local_Syntax.T, (*local syntax*)
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
- facts: Facts.T, (*local facts*)
+ facts: Facts.T, (*local facts, based on initial global facts*)
cases: cases}; (*named case contexts: case, is_proper, running index*)
fun make_data (mode, syntax, tsig, consts, facts, cases) =
@@ -219,9 +220,12 @@
(
type T = data;
fun init thy =
- make_data (mode_default, Local_Syntax.init thy,
- (Sign.tsig_of thy, Sign.tsig_of thy),
- (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
+ make_data (mode_default,
+ Local_Syntax.init thy,
+ (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
+ (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
+ Global_Theory.facts_of thy,
+ empty_cases);
);
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
@@ -274,7 +278,6 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_data;
-val facts_of = #facts o rep_data;
val cases_of = #cases o rep_data;
@@ -334,31 +337,30 @@
in (res, ctxt |> transfer thy') end;
-
-(** pretty printing **)
+(* hybrid facts *)
-(* extern *)
+val facts_of = #facts o rep_data;
-fun which_facts ctxt name =
+fun facts_of_fact ctxt name =
let
val local_facts = facts_of ctxt;
val global_facts = Global_Theory.facts_of (theory_of ctxt);
in
- if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
+ if Facts.defined local_facts name
then local_facts else global_facts
end;
-fun markup_fact ctxt name = Name_Space.markup (Facts.space_of (which_facts ctxt name)) name;
-
-fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
+fun markup_extern_fact ctxt name =
+ Facts.markup_extern ctxt (facts_of_fact ctxt name) name;
-(* pretty *)
+
+(** pretty printing **)
fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
fun pretty_fact_name ctxt a =
- Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
+ Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"];
fun pretty_fact ctxt =
let
@@ -908,12 +910,22 @@
end;
-(* get_thm(s) *)
+(* get facts *)
local
-fun retrieve_thms pick ctxt (Facts.Fact s) =
+fun retrieve_global context =
+ Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
+
+fun retrieve_generic (context as Context.Proof ctxt) (xname, pos) =
+ if can (fn () => Facts.retrieve context (facts_of ctxt) (xname, Position.none)) ()
+ then Facts.retrieve context (facts_of ctxt) (xname, pos)
+ else retrieve_global context (xname, pos)
+ | retrieve_generic context arg = retrieve_global context arg;
+
+fun retrieve pick context (Facts.Fact s) =
let
+ val ctxt = Context.the_proof context;
val pos = Syntax.read_token_pos s;
val prop =
Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
@@ -924,34 +936,27 @@
fun prove_fact th =
Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
val results = map_filter (try prove_fact) (potential_facts ctxt prop');
- val res =
+ val thm =
(case distinct Thm.eq_thm_prop results of
- [res] => res
+ [thm] => thm
| [] => err "Failed to retrieve literal fact"
| _ => err "Ambiguous specification of literal fact");
- in pick ("", Position.none) [res] end
- | retrieve_thms pick ctxt xthmref =
+ in pick ("", Position.none) [thm] end
+ | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
let
- val thy = theory_of ctxt;
- val local_facts = facts_of ctxt;
- val thmref = Facts.map_name_of_ref (Facts.intern local_facts) xthmref;
- val name = Facts.name_of_ref thmref;
- val pos = Facts.pos_of_ref xthmref;
- val thms =
- if name = "" then [Thm.transfer thy Drule.dummy_thm]
- else
- (case Facts.lookup (Context.Proof ctxt) local_facts name of
- SOME (_, ths) =>
- (Context_Position.report ctxt pos
- (Name_Space.markup (Facts.space_of local_facts) name);
- map (Thm.transfer thy) (Facts.select thmref ths))
- | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
- in pick (name, pos) thms end;
+ val thy = Context.theory_of context;
+ val (name, thms) =
+ (case xname of
+ "" => (xname, [Thm.transfer thy Drule.dummy_thm])
+ | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+ | _ => retrieve_generic context (xname, pos));
+ in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
in
-val get_fact = retrieve_thms (K I);
-val get_fact_single = retrieve_thms Facts.the_single;
+val get_fact_generic = retrieve (K I);
+val get_fact = retrieve (K I) o Context.Proof;
+val get_fact_single = retrieve Facts.the_single o Context.Proof;
fun get_thms ctxt = get_fact ctxt o Facts.named;
fun get_thm ctxt = get_fact_single ctxt o Facts.named;
@@ -1162,8 +1167,11 @@
(Name_Space.del_table name cases, index)
| update_case context is_proper (name, SOME c) (cases, index) =
let
- val (_, cases') = cases |> Name_Space.define context false
- (Binding.make (name, Position.none), ((c, is_proper), index));
+ val binding =
+ Binding.make (name, Position.none)
+ |> not is_proper ? Binding.conceal;
+ val (_, cases') = cases
+ |> Name_Space.define context false (binding, ((c, is_proper), index));
val index' = index + 1;
in (cases', index') end;
--- a/src/Pure/Isar/toplevel.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Sat Mar 15 03:37:22 2014 +0100
@@ -590,11 +590,12 @@
(* post-transition hooks *)
local
- val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
+ val hooks =
+ Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list);
in
-fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = ! hooks;
+fun add_hook hook = Synchronized.change hooks (cons hook);
+fun get_hooks () = Synchronized.value hooks;
end;
--- a/src/Pure/Thy/thy_load.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Mar 15 03:37:22 2014 +0100
@@ -190,17 +190,18 @@
in (thy, present, size text) end;
-(* document antiquotation *)
+(* antiquotations *)
-fun file_antiq strict ctxt (name, pos) =
+local
+
+fun check_path strict ctxt dir (name, pos) =
let
val _ = Context_Position.report ctxt pos Markup.language_path;
- val dir = master_directory (Proof_Context.theory_of ctxt);
val path = Path.append dir (Path.explode name)
handle ERROR msg => error (msg ^ Position.here pos);
- val _ = Context_Position.report ctxt pos (Markup.path name);
+ val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
val _ =
if can Path.expand path andalso File.exists path then ()
else
@@ -213,16 +214,30 @@
Context_Position.if_visible ctxt Output.report
(Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
end;
+ in path end;
+
+fun file_antiq strict ctxt (name, pos) =
+ let
+ val dir = master_directory (Proof_Context.theory_of ctxt);
+ val _ = check_path strict ctxt dir (name, pos);
in
space_explode "/" name
|> map Thy_Output.verb_text
|> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
end;
+in
+
val _ = Theory.setup
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
(file_antiq true o #context) #>
- (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
- (file_antiq false o #context)));
+ Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+ (file_antiq false o #context) #>
+ ML_Antiquotation.value (Binding.name "path")
+ (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
+ let val path = check_path true ctxt Path.current arg
+ in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
end;
+
+end;
--- a/src/Pure/Tools/find_theorems.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sat Mar 15 03:37:22 2014 +0100
@@ -354,8 +354,9 @@
fun nicer_shortest ctxt =
let
- val space = Facts.space_of (Proof_Context.facts_of ctxt);
- val extern_shortest = Name_Space.extern_shortest ctxt space;
+ fun extern_shortest name =
+ Name_Space.extern_shortest ctxt
+ (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
nicer_name (extern_shortest x, i) (extern_shortest y, j)
@@ -454,7 +455,7 @@
Facts.Named ((name, _), sel) => (name, sel)
| Facts.Fact _ => raise Fail "Illegal literal fact");
in
- [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
+ [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name),
Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
end;
--- a/src/Pure/Tools/keywords.scala Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/Tools/keywords.scala Sat Mar 15 03:37:22 2014 +0100
@@ -25,7 +25,6 @@
"thy_heading4" -> "theory-heading",
"thy_load" -> "theory-decl",
"thy_decl" -> "theory-decl",
- "thy_script" -> "theory-script",
"thy_goal" -> "theory-goal",
"qed_script" -> "qed",
"qed_block" -> "qed-block",
--- a/src/Pure/axclass.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/axclass.ML Sat Mar 15 03:37:22 2014 +0100
@@ -391,9 +391,9 @@
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
- val (th', thy') =
- Global_Theory.store_thm
- (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
+ val binding =
+ Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
+ val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val th'' = th'
|> Thm.unconstrainT
|> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
@@ -412,9 +412,9 @@
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val (th', thy') =
- Global_Theory.store_thm
- (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
+ val binding =
+ Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
+ val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val args = Name.invent_names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
--- a/src/Pure/consts.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/consts.ML Sat Mar 15 03:37:22 2014 +0100
@@ -10,6 +10,7 @@
type T
val eq_consts: T * T -> bool
val change_base: bool -> T -> T
+ val change_ignore: T -> T
val retrieve_abbrevs: T -> string list -> term -> (term * term) list
val dest: T ->
{const_space: Name_Space.T,
@@ -69,6 +70,9 @@
fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
(Name_Space.change_base begin decls, constraints, rev_abbrevs));
+val change_ignore = map_consts (fn (decls, constraints, rev_abbrevs) =>
+ (Name_Space.change_ignore decls, constraints, rev_abbrevs));
+
(* reverted abbrevs *)
--- a/src/Pure/facts.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/facts.ML Sat Mar 15 03:37:22 2014 +0100
@@ -26,7 +26,9 @@
val check: Context.generic -> T -> xstring * Position.T -> string
val intern: T -> xstring -> string
val extern: Proof.context -> T -> string -> xstring
+ val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val lookup: Context.generic -> T -> string -> (bool * thm list) option
+ val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
val defined: T -> string -> bool
val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
val dest_static: T list -> T -> (string * thm list) list
@@ -155,6 +157,7 @@
val intern = Name_Space.intern o space_of;
fun extern ctxt = Name_Space.extern ctxt o space_of;
+fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
val defined = is_some oo (Name_Space.lookup_key o facts_of);
@@ -164,6 +167,18 @@
| SOME (_, Static ths) => SOME (true, ths)
| SOME (_, Dynamic f) => SOME (false, f context));
+fun retrieve context facts (xname, pos) =
+ let
+ val name = check context facts (xname, pos);
+ val thms =
+ (case lookup context facts name of
+ SOME (static, thms) =>
+ (if static then ()
+ else Context_Position.report_generic context pos (Markup.dynamic_fact name);
+ thms)
+ | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
+ in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+
fun fold_static f =
Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
@@ -195,7 +210,10 @@
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
let
val facts' = Name_Space.merge_tables (facts1, facts2);
- val props' = Net.merge (is_equal o prop_ord) (props1, props2);
+ val props' =
+ if Net.is_empty props2 then props1
+ else if Net.is_empty props1 then props2
+ else Net.merge (is_equal o prop_ord) (props1, props2); (*beware of non-canonical merge*)
in make_facts facts' props' end;
--- a/src/Pure/global_theory.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/global_theory.ML Sat Mar 15 03:37:22 2014 +0100
@@ -11,7 +11,6 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
val all_thms_of: theory -> (string * thm) list
@@ -64,31 +63,13 @@
fun hide_fact fully name = Data.map (Facts.hide fully name);
-(** retrieve theorems **)
-
-fun get_fact context thy xthmref =
- let
- val facts = facts_of thy;
- val xname = Facts.name_of_ref xthmref;
- val pos = Facts.pos_of_ref xthmref;
+(* retrieve theorems *)
- val name =
- (case intern_fact thy xname of
- "_" => "Pure.asm_rl"
- | name => name);
- val res = Facts.lookup context facts name;
- in
- (case res of
- NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)
- | SOME (static, ths) =>
- (Context_Position.report_generic context pos (Name_Space.markup (Facts.space_of facts) name);
- if static then ()
- else Context_Position.report_generic context pos (Markup.dynamic_fact name);
- Facts.select xthmref (map (Thm.transfer thy) ths)))
- end;
+fun get_thms thy xname =
+ #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
-fun get_thms thy = get_fact (Context.Theory thy) thy o Facts.named;
-fun get_thm thy name = Facts.the_single (name, Position.none) (get_thms thy name);
+fun get_thm thy xname =
+ Facts.the_single (xname, Position.none) (get_thms thy xname);
fun all_thms_of thy =
Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
--- a/src/Pure/net.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/net.ML Sat Mar 15 03:37:22 2014 +0100
@@ -253,7 +253,7 @@
maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
fun merge eq (net1, net2) =
- fold (insert_safe eq) (dest net2) net1; (* FIXME non-standard merge order!?! *)
+ fold (insert_safe eq) (dest net2) net1; (* FIXME non-canonical merge order!?! *)
fun content net = map #2 (dest net);
--- a/src/Pure/type.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Pure/type.ML Sat Mar 15 03:37:22 2014 +0100
@@ -26,6 +26,7 @@
types: decl Name_Space.table,
log_types: string list}
val change_base: bool -> tsig -> tsig
+ val change_ignore: tsig -> tsig
val empty_tsig: tsig
val class_space: tsig -> Name_Space.T
val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
@@ -180,6 +181,9 @@
fun change_base begin (TSig {classes, default, types, log_types}) =
make_tsig (classes, default, Name_Space.change_base begin types, log_types);
+fun change_ignore (TSig {classes, default, types, log_types}) =
+ make_tsig (classes, default, Name_Space.change_ignore types, log_types);
+
fun build_tsig (classes, default, types) =
let
val log_types =
--- a/src/Tools/WWW_Find/unicode_symbols.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Sat Mar 15 03:37:22 2014 +0100
@@ -177,7 +177,7 @@
local
val (fromsym, fromabbr, tosym, toabbr) =
- read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
+ read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
in
val symbol_to_unicode = Symtab.lookup fromsym;
val abbrev_to_unicode = Symtab.lookup fromabbr;
--- a/src/Tools/jEdit/src/rendering.scala Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Mar 15 03:37:22 2014 +0100
@@ -53,7 +53,6 @@
import JEditToken._
Map[String, Byte](
Keyword.THY_END -> KEYWORD2,
- Keyword.THY_SCRIPT -> LABEL,
Keyword.QED_SCRIPT -> DIGIT,
Keyword.PRF_SCRIPT -> DIGIT,
Keyword.PRF_ASM -> KEYWORD3,
@@ -471,7 +470,8 @@
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_valid(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
- Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
+ val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+ Some(add(prev, r, (true, XML.Text(text))))
case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
--- a/src/Tools/misc_legacy.ML Sat Mar 15 01:36:38 2014 +0100
+++ b/src/Tools/misc_legacy.ML Sat Mar 15 03:37:22 2014 +0100
@@ -246,10 +246,11 @@
val char_vec = Vector.tabulate (62, gensym_char);
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
-val gensym_seed = Unsynchronized.ref (0: int);
+val gensym_seed = Synchronized.var "gensym_seed" (0: int);
in
- fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
+ fun gensym pre =
+ Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
end;
--- a/src/ZF/Inductive_ZF.thy Sat Mar 15 01:36:38 2014 +0100
+++ b/src/ZF/Inductive_ZF.thy Sat Mar 15 03:37:22 2014 +0100
@@ -14,8 +14,7 @@
theory Inductive_ZF
imports Fixedpt QPair Nat_ZF
keywords
- "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
- "inductive_cases" :: thy_script and
+ "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
"domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
"elimination" "induction" "case_eqns" "recursor_eqns"
begin