--- a/NEWS Wed Sep 18 20:44:10 2013 +0200
+++ b/NEWS Wed Sep 18 20:54:46 2013 +0200
@@ -402,6 +402,11 @@
*** ML ***
+* Improved printing of exception trace in Poly/ML 5.5.1, with regular
+tracing output in the command transaction context instead of physical
+stdout. See also Toplevel.debug, Toplevel.debugging and
+ML_Compiler.exn_trace.
+
* Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function
"check_property" allows to check specifications of the form "ALL x y
z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its
--- a/src/Doc/IsarImplementation/Integration.thy Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy Wed Sep 18 20:54:46 2013 +0200
@@ -79,10 +79,8 @@
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
state if available, otherwise raises @{ML Toplevel.UNDEF}.
- \item @{ML "Toplevel.debug := true"} enables low-level exception
- trace of the ML runtime system. Note that the result might appear
- on some raw output window only, outside the formal context of the
- source text.
+ \item @{ML "Toplevel.debug := true"} enables exception trace of the
+ ML runtime system.
\item @{ML "Toplevel.timing := true"} makes the toplevel print timing
information for each Isar command being executed.
--- a/src/Doc/IsarImplementation/ML.thy Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy Wed Sep 18 20:54:46 2013 +0200
@@ -1163,7 +1163,7 @@
@{index_ML Fail: "string -> exn"} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
@{index_ML reraise: "exn -> 'a"} \\
- @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
+ @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
\end{mldecls}
\begin{description}
@@ -1191,14 +1191,13 @@
while preserving its implicit position information (if possible,
depending on the ML platform).
- \item @{ML exception_trace}~@{ML_text "(fn () =>"}~@{text
+ \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
"e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
a full trace of its stack of nested exceptions (if possible,
- depending on the ML platform).\footnote{In versions of Poly/ML the
- trace will appear on raw stdout of the Isabelle process.}
+ depending on the ML platform).}
- Inserting @{ML exception_trace} into ML code temporarily is useful
- for debugging, but not suitable for production code.
+ Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
+ useful for debugging, but not suitable for production code.
\end{description}
*}
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 18 20:44:10 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 18 20:54:46 2013 +0200
@@ -15,7 +15,9 @@
notation inner (infix "\<bullet>" 70)
-lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
+lemma square_bound_lemma:
+ fixes x :: real
+ shows "x < (1 + x) * (1 + x)"
proof -
have "(x + 1/2)\<^sup>2 + 3/4 > 0"
using zero_le_power2[of "x+1/2"] by arith
@@ -121,10 +123,10 @@
apply arith
done
-lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
+lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
by (metis not_le norm_ge_square)
-lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
+lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
by (metis norm_le_square not_less)
text{* Dot product in terms of the norm rather than conversely. *}
@@ -249,7 +251,7 @@
subsection {* Linear functions. *}
lemma linear_iff:
- "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
+ "linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
(is "linear f \<longleftrightarrow> ?rhs")
proof
assume "linear f" then interpret f: linear f .
@@ -282,7 +284,7 @@
lemma linear_compose_setsum:
assumes fS: "finite S"
and lS: "\<forall>a \<in> S. linear (f a)"
- shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)"
+ shows "linear (\<lambda>x. setsum (\<lambda>a. f a x) S)"
using lS
apply (induct rule: finite_induct[OF fS])
apply (auto simp add: linear_zero intro: linear_compose_add)
@@ -301,10 +303,10 @@
lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
using linear_cmul [where c="-1"] by simp
-lemma linear_add: "linear f \<Longrightarrow> f(x + y) = f x + f y"
+lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
by (metis linear_iff)
-lemma linear_sub: "linear f \<Longrightarrow> f(x - y) = f x - f y"
+lemma linear_sub: "linear f \<Longrightarrow> f (x - y) = f x - f y"
by (simp add: diff_minus linear_add linear_neg)
lemma linear_setsum:
@@ -679,7 +681,7 @@
lemma forall_pos_mono_1:
"(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
- (\<And>n. P(inverse(real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+ (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
apply (rule forall_pos_mono)
apply auto
apply (atomize)
@@ -711,7 +713,7 @@
where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )"
definition (in real_vector) "span S = (subspace hull S)"
-definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S - {a}))"
+definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
text {* Closure properties of subspaces. *}
@@ -1085,7 +1087,7 @@
lemma in_span_delete:
assumes a: "a \<in> span S"
- and na: "a \<notin> span (S-{b})"
+ and na: "a \<notin> span (S - {b})"
shows "b \<in> span (insert a (S - {b}))"
apply (rule in_span_insert)
apply (rule set_rev_mp)
@@ -1149,7 +1151,7 @@
proof cases
assume xS: "x \<in> S"
have S1: "S = (S - {x}) \<union> {x}"
- and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \<inter> {x} = {}"
+ and Sss:"finite (S - {x})" "finite {x}" "(S - {x}) \<inter> {x} = {}"
using xS fS by auto
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =(\<Sum>v\<in>S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x"
using xS
@@ -1407,11 +1409,11 @@
by auto
have ?ths
proof cases
- assume stb: "s \<subseteq> span(t - {b})"
- from ft have ftb: "finite (t -{b})"
+ assume stb: "s \<subseteq> span (t - {b})"
+ from ft have ftb: "finite (t - {b})"
by auto
from less(1)[OF cardlt ftb s stb]
- obtain u where u: "card u = card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
+ obtain u where u: "card u = card (t - {b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u"
and fu: "finite u" by blast
let ?w = "insert b u"
have th0: "s \<subseteq> insert b u"
@@ -1434,7 +1436,7 @@
by blast
from th show ?thesis by blast
next
- assume stb: "\<not> s \<subseteq> span(t - {b})"
+ assume stb: "\<not> s \<subseteq> span (t - {b})"
from stb obtain a where a: "a \<in> s" "a \<notin> span (t - {b})"
by blast
have ab: "a \<noteq> b"
@@ -1465,8 +1467,8 @@
then have sp': "s \<subseteq> span (insert a (t - {b}))"
by blast
from less(1)[OF mlt ft' s sp'] obtain u where u:
- "card u = card (insert a (t -{b}))"
- "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
+ "card u = card (insert a (t - {b}))"
+ "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t - {b})"
"s \<subseteq> span u" by blast
from u a b ft at ct0 have "?P u"
by auto
@@ -1762,8 +1764,8 @@
subsection {* We continue. *}
lemma independent_bound:
- fixes S:: "('a::euclidean_space) set"
- shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a::euclidean_space)"
+ fixes S :: "'a::euclidean_space set"
+ shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
using independent_span_bound[OF finite_Basis, of S] by auto
lemma dependent_biggerset:
@@ -1910,29 +1912,29 @@
proof -
{
fix a
- assume a: "a \<in> B" "a \<in> span (B -{a})"
+ assume a: "a \<in> B" "a \<in> span (B - {a})"
from a fB have c0: "card B \<noteq> 0"
by auto
- from a fB have cb: "card (B -{a}) = card B - 1"
+ from a fB have cb: "card (B - {a}) = card B - 1"
by auto
- from BV a have th0: "B -{a} \<subseteq> V"
+ from BV a have th0: "B - {a} \<subseteq> V"
by blast
{
fix x
assume x: "x \<in> V"
- from a have eq: "insert a (B -{a}) = B"
+ from a have eq: "insert a (B - {a}) = B"
by blast
from x VB have x': "x \<in> span B"
by blast
from span_trans[OF a(2), unfolded eq, OF x']
- have "x \<in> span (B -{a})" .
+ have "x \<in> span (B - {a})" .
}
- then have th1: "V \<subseteq> span (B -{a})"
+ then have th1: "V \<subseteq> span (B - {a})"
by blast
- have th2: "finite (B -{a})"
+ have th2: "finite (B - {a})"
using fB by auto
from span_card_ge_dim[OF th0 th1 th2]
- have c: "dim V \<le> card (B -{a})" .
+ have c: "dim V \<le> card (B - {a})" .
from c c0 dVB cb have False by simp
}
then show ?thesis
@@ -2036,9 +2038,9 @@
assume a: "a \<in> S" "f a \<in> span (f ` S - {f a})"
have eq: "f ` S - {f a} = f ` (S - {a})"
using fi by (auto simp add: inj_on_def)
- from a have "f a \<in> f ` span (S -{a})"
+ from a have "f a \<in> f ` span (S - {a})"
unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
- then have "a \<in> span (S -{a})"
+ then have "a \<in> span (S - {a})"
using fi by (auto simp add: inj_on_def)
with a(1) iS have False
by (simp add: dependent_def)
@@ -2279,7 +2281,7 @@
have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
unfolding span_linear_image[OF lf]
apply (rule imageI)
- using k span_mono[of "b-{a}" b]
+ using k span_mono[of "b - {a}" b]
apply blast
done
then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
@@ -2289,8 +2291,8 @@
have xsb: "x \<in> span b"
proof (cases "k = 0")
case True
- with k have "x \<in> span (b -{a})" by simp
- then show ?thesis using span_mono[of "b-{a}" b]
+ with k have "x \<in> span (b - {a})" by simp
+ then show ?thesis using span_mono[of "b - {a}" b]
by blast
next
case False
@@ -2729,7 +2731,7 @@
by auto
have "x = y"
proof (rule ccontr)
- assume xy: "x \<noteq> y"
+ assume xy: "\<not> ?thesis"
have th: "card S \<le> card (f ` (S - {y}))"
unfolding c
apply (rule card_mono)
@@ -2741,7 +2743,7 @@
apply (rule bexI[where x=x])
apply auto
done
- also have " \<dots> \<le> card (S -{y})"
+ also have " \<dots> \<le> card (S - {y})"
apply (rule card_image_le)
using fS by simp
also have "\<dots> \<le> card S - 1" using y fS by simp
@@ -2904,21 +2906,22 @@
subsection {* Infinity norm *}
-definition "infnorm (x::'a::euclidean_space) = Sup { abs (x \<bullet> b) |b. b \<in> Basis}"
-
-lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
- by auto
+definition "infnorm (x::'a::euclidean_space) = Sup {abs (x \<bullet> b) |b. b \<in> Basis}"
lemma infnorm_set_image:
- "{abs ((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs(x \<bullet> i)) ` Basis"
+ fixes x :: "'a::euclidean_space"
+ shows "{abs (x \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs (x \<bullet> i)) ` Basis"
by blast
-lemma infnorm_Max: "infnorm (x::'a::euclidean_space) = Max ((\<lambda>i. abs(x \<bullet> i)) ` Basis)"
+lemma infnorm_Max:
+ fixes x :: "'a::euclidean_space"
+ shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
lemma infnorm_set_lemma:
- "finite {abs((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis}"
- "{abs(x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
+ fixes x :: "'a::euclidean_space"
+ shows "finite {abs (x \<bullet> i) |i. i \<in> Basis}"
+ and "{abs (x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
unfolding infnorm_set_image
by auto
@@ -2983,7 +2986,7 @@
shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
by (simp add: infnorm_Max)
-lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
+lemma infnorm_mul: "infnorm (a *\<^sub>R x) = abs a * infnorm x"
unfolding infnorm_Max
proof (safe intro!: Max_eqI)
let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
@@ -3015,7 +3018,9 @@
by (subst (1 2) euclidean_representation[symmetric, where 'a='a])
(simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
-lemma norm_le_infnorm: "norm x \<le> sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
+lemma norm_le_infnorm:
+ fixes x :: "'a::euclidean_space"
+ shows "norm x \<le> sqrt DIM('a) * infnorm x"
proof -
let ?d = "DIM('a)"
have "real ?d \<ge> 0"
@@ -3027,7 +3032,7 @@
have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
unfolding power_mult_distrib d2
unfolding real_of_nat_def
- apply(subst euclidean_inner)
+ apply (subst euclidean_inner)
apply (subst power2_abs[symmetric])
apply (rule order_trans[OF setsum_bounded[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
apply (auto simp add: power2_eq_square[symmetric])
@@ -3090,8 +3095,8 @@
qed
lemma norm_cauchy_schwarz_abs_eq:
- "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow>
- norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm(x) *\<^sub>R y = - norm y *\<^sub>R x"
+ "abs (x \<bullet> y) = norm x * norm y \<longleftrightarrow>
+ norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
(is "?lhs \<longleftrightarrow> ?rhs")
proof -
have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a"
--- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy Wed Sep 18 20:44:10 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Wed Sep 18 20:54:46 2013 +0200
@@ -10,97 +10,111 @@
lemma norm_cmul_rule_thm:
fixes x :: "'a::real_normed_vector"
- shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+ shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)"
unfolding norm_scaleR
apply (erule mult_left_mono)
apply simp
done
- (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
+(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
lemma norm_add_rule_thm:
fixes x1 x2 :: "'a::real_normed_vector"
shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
by (rule order_trans [OF norm_triangle_ineq add_mono])
-lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
+lemma ge_iff_diff_ge_0:
+ fixes a :: "'a::linordered_ring"
+ shows "a \<ge> b \<equiv> a - b \<ge> 0"
by (simp add: field_simps)
lemma pth_1:
fixes x :: "'a::real_normed_vector"
- shows "x == scaleR 1 x" by simp
+ shows "x \<equiv> scaleR 1 x" by simp
lemma pth_2:
fixes x :: "'a::real_normed_vector"
- shows "x - y == x + -y" by (atomize (full)) simp
+ shows "x - y \<equiv> x + -y"
+ by (atomize (full)) simp
lemma pth_3:
fixes x :: "'a::real_normed_vector"
- shows "- x == scaleR (-1) x" by simp
+ shows "- x \<equiv> scaleR (-1) x"
+ by simp
lemma pth_4:
fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+ shows "scaleR 0 x \<equiv> 0"
+ and "scaleR c 0 = (0::'a)"
+ by simp_all
lemma pth_5:
fixes x :: "'a::real_normed_vector"
- shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+ shows "scaleR c (scaleR d x) \<equiv> scaleR (c * d) x"
+ by simp
lemma pth_6:
fixes x :: "'a::real_normed_vector"
- shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+ shows "scaleR c (x + y) \<equiv> scaleR c x + scaleR c y"
by (simp add: scaleR_right_distrib)
lemma pth_7:
fixes x :: "'a::real_normed_vector"
- shows "0 + x == x" and "x + 0 == x" by simp_all
+ shows "0 + x \<equiv> x"
+ and "x + 0 \<equiv> x"
+ by simp_all
lemma pth_8:
fixes x :: "'a::real_normed_vector"
- shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+ shows "scaleR c x + scaleR d x \<equiv> scaleR (c + d) x"
by (simp add: scaleR_left_distrib)
lemma pth_9:
- fixes x :: "'a::real_normed_vector" shows
- "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
- "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
- "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+ fixes x :: "'a::real_normed_vector"
+ shows "(scaleR c x + z) + scaleR d x \<equiv> scaleR (c + d) x + z"
+ and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z"
+ and "(scaleR c x + w) + (scaleR d x + z) \<equiv> scaleR (c + d) x + (w + z)"
by (simp_all add: algebra_simps)
lemma pth_a:
fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x + y == y" by simp
+ shows "scaleR 0 x + y \<equiv> y"
+ by simp
lemma pth_b:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
- "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
- "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d y \<equiv> scaleR c x + scaleR d y"
+ and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)"
+ and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)"
+ and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR c x + (w + (scaleR d y + z))"
by (simp_all add: algebra_simps)
lemma pth_c:
- fixes x :: "'a::real_normed_vector" shows
- "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
- "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
- "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
- "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d y \<equiv> scaleR d y + scaleR c x"
+ and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)"
+ and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)"
+ and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR d y + ((scaleR c x + w) + z)"
by (simp_all add: algebra_simps)
lemma pth_d:
fixes x :: "'a::real_normed_vector"
- shows "x + 0 == x" by simp
+ shows "x + 0 \<equiv> x"
+ by simp
lemma norm_imp_pos_and_ge:
fixes x :: "'a::real_normed_vector"
- shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+ shows "norm x \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
by atomize auto
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
+lemma real_eq_0_iff_le_ge_0:
+ fixes x :: real
+ shows "x = 0 \<equiv> x \<ge> 0 \<and> - x \<ge> 0"
+ by arith
lemma norm_pths:
- fixes x :: "'a::real_normed_vector" shows
- "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
- "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
+ fixes x :: "'a::real_normed_vector"
+ shows "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
+ and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
using norm_ge_zero[of "x - y"] by auto
lemmas arithmetic_simps =
@@ -112,14 +126,16 @@
ML_file "normarith.ML"
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {*
+ Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
*} "prove simple linear statements about vector norms"
-text{* Hence more metric properties. *}
+
+text {* Hence more metric properties. *}
lemma dist_triangle_add:
fixes x y x' y' :: "'a::real_normed_vector"
- shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+ shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
by norm
lemma dist_triangle_add_half:
--- a/src/Pure/Concurrent/simple_thread.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Sep 18 20:54:46 2013 +0200
@@ -24,7 +24,7 @@
fun fork interrupts body =
Thread.fork (fn () =>
- exception_trace (fn () =>
+ print_exception_trace General.exnMessage (fn () =>
body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
attributes interrupts);
--- a/src/Pure/Isar/rule_insts.ML Wed Sep 18 20:44:10 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-(* Title: Pure/Isar/rule_insts.ML
- Author: Makarius
-
-Rule instantiations -- operations within a rule/subgoal context.
-*)
-
-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 res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val thin_tac: Proof.context -> string -> int -> tactic
- val subgoal_tac: Proof.context -> string -> int -> tactic
- val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
- (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
-end;
-
-signature RULE_INSTS =
-sig
- include BASIC_RULE_INSTS
- val make_elim_preserve: thm -> thm
-end;
-
-structure Rule_Insts: RULE_INSTS =
-struct
-
-(** reading instantiations **)
-
-local
-
-fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
-
-fun the_sort tvars (xi: indexname) =
- (case AList.lookup (op =) tvars xi of
- SOME S => S
- | NONE => error_var "No such type variable in theorem: " xi);
-
-fun the_type vars (xi: indexname) =
- (case AList.lookup (op =) vars xi of
- SOME T => T
- | NONE => error_var "No such variable in theorem: " xi);
-
-fun instantiate inst =
- Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
- Envir.beta_norm;
-
-fun make_instT f v =
- let
- val T = TVar v;
- val T' = f T;
- in if T = T' then NONE else SOME (T, T') end;
-
-fun make_inst f v =
- let
- val t = Var v;
- val t' = f t;
- in if t aconv t' then NONE else SOME (t, t') end;
-
-val add_used =
- (Thm.fold_terms o fold_types o fold_atyps)
- (fn TFree (a, _) => insert (op =) a
- | TVar ((a, _), _) => insert (op =) a
- | _ => I);
-
-in
-
-fun read_termTs ctxt schematic ss Ts =
- let
- fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
- val ts = map2 parse Ts ss;
- val ts' =
- map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
- |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
- |> Variable.polymorphic ctxt;
- val Ts' = map Term.fastype_of ts';
- val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
- in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
-
-fun read_insts ctxt mixed_insts (tvars, vars) =
- let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
-
- val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
-
-
- (* type instantiations *)
-
- fun readT (xi, s) =
- let
- val S = the_sort tvars xi;
- val T = Syntax.read_typ ctxt s;
- in
- if Sign.of_sort thy (T, S) then ((xi, S), T)
- else error_var "Incompatible sort for typ instantiation of " xi
- end;
-
- val instT1 = Term_Subst.instantiateT (map readT type_insts);
- val vars1 = map (apsnd instT1) vars;
-
-
- (* term instantiations *)
-
- val (xs, ss) = split_list term_insts;
- val Ts = map (the_type vars1) xs;
- val (ts, inferred) = read_termTs ctxt false ss Ts;
-
- val instT2 = Term.typ_subst_TVars inferred;
- val vars2 = map (apsnd instT2) vars1;
- val inst2 = instantiate (xs ~~ ts);
-
-
- (* result *)
-
- val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
- val inst_vars = map_filter (make_inst inst2) vars2;
- in
- (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
- end;
-
-fun read_instantiate_mixed ctxt mixed_insts thm =
- let
- val ctxt' = ctxt
- |> 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 [];
- val vars = Thm.fold_terms Term.add_vars thm [];
- val insts = read_insts ctxt' mixed_insts (tvars, vars);
- in
- Drule.instantiate_normalize insts thm
- |> Rule_Cases.save thm
- end;
-
-fun read_instantiate_mixed' ctxt (args, concl_args) thm =
- let
- fun zip_vars _ [] = []
- | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
- | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
- | zip_vars [] _ = error "More instantiations than variables in theorem";
- 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;
-
-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 instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
-
-
-
-(** attributes **)
-
-(* where: named instantiation *)
-
-val _ = Theory.setup
- (Attrib.setup (Binding.name "where")
- (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
- (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
- "named instantiation of theorem");
-
-
-(* of: positional instantiation (terms only) *)
-
-local
-
-val inst = Args.maybe Args.name_source;
-val concl = Args.$$$ "concl" -- Args.colon;
-
-val insts =
- Scan.repeat (Scan.unless concl inst) --
- Scan.optional (concl |-- Scan.repeat inst) [];
-
-in
-
-val _ = Theory.setup
- (Attrib.setup (Binding.name "of")
- (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
- "positional instantiation of theorem");
-
-end;
-
-
-
-(** tactics **)
-
-(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
-
-(* FIXME cleanup this mess!!! *)
-
-fun bires_inst_tac bires_flag ctxt insts thm =
- let
- val thy = Proof_Context.theory_of ctxt;
- (* Separate type and term insts *)
- fun has_type_var ((x, _), _) =
- (case Symbol.explode x of "'" :: _ => true | _ => false);
- val Tinsts = filter has_type_var insts;
- val tinsts = filter_out has_type_var insts;
-
- (* Tactic *)
- fun tac i st = CSUBGOAL (fn (cgoal, _) =>
- let
- val goal = term_of cgoal;
- val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*)
- val params = rev (Term.rename_wrt_term goal params)
- (*as they are printed: bound variables with*)
- (*the same name are renamed during printing*)
-
- val (param_names, ctxt') = ctxt
- |> Variable.declare_thm thm
- |> Thm.fold_terms Variable.declare_constraints st
- |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
-
- (* Process type insts: Tinsts_env *)
- fun absent xi = error
- ("No such variable in theorem: " ^ Term.string_of_vname xi);
- val (rtypes, rsorts) = Drule.types_sorts thm;
- fun readT (xi, s) =
- let val S = case rsorts xi of SOME S => S | NONE => absent xi;
- val T = Syntax.read_typ ctxt' s;
- val U = TVar (xi, S);
- in if Sign.typ_instance thy (T, U) then (U, T)
- else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
- end;
- val Tinsts_env = map readT Tinsts;
- (* Preprocess rule: extract vars and their types, apply Tinsts *)
- fun get_typ xi =
- (case rtypes xi of
- SOME T => typ_subst_atomic Tinsts_env T
- | NONE => absent xi);
- val (xis, ss) = Library.split_list tinsts;
- val Ts = map get_typ xis;
-
- val (ts, envT) = read_termTs ctxt' true ss Ts;
- val envT' = map (fn (ixn, T) =>
- (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
- val cenv =
- map
- (fn (xi, t) =>
- pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
- (distinct
- (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
- (xis ~~ ts));
- (* Lift and instantiate rule *)
- val maxidx = Thm.maxidx_of st;
- val paramTs = map #2 params
- and inc = maxidx+1
- fun liftvar (Var ((a,j), T)) =
- Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
- | liftvar t = raise TERM("Variable expected", [t]);
- fun liftterm t =
- fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
- fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
- val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
- val rule = Drule.instantiate_normalize
- (map lifttvar envT', map liftpair cenv)
- (Thm.lift_rule cgoal thm)
- in
- compose_tac (bires_flag, rule, nprems_of thm) i
- end) i st;
- in tac end;
-
-val res_inst_tac = bires_inst_tac false;
-val eres_inst_tac = bires_inst_tac true;
-
-
-(* forward resolution *)
-
-fun make_elim_preserve rl =
- let
- val cert = Thm.cterm_of (Thm.theory_of_thm rl);
- val maxidx = Thm.maxidx_of rl;
- fun cvar xi = cert (Var (xi, propT));
- val revcut_rl' =
- Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
- (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
- in
- (case Seq.list_of
- (Thm.bicompose {flatten = true, match = false, incremented = false}
- (false, rl, Thm.nprems_of rl) 1 revcut_rl')
- of
- [th] => th
- | _ => raise THM ("make_elim_preserve", 1, [rl]))
- end;
-
-(*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
-
-(*forward tactic applies a rule to an assumption without deleting it*)
-fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
-
-(*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
-
-
-(* derived tactics *)
-
-(*deletion of an assumption*)
-fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
-
-(*Introduce the given proposition as lemma and subgoal*)
-fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
-
-
-
-(** methods **)
-
-(* rule_tac etc. -- refer to dynamic goal state! *)
-
-fun method inst_tac tac =
- Args.goal_spec --
- Scan.optional (Scan.lift
- (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
- Args.$$$ "in")) [] --
- Attrib.thms >>
- (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
- if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
- else
- (case thms of
- [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
- | _ => error "Cannot have instantiations with multiple rules")));
-
-val res_inst_meth = method res_inst_tac (K resolve_tac);
-val eres_inst_meth = method eres_inst_tac (K eresolve_tac);
-val cut_inst_meth = method cut_inst_tac (K cut_rules_tac);
-val dres_inst_meth = method dres_inst_tac (K dresolve_tac);
-val forw_inst_meth = method forw_inst_tac (K forward_tac);
-
-
-(* setup *)
-
-val _ = Theory.setup
- (Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
- Method.setup (Binding.name "erule_tac") eres_inst_meth
- "apply rule in elimination manner (dynamic instantiation)" #>
- Method.setup (Binding.name "drule_tac") dres_inst_meth
- "apply rule in destruct manner (dynamic instantiation)" #>
- Method.setup (Binding.name "frule_tac") forw_inst_meth
- "apply rule in forward manner (dynamic instantiation)" #>
- Method.setup (Binding.name "cut_tac") cut_inst_meth "cut rule (dynamic instantiation)" #>
- Method.setup (Binding.name "subgoal_tac")
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
- (fn (quant, props) => fn ctxt =>
- SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
- "insert subgoal (dynamic instantiation)" #>
- Method.setup (Binding.name "thin_tac")
- (Args.goal_spec -- Scan.lift Args.name_source >>
- (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
- "remove premise (dynamic instantiation)");
-
-end;
-
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
-open Basic_Rule_Insts;
--- a/src/Pure/Isar/runtime.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Isar/runtime.ML Wed Sep 18 20:54:46 2013 +0200
@@ -17,8 +17,8 @@
val exn_messages_ids: exn_info -> exn -> error list
val exn_messages: exn_info -> exn -> (serial * string) list
val exn_message: exn_info -> exn -> string
- val debugging: ('a -> 'b) -> 'a -> 'b
- val controlled_execution: ('a -> 'b) -> 'a -> 'b
+ val debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+ val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
end;
@@ -137,13 +137,13 @@
(** controlled execution **)
-fun debugging f x =
+fun debugging exn_message f x =
if ! debug
- then exception_trace (fn () => f x)
+ then print_exception_trace exn_message (fn () => f x)
else f x;
-fun controlled_execution f x =
- (f |> debugging |> Future.interruptible_task) x;
+fun controlled_execution exn_message f x =
+ (f |> debugging exn_message |> Future.interruptible_task) x;
fun toplevel_error output_exn f x = f x
handle exn =>
--- a/src/Pure/Isar/toplevel.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Sep 18 20:54:46 2013 +0200
@@ -26,10 +26,12 @@
val print_state: bool -> state -> unit
val pretty_abstract: state -> Pretty.T
val quiet: bool Unsynchronized.ref
- val debug: bool Unsynchronized.ref
val interact: bool Unsynchronized.ref
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
+ val debug: bool Unsynchronized.ref
+ val debugging: ('a -> 'b) -> 'a -> 'b
+ val controlled_execution: ('a -> 'b) -> 'a -> 'b
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
@@ -226,20 +228,26 @@
(** toplevel transitions **)
val quiet = Unsynchronized.ref false; (*Proof General legacy*)
-val debug = Runtime.debug;
val interact = Unsynchronized.ref false; (*Proof General legacy*)
val timing = Unsynchronized.ref false; (*Proof General legacy*)
val profiling = Unsynchronized.ref 0;
+
+(* controlled execution *)
+
+val debug = Runtime.debug;
+fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
+fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
+
fun program body =
(body
- |> Runtime.controlled_execution
+ |> controlled_execution
|> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
fun thread interrupts body =
Thread.fork
(((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
- |> Runtime.debugging
+ |> debugging
|> Runtime.toplevel_error
(fn exn =>
Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
@@ -268,7 +276,7 @@
val (result, err) =
cont_node
- |> Runtime.controlled_execution f
+ |> controlled_execution f
|> state_error NONE
handle exn => state_error (SOME exn) cont_node;
in
@@ -297,11 +305,11 @@
local
fun apply_tr _ (Init f) (State (NONE, _)) =
- State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE)
+ State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
| apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
exit_transaction state
| apply_tr int (Keep f) state =
- Runtime.controlled_execution (fn x => tap (f int) x) state
+ controlled_execution (fn x => tap (f int) x) state
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
apply_transaction (fn x => f int x) g state
| apply_tr _ _ _ = raise UNDEF;
--- a/src/Pure/ML-Systems/polyml.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Wed Sep 18 20:54:46 2013 +0200
@@ -75,7 +75,7 @@
(* ML runtime system *)
-val exception_trace = PolyML.exception_trace;
+fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
val timing = PolyML.timing;
val profiling = PolyML.profiling;
--- a/src/Pure/ML-Systems/smlnj.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Sep 18 20:54:46 2013 +0200
@@ -73,7 +73,7 @@
fun profile (n: int) f x = f x;
(*dummy implementation*)
-fun exception_trace f = f ();
+fun print_exception_trace (_: exn -> string) f = f ();
(* ML command execution *)
--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML Wed Sep 18 20:54:46 2013 +0200
@@ -4,11 +4,11 @@
Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
*)
-fun exception_trace e =
+fun print_exception_trace exn_message e =
PolyML.Exception.traceException
(e, fn (trace, exn) =>
let
- val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
+ val title = "Exception trace - " ^ exn_message exn;
val _ = tracing (cat_lines (title :: trace));
in reraise exn end);
--- a/src/Pure/ML/ml_compiler.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/ml_compiler.ML Wed Sep 18 20:54:46 2013 +0200
@@ -9,6 +9,7 @@
val exn_messages_ids: exn -> Runtime.error list
val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
+ val exn_trace: (unit -> 'a) -> 'a
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
@@ -22,6 +23,7 @@
val exn_messages_ids = Runtime.exn_messages_ids exn_info;
val exn_messages = Runtime.exn_messages exn_info;
val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
fun eval verbose pos toks =
let
--- a/src/Pure/ML/ml_compiler_polyml.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Sep 18 20:54:46 2013 +0200
@@ -36,6 +36,7 @@
val exn_messages_ids = Runtime.exn_messages_ids exn_info;
val exn_messages = Runtime.exn_messages exn_info;
val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
(* parse trees *)
@@ -165,7 +166,7 @@
| SOME code =>
apply_result
((code
- |> Runtime.debugging
+ |> Runtime.debugging exn_message
|> Runtime.toplevel_error (err o exn_message)) ())));
--- a/src/Pure/PIDE/command.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/PIDE/command.ML Wed Sep 18 20:54:46 2013 +0200
@@ -212,7 +212,7 @@
Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
fun print_error tr e =
- (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
+ (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
handle exn =>
if Exn.is_interrupt exn then reraise exn
else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
@@ -256,7 +256,7 @@
let
val params = {command_name = command_name, args = args};
in
- (case Exn.capture (Runtime.controlled_execution get_pr) params of
+ (case Exn.capture (Toplevel.controlled_execution get_pr) params of
Exn.Res NONE => NONE
| Exn.Res (SOME pr) => SOME (make_print name args pr)
| Exn.Exn exn => SOME (bad_print name args exn))
--- a/src/Pure/Pure.thy Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/Pure.thy Wed Sep 18 20:54:46 2013 +0200
@@ -103,6 +103,7 @@
begin
ML_file "Isar/isar_syn.ML"
+ML_file "Tools/rule_insts.ML";
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
ML_file "Tools/proof_general_pure.ML"
--- a/src/Pure/ROOT Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ROOT Wed Sep 18 20:54:46 2013 +0200
@@ -130,7 +130,6 @@
"Isar/proof_display.ML"
"Isar/proof_node.ML"
"Isar/rule_cases.ML"
- "Isar/rule_insts.ML"
"Isar/runtime.ML"
"Isar/spec_rules.ML"
"Isar/specification.ML"
--- a/src/Pure/ROOT.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/ROOT.ML Wed Sep 18 20:54:46 2013 +0200
@@ -75,7 +75,11 @@
then use "ML/exn_properties_polyml.ML"
else use "ML/exn_properties_dummy.ML";
-if ML_System.name = "polyml-5.5.0"
+if ML_System.name = "polyml-5.5.1"
+then use "ML/exn_trace_polyml-5.5.1.ML"
+else ();
+
+if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
then use "ML/ml_statistics_polyml-5.5.0.ML"
else use "ML/ml_statistics_dummy.ML";
@@ -184,7 +188,6 @@
use "Isar/runtime.ML";
use "ML/ml_compiler.ML";
if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
-if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
(*global execution*)
use "PIDE/document_id.ML";
@@ -278,7 +281,6 @@
use "Thy/rail.ML";
(*theory and proof operations*)
-use "Isar/rule_insts.ML";
use "Thy/thm_deps.ML";
use "Isar/isar_cmd.ML";
--- a/src/Pure/System/gui.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/System/gui.scala Wed Sep 18 20:54:46 2013 +0200
@@ -1,13 +1,13 @@
/* Title: Pure/System/gui.scala
Author: Makarius
-Elementary GUI tools.
+Basic GUI tools (for AWT/Swing).
*/
package isabelle
-import java.awt.{Image, Component, Toolkit}
+import java.awt.{Image, Component, Container, Toolkit, Window}
import javax.swing.{ImageIcon, JOptionPane, UIManager}
import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -35,10 +35,12 @@
/* simple dialogs */
- def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
+ def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+ : ScrollPane =
{
val text = new TextArea(txt)
if (width > 0) text.columns = width
+ if (height > 0 && split_lines(txt).length > height) text.rows = height
text.editable = editable
new ScrollPane(text)
}
@@ -117,5 +119,29 @@
new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
def isabelle_image(): Image = isabelle_icon().getImage
+
+
+ /* component hierachy */
+
+ def get_parent(component: Component): Option[Container] =
+ component.getParent match {
+ case null => None
+ case parent => Some(parent)
+ }
+
+ def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
+ private var next_elem = get_parent(component)
+ def hasNext(): Boolean = next_elem.isDefined
+ def next(): Container =
+ next_elem match {
+ case Some(parent) =>
+ next_elem = get_parent(parent)
+ parent
+ case None => Iterator.empty.next()
+ }
+ }
+
+ def parent_window(component: Component): Option[Window] =
+ ancestors(component).collectFirst({ case x: Window => x })
}
--- a/src/Pure/System/isabelle_process.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 18 20:54:46 2013 +0200
@@ -48,7 +48,7 @@
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
| SOME cmd =>
- (Runtime.debugging cmd args handle exn =>
+ (Toplevel.debugging cmd args handle exn =>
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
ML_Compiler.exn_message exn)));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/wrap_panel.scala Wed Sep 18 20:54:46 2013 +0200
@@ -0,0 +1,123 @@
+/* Title: Pure/System/wrap_panel.scala
+ Author: Makarius
+
+Panel with improved FlowLayout for wrapping of components over
+multiple lines, see also
+http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
+scala.swing.FlowPanel.
+*/
+
+package isabelle
+
+
+import java.awt.{FlowLayout, Container, Dimension}
+import javax.swing.{JComponent, JPanel, JScrollPane}
+
+import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
+
+
+object Wrap_Panel
+{
+ val Alignment = FlowPanel.Alignment
+
+ class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
+ extends FlowLayout(align: Int, hgap: Int, vgap: Int)
+ {
+ override def preferredLayoutSize(target: Container): Dimension =
+ layout_size(target, true)
+
+ override def minimumLayoutSize(target: Container): Dimension =
+ {
+ val minimum = layout_size(target, false)
+ minimum.width -= (getHgap + 1)
+ minimum
+ }
+
+ private def layout_size(target: Container, preferred: Boolean): Dimension =
+ {
+ target.getTreeLock.synchronized
+ {
+ val target_width =
+ if (target.getSize.width == 0) Integer.MAX_VALUE
+ else target.getSize.width
+
+ val hgap = getHgap
+ val vgap = getVgap
+ val insets = target.getInsets
+ val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
+ val max_width = target_width - horizontal_insets_and_gap
+
+
+ /* fit components into rows */
+
+ val dim = new Dimension(0, 0)
+ var row_width = 0
+ var row_height = 0
+ def add_row()
+ {
+ dim.width = dim.width max row_width
+ if (dim.height > 0) dim.height += vgap
+ dim.height += row_height
+ }
+
+ for {
+ i <- 0 until target.getComponentCount
+ m = target.getComponent(i)
+ if m.isVisible
+ d = if (preferred) m.getPreferredSize else m.getMinimumSize()
+ }
+ {
+ if (row_width + d.width > max_width) {
+ add_row()
+ row_width = 0
+ row_height = 0
+ }
+
+ if (row_width != 0) row_width += hgap
+
+ row_width += d.width
+ row_height = row_height max d.height
+ }
+ add_row()
+
+ dim.width += horizontal_insets_and_gap
+ dim.height += insets.top + insets.bottom + vgap * 2
+
+
+ /* special treatment for ScrollPane */
+
+ val scroll_pane =
+ GUI.ancestors(target).exists(
+ {
+ case _: JScrollPane => true
+ case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
+ case _ => false
+ })
+ if (scroll_pane && target.isValid)
+ dim.width -= (hgap + 1)
+
+ dim
+ }
+ }
+ }
+}
+
+
+class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
+ extends Panel with SequentialContainer.Wrapper
+{
+ override lazy val peer: JPanel =
+ new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
+
+ def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
+ def this() = this(Wrap_Panel.Alignment.Center)()
+
+ contents ++= contents0
+
+ private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
+
+ def vGap: Int = layoutManager.getVgap
+ def vGap_=(n: Int) { layoutManager.setVgap(n) }
+ def hGap: Int = layoutManager.getHgap
+ def hGap_=(n: Int) { layoutManager.setHgap(n) }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/rule_insts.ML Wed Sep 18 20:54:46 2013 +0200
@@ -0,0 +1,362 @@
+(* Title: Pure/Tools/rule_insts.ML
+ Author: Makarius
+
+Rule instantiations -- operations within implicit rule / subgoal context.
+*)
+
+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 res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val thin_tac: Proof.context -> string -> int -> tactic
+ val subgoal_tac: Proof.context -> string -> int -> tactic
+end;
+
+signature RULE_INSTS =
+sig
+ include BASIC_RULE_INSTS
+ 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
+end;
+
+structure Rule_Insts: RULE_INSTS =
+struct
+
+(** reading instantiations **)
+
+local
+
+fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
+
+fun the_sort tvars (xi: indexname) =
+ (case AList.lookup (op =) tvars xi of
+ SOME S => S
+ | NONE => error_var "No such type variable in theorem: " xi);
+
+fun the_type vars (xi: indexname) =
+ (case AList.lookup (op =) vars xi of
+ SOME T => T
+ | NONE => error_var "No such variable in theorem: " xi);
+
+fun instantiate inst =
+ Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+ Envir.beta_norm;
+
+fun make_instT f v =
+ let
+ val T = TVar v;
+ val T' = f T;
+ in if T = T' then NONE else SOME (T, T') end;
+
+fun make_inst f v =
+ let
+ val t = Var v;
+ val t' = f t;
+ in if t aconv t' then NONE else SOME (t, t') end;
+
+val add_used =
+ (Thm.fold_terms o fold_types o fold_atyps)
+ (fn TFree (a, _) => insert (op =) a
+ | TVar ((a, _), _) => insert (op =) a
+ | _ => I);
+
+in
+
+fun read_termTs ctxt schematic ss Ts =
+ let
+ fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
+ val ts = map2 parse Ts ss;
+ val ts' =
+ map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
+ |> Syntax.check_terms ((schematic ? Proof_Context.set_mode Proof_Context.mode_schematic) ctxt)
+ |> Variable.polymorphic ctxt;
+ val Ts' = map Term.fastype_of ts';
+ val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
+ in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
+
+fun read_insts ctxt mixed_insts (tvars, vars) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
+
+ val (type_insts, term_insts) = List.partition (String.isPrefix "'" o fst o fst) mixed_insts;
+
+
+ (* type instantiations *)
+
+ fun readT (xi, s) =
+ let
+ val S = the_sort tvars xi;
+ val T = Syntax.read_typ ctxt s;
+ in
+ if Sign.of_sort thy (T, S) then ((xi, S), T)
+ else error_var "Incompatible sort for typ instantiation of " xi
+ end;
+
+ val instT1 = Term_Subst.instantiateT (map readT type_insts);
+ val vars1 = map (apsnd instT1) vars;
+
+
+ (* term instantiations *)
+
+ val (xs, ss) = split_list term_insts;
+ val Ts = map (the_type vars1) xs;
+ val (ts, inferred) = read_termTs ctxt false ss Ts;
+
+ val instT2 = Term.typ_subst_TVars inferred;
+ val vars2 = map (apsnd instT2) vars1;
+ val inst2 = instantiate (xs ~~ ts);
+
+
+ (* result *)
+
+ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
+ val inst_vars = map_filter (make_inst inst2) vars2;
+ in
+ (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
+ end;
+
+fun read_instantiate_mixed ctxt mixed_insts thm =
+ let
+ val ctxt' = ctxt
+ |> 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 [];
+ val vars = Thm.fold_terms Term.add_vars thm [];
+ val insts = read_insts ctxt' mixed_insts (tvars, vars);
+ in
+ Drule.instantiate_normalize insts thm
+ |> Rule_Cases.save thm
+ end;
+
+fun read_instantiate_mixed' ctxt (args, concl_args) thm =
+ let
+ fun zip_vars _ [] = []
+ | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
+ | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
+ | zip_vars [] _ = error "More instantiations than variables in theorem";
+ 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;
+
+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 instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
+
+
+
+(** attributes **)
+
+(* where: named instantiation *)
+
+val _ = Theory.setup
+ (Attrib.setup @{binding "where"}
+ (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
+ (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
+ "named instantiation of theorem");
+
+
+(* of: positional instantiation (terms only) *)
+
+local
+
+val inst = Args.maybe Args.name_source;
+val concl = Args.$$$ "concl" -- Args.colon;
+
+val insts =
+ Scan.repeat (Scan.unless concl inst) --
+ Scan.optional (concl |-- Scan.repeat inst) [];
+
+in
+
+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)))
+ "positional instantiation of theorem");
+
+end;
+
+
+
+(** tactics **)
+
+(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
+
+(* FIXME cleanup this mess!!! *)
+
+fun bires_inst_tac bires_flag ctxt insts thm =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ (* Separate type and term insts *)
+ fun has_type_var ((x, _), _) =
+ (case Symbol.explode x of "'" :: _ => true | _ => false);
+ val Tinsts = filter has_type_var insts;
+ val tinsts = filter_out has_type_var insts;
+
+ (* Tactic *)
+ fun tac i st = CSUBGOAL (fn (cgoal, _) =>
+ let
+ val goal = term_of cgoal;
+ val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*)
+ val params = rev (Term.rename_wrt_term goal params)
+ (*as they are printed: bound variables with*)
+ (*the same name are renamed during printing*)
+
+ val (param_names, ctxt') = ctxt
+ |> Variable.declare_thm thm
+ |> Thm.fold_terms Variable.declare_constraints st
+ |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+
+ (* Process type insts: Tinsts_env *)
+ fun absent xi = error
+ ("No such variable in theorem: " ^ Term.string_of_vname xi);
+ val (rtypes, rsorts) = Drule.types_sorts thm;
+ fun readT (xi, s) =
+ let val S = case rsorts xi of SOME S => S | NONE => absent xi;
+ val T = Syntax.read_typ ctxt' s;
+ val U = TVar (xi, S);
+ in if Sign.typ_instance thy (T, U) then (U, T)
+ else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
+ end;
+ val Tinsts_env = map readT Tinsts;
+ (* Preprocess rule: extract vars and their types, apply Tinsts *)
+ fun get_typ xi =
+ (case rtypes xi of
+ SOME T => typ_subst_atomic Tinsts_env T
+ | NONE => absent xi);
+ val (xis, ss) = Library.split_list tinsts;
+ val Ts = map get_typ xis;
+
+ val (ts, envT) = read_termTs ctxt' true ss Ts;
+ val envT' = map (fn (ixn, T) =>
+ (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
+ val cenv =
+ map
+ (fn (xi, t) =>
+ pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
+ (distinct
+ (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
+ (xis ~~ ts));
+ (* Lift and instantiate rule *)
+ val maxidx = Thm.maxidx_of st;
+ val paramTs = map #2 params
+ and inc = maxidx+1
+ fun liftvar (Var ((a,j), T)) =
+ Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
+ | liftvar t = raise TERM("Variable expected", [t]);
+ fun liftterm t =
+ fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
+ fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
+ val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
+ val rule = Drule.instantiate_normalize
+ (map lifttvar envT', map liftpair cenv)
+ (Thm.lift_rule cgoal thm)
+ in
+ compose_tac (bires_flag, rule, nprems_of thm) i
+ end) i st;
+ in tac end;
+
+val res_inst_tac = bires_inst_tac false;
+val eres_inst_tac = bires_inst_tac true;
+
+
+(* forward resolution *)
+
+fun make_elim_preserve rl =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm rl);
+ val maxidx = Thm.maxidx_of rl;
+ fun cvar xi = cert (Var (xi, propT));
+ val revcut_rl' =
+ Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
+ (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
+ in
+ (case Seq.list_of
+ (Thm.bicompose {flatten = true, match = false, incremented = false}
+ (false, rl, Thm.nprems_of rl) 1 revcut_rl')
+ of
+ [th] => th
+ | _ => raise THM ("make_elim_preserve", 1, [rl]))
+ end;
+
+(*instantiate and cut -- for atomic fact*)
+fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
+
+(*forward tactic applies a rule to an assumption without deleting it*)
+fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
+
+(*dresolve tactic applies a rule to replace an assumption*)
+fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
+
+
+(* derived tactics *)
+
+(*deletion of an assumption*)
+fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
+
+(*Introduce the given proposition as lemma and subgoal*)
+fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
+
+
+
+(* method wrapper *)
+
+fun method inst_tac tac =
+ Args.goal_spec --
+ Scan.optional (Scan.lift
+ (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+ Args.$$$ "in")) [] --
+ Attrib.thms >>
+ (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
+ if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
+ else
+ (case thms of
+ [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+ | _ => error "Cannot have instantiations with multiple rules")));
+
+
+(* setup *)
+
+(*warning: rule_tac etc. refer to dynamic subgoal context!*)
+
+val _ = Theory.setup
+ (Method.setup @{binding rule_tac} (method res_inst_tac (K resolve_tac))
+ "apply rule (dynamic instantiation)" #>
+ Method.setup @{binding erule_tac} (method eres_inst_tac (K eresolve_tac))
+ "apply rule in elimination manner (dynamic instantiation)" #>
+ Method.setup @{binding drule_tac} (method dres_inst_tac (K dresolve_tac))
+ "apply rule in destruct manner (dynamic instantiation)" #>
+ Method.setup @{binding frule_tac} (method forw_inst_tac (K forward_tac))
+ "apply rule in forward manner (dynamic instantiation)" #>
+ Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
+ "cut rule (dynamic instantiation)" #>
+ Method.setup @{binding subgoal_tac}
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+ (fn (quant, props) => fn ctxt =>
+ SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
+ "insert subgoal (dynamic instantiation)" #>
+ Method.setup @{binding thin_tac}
+ (Args.goal_spec -- Scan.lift Args.name_source >>
+ (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
+ "remove premise (dynamic instantiation)");
+
+end;
+
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
+open Basic_Rule_Insts;
--- a/src/Pure/build-jars Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Pure/build-jars Wed Sep 18 20:54:46 2013 +0200
@@ -65,6 +65,7 @@
System/system_channel.scala
System/system_dialog.scala
System/utf8.scala
+ System/wrap_panel.scala
Thy/html.scala
Thy/present.scala
Thy/thy_header.scala
--- a/src/Tools/WWW_Find/scgi_server.ML Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML Wed Sep 18 20:54:46 2013 +0200
@@ -53,7 +53,7 @@
ConditionVar.wait (thread_wait, thread_wait_mutex));
add_thread
(Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *)
- (fn () => exception_trace threadf,
+ (fn () => ML_Compiler.exn_trace threadf,
[Thread.EnableBroadcastInterrupt true,
Thread.InterruptState
Thread.InterruptAsynchOnce])))
--- a/src/Tools/jEdit/etc/options Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/etc/options Wed Sep 18 20:54:46 2013 +0200
@@ -3,6 +3,9 @@
public option jedit_logic : string = ""
-- "default logic session"
+public option jedit_auto_load : bool = false
+ -- "load all required files automatically to resolve theory imports"
+
public option jedit_reset_font_size : int = 18
-- "reset font size for main text area"
--- a/src/Tools/jEdit/src/find_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
+import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -154,7 +154,7 @@
}
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), context, limit, allow_dups,
process_indicator.component, apply_query, zoom)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -78,11 +78,11 @@
override def init()
{
- JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
}
override def exit()
{
- JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button}
+import scala.swing.Button
import scala.swing.event.ButtonClicked
import java.lang.System
@@ -94,7 +94,7 @@
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
add(controls.peer, BorderLayout.NORTH)
@@ -113,14 +113,14 @@
override def init()
{
- JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main_actor
handle_resize()
}
override def exit()
{
- JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main_actor
delay_resize.revoke()
}
--- a/src/Tools/jEdit/src/isabelle.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Sep 18 20:54:46 2013 +0200
@@ -9,6 +9,9 @@
import isabelle._
+import scala.swing.CheckBox
+import scala.swing.event.ButtonClicked
+
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.textarea.JEditTextArea
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -112,6 +115,14 @@
def reset_continuous_checking() { continuous_checking = false }
def toggle_continuous_checking() { continuous_checking = !continuous_checking }
+ class Continuous_Checking extends CheckBox("Continuous checking")
+ {
+ tooltip = "Continuous checking of proof document (visible and required parts)"
+ reactions += { case ButtonClicked(_) => continuous_checking = selected }
+ def load() { selected = continuous_checking }
+ load()
+ }
+
/* required document nodes */
--- a/src/Tools/jEdit/src/jedit_lib.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Sep 18 20:54:46 2013 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
+import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
import java.awt.event.{KeyEvent, KeyListener}
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
@@ -92,30 +92,6 @@
}
- /* GUI components */
-
- def get_parent(component: Component): Option[Container] =
- component.getParent match {
- case null => None
- case parent => Some(parent)
- }
-
- def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
- private var next_elem = get_parent(component)
- def hasNext(): Boolean = next_elem.isDefined
- def next(): Container =
- next_elem match {
- case Some(parent) =>
- next_elem = get_parent(parent)
- parent
- case None => Iterator.empty.next()
- }
- }
-
- def parent_window(component: Component): Option[Window] =
- ancestors(component).collectFirst({ case x: Window => x })
-
-
/* basic tooltips, with multi-line support */
def wrap_tooltip(text: String): String =
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
import java.lang.System
@@ -155,6 +155,7 @@
}
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/plugin.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 18 20:54:46 2013 +0200
@@ -170,21 +170,27 @@
filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
if (!files.isEmpty) {
- val files_list = new ListView(files.sorted)
- for (i <- 0 until files.length)
- files_list.selection.indices += i
+ if (PIDE.options.bool("jedit_auto_load")) {
+ files.foreach(file => jEdit.openFile(null: View, file))
+ }
+ else {
+ val files_list = new ListView(files.sorted)
+ for (i <- 0 until files.length)
+ files_list.selection.indices += i
- val answer =
- GUI.confirm_dialog(view,
- "Auto loading of required files",
- JOptionPane.YES_NO_OPTION,
- "The following files are required to resolve theory imports.",
- "Reload selected files now?",
- new ScrollPane(files_list))
- if (answer == 0) {
- files.foreach(file =>
- if (files_list.selection.items.contains(file))
- jEdit.openFile(null: View, file))
+ val answer =
+ GUI.confirm_dialog(view,
+ "Auto loading of required files",
+ JOptionPane.YES_NO_OPTION,
+ "The following files are required to resolve theory imports.",
+ "Reload selected files now?",
+ new ScrollPane(files_list),
+ new Isabelle.Continuous_Checking)
+ if (answer == 0) {
+ files.foreach(file =>
+ if (files_list.selection.items.contains(file))
+ jEdit.openFile(null: View, file))
+ }
}
}
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Sep 18 20:54:46 2013 +0200
@@ -50,7 +50,7 @@
case top :: _ if top.results == results && top.info == info => top
case _ =>
val (old, rest) =
- JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
+ GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
case None => (stack, Nil)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, Component, Label, TextField, CheckBox}
+import scala.swing.{Button, Component, Label, TextField, CheckBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -174,7 +174,7 @@
}
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
provers_label, Component.wrap(provers), isar_proofs,
process_indicator.component, apply_query, cancel_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -12,7 +12,7 @@
import java.awt.Font
import scala.swing.event.ValueChanged
-import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
+import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
import org.gjt.sp.jedit.View
@@ -60,16 +60,16 @@
pages ++=
Symbol.groups map { case (group, symbols) =>
new TabbedPane.Page(group,
- new FlowPanel {
+ new ScrollPane(new Wrap_Panel {
contents ++= symbols.map(new Symbol_Component(_))
if (group == "control") contents += new Reset_Component
- }, null)
+ }), null)
}
pages += new TabbedPane.Page("search", new BorderPanel {
val search = new TextField(10)
- val results_panel = new FlowPanel
+ val results_panel = new Wrap_Panel
add(search, BorderPanel.Position.North)
- add(results_panel, BorderPanel.Position.Center)
+ add(new ScrollPane(results_panel), BorderPanel.Position.Center)
listenTo(search)
val delay_search =
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -10,9 +10,9 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
+import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
+import scala.swing.event.{MouseClicked, MouseMoved}
import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
@@ -73,17 +73,12 @@
session_phase.text = " " + phase_text(phase) + " "
}
- private val continuous_checking = new CheckBox("Continuous checking") {
- tooltip = "Continuous checking of proof document (visible and required parts)"
- reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected }
- def load() { selected = Isabelle.continuous_checking }
- load()
- }
+ private val continuous_checking = new Isabelle.Continuous_Checking
private val logic = Isabelle_Logic.logic_selector(true)
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 18 20:44:10 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 18 20:54:46 2013 +0200
@@ -10,7 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
+import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}
import java.lang.System
@@ -142,7 +142,8 @@
s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
add(controls.peer, BorderLayout.NORTH)