--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Aug 30 20:50:45 2017 +0200
@@ -314,7 +314,7 @@
then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on \<Omega>"
by (auto simp: integrable_on_def cong: has_integral_cong)
then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on (\<Omega> \<union> B n)"
- by (rule integrable_on_superset[rotated 2]) auto
+ by (rule integrable_on_superset) auto
then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on B n"
unfolding B_def by (rule integrable_on_subcbox) auto
then show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue_on \<Omega>' \<rightarrow>\<^sub>M borel"
@@ -2717,7 +2717,7 @@
note intl = has_integral_integrable[OF int]
have af: "f absolutely_integrable_on (closure S)"
using nonneg
- by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
+ by (intro absolutely_integrable_onI intl integrable_eq[OF intl]) simp
then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Wed Aug 30 20:50:45 2017 +0200
@@ -261,8 +261,8 @@
have f'_nonpos: "f' \<le> 0" using assms by (simp add: f'_def divide_simps)
let ?f = "\<lambda>t. (t - x) * f' + inverse x"
let ?F = "\<lambda>t. (t - x)^2 * f' / 2 + t * inverse x"
- have diff: "\<forall>t\<in>{x..x+a}. (?F has_vector_derivative ?f t)
- (at t within {x..x+a})" using assms
+ have diff: "\<And>t. t \<in> {x..x+a} \<Longrightarrow> (?F has_vector_derivative ?f t) (at t within {x..x+a})"
+ using assms
by (auto intro!: derivative_eq_intros
simp: has_field_derivative_iff_has_vector_derivative[symmetric])
from assms have "(?f has_integral (?F (x+a) - ?F x)) {x..x+a}"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 30 20:50:45 2017 +0200
@@ -716,7 +716,7 @@
using assms(1)
by auto
-lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
+lemma integrable_eq: "\<lbrakk>f integrable_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g integrable_on s"
unfolding integrable_on_def
using has_integral_eq[of s f g] has_integral_eq by blast
@@ -2615,79 +2615,70 @@
and "Inf {a..b} = a"
using assms by auto
-lemma fundamental_theorem_of_calculus:
+theorem fundamental_theorem_of_calculus:
fixes f :: "real \<Rightarrow> 'a::banach"
- assumes "a \<le> b"
- and vecd: "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
+ assumes "a \<le> b"
+ and vecd: "\<And>x. x \<in> {a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a..b})"
shows "(f' has_integral (f b - f a)) {a..b}"
unfolding has_integral_factor_content box_real[symmetric]
proof safe
fix e :: real
assume "e > 0"
- then have "\<forall>x. \<exists>d>0.
- x \<in> {a..b} \<longrightarrow>
- (\<forall>y\<in>{a..b}.
- norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
+ then have "\<forall>x. \<exists>d>0. x \<in> {a..b} \<longrightarrow>
+ (\<forall>y\<in>{a..b}. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
then obtain d where d: "\<And>x. 0 < d x"
"\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y-x) < d x\<rbrakk>
\<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x)"
- by metis
-
+ by metis
show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
- apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
- apply safe
- apply (rule gauge_ball_dependent)
- apply rule
- apply (rule d(1))
- proof -
+ proof (rule exI, safe)
+ show "gauge (\<lambda>x. ball x (d x))"
+ using d(1) gauge_ball_dependent by blast
+ next
fix p
- assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
- unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric]
- unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric]
- unfolding sum_distrib_left
- defer
- unfolding sum_subtractf[symmetric]
+ assume ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x (d x)) fine p"
+ have ba: "b - a = (\<Sum>(x,K)\<in>p. Sup K - Inf K)" "f b - f a = (\<Sum>(x,K)\<in>p. f(Sup K) - f(Inf K))"
+ using additive_tagged_division_1[where f= "\<lambda>x. x"] additive_tagged_division_1[where f= f]
+ \<open>a \<le> b\<close> ptag by auto
+ have "norm (\<Sum>(x, K) \<in> p. (content K *\<^sub>R f' x) - (f (Sup K) - f (Inf K)))
+ \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))"
proof (rule sum_norm_le,safe)
- fix x k
- assume "(x, k) \<in> p"
- note xk = tagged_division_ofD(2-4)[OF as(1) this]
- then obtain u v where k: "k = cbox u v" by blast
- have *: "u \<le> v"
- using xk unfolding k by auto
- have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
- using as(2)[unfolded fine_def,rule_format,OF \<open>(x,k)\<in>p\<close>,unfolded split_conv subset_eq] .
- have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
- norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
- apply (rule order_trans[OF _ norm_triangle_ineq4])
- apply (rule eq_refl)
- apply (rule arg_cong[where f=norm])
- unfolding scaleR_diff_left
- apply (auto simp add:algebra_simps)
- done
+ fix x K
+ assume "(x, K) \<in> p"
+ then have "x \<in> K" and kab: "K \<subseteq> cbox a b"
+ using ptag by blast+
+ then obtain u v where k: "K = cbox u v" and "x \<in> K" and kab: "K \<subseteq> cbox a b"
+ using ptag \<open>(x, K) \<in> p\<close> by auto
+ have "u \<le> v"
+ using \<open>x \<in> K\<close> unfolding k by auto
+ have ball: "\<forall>y\<in>K. y \<in> ball x (d x)"
+ using finep \<open>(x, K) \<in> p\<close> by blast
+ have "u \<in> K" "v \<in> K"
+ by (simp_all add: \<open>u \<le> v\<close> k)
+ have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) = norm (f u - f x - (u - x) *\<^sub>R f' x - (f v - f x - (v - x) *\<^sub>R f' x))"
+ by (auto simp add: algebra_simps)
+ also have "... \<le> norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
+ by (rule norm_triangle_ineq4)
+ finally have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
+ norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" .
also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
- apply (rule add_mono)
- apply (rule d(2)[of "x" "u",unfolded o_def])
- prefer 4
- apply (rule d(2)[of "x" "v",unfolded o_def])
- using ball[rule_format,of u] ball[rule_format,of v]
- using xk(1-2)
- unfolding k subset_eq
- apply (auto simp add:dist_real_def)
- done
- also have "\<dots> \<le> e * (Sup k - Inf k)"
- unfolding k interval_bounds_real[OF *]
- using xk(1)
- unfolding k
- by (auto simp add: dist_real_def field_simps)
- finally show "norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le>
- e * (Sup k - Inf k)"
- unfolding box_real k interval_bounds_real[OF *] content_real[OF *]
- interval_upperbound_real interval_lowerbound_real
- .
+ proof (rule add_mono)
+ show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
+ apply (rule d(2)[of x u])
+ using \<open>x \<in> K\<close> kab \<open>u \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+ show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
+ apply (rule d(2)[of x v])
+ using \<open>x \<in> K\<close> kab \<open>v \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+ qed
+ also have "\<dots> \<le> e * (Sup K - Inf K)"
+ using \<open>x \<in> K\<close> by (auto simp: k interval_bounds_real[OF \<open>u \<le> v\<close>] field_simps)
+ finally show "norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (Sup K - Inf K)"
+ using \<open>u \<le> v\<close> by (simp add: k)
qed
+ with \<open>a \<le> b\<close> show "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
+ by (auto simp: ba split_def sum_subtractf [symmetric] sum_distrib_left)
qed
qed
@@ -2697,7 +2688,7 @@
shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
proof -
have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
- apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
+ apply (rule fundamental_theorem_of_calculus [OF assms])
unfolding power2_eq_square
by (rule derivative_eq_intros | simp)+
then show ?thesis
@@ -3144,10 +3135,10 @@
using antiderivative_continuous[OF assms] by metis
have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
proof -
- have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
+ have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
then show ?thesis
- by (simp add: fundamental_theorem_of_calculus that(3))
+ by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
qed
then show ?thesis
using that by blast
@@ -3158,39 +3149,30 @@
lemma has_integral_twiddle:
assumes "0 < r"
- and "\<forall>x. h(g x) = x"
- and "\<forall>x. g(h x) = x"
+ and hg: "\<And>x. h(g x) = x"
+ and gh: "\<And>x. g(h x) = x"
and contg: "\<And>x. continuous (at x) g"
- and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
- and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
- and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
+ and g: "\<And>u v. \<exists>w z. g ` cbox u v = cbox w z"
+ and h: "\<And>u v. \<exists>w z. h ` cbox u v = cbox w z"
+ and r: "\<And>u v. content(g ` cbox u v) = r * content (cbox u v)"
and intfi: "(f has_integral i) (cbox a b)"
shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
-proof -
- show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
- apply cases
- defer
- apply (rule *)
- apply assumption
- proof goal_cases
- case prems: 1
- then show ?thesis
- unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
- qed
- assume "cbox a b \<noteq> {}"
+proof (cases "cbox a b = {}")
+ case True
+ then show ?thesis
+ using intfi by auto
+next
+ case False
obtain w z where wz: "h ` cbox a b = cbox w z"
using h by blast
have inj: "inj g" "inj h"
- apply (metis assms(2) injI)
- by (metis assms(3) injI)
+ using hg gh injI by metis+
from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
- show ?thesis
- unfolding h_eq has_integral
- unfolding h_eq[symmetric]
- proof safe
- fix e :: real
- assume e: "e > 0"
- with \<open>0 < r\<close> have "e * r > 0" by simp
+ have "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p
+ \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+ if "e > 0" for e
+ proof -
+ have "e * r > 0" using that \<open>0 < r\<close> by simp
with intfi[unfolded has_integral]
obtain d where d: "gauge d"
"\<And>p. p tagged_division_of cbox a b \<and> d fine p
@@ -3199,69 +3181,49 @@
define d' where "d' x = {y. g y \<in> d (g x)}" for x
have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
unfolding d'_def ..
- show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p
- \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+ show ?thesis
proof (rule_tac x=d' in exI, safe)
show "gauge d'"
- using d(1)
- unfolding gauge_def d'
- using continuous_open_preimage_univ[OF _ contg]
- by auto
+ using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
+ next
fix p
- assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
- note p = tagged_division_ofD[OF as(1)]
- have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of (cbox a b) \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
+ assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
+ note p = tagged_division_ofD[OF ptag]
+ have gab: "g y \<in> cbox a b" if "y \<in> K" "(x, K) \<in> p" for x y K
+ by (metis hg inj(2) inj_image_mem_iff p(3) subsetCE that that)
+ have gimp: "(\<lambda>(x,K). (g x, g ` K)) ` p tagged_division_of (cbox a b) \<and>
+ d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
unfolding tagged_division_of
proof safe
show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
- using as by auto
+ using ptag by auto
show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
- using as(2) unfolding fine_def d' by auto
+ using finep unfolding fine_def d' by auto
+ next
fix x k
- assume xk[intro]: "(x, k) \<in> p"
+ assume xk: "(x, k) \<in> p"
show "g x \<in> g ` k"
using p(2)[OF xk] by auto
show "\<exists>u v. g ` k = cbox u v"
using p(4)[OF xk] using assms(5-6) by auto
- {
- fix y
- assume "y \<in> k"
- then show "g y \<in> cbox a b" "g y \<in> cbox a b"
- using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
- using assms(2)[rule_format,of y]
- unfolding inj_image_mem_iff[OF inj(2)]
- by auto
- }
- fix x' k'
- assume xk': "(x', k') \<in> p"
- fix z
- assume z: "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
- have same: "(x, k) = (x', k')"
- apply -
- apply (rule ccontr)
- apply (drule p(5)[OF xk xk'])
- proof -
- assume as: "interior k \<inter> interior k' = {}"
- have "z \<in> g ` (interior k \<inter> interior k')"
- using interior_image_subset[OF \<open>inj g\<close> contg] z
+ fix x' K' u
+ assume xk': "(x', K') \<in> p" and u: "u \<in> interior (g ` k)" "u \<in> interior (g ` K')"
+ have "interior k \<inter> interior K' \<noteq> {}"
+ proof
+ assume "interior k \<inter> interior K' = {}"
+ moreover have "u \<in> g ` (interior k \<inter> interior K')"
+ using interior_image_subset[OF \<open>inj g\<close> contg] u
unfolding image_Int[OF inj(1)] by blast
- then show False
- using as by blast
+ ultimately show False by blast
qed
+ then have same: "(x, k) = (x', K')"
+ using ptag xk' xk by blast
then show "g x = g x'"
by auto
- {
- fix z
- assume "z \<in> k"
- then show "g z \<in> g ` k'"
- using same by auto
- }
- {
- fix z
- assume "z \<in> k'"
- then show "g z \<in> g ` k"
- using same by auto
- }
+ show "g u \<in> g ` K'"if "u \<in> k" for u
+ using that same by auto
+ show "g u \<in> g ` k"if "u \<in> K'" for u
+ using that same by auto
next
fix x
assume "x \<in> cbox a b"
@@ -3269,31 +3231,26 @@
using p(6) by auto
then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
- apply (clarsimp simp: )
+ apply clarsimp
by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
- qed
- note ** = d(2)[OF this]
- have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
- using inj(1) unfolding inj_on_def by fastforce
- have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
- using assms(7)
- apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
- apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
- apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
- done
+ qed (use gab in auto)
+ have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
+ using inj(1) unfolding inj_on_def by fastforce
+ have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
+ using r
+ apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
+ apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
+ apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
+ done
also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
- unfolding scaleR_diff_right scaleR_scaleR
- using assms(1)
- by auto
- finally have *: "?l = ?r" .
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
- using **
- unfolding *
- unfolding norm_scaleR
- using assms(1)
- by (auto simp add:field_simps)
+ using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
+ finally have eq: "?l = ?r" .
+ show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
+ using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
qed
qed
+ then show ?thesis
+ by (auto simp: h_eq has_integral)
qed
@@ -4408,10 +4365,7 @@
then have "?g integrable_on cbox c d"
using assms has_integral_integrable integrable_subinterval by blast
then have "f integrable_on cbox c d"
- apply -
- apply (rule integrable_eq)
- apply auto
- done
+ by (rule integrable_eq) auto
moreover then have "i = integral (cbox c d) f"
by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
ultimately show ?r by auto
@@ -4591,9 +4545,9 @@
lemma integrable_on_superset:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
- and "s \<subseteq> t"
- and "f integrable_on s"
+ assumes "f integrable_on S"
+ and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
+ and "S \<subseteq> t"
shows "f integrable_on t"
using assms
unfolding integrable_on_def
@@ -4601,7 +4555,7 @@
lemma integral_restrict_UNIV [intro]:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
+ shows "f integrable_on S \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
apply (rule integral_unique)
unfolding has_integral_restrict_UNIV
apply auto
@@ -6881,7 +6835,7 @@
proof -
have "((\<lambda>(x, y). f x y) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (prod.swap ` (cbox (c, a) (d, b)))"
apply (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
- apply (auto simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)
+ apply (force simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)+
done
then show ?thesis
by force
@@ -6934,10 +6888,10 @@
fix k ::nat
have "(\<lambda>x. exp (-a*x)) integrable_on {c..of_real k}" (is ?P)
unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
- hence int: "(f k) integrable_on {c..of_real k}"
- by (rule integrable_eq[rotated]) (simp add: f_def)
- show "f k integrable_on {c..}"
- by (rule integrable_on_superset[OF _ _ int]) (auto simp: f_def)
+ hence "(f k) integrable_on {c..of_real k}"
+ by (rule integrable_eq) (simp add: f_def)
+ then show "f k integrable_on {c..}"
+ by (rule integrable_on_superset) (auto simp: f_def)
next
fix x assume x: "x \<in> {c..}"
have "sequentially \<le> principal {nat \<lceil>x\<rceil>..}" unfolding at_top_def by (simp add: Inf_lower)
@@ -7118,9 +7072,9 @@
from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
by (auto intro!: integrable_continuous_real continuous_intros)
hence "f n integrable_on {a..n}"
- by (rule integrable_eq [rotated]) (auto simp: f_def)
+ by (rule integrable_eq) (auto simp: f_def)
thus "f n integrable_on {a..}"
- by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
+ by (rule integrable_on_superset) (auto simp: f_def)
next
fix n :: nat and x :: real
show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
--- a/src/HOL/Analysis/Improper_Integral.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy Wed Aug 30 20:50:45 2017 +0200
@@ -220,7 +220,10 @@
qed
qed
then show ?thesis
- using assms by (auto simp: equiintegrable_on_def integrable_eq)
+ using assms
+ apply (auto simp: equiintegrable_on_def)
+ apply (rule integrable_eq)
+ by auto
qed
subsection\<open>Subinterval restrictions for equiintegrable families\<close>
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Aug 30 20:50:45 2017 +0200
@@ -1386,6 +1386,22 @@
lemmas fps_numeral_simps =
fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
+lemma subdegree_div:
+ assumes "q dvd p"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q"
+proof (cases "p = 0")
+ case False
+ from assms have "p = p div q * q" by simp
+ also from assms False have "subdegree \<dots> = subdegree (p div q) + subdegree q"
+ by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff)
+ finally show ?thesis by simp
+qed simp_all
+
+lemma subdegree_div_unit:
+ assumes "q $ 0 \<noteq> 0"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p"
+ using assms by (subst subdegree_div) simp_all
+
subsection \<open>Formal power series form a Euclidean ring\<close>
--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 30 20:50:45 2017 +0200
@@ -1388,6 +1388,9 @@
for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
by (auto simp: degree_mult_eq)
+lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
+ by (induction n) (simp_all add: degree_mult_eq)
+
lemma degree_mult_right_le:
fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
assumes "q \<noteq> 0"
@@ -2454,9 +2457,6 @@
qed
qed
-lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
- by (induct n arbitrary: f) auto
-
lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
unfolding pderiv_coeffs_def
proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
@@ -2539,6 +2539,10 @@
apply (simp add: algebra_simps)
done
+lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
+ by (induction p rule: pCons_induct)
+ (auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
+
lemma pderiv_prod: "pderiv (prod f (as)) = (\<Sum>a\<in>as. prod f (as - {a}) * pderiv (f a))"
proof (induct as rule: infinite_finite_induct)
case (insert a as)
--- a/src/HOL/List.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/List.thy Wed Aug 30 20:50:45 2017 +0200
@@ -3108,7 +3108,10 @@
done
lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+ by (induct n) simp_all
+
+lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
+ by (induct n arbitrary: f) auto
lemma nth_take_lemma:
--- a/src/HOL/SMT.thy Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/SMT.thy Wed Aug 30 20:50:45 2017 +0200
@@ -1,12 +1,13 @@
(* Title: HOL/SMT.thy
Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, VU Amsterdam
*)
section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
theory SMT
-imports Divides
-keywords "smt_status" :: diag
+ imports Divides
+ keywords "smt_status" :: diag
begin
subsection \<open>A skolemization tactic and proof method\<close>
--- a/src/HOL/Tools/SMT/cvc4_interface.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML Wed Aug 30 20:50:45 2017 +0200
@@ -7,24 +7,30 @@
signature CVC4_INTERFACE =
sig
val smtlib_cvc4C: SMT_Util.class
+ val hosmtlib_cvc4C: SMT_Util.class
end;
structure CVC4_Interface: CVC4_INTERFACE =
struct
-val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+val cvc4C = ["cvc4"]
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
+val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
(* interface *)
local
- fun translate_config ctxt =
- {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
- serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+ fun translate_config order ctxt =
+ {order = order,
+ logic = K "(set-logic ALL_SUPPORTED)\n",
+ fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
in
-val _ =
- Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+val _ = Theory.setup (Context.theory_map
+ (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
+ SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
end
--- a/src/HOL/Tools/SMT/smt_builtin.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Wed Aug 30 20:50:45 2017 +0200
@@ -11,11 +11,11 @@
(*built-in types*)
val add_builtin_typ: SMT_Util.class ->
- typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+ typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
Context.generic
val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
Context.generic
- val dest_builtin_typ: Proof.context -> typ -> string option
+ val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
val is_builtin_typ_ext: Proof.context -> typ -> bool
(*built-in numbers*)
@@ -93,7 +93,8 @@
structure Builtins = Generic_Data
(
type T =
- (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+ (Proof.context -> typ -> bool,
+ (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
(term list bfun, bfunr option bfun) btab
val empty = ([], Symtab.empty)
val extend = I
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Aug 30 20:50:45 2017 +0200
@@ -32,6 +32,7 @@
val statistics: bool Config.T
val monomorph_limit: int Config.T
val monomorph_instances: int Config.T
+ val higher_order: bool Config.T
val nat_as_int: bool Config.T
val infer_triggers: bool Config.T
val debug_files: string Config.T
@@ -180,6 +181,7 @@
val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
--- a/src/HOL/Tools/SMT/smt_real.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Aug 30 20:50:45 2017 +0200
@@ -32,7 +32,7 @@
val setup_builtins =
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
- (@{typ real}, K (SOME "Real"), real_num) #>
+ (@{typ real}, K (SOME ("Real", [])), real_num) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
(@{const less (real)}, "<"),
(@{const less_eq (real)}, "<="),
--- a/src/HOL/Tools/SMT/smt_systems.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Wed Aug 30 20:50:45 2017 +0200
@@ -62,6 +62,7 @@
end
+
(* CVC4 *)
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -75,8 +76,16 @@
"--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
fun select_class ctxt =
- if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
- else SMTLIB_Interface.smtlibC
+ if Config.get ctxt cvc4_extensions then
+ if Config.get ctxt SMT_Config.higher_order then
+ CVC4_Interface.hosmtlib_cvc4C
+ else
+ CVC4_Interface.smtlib_cvc4C
+ else
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
in
val cvc4: SMT_Solver.solver_config = {
@@ -93,11 +102,20 @@
end
+
(* veriT *)
+local
+ fun select_class ctxt =
+ if Config.get ctxt SMT_Config.higher_order then
+ SMTLIB_Interface.hosmtlibC
+ else
+ SMTLIB_Interface.smtlibC
+in
+
val veriT: SMT_Solver.solver_config = {
name = "verit",
- class = K SMTLIB_Interface.smtlibC,
+ class = select_class,
avail = make_avail "VERIT",
command = make_command "VERIT",
options = (fn ctxt => [
@@ -113,6 +131,9 @@
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }
+end
+
+
(* Z3 *)
val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Aug 30 20:50:45 2017 +0200
@@ -10,8 +10,8 @@
datatype squant = SForall | SExists
datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
datatype sterm =
- SVar of int |
- SApp of string * sterm list |
+ SVar of int * sterm list |
+ SConst of string * sterm list |
SQua of squant * string list * sterm spattern list * sterm
(*translation configuration*)
@@ -21,6 +21,7 @@
dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
funcs: (string * (string list * string)) list }
type config = {
+ order: SMT_Util.order,
logic: term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -50,8 +51,8 @@
SPat of 'a list | SNoPat of 'a list
datatype sterm =
- SVar of int |
- SApp of string * sterm list |
+ SVar of int * sterm list |
+ SConst of string * sterm list |
SQua of squant * string list * sterm spattern list * sterm
@@ -64,6 +65,7 @@
funcs: (string * (string list * string)) list }
type config = {
+ order: SMT_Util.order,
logic: term list -> string,
fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -147,7 +149,7 @@
fun add_typ' T proper =
(case SMT_Builtin.dest_builtin_typ ctxt' T of
- SOME n => pair n
+ SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
| NONE => add_typ T proper)
fun tr_select sel =
@@ -425,11 +427,12 @@
| transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
| transT (T as Type _) =
(case SMT_Builtin.dest_builtin_typ ctxt T of
- SOME n => pair n
+ SOME (n, []) => pair n
+ | SOME (n, Ts) =>
+ fold_map transT Ts
+ #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
| NONE => add_typ T true)
- fun app n ts = SApp (n, ts)
-
fun trans t =
(case Term.strip_comb t of
(Const (qn, _), [Abs (_, T, t1)]) =>
@@ -440,17 +443,17 @@
| NONE => raise TERM ("unsupported quantifier", [t]))
| (u as Const (c as (_, T)), ts) =>
(case builtin ctxt c ts of
- SOME (n, _, us, _) => fold_map trans us #>> app n
- | NONE => transs u T ts)
- | (u as Free (_, T), ts) => transs u T ts
- | (Bound i, []) => pair (SVar i)
+ SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
+ | NONE => trans_applied_fun u T ts)
+ | (u as Free (_, T), ts) => trans_applied_fun u T ts
+ | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
| _ => raise TERM ("bad SMT term", [t]))
- and transs t T ts =
+ and trans_applied_fun t T ts =
let val (Us, U) = SMT_Util.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
- add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
+ add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
end
val (us, trx') = fold_map trans ts trx
@@ -480,7 +483,7 @@
fun translate ctxt smt_options comments ithms =
let
- val {logic, fp_kinds, serialize} = get_config ctxt
+ val {order, logic, fp_kinds, serialize} = get_config ctxt
fun no_dtyps (tr_context, ctxt) ts =
((Termtab.empty, [], tr_context, ctxt), ts)
@@ -510,10 +513,14 @@
|> rpair ctxt1
|-> Lambda_Lifting.lift_lambdas NONE is_binder
|-> (fn (ts', ll_defs) => fn ctxt' =>
- (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
-
+ let
+ val ts'' = map mk_trigger ll_defs @ ts'
+ |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
+ in
+ (ctxt', (ts'', ll_defs))
+ end)
val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
- |>> apfst (cons fun_app_eq)
+ |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
in
(ts4, tr_context)
|-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
--- a/src/HOL/Tools/SMT/smt_util.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Wed Aug 30 20:50:45 2017 +0200
@@ -10,6 +10,8 @@
val repeat: ('a -> 'a option) -> 'a -> 'a
val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
+ datatype order = First_Order | Higher_Order
+
(*class dictionaries*)
type class = string list
val basicC: class
@@ -79,6 +81,11 @@
in rep end
+(* order *)
+
+datatype order = First_Order | Higher_Order
+
+
(* class dictionaries *)
type class = string list
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Aug 30 20:50:45 2017 +0200
@@ -8,8 +8,9 @@
signature SMTLIB_INTERFACE =
sig
val smtlibC: SMT_Util.class
+ val hosmtlibC: SMT_Util.class
val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
- val translate_config: Proof.context -> SMT_Translate.config
+ val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
val assert_name_of_index: int -> string
val assert_index_of_name: string -> int
val assert_prefix : string
@@ -18,7 +19,10 @@
structure SMTLIB_Interface: SMTLIB_INTERFACE =
struct
-val smtlibC = ["smtlib"]
+val hoC = ["ho"]
+
+val smtlibC = ["smtlib"] (* SMT-LIB 2 *)
+val hosmtlibC = smtlibC @ hoC (* possibly SMT-LIB 3 *)
(* builtins *)
@@ -36,9 +40,11 @@
in
val setup_builtins =
+ SMT_Builtin.add_builtin_typ hosmtlibC
+ (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
fold (SMT_Builtin.add_builtin_typ smtlibC) [
- (@{typ bool}, K (SOME "Bool"), K (K NONE)),
- (@{typ int}, K (SOME "Int"), int_num)] #>
+ (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
+ (@{typ int}, K (SOME ("Int", [])), int_num)] #>
fold (SMT_Builtin.add_builtin_fun' smtlibC) [
(@{const True}, "true"),
(@{const False}, "false"),
@@ -90,9 +96,11 @@
fun var i = "?v" ^ string_of_int i
-fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
- | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
- | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
+fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
+ | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
+ SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
+ | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
+ | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
| tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
let
@@ -157,13 +165,15 @@
(* interface *)
-fun translate_config ctxt = {
+fun translate_config order ctxt = {
+ order = order,
logic = choose_logic ctxt,
fp_kinds = [],
serialize = serialize}
val _ = Theory.setup (Context.theory_map
(setup_builtins #>
- SMT_Translate.add_config (smtlibC, translate_config)))
+ SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
+ SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
end;
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Aug 30 20:50:45 2017 +0200
@@ -24,15 +24,19 @@
structure Z3_Interface: Z3_INTERFACE =
struct
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
+val z3C = ["z3"]
+
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
(* interface *)
local
fun translate_config ctxt =
- {logic = K "", fp_kinds = [BNF_Util.Least_FP],
- serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+ {order = SMT_Util.First_Order,
+ logic = K "",
+ fp_kinds = [BNF_Util.Least_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
fun is_div_mod @{const divide (int)} = true
| is_div_mod @{const modulo (int)} = true
--- a/src/HOL/Word/Tools/smt_word.ML Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML Wed Aug 30 20:50:45 2017 +0200
@@ -28,7 +28,8 @@
fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
- fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T)
+ fun word_typ (Type (@{type_name word}, [T])) =
+ Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
| word_typ _ = NONE
fun word_num (Type (@{type_name word}, [T])) k =
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Aug 30 18:35:23 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Aug 30 20:50:45 2017 +0200
@@ -22,6 +22,7 @@
declare -a SOURCES_BASE=(
"src-base/isabelle_encoding.scala"
"src-base/plugin.scala"
+ "src-base/syntax_style.scala"
)
declare -a RESOURCES_BASE=(
--- a/src/Tools/jEdit/src-base/plugin.scala Wed Aug 30 18:35:23 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala Wed Aug 30 20:50:45 2017 +0200
@@ -10,6 +10,7 @@
import isabelle._
import org.gjt.sp.jedit.EBPlugin
+import org.gjt.sp.util.SyntaxUtilities
class Plugin extends EBPlugin
@@ -17,5 +18,7 @@
override def start()
{
Isabelle_System.init()
+
+ SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/syntax_style.scala Wed Aug 30 20:50:45 2017 +0200
@@ -0,0 +1,32 @@
+/* Title: Tools/jEdit/src-base/syntax_style.scala
+ Author: Makarius
+
+Extended syntax styles: dummy version.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+
+
+object Syntax_Style
+{
+ private val plain_range: Int = JEditToken.ID_COUNT
+ private val full_range = 6 * plain_range + 1
+
+ object Dummy_Extender extends SyntaxUtilities.StyleExtender
+ {
+ override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+ {
+ val new_styles = new Array[SyntaxStyle](full_range)
+ for (i <- 0 until full_range) {
+ new_styles(i) = styles(i % plain_range)
+ }
+ new_styles
+ }
+ }
+}