--- a/NEWS Fri Aug 26 23:02:00 2011 +0200
+++ b/NEWS Sat Aug 27 09:02:25 2011 +0200
@@ -200,6 +200,39 @@
tendsto_vector ~> vec_tendstoI
Cauchy_vector ~> vec_CauchyI
+* Session Multivariate_Analysis: Several duplicate theorems have been
+removed, and other theorems have been renamed. INCOMPATIBILITY.
+
+ eventually_conjI ~> eventually_conj
+ eventually_and ~> eventually_conj_iff
+ eventually_false ~> eventually_False
+ setsum_norm ~> norm_setsum
+ Lim_ident_at ~> LIM_ident
+ Lim_const ~> tendsto_const
+ Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
+ Lim_neg ~> tendsto_minus
+ Lim_add ~> tendsto_add
+ Lim_sub ~> tendsto_diff
+ Lim_mul ~> tendsto_scaleR
+ Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
+ Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
+ Lim_linear ~> bounded_linear.tendsto
+ Lim_component ~> tendsto_euclidean_component
+ Lim_component_cart ~> tendsto_vec_nth
+ Lim_inner ~> tendsto_inner [OF tendsto_const]
+ dot_lsum ~> inner_setsum_left
+ dot_rsum ~> inner_setsum_right
+ continuous_on_neg ~> continuous_on_minus
+ continuous_on_sub ~> continuous_on_diff
+ continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]
+ continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]
+ continuous_on_mul ~> continuous_on_scaleR
+ continuous_on_mul_real ~> continuous_on_mult
+ continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
+ subset_interior ~> interior_mono
+ subset_closure ~> closure_mono
+ closure_univ ~> closure_UNIV
+
* Complex_Main: The locale interpretations for the bounded_linear and
bounded_bilinear locales have been removed, in order to reduce the
number of duplicate lemmas. Users must use the original names for
@@ -213,6 +246,16 @@
mult_right.setsum ~> setsum_right_distrib
mult_left.diff ~> left_diff_distrib
+* Complex_Main: Several redundant theorems about real numbers have
+been removed or generalized and renamed. INCOMPATIBILITY.
+
+ real_0_le_divide_iff ~> zero_le_divide_iff
+ realpow_two_disj ~> power2_eq_iff
+ real_squared_diff_one_factored ~> square_diff_one_factored
+ realpow_two_diff ~> square_diff_square_factored
+ exp_ln_eq ~> ln_unique
+ lemma_DERIV_subst ~> DERIV_cong
+
*** Document preparation ***
--- a/src/HOL/Algebra/Congruence.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Algebra/Congruence.thy Sat Aug 27 09:02:25 2011 +0200
@@ -29,15 +29,15 @@
where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
definition
- eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
+ eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index>")
where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
definition
- eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
+ eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index>")
where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
definition
- eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
+ eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index>")
where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
abbreviation
--- a/src/HOL/Algebra/Group.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Algebra/Group.thy Sat Aug 27 09:02:25 2011 +0200
@@ -154,7 +154,7 @@
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
by (simp add: m_assoc Units_closed del: Units_l_inv)
- with G show "y = z" by (simp add: Units_l_inv)
+ with G show "y = z" by simp
next
assume eq: "y = z"
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
@@ -332,7 +332,7 @@
proof -
assume x: "x \<in> carrier G"
then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
- by (simp add: m_assoc [symmetric] l_inv)
+ by (simp add: m_assoc [symmetric])
with x show ?thesis by (simp del: r_one)
qed
@@ -372,7 +372,7 @@
proof -
assume G: "x \<in> carrier G" "y \<in> carrier G"
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
- by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
+ by (simp add: m_assoc) (simp add: m_assoc [symmetric])
with G show ?thesis by (simp del: l_inv Units_l_inv)
qed
@@ -446,7 +446,7 @@
lemma (in group) one_in_subset:
"[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
==> \<one> \<in> H"
-by (force simp add: l_inv)
+by force
text {* A characterization of subgroups: closed, non-empty subset. *}
--- a/src/HOL/Algebra/Lattice.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Algebra/Lattice.thy Sat Aug 27 09:02:25 2011 +0200
@@ -34,7 +34,8 @@
subsubsection {* The order relation *}
-context weak_partial_order begin
+context weak_partial_order
+begin
lemma le_cong_l [intro, trans]:
"\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
@@ -85,7 +86,7 @@
and yy': "y .= y'"
and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
shows "x \<sqsubset> y'"
- using assms unfolding lless_def by (auto intro: trans sym)
+ using assms unfolding lless_def by (auto intro: trans sym) (*slow*)
lemma (in weak_partial_order) lless_antisym:
@@ -574,8 +575,7 @@
proof (cases "A = {}")
case True
with insert show ?thesis
- by simp (simp add: least_cong [OF weak_sup_of_singleton]
- sup_of_singleton_closed sup_of_singletonI)
+ by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
(* The above step is hairy; least_cong can make simp loop.
Would want special version of simp to apply least_cong. *)
next
@@ -1282,7 +1282,7 @@
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
- proof qed auto
+ by default auto
next
fix B
assume B: "B \<subseteq> carrier ?L"
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Aug 27 09:02:25 2011 +0200
@@ -436,10 +436,10 @@
apply(rule TrueI)+
--{* Parallel *}
apply(simp add: SEM_def sem_def)
- apply clarify
+ apply(clarify, rename_tac x y i Ts')
apply(frule Parallel_length_post_PStar)
apply clarify
- apply(drule_tac j=xb in Parallel_Strong_Soundness)
+ apply(drule_tac j=i in Parallel_Strong_Soundness)
apply clarify
apply simp
apply force
--- a/src/HOL/IsaMakefile Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/IsaMakefile Sat Aug 27 09:02:25 2011 +0200
@@ -1175,6 +1175,7 @@
Multivariate_Analysis/L2_Norm.thy \
Multivariate_Analysis/Linear_Algebra.thy \
Multivariate_Analysis/Multivariate_Analysis.thy \
+ Multivariate_Analysis/Norm_Arith.thy \
Multivariate_Analysis/Operator_Norm.thy \
Multivariate_Analysis/Path_Connected.thy \
Multivariate_Analysis/ROOT.ML \
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Sat Aug 27 09:02:25 2011 +0200
@@ -2391,8 +2391,6 @@
shows "limsup X \<le> limsup Y"
using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-declare trivial_limit_sequentially[simp]
-
lemma
fixes X :: "nat \<Rightarrow> ereal"
shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
--- a/src/HOL/Lim.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Lim.thy Sat Aug 27 09:02:25 2011 +0200
@@ -444,46 +444,51 @@
subsection {* Relation of LIM and LIMSEQ *}
+lemma sequentially_imp_eventually_within:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a within s)"
+proof (rule ccontr)
+ let ?I = "\<lambda>n. inverse (real (Suc n))"
+ def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
+ assume "\<not> eventually P (at a within s)"
+ hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
+ unfolding Limits.eventually_within Limits.eventually_at by fast
+ hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
+ hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
+ unfolding F_def by (rule someI_ex)
+ hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
+ and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
+ by fast+
+ from LIMSEQ_inverse_real_of_nat have "F ----> a"
+ by (rule metric_tendsto_imp_tendsto,
+ simp add: dist_norm F2 less_imp_le)
+ hence "eventually (\<lambda>n. P (F n)) sequentially"
+ using assms F0 F1 by simp
+ thus "False" by (simp add: F3)
+qed
+
+lemma sequentially_imp_eventually_at:
+ fixes a :: "'a::metric_space"
+ assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
+ eventually (\<lambda>n. P (f n)) sequentially"
+ shows "eventually P (at a)"
+ using assms sequentially_imp_eventually_within [where s=UNIV]
+ unfolding within_UNIV by simp
+
lemma LIMSEQ_SEQ_conv1:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
assumes f: "f -- a --> l"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
using tendsto_compose_eventually [OF f, where F=sequentially] by simp
-lemma LIMSEQ_SEQ_conv2_lemma:
- fixes a :: "'a::metric_space"
- assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
- shows "eventually P (at a)"
-proof (rule ccontr)
- let ?I = "\<lambda>n. inverse (real (Suc n))"
- let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
- assume "\<not> eventually P (at a)"
- hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
- unfolding eventually_at by simp
- hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
- by (rule someI_ex)
- hence F1: "\<And>n. ?F n \<noteq> a"
- and F2: "\<And>n. dist (?F n) a < ?I n"
- and F3: "\<And>n. \<not> P (?F n)"
- by fast+
- have "?F ----> a"
- using LIMSEQ_inverse_real_of_nat
- by (rule metric_tendsto_imp_tendsto,
- simp add: dist_norm F2 [THEN less_imp_le])
- moreover have "\<forall>n. ?F n \<noteq> a"
- by (rule allI) (rule F1)
- ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
- using assms by simp
- thus "False" by (simp add: F3)
-qed
-
lemma LIMSEQ_SEQ_conv2:
fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
shows "f -- a --> l"
using assms unfolding tendsto_def [where l=l]
- by (simp add: LIMSEQ_SEQ_conv2_lemma)
+ by (simp add: sequentially_imp_eventually_at)
lemma LIMSEQ_SEQ_conv:
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
--- a/src/HOL/List.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/List.thy Sat Aug 27 09:02:25 2011 +0200
@@ -4703,7 +4703,7 @@
qed
-text{* Accessible part of @{term listrel1} relations: *}
+text{* Accessible part and wellfoundedness: *}
lemma Cons_acc_listrel1I [intro!]:
"x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
@@ -4729,6 +4729,9 @@
apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
done
+lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
+by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
+
subsubsection {* Lifting Relations to Lists: all elements *}
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200
@@ -792,7 +792,7 @@
have "subspace ?P"
by (auto simp add: subspace_def)
ultimately show ?thesis
- using x span_induct[of ?B ?P x] iS by blast
+ using x span_induct[of x ?B ?P] iS by blast
qed
lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
@@ -2001,8 +2001,4 @@
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200
@@ -229,12 +229,18 @@
from g(1) gS giS gBC show ?thesis by blast
qed
+lemma closure_bounded_linear_image:
+ assumes f: "bounded_linear f"
+ shows "f ` (closure S) \<subseteq> closure (f ` S)"
+ using linear_continuous_on [OF f] closed_closure closure_subset
+ by (rule image_closure_subset)
+
lemma closure_linear_image:
fixes f :: "('m::euclidean_space) => ('n::real_normed_vector)"
assumes "linear f"
shows "f ` (closure S) <= closure (f ` S)"
-using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f]
-linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
+ using assms unfolding linear_conv_bounded_linear
+ by (rule closure_bounded_linear_image)
lemma closure_injective_linear_image:
fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
@@ -254,23 +260,16 @@
shows "closure (S <*> T) = closure S <*> closure T"
by (rule closure_Times)
-lemma closure_scaleR: (* TODO: generalize to real_normed_vector *)
-fixes S :: "('n::euclidean_space) set"
-shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
-proof-
-{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
- linear_scaleR injective_scaleR by auto
-}
-moreover
-{ assume zero: "c=0 & S ~= {}"
- hence "closure S ~= {}" using closure_subset by auto
- hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
- moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
- ultimately have ?thesis using zero by auto
-}
-moreover
-{ assume "S={}" hence ?thesis by auto }
-ultimately show ?thesis by blast
+lemma closure_scaleR:
+ fixes S :: "('a::real_normed_vector) set"
+ shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+proof
+ show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
+ using bounded_linear_scaleR_right
+ by (rule closure_bounded_linear_image)
+ show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
+ by (intro closure_minimal image_mono closure_subset
+ closed_scaling closed_closure)
qed
lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
@@ -859,9 +858,8 @@
qed
lemma cone_closure:
-fixes S :: "('m::euclidean_space) set"
-assumes "cone S"
-shows "cone (closure S)"
+ fixes S :: "('a::real_normed_vector) set"
+ assumes "cone S" shows "cone (closure S)"
proof-
{ assume "S = {}" hence ?thesis by auto }
moreover
@@ -2310,12 +2308,7 @@
lemma closure_affine_hull:
fixes S :: "('n::euclidean_space) set"
shows "closure S <= affine hull S"
-proof-
-have "closure S <= closure (affine hull S)" using subset_closure by auto
-moreover have "closure (affine hull S) = affine hull S"
- using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
-ultimately show ?thesis by auto
-qed
+ by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
lemma closure_same_affine_hull:
fixes S :: "('n::euclidean_space) set"
@@ -2580,6 +2573,37 @@
done
qed
+lemma finite_imp_compact_convex_hull:
+ fixes s :: "('a::real_normed_vector) set"
+ assumes "finite s" shows "compact (convex hull s)"
+proof (cases "s = {}")
+ case True thus ?thesis by simp
+next
+ case False with assms show ?thesis
+ proof (induct rule: finite_ne_induct)
+ case (singleton x) show ?case by simp
+ next
+ case (insert x A)
+ let ?f = "\<lambda>(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y"
+ let ?T = "{0..1::real} \<times> (convex hull A)"
+ have "continuous_on ?T ?f"
+ unfolding split_def continuous_on by (intro ballI tendsto_intros)
+ moreover have "compact ?T"
+ by (intro compact_Times compact_interval insert)
+ ultimately have "compact (?f ` ?T)"
+ by (rule compact_continuous_image)
+ also have "?f ` ?T = convex hull (insert x A)"
+ unfolding convex_hull_insert [OF `A \<noteq> {}`]
+ apply safe
+ apply (rule_tac x=a in exI, simp)
+ apply (rule_tac x="1 - a" in exI, simp)
+ apply fast
+ apply (rule_tac x="(u, b)" in image_eqI, simp_all)
+ done
+ finally show "compact (convex hull (insert x A))" .
+ qed
+qed
+
lemma compact_convex_hull: fixes s::"('a::euclidean_space) set"
assumes "compact s" shows "compact(convex hull s)"
proof(cases "s={}")
@@ -2654,11 +2678,6 @@
qed
qed
-lemma finite_imp_compact_convex_hull:
- fixes s :: "('a::euclidean_space) set"
- shows "finite s \<Longrightarrow> compact(convex hull s)"
-by (metis compact_convex_hull finite_imp_compact)
-
subsection {* Extremal points of a simplex are some vertices. *}
lemma dist_increases_online:
@@ -2738,7 +2757,7 @@
qed (auto simp add: assms)
lemma simplex_furthest_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
proof-
@@ -2754,12 +2773,12 @@
qed
lemma simplex_furthest_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
using simplex_furthest_le[of s] by (cases "s={}")auto
lemma simplex_extremal_le:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
proof-
@@ -2780,7 +2799,7 @@
qed
lemma simplex_extremal_le_exists:
- fixes s :: "('a::euclidean_space) set"
+ fixes s :: "('a::real_inner) set"
shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
\<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
@@ -3094,7 +3113,6 @@
subsection {* Convexity of cone hulls *}
lemma convex_cone_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "convex S"
shows "convex (cone hull S)"
proof-
@@ -3126,7 +3144,6 @@
qed
lemma cone_convex_hull:
-fixes S :: "('m::euclidean_space) set"
assumes "cone S"
shows "cone (convex hull S)"
proof-
@@ -3453,22 +3470,27 @@
ultimately show ?thesis using injpi by auto qed qed
qed auto qed
-lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set"
- assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
+lemma homeomorphic_convex_compact_lemma:
+ fixes s :: "('a::euclidean_space) set"
+ assumes "convex s" and "compact s" and "cball 0 1 \<subseteq> s"
shows "s homeomorphic (cball (0::'a) 1)"
- apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
- fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
- hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq
- apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball)
- unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
- fix y assume "dist (u *\<^sub>R x) y < 1 - u"
- hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
- using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
- unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
- apply (rule mult_left_le_imp_le[of "1 - u"])
- unfolding mult_assoc[symmetric] using `u<1` by auto
- thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
- using as unfolding scaleR_scaleR by auto qed auto
+proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
+ fix x u assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+ have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball)
+ moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
+ unfolding centre_in_ball using `u < 1` by simp
+ moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+ proof
+ fix y assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
+ hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball .
+ with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
+ by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
+ with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
+ with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
+ using `x \<in> s` `0 \<le> u` `u < 1` [THEN less_imp_le] by (rule mem_convex)
+ thus "y \<in> s" using `u < 1` by simp
+ qed
+ ultimately have "u *\<^sub>R x \<in> interior s" ..
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set"
@@ -3621,8 +3643,8 @@
assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$$k \<le> y" "y \<le> (f a)$$k"
shows "\<exists>x\<in>{a..b}. (f x)$$k = y"
apply(subst neg_equal_iff_equal[THEN sym])
- using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"] using assms using continuous_on_neg
- by auto
+ using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
+ using assms using continuous_on_minus by auto
lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> 'a::euclidean_space"
shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -4042,7 +4064,7 @@
then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
- have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
+ have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
by(auto simp add:field_simps norm_minus_commute)
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
@@ -4380,7 +4402,7 @@
shows "closure(rel_interior S) = closure S"
proof-
have h1: "closure(rel_interior S) <= closure S"
- using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
+ using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
{ assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S"
using rel_interior_convex_nonempty assms by auto
{ fix x assume x_def: "x : closure S"
@@ -4517,7 +4539,7 @@
proof-
have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
moreover have "?B --> (closure S1 <= closure S2)"
- by (metis assms(1) convex_closure_rel_interior subset_closure)
+ by (metis assms(1) convex_closure_rel_interior closure_mono)
moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
ultimately show ?thesis by blast
qed
@@ -4777,7 +4799,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4790,7 +4812,7 @@
using convex_closure_rel_interior_inter assms by auto
moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)"
using rel_interior_inter_aux
- subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+ closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
ultimately show ?thesis using closure_inter[of I] by auto
qed
@@ -4886,7 +4908,7 @@
proof-
have *: "S Int closure T = S" using assms by auto
have "~(rel_interior S <= rel_frontier T)"
- using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
+ using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
@@ -4911,8 +4933,8 @@
also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto
also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto
finally have "closure (f ` S) = closure (f ` rel_interior S)"
- using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
- subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
+ using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure
+ closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"]
closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sat Aug 27 09:02:25 2011 +0200
@@ -785,7 +785,7 @@
have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
apply(rule rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"])
defer
- apply(rule continuous_on_intros assms(2) continuous_on_cmul[where 'b=real, unfolded real_scaleR_def])+
+ apply(rule continuous_on_intros assms(2))+
proof
fix x assume x:"x \<in> {a<..<b}"
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
@@ -869,7 +869,7 @@
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
by (auto simp add: algebra_simps)
hence 1:"continuous_on {0..1} (f \<circ> ?p)" apply-
- apply(rule continuous_on_intros continuous_on_vmul)+
+ apply(rule continuous_on_intros)+
unfolding continuous_on_eq_continuous_within
apply(rule,rule differentiable_imp_continuous_within)
unfolding differentiable_def apply(rule_tac x="f' xa" in exI)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200
@@ -149,7 +149,7 @@
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
proof -
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
- by (simp add: euclidean_component_diff)
+ by simp
then show "x = y"
unfolding euclidean_component_def euclidean_all_zero by simp
qed
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Sat Aug 27 09:02:25 2011 +0200
@@ -44,7 +44,7 @@
have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
- apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+ apply(rule continuous_on_scaleR) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sat Aug 27 09:02:25 2011 +0200
@@ -378,7 +378,7 @@
interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
\<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
- show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
+ show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
using division_ofD(5)[OF assms(1) k1(2) k2(2)]
using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
@@ -407,9 +407,9 @@
show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
{ fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
- { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
+ { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
using assms(3) by blast } moreover
- { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
+ { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
using assms(3) by blast} ultimately
show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
fix k assume k:"k \<in> p1 \<union> p2" show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
@@ -573,7 +573,7 @@
show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
- apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+ apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
unfolding division_of_def by(metis bounded_Union bounded_interval)
@@ -823,7 +823,7 @@
fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
- have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
+ have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
using p1(3) p2(3) using xk xk' by auto qed
@@ -842,7 +842,7 @@
show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
- using assms(3)[rule_format] subset_interior by blast
+ using assms(3)[rule_format] interior_mono by blast
show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
qed
@@ -1703,7 +1703,7 @@
by(rule le_less_trans[OF norm_le_l1])
hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
thus False unfolding mem_Collect_eq using e x k by auto
- qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
+ qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
thus "content b *\<^sub>R f a = 0" by auto
qed auto
also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
@@ -2563,7 +2563,7 @@
proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}" "{m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}"
have "({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
- note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
+ note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
thus "content ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[THEN sym] .
qed qed
@@ -3516,7 +3516,7 @@
proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
- have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
@@ -3528,7 +3528,7 @@
proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
- have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+ have "{?v <..< b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
moreover have " ((b + ?v)/2) \<in> {?v <..< b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
@@ -4390,7 +4390,7 @@
from this(2) guess u v apply-by(erule exE)+ note uv=this
have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
- note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+ note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
@@ -4403,7 +4403,7 @@
have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
using as unfolding r_def by auto
have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
- apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+ apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto
qed(insert qq, auto)
@@ -4462,6 +4462,61 @@
proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
+subsection {* Geometric progression *}
+
+text {* FIXME: Should one or more of these theorems be moved to @{file
+"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+
+lemma sum_gp_basic:
+ fixes x :: "'a::ring_1"
+ shows "(1 - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
+proof-
+ def y \<equiv> "1 - x"
+ have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
+ by (induct n, simp, simp add: algebra_simps)
+ thus ?thesis
+ unfolding y_def by simp
+qed
+
+lemma sum_gp_multiplied: assumes mn: "m <= n"
+ shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
+ (is "?lhs = ?rhs")
+proof-
+ let ?S = "{0..(n - m)}"
+ from mn have mn': "n - m \<ge> 0" by arith
+ let ?f = "op + m"
+ have i: "inj_on ?f ?S" unfolding inj_on_def by auto
+ have f: "?f ` ?S = {m..n}"
+ using mn apply (auto simp add: image_iff Bex_def) by arith
+ have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
+ by (rule ext, simp add: power_add power_mult)
+ from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
+ have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
+ then show ?thesis unfolding sum_gp_basic using mn
+ by (simp add: field_simps power_add[symmetric])
+qed
+
+lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
+ (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
+ else (x^ m - x^ (Suc n)) / (1 - x))"
+proof-
+ {assume nm: "n < m" hence ?thesis by simp}
+ moreover
+ {assume "\<not> n < m" hence nm: "m \<le> n" by arith
+ {assume x: "x = 1" hence ?thesis by simp}
+ moreover
+ {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
+ from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+ ultimately have ?thesis by metis
+ }
+ ultimately show ?thesis by metis
+qed
+
+lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
+ (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+ unfolding sum_gp[of x m "m + n"] power_Suc
+ by (simp add: field_simps power_add)
+
subsection {* monotone convergence (bounded interval first). *}
lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sat Aug 27 09:02:25 2011 +0200
@@ -8,11 +8,6 @@
imports
Euclidean_Space
"~~/src/HOL/Library/Infinite_Set"
- L2_Norm
- "~~/src/HOL/Library/Convex"
- "~~/src/HOL/Library/Sum_of_Squares"
-uses
- ("normarith.ML")
begin
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -66,7 +61,7 @@
*)
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
- by (simp add: setL2_def power2_eq_square)
+ by (simp add: power2_eq_square)
lemma norm_cauchy_schwarz:
shows "inner x y <= norm x * norm y"
@@ -154,111 +149,6 @@
then show "x = y" by (simp)
qed
-subsection{* General linear decision procedure for normed spaces. *}
-
-lemma norm_cmul_rule_thm:
- fixes x :: "'a::real_normed_vector"
- shows "b >= norm(x) ==> \<bar>c\<bar> * b >= 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 *)
-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"
- by (simp add: field_simps)
-
-lemma pth_1:
- fixes x :: "'a::real_normed_vector"
- shows "x == scaleR 1 x" by simp
-
-lemma pth_2:
- fixes x :: "'a::real_normed_vector"
- shows "x - y == x + -y" by (atomize (full)) simp
-
-lemma pth_3:
- fixes x :: "'a::real_normed_vector"
- shows "- x == 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
-
-lemma pth_5:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c (scaleR d x) == 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"
- 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
-
-lemma pth_8:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR c x + scaleR d x == 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)"
- by (simp_all add: algebra_simps)
-
-lemma pth_a:
- fixes x :: "'a::real_normed_vector"
- shows "scaleR 0 x + y == 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))"
- 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)"
- by (simp_all add: algebra_simps)
-
-lemma pth_d:
- fixes x :: "'a::real_normed_vector"
- shows "x + 0 == 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"
- by atomize auto
-
-lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == 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)"
- using norm_ge_zero[of "x - y"] by auto
-
-use "normarith.ML"
-
-method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "prove simple linear statements about vector norms"
-
-
-text{* Hence more metric properties. *}
-
lemma norm_triangle_half_r:
shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
@@ -274,16 +164,6 @@
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-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'"
- by norm
-
-lemma dist_triangle_add_half:
- fixes x x' y y' :: "'a::real_normed_vector"
- shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
- by norm
-
lemma setsum_clauses:
shows "setsum f {} = 0"
and "finite S \<Longrightarrow> setsum f (insert x S) =
@@ -311,12 +191,6 @@
apply (rule setsum_mono_zero_right[OF fT fST])
by (auto intro: setsum_0')
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
-lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
- apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
proof
assume "\<forall>x. x \<bullet> y = x \<bullet> z"
@@ -702,65 +576,6 @@
then show ?thesis by blast
qed
-subsection {* Geometric progression *}
-
-lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
- (is "?lhs = ?rhs")
-proof-
- {assume x1: "x = 1" hence ?thesis by simp}
- moreover
- {assume x1: "x\<noteq>1"
- hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
- from geometric_sum[OF x1, of "Suc n", unfolded x1']
- have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
- unfolding atLeastLessThanSuc_atLeastAtMost
- using x1' apply (auto simp only: field_simps)
- apply (simp add: field_simps)
- done
- then have ?thesis by (simp add: field_simps) }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_multiplied: assumes mn: "m <= n"
- shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
- (is "?lhs = ?rhs")
-proof-
- let ?S = "{0..(n - m)}"
- from mn have mn': "n - m \<ge> 0" by arith
- let ?f = "op + m"
- have i: "inj_on ?f ?S" unfolding inj_on_def by auto
- have f: "?f ` ?S = {m..n}"
- using mn apply (auto simp add: image_iff Bex_def) by arith
- have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
- by (rule ext, simp add: power_add power_mult)
- from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
- have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
- then show ?thesis unfolding sum_gp_basic using mn
- by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
- (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
- else (x^ m - x^ (Suc n)) / (1 - x))"
-proof-
- {assume nm: "n < m" hence ?thesis by simp}
- moreover
- {assume "\<not> n < m" hence nm: "m \<le> n" by arith
- {assume x: "x = 1" hence ?thesis by simp}
- moreover
- {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
- ultimately have ?thesis by metis
- }
- ultimately show ?thesis by metis
-qed
-
-lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- unfolding sum_gp[of x m "m + n"] power_Suc
- by (simp add: field_simps power_add)
-
-
subsection{* A bit of linear algebra. *}
definition (in real_vector)
@@ -807,6 +622,9 @@
apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
done
+lemma subspace_linear_vimage: "linear f \<Longrightarrow> subspace S \<Longrightarrow> subspace (f -` S)"
+ by (auto simp add: subspace_def linear_def linear_0[of f])
+
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
by (auto simp add: subspace_def linear_def linear_0[of f])
@@ -816,6 +634,11 @@
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
by (simp add: subspace_def)
+lemma subspace_Times: "\<lbrakk>subspace A; subspace B\<rbrakk> \<Longrightarrow> subspace (A \<times> B)"
+ unfolding subspace_def zero_prod_def by simp
+
+text {* Properties of span. *}
+
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
by (metis span_def hull_mono)
@@ -834,8 +657,16 @@
by (metis span_def hull_subset subset_eq)
(metis subspace_span subspace_def)+
-lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
- and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
+lemma span_unique:
+ "\<lbrakk>S \<subseteq> T; subspace T; \<And>T'. \<lbrakk>S \<subseteq> T'; subspace T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk> \<Longrightarrow> span S = T"
+ unfolding span_def by (rule hull_unique)
+
+lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
+ unfolding span_def by (rule hull_minimal)
+
+lemma (in real_vector) span_induct:
+ assumes x: "x \<in> span S" and P: "subspace P" and SP: "\<And>x. x \<in> S ==> x \<in> P"
+ shows "x \<in> P"
proof-
from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
@@ -967,105 +798,76 @@
text {* Mapping under linear image. *}
-lemma span_linear_image: assumes lf: "linear f"
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+ by auto (* TODO: move *)
+
+lemma span_linear_image:
+ assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
-proof-
- {fix x
- assume x: "x \<in> span (f ` S)"
- have "x \<in> f ` span S"
- apply (rule span_induct[where x=x and S = "f ` S"])
- apply (clarsimp simp add: image_iff)
- apply (frule span_superset)
- apply blast
- apply (rule subspace_linear_image[OF lf])
- apply (rule subspace_span)
- apply (rule x)
- done}
- moreover
- {fix x assume x: "x \<in> span S"
- have "x \<in> {x. f x \<in> span (f ` S)}"
- apply (rule span_induct[where S=S])
- apply simp
- apply (rule span_superset)
- apply simp
- apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
- apply (rule x)
- done
- hence "f x \<in> span (f ` S)" by simp
- }
- ultimately show ?thesis by blast
+proof (rule span_unique)
+ show "f ` S \<subseteq> f ` span S"
+ by (intro image_mono span_inc)
+ show "subspace (f ` span S)"
+ using lf subspace_span by (rule subspace_linear_image)
+next
+ fix T assume "f ` S \<subseteq> T" and "subspace T" thus "f ` span S \<subseteq> T"
+ unfolding image_subset_iff_subset_vimage
+ by (intro span_minimal subspace_linear_vimage lf)
+qed
+
+lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+proof (rule span_unique)
+ show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+ by safe (force intro: span_clauses)+
+next
+ have "linear (\<lambda>(a, b). a + b)"
+ by (simp add: linear_def scaleR_add_right)
+ moreover have "subspace (span A \<times> span B)"
+ by (intro subspace_Times subspace_span)
+ ultimately show "subspace ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
+ by (rule subspace_linear_image)
+next
+ fix T assume "A \<union> B \<subseteq> T" and "subspace T"
+ thus "(\<lambda>(a, b). a + b) ` (span A \<times> span B) \<subseteq> T"
+ by (auto intro!: subspace_add elim: span_induct)
qed
text {* The key breakdown property. *}
+lemma span_singleton: "span {x} = range (\<lambda>k. k *\<^sub>R x)"
+proof (rule span_unique)
+ show "{x} \<subseteq> range (\<lambda>k. k *\<^sub>R x)"
+ by (fast intro: scaleR_one [symmetric])
+ show "subspace (range (\<lambda>k. k *\<^sub>R x))"
+ unfolding subspace_def
+ by (auto intro: scaleR_add_left [symmetric])
+ fix T assume "{x} \<subseteq> T" and "subspace T" thus "range (\<lambda>k. k *\<^sub>R x) \<subseteq> T"
+ unfolding subspace_def by auto
+qed
+
+lemma span_insert:
+ "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+proof -
+ have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
+ unfolding span_union span_singleton
+ apply safe
+ apply (rule_tac x=k in exI, simp)
+ apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
+ apply simp
+ apply (rule right_minus)
+ done
+ thus ?thesis by simp
+qed
+
lemma span_breakdown:
assumes bS: "b \<in> S" and aS: "a \<in> span S"
- shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
-proof-
- {fix x assume xS: "x \<in> S"
- {assume ab: "x = b"
- then have "?P x"
- apply simp
- apply (rule exI[where x="1"], simp)
- by (rule span_0)}
- moreover
- {assume ab: "x \<noteq> b"
- then have "?P x" using xS
- apply -
- apply (rule exI[where x=0])
- apply (rule span_superset)
- by simp}
- ultimately have "x \<in> Collect ?P" by blast}
- moreover have "subspace (Collect ?P)"
- unfolding subspace_def
- apply auto
- apply (rule exI[where x=0])
- using span_0[of "S - {b}"]
- apply simp
- apply (rule_tac x="k + ka" in exI)
- apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
- apply (simp only: )
- apply (rule span_add)
- apply assumption+
- apply (simp add: algebra_simps)
- apply (rule_tac x= "c*k" in exI)
- apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
- apply (simp only: )
- apply (rule span_mul)
- apply assumption
- by (simp add: algebra_simps)
- ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
- thus "?P a" by simp
-qed
+ shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})"
+ using assms span_insert [of b "S - {b}"]
+ by (simp add: insert_absorb)
lemma span_breakdown_eq:
- "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
- {assume x: "x \<in> span (insert a S)"
- from x span_breakdown[of "a" "insert a S" "x"]
- have ?rhs apply clarsimp
- apply (rule_tac x= "k" in exI)
- apply (rule set_rev_mp[of _ "span (S - {a})" _])
- apply assumption
- apply (rule span_mono)
- apply blast
- done}
- moreover
- { fix k assume k: "x - k *\<^sub>R a \<in> span S"
- have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
- have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
- apply (rule span_add)
- apply (rule set_rev_mp[of _ "span S" _])
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- apply (rule span_superset)
- apply blast
- done
- then have ?lhs using eq by metis}
- ultimately show ?thesis by blast
-qed
+ "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)"
+ by (simp add: span_insert)
text {* Hence some "reversal" results. *}
@@ -1122,26 +924,16 @@
text {* Transitivity property. *}
+lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
+ unfolding span_def by (rule hull_redundant)
+
lemma span_trans:
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
shows "y \<in> span S"
-proof-
- from span_breakdown[of x "insert x S" y, OF insertI1 y]
- obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
- have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
- show ?thesis
- apply (subst eq)
- apply (rule span_add)
- apply (rule set_rev_mp)
- apply (rule k)
- apply (rule span_mono)
- apply blast
- apply (rule span_mul)
- by (rule x)
-qed
+ using assms by (simp only: span_redundant)
lemma span_insert_0[simp]: "span (insert 0 S) = span S"
- using span_mono[of S "insert 0 S"] by (auto intro: span_trans span_0)
+ by (simp only: span_redundant span_0)
text {* An explicit expansion is sometimes needed. *}
@@ -1273,43 +1065,6 @@
ultimately show ?thesis by blast
qed
-lemma Int_Un_cancel: "(A \<union> B) \<inter> A = A" "(A \<union> B) \<inter> B = B" by auto
-
-lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
-proof safe
- fix x assume "x \<in> span (A \<union> B)"
- then obtain S u where S: "finite S" "S \<subseteq> A \<union> B" and x: "x = (\<Sum>v\<in>S. u v *\<^sub>R v)"
- unfolding span_explicit by auto
-
- let ?Sa = "\<Sum>v\<in>S\<inter>A. u v *\<^sub>R v"
- let ?Sb = "(\<Sum>v\<in>S\<inter>(B - A). u v *\<^sub>R v)"
- show "x \<in> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
- proof
- show "x = (case (?Sa, ?Sb) of (a, b) \<Rightarrow> a + b)"
- unfolding x using S
- by (simp, subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
-
- from S have "?Sa \<in> span A" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> A"])
- moreover from S have "?Sb \<in> span B" unfolding span_explicit
- by (auto intro!: exI[of _ "S \<inter> (B - A)"])
- ultimately show "(?Sa, ?Sb) \<in> span A \<times> span B" by simp
- qed
-next
- fix a b assume "a \<in> span A" and "b \<in> span B"
- then obtain Sa ua Sb ub where span:
- "finite Sa" "Sa \<subseteq> A" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
- "finite Sb" "Sb \<subseteq> B" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
- unfolding span_explicit by auto
- let "?u v" = "(if v \<in> Sa then ua v else 0) + (if v \<in> Sb then ub v else 0)"
- from span have "finite (Sa \<union> Sb)" "Sa \<union> Sb \<subseteq> A \<union> B"
- and "a + b = (\<Sum>v\<in>(Sa\<union>Sb). ?u v *\<^sub>R v)"
- unfolding setsum_addf scaleR_left_distrib
- by (auto simp add: if_distrib cond_application_beta setsum_cases Int_Un_cancel)
- thus "a + b \<in> span (A \<union> B)"
- unfolding span_explicit by (auto intro!: exI[of _ ?u])
-qed
-
text {* This is useful for building a basis step-by-step. *}
lemma independent_insert:
@@ -1495,30 +1250,6 @@
apply (simp add: inner_setsum_right dot_basis)
done
-lemma dimensionI:
- assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
- independent (basis ` {..<d} :: 'a set);
- inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
- shows "P DIM('a::euclidean_space)"
- using DIM_positive basis_finite independent_basis basis_inj
- by (rule assms)
-
-lemma (in euclidean_space) dimension_eq:
- assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
- assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
- shows "DIM('a) = d"
-proof (rule linorder_cases [of "DIM('a)" d])
- assume "DIM('a) < d"
- hence "basis DIM('a) \<noteq> 0" by (rule assms)
- thus ?thesis by simp
-next
- assume "d < DIM('a)"
- hence "basis d \<noteq> 0" by simp
- thus ?thesis by (simp add: assms)
-next
- assume "DIM('a) = d" thus ?thesis .
-qed
-
lemma (in euclidean_space) range_basis:
"range basis = insert 0 (basis ` {..<DIM('a)})"
proof -
@@ -1628,22 +1359,6 @@
ultimately show ?thesis by metis
qed
-subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
-
-class ordered_euclidean_space = ord + euclidean_space +
- assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
- and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
-
-lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
- unfolding eucl_less[where 'a='a] by auto
-
-lemma euclidean_trans[trans]:
- fixes x y z :: "'a::ordered_euclidean_space"
- shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
- and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
-
subsection {* Linearity and Bilinearity continued *}
lemma linear_bounded:
@@ -2035,8 +1750,15 @@
lemma vector_sub_project_orthogonal: "(b::'a::euclidean_space) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *\<^sub>R b) = 0"
unfolding inner_simps by auto
+lemma pairwise_orthogonal_insert:
+ assumes "pairwise orthogonal S"
+ assumes "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
+ shows "pairwise orthogonal (insert x S)"
+ using assms unfolding pairwise_def
+ by (auto simp add: orthogonal_commute)
+
lemma basis_orthogonal:
- fixes B :: "('a::euclidean_space) set"
+ fixes B :: "('a::real_inner) set"
assumes fB: "finite B"
shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
(is " \<exists>C. ?P B C")
@@ -2064,48 +1786,20 @@
by (rule span_superset)}
then have SC: "span ?C = span (insert a B)"
unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
- thm pairwise_def
- {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
- {assume xa: "x = ?a" and ya: "y = ?a"
- have "orthogonal x y" using xa ya xy by blast}
- moreover
- {assume xa: "x = ?a" and ya: "y \<noteq> ?a" "y \<in> C"
- from ya have Cy: "C = insert y (C - {y})" by blast
- have fth: "finite (C - {y})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cy)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<noteq> ?a" "x \<in> C" and ya: "y = ?a"
- from xa have Cx: "C = insert x (C - {x})" by blast
- have fth: "finite (C - {x})" using C by simp
- have "orthogonal x y"
- using xa ya
- unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
- apply simp
- apply (subst Cx)
- using C(1) fth
- apply (simp only: setsum_clauses)
- apply (subst inner_commute[of x])
- apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
- apply (rule setsum_0')
- apply clarsimp
- apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
- by auto}
- moreover
- {assume xa: "x \<in> C" and ya: "y \<in> C"
- have "orthogonal x y" using xa ya xy C(4) unfolding pairwise_def by blast}
- ultimately have "orthogonal x y" using xC yC by blast}
- then have CPO: "pairwise orthogonal ?C" unfolding pairwise_def by blast
+ { fix y assume yC: "y \<in> C"
+ hence Cy: "C = insert y (C - {y})" by blast
+ have fth: "finite (C - {y})" using C by simp
+ have "orthogonal ?a y"
+ unfolding orthogonal_def
+ unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
+ unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
+ apply (clarsimp simp add: inner_commute[of y a])
+ apply (rule setsum_0')
+ apply clarsimp
+ apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
+ using `y \<in> C` by auto }
+ with `pairwise orthogonal C` have CPO: "pairwise orthogonal ?C"
+ by (rule pairwise_orthogonal_insert)
from fC cC SC CPO have "?P (insert a B) ?C" by blast
then show ?case by blast
qed
@@ -2166,7 +1860,7 @@
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
apply simp unfolding inner_simps
- apply (clarsimp simp add: inner_add dot_lsum)
+ apply (clarsimp simp add: inner_add inner_setsum_left)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
@@ -3017,7 +2711,23 @@
apply simp
done
-subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
+subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
+
+class ordered_euclidean_space = ord + euclidean_space +
+ assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
+ and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
+
+lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
+ unfolding eucl_less[where 'a='a] by auto
+
+lemma euclidean_trans[trans]:
+ fixes x y z :: "'a::ordered_euclidean_space"
+ shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+ and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+ unfolding eucl_less[where 'a='a] eucl_le[where 'a='a]
+ by (fast intro: less_trans, fast intro: le_less_trans,
+ fast intro: order_trans)
lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
@@ -3036,8 +2746,6 @@
shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
unfolding basis_complex_def by auto
-subsection {* Products Spaces *}
-
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
(* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
unfolding dimension_prod_def by (rule add_commute)
@@ -3051,5 +2759,4 @@
instance proof qed (auto simp: less_prod_def less_eq_prod_def)
end
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Sat Aug 27 09:02:25 2011 +0200
@@ -0,0 +1,124 @@
+(* Title: HOL/Multivariate_Analysis/Norm_Arith.thy
+ Author: Amine Chaieb, University of Cambridge
+*)
+
+header {* General linear decision procedure for normed spaces *}
+
+theory Norm_Arith
+imports "~~/src/HOL/Library/Sum_of_Squares"
+uses ("normarith.ML")
+begin
+
+lemma norm_cmul_rule_thm:
+ fixes x :: "'a::real_normed_vector"
+ shows "b >= norm(x) ==> \<bar>c\<bar> * b >= 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 *)
+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"
+ by (simp add: field_simps)
+
+lemma pth_1:
+ fixes x :: "'a::real_normed_vector"
+ shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+ fixes x :: "'a::real_normed_vector"
+ shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+ fixes x :: "'a::real_normed_vector"
+ shows "- x == 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
+
+lemma pth_5:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c (scaleR d x) == 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"
+ 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
+
+lemma pth_8:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR c x + scaleR d x == 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)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_a:
+ fixes x :: "'a::real_normed_vector"
+ shows "scaleR 0 x + y == 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))"
+ 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)"
+ by (simp_all add: algebra_simps)
+
+lemma pth_d:
+ fixes x :: "'a::real_normed_vector"
+ shows "x + 0 == 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"
+ by atomize auto
+
+lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == 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)"
+ using norm_ge_zero[of "x - y"] by auto
+
+use "normarith.ML"
+
+method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
+*} "prove simple linear statements about vector norms"
+
+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'"
+ by norm
+
+lemma dist_triangle_add_half:
+ fixes x x' y y' :: "'a::real_normed_vector"
+ shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+ by norm
+
+end
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Sat Aug 27 09:02:25 2011 +0200
@@ -92,7 +92,7 @@
lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
have *:"\<And>g. path g \<Longrightarrow> path(reversepath g)" unfolding path_def reversepath_def
apply(rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1 - x"])
- apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id)
+ apply(intro continuous_on_intros)
apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto
show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed
@@ -108,8 +108,9 @@
by auto
thus "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" apply -apply rule
apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose)
- apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer
- apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
+ apply (intro continuous_on_intros) defer
+ apply (intro continuous_on_intros)
+ apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3
apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption)
apply(rule) defer apply rule proof-
fix x assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
@@ -132,10 +133,10 @@
done
show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof-
show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer
- unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id)
+ unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next
show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer
- apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const)
+ apply(rule continuous_on_compose) apply (intro continuous_on_intros)
unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def]
by (auto simp add: mult_ac) qed qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Aug 27 09:02:25 2011 +0200
@@ -7,7 +7,7 @@
header {* Elementary topology in Euclidean space. *}
theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
begin
(* to be moved elsewhere *)
@@ -20,7 +20,7 @@
apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
apply(rule member_le_setL2) by auto
-subsection {* General notion of a topologies as values *}
+subsection {* General notion of a topology as a value *}
definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
@@ -555,37 +555,61 @@
subsection {* Interior of a Set *}
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+ assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+ shows "x \<in> interior S"
+ using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+ assumes "x \<in> interior S"
+ obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+ using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+ by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+ by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+ by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+ by (intro equalityI interior_subset interior_maximal subset_refl)
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
- apply (simp add: set_eq_iff interior_def)
- apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
- apply (simp add: interior_def)
- apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
- by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
- apply (simp add: interior_def)
- by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+ by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
by (metis interior_maximal interior_subset subset_trans)
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
- apply (rule equalityI, simp)
- apply (metis Int_lower1 Int_lower2 subset_interior)
- by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+ using open_empty by (rule interior_open)
+
+lemma interior_UNIV [simp]: "interior UNIV = UNIV"
+ using open_UNIV by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+ using open_interior by (rule interior_open)
+
+lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+ by (auto simp add: interior_def)
+
+lemma interior_unique:
+ assumes "T \<subseteq> S" and "open T"
+ assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+ shows "interior S = T"
+ by (intro equalityI assms interior_subset open_interior interior_maximal)
+
+lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+ by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
+ Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+ using open_contains_ball_eq [where S="interior S"]
+ by (simp add: open_subset_interior)
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
@@ -599,21 +623,20 @@
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S" and iT: "interior T = {}"
- shows "interior(S \<union> T) = interior S"
+ shows "interior (S \<union> T) = interior S"
proof
- show "interior S \<subseteq> interior (S\<union>T)"
- by (rule subset_interior, blast)
+ show "interior S \<subseteq> interior (S \<union> T)"
+ by (rule interior_mono, rule Un_upper1)
next
show "interior (S \<union> T) \<subseteq> interior S"
proof
fix x assume "x \<in> interior (S \<union> T)"
- then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
- unfolding interior_def by fast
+ then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
show "x \<in> interior S"
proof (rule ccontr)
assume "x \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
- unfolding interior_def set_eq_iff by fast
+ unfolding interior_def by fast
from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +651,16 @@
by (intro Sigma_mono interior_subset)
show "open (interior A \<times> interior B)"
by (intro open_Times open_interior)
- show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
- apply (simp add: open_prod_def, clarify)
- apply (drule (1) bspec, clarify, rename_tac C D)
- apply (simp add: interior_def, rule conjI)
- apply (rule_tac x=C in exI, clarsimp)
- apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
- apply (rule_tac x=D in exI, clarsimp)
- apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
- done
+ fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+ proof (safe)
+ fix x y assume "(x, y) \<in> T"
+ then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+ using `open T` unfolding open_prod_def by fast
+ hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+ using `T \<subseteq> A \<times> B` by auto
+ thus "x \<in> interior A" and "y \<in> interior B"
+ by (auto intro: interiorI)
+ qed
qed
@@ -644,119 +668,50 @@
definition "closure S = S \<union> {x | x. x islimpt S}"
+lemma interior_closure: "interior S = - (closure (- S))"
+ unfolding interior_def closure_def islimpt_def by auto
+
lemma closure_interior: "closure S = - interior (- S)"
-proof-
- { fix x
- have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs")
- proof
- let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
- assume "?lhs"
- hence *:"\<not> ?exT x"
- unfolding interior_def
- by simp
- { assume "\<not> ?rhs"
- hence False using *
- unfolding closure_def islimpt_def
- by blast
- }
- thus "?rhs"
- by blast
- next
- assume "?rhs" thus "?lhs"
- unfolding closure_def interior_def islimpt_def
- by blast
- qed
- }
- thus ?thesis
- by blast
-qed
-
-lemma interior_closure: "interior S = - (closure (- S))"
-proof-
- { fix x
- have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
- unfolding interior_def closure_def islimpt_def
- by auto
- }
- thus ?thesis
- by blast
-qed
+ unfolding interior_closure by simp
lemma closed_closure[simp, intro]: "closed (closure S)"
-proof-
- have "closed (- interior (-S))" by blast
- thus ?thesis using closure_interior[of S] by simp
-qed
+ unfolding closure_interior by (simp add: closed_Compl)
+
+lemma closure_subset: "S \<subseteq> closure S"
+ unfolding closure_def by simp
lemma closure_hull: "closure S = closed hull S"
-proof-
- have "S \<subseteq> closure S"
- unfolding closure_def
- by blast
- moreover
- have "closed (closure S)"
- using closed_closure[of S]
- by assumption
- moreover
- { fix t
- assume *:"S \<subseteq> t" "closed t"
- { fix x
- assume "x islimpt S"
- hence "x islimpt t" using *(1)
- using islimpt_subset[of x, of S, of t]
- by blast
- }
- with * have "closure S \<subseteq> t"
- unfolding closure_def
- using closed_limpt[of t]
- by auto
- }
- ultimately show ?thesis
- using hull_unique[of S, of "closure S", of closed]
- by simp
-qed
+ unfolding hull_def closure_interior interior_def by auto
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
- unfolding closure_hull
- using hull_eq[of closed, OF closed_Inter, of S]
- by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
- using closure_eq[of S]
- by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
- unfolding closure_hull
- using hull_hull[of closed S]
- by assumption
-
-lemma closure_subset: "S \<subseteq> closure S"
- unfolding closure_hull
- using hull_subset[of S closed]
- by assumption
-
-lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
- unfolding closure_hull
- using hull_mono[of S T closed]
- by assumption
-
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
- using hull_minimal[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
- using hull_unique[of S T closed]
- unfolding closure_hull
- by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
- using closed_empty closure_closed[of "{}"]
- by simp
-
-lemma closure_univ[simp]: "closure UNIV = UNIV"
- using closure_closed[of UNIV]
- by simp
+ unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+ unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
+ unfolding closure_hull by (rule hull_hull)
+
+lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
+ unfolding closure_hull by (rule hull_mono)
+
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
+ unfolding closure_hull by (rule hull_minimal)
+
+lemma closure_unique:
+ assumes "S \<subseteq> T" and "closed T"
+ assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+ shows "closure S = T"
+ using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
+ using closed_empty by (rule closure_closed)
+
+lemma closure_UNIV [simp]: "closure UNIV = UNIV"
+ using closed_UNIV by (rule closure_closed)
+
+lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
+ unfolding closure_interior by simp
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
using closure_empty closure_subset[of S]
@@ -797,26 +752,19 @@
by blast
qed
-lemma closure_complement: "closure(- S) = - interior(S)"
-proof-
- have "S = - (- S)"
- by auto
- thus ?thesis
- unfolding closure_interior
- by auto
-qed
-
-lemma interior_complement: "interior(- S) = - closure(S)"
- unfolding closure_interior
- by blast
+lemma closure_complement: "closure (- S) = - interior S"
+ unfolding closure_interior by simp
+
+lemma interior_complement: "interior (- S) = - closure S"
+ unfolding closure_interior by simp
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
show "A \<times> B \<subseteq> closure A \<times> closure B"
by (intro Sigma_mono closure_subset)
show "closed (closure A \<times> closure B)"
by (intro closed_Times closed_closure)
- show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+ fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
apply (simp add: closed_def open_prod_def, clarify)
apply (rule ccontr)
apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1090,8 +1038,7 @@
assumes "x \<in> interior S"
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
proof-
- from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
- unfolding interior_def by fast
+ from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2783,8 +2730,8 @@
fixes x :: "'a::t1_space"
shows "closure (insert x s) = insert x (closure s)"
apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
apply (simp add: closure_minimal)
done
@@ -3351,10 +3298,9 @@
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
-unfolding interior_def
-apply simp
-by (meson continuous_on_eq_continuous_at continuous_on_subset)
+ shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+ by (erule interiorE, drule (1) continuous_on_subset,
+ simp add: continuous_on_eq_continuous_at)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3363,56 +3309,41 @@
text {* Characterization of various kinds of continuity in terms of sequences. *}
-(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
lemma continuous_within_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a within s) f \<longleftrightarrow>
(\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (x n) a < e"
- fix e::real assume "e>0"
- from `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e" unfolding continuous_within Lim_within using `e>0` by auto
- from x(2) `d>0` obtain N where N:"\<forall>n\<ge>N. dist (x n) a < d" by auto
- hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
- apply(rule_tac x=N in exI) using N d apply auto using x(1)
- apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
- apply(erule_tac x="x n" in ballE) apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
+ { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
+ fix T::"'b set" assume "open T" and "f a \<in> T"
+ with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
+ unfolding continuous_within tendsto_def eventually_within by auto
+ have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
+ using x(2) `d>0` by simp
+ hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
+ proof (rule eventually_elim1)
+ fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
+ using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
+ qed
}
- thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
+ thus ?rhs unfolding tendsto_iff unfolding tendsto_def by simp
next
- assume ?rhs
- { fix e::real assume "e>0"
- assume "\<not> (\<exists>d>0. \<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) (f a) < e)"
- hence "\<forall>d. \<exists>x. d>0 \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)" by blast
- then obtain x where x:"\<forall>d>0. x d \<in> s \<and> (0 < dist (x d) a \<and> dist (x d) a < d \<and> \<not> dist (f (x d)) (f a) < e)"
- using choice[of "\<lambda>d x.0<d \<longrightarrow> x\<in>s \<and> (0 < dist x a \<and> dist x a < d \<and> \<not> dist (f x) (f a) < e)"] by auto
- { fix d::real assume "d>0"
- hence "\<exists>N::nat. inverse (real (N + 1)) < d" using real_arch_inv[of d] by (auto, rule_tac x="n - 1" in exI)auto
- then obtain N::nat where N:"inverse (real (N + 1)) < d" by auto
- { fix n::nat assume n:"n\<ge>N"
- hence "dist (x (inverse (real (n + 1)))) a < inverse (real (n + 1))" using x[THEN spec[where x="inverse (real (n + 1))"]] by auto
- moreover have "inverse (real (n + 1)) < d" using N n by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero)
- ultimately have "dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "\<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < d" by auto
- }
- hence "(\<forall>n::nat. x (inverse (real (n + 1))) \<in> s) \<and> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (x (inverse (real (n + 1)))) a < e)" using x by auto
- hence "\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist (f (x (inverse (real (n + 1))))) (f a) < e" using `?rhs`[THEN spec[where x="\<lambda>n::nat. x (inverse (real (n+1)))"], unfolded Lim_sequentially] by auto
- hence "False" apply(erule_tac x=e in allE) using `e>0` using x by auto
- }
- thus ?lhs unfolding continuous_within unfolding Lim_within unfolding Lim_sequentially by blast
+ assume ?rhs thus ?lhs
+ unfolding continuous_within tendsto_def [where l="f a"]
+ by (simp add: sequentially_imp_eventually_within)
qed
lemma continuous_at_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)"
- using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
+ using continuous_within_sequentially[of a UNIV f]
+ unfolding within_UNIV by auto
lemma continuous_on_sequentially:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
shows "continuous_on s f \<longleftrightarrow>
(\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3527,16 +3458,10 @@
text{* Same thing for setwise continuity. *}
-lemma continuous_on_const:
- "continuous_on s (\<lambda>x. c)"
+lemma continuous_on_const: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_cmul:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
- unfolding continuous_on_def by (auto intro: tendsto_intros)
-
-lemma continuous_on_neg:
+lemma continuous_on_minus:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
@@ -3547,12 +3472,46 @@
\<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
-lemma continuous_on_sub:
+lemma continuous_on_diff:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g
\<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
unfolding continuous_on_def by (auto intro: tendsto_intros)
+lemma (in bounded_linear) continuous_on:
+ "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) continuous_on:
+ "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
+ unfolding continuous_on_def by (fast intro: tendsto)
+
+lemma continuous_on_scaleR:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
+ using bounded_bilinear_scaleR assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_mult:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. f x * g x)"
+ using bounded_bilinear_mult assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_inner:
+ fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
+ assumes "continuous_on s f" and "continuous_on s g"
+ shows "continuous_on s (\<lambda>x. inner (f x) (g x))"
+ using bounded_bilinear_inner assms
+ by (rule bounded_bilinear.continuous_on)
+
+lemma continuous_on_euclidean_component:
+ "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $$ i)"
+ using bounded_linear_euclidean_component
+ by (rule bounded_linear.continuous_on)
+
text{* Same thing for uniform continuity, using sequential formulations. *}
lemma uniformly_continuous_on_const:
@@ -3796,13 +3755,20 @@
lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
- apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s"
- hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
- thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
- apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
- proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
- thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+ fix x assume "x \<in> interior (f ` s)"
+ then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+ hence "x \<in> f ` s" by auto
+ then obtain y where y: "y \<in> s" "x = f y" by auto
+ have "open (vimage f T)"
+ using assms(1) `open T` by (rule continuous_open_vimage)
+ moreover have "y \<in> vimage f T"
+ using `x = f y` `x \<in> T` by simp
+ moreover have "vimage f T \<subseteq> s"
+ using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+ ultimately have "y \<in> interior s" ..
+ with `x = f y` show "x \<in> f ` interior s" ..
+qed
text {* Equality of continuous functions on closure and related results. *}
@@ -3989,28 +3955,10 @@
lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul
continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-lemma continuous_on_vmul:
- fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
- shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
- unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
- fixes c :: "'a::metric_space \<Rightarrow> real"
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- shows "continuous_on s c \<Longrightarrow> continuous_on s f
- ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
- unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemma continuous_on_mul_real:
- fixes f :: "'a::metric_space \<Rightarrow> real"
- fixes g :: "'a::metric_space \<Rightarrow> real"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g
- ==> continuous_on s (\<lambda>x. f x * g x)"
- using continuous_on_mul[of s f g] unfolding real_scaleR_def .
-
lemmas continuous_on_intros = continuous_on_add continuous_on_const
- continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg
- continuous_on_sub continuous_on_mul continuous_on_vmul continuous_on_mul_real
+ continuous_on_id continuous_on_compose continuous_on_minus
+ continuous_on_diff continuous_on_scaleR continuous_on_mult
+ continuous_on_inner continuous_on_euclidean_component
uniformly_continuous_on_add uniformly_continuous_on_const
uniformly_continuous_on_id uniformly_continuous_on_compose
uniformly_continuous_on_cmul uniformly_continuous_on_neg
@@ -4870,13 +4818,15 @@
finally show "closed {a .. b}" .
qed
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+ fixes a b :: "'a::ordered_euclidean_space"
+ shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
- show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+ show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+ by (rule interior_maximal)
next
- { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
- then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+ { fix x assume "x \<in> interior {a..b}"
+ then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
{ fix i assume i:"i<DIM('a)"
have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4891,7 +4841,7 @@
hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
unfolding basis_component using `e>0` i by auto }
hence "x \<in> {a<..<b}" unfolding mem_interval by auto }
- thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+ thus "?L \<subseteq> ?R" ..
qed
lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"
@@ -5149,21 +5099,12 @@
finally show ?thesis .
qed
-lemma Lim_inner:
- assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
- by (intro tendsto_intros assms)
-
lemma continuous_at_inner: "continuous (at x) (inner a)"
unfolding continuous_at by (intro tendsto_intros)
lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x $$ i)"
unfolding euclidean_component_def by (rule continuous_at_inner)
-lemma continuous_on_inner:
- fixes s :: "'a::real_inner set"
- shows "continuous_on s (inner a)"
- unfolding continuous_on by (rule ballI) (intro tendsto_intros)
-
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
by (simp add: closed_Collect_le)
@@ -5440,8 +5381,7 @@
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
apply(rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
- using assms apply auto
- using continuous_on_cmul[OF continuous_on_id] by auto
+ using assms by (auto simp add: continuous_on_intros)
lemma homeomorphic_translation:
fixes s :: "'a::real_normed_vector set"
@@ -5763,15 +5703,13 @@
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
- apply(auto simp add: pth_3[symmetric]
- intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
+ apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
}
ultimately show ?thesis using False by auto
@@ -6040,19 +5978,4 @@
declare tendsto_const [intro] (* FIXME: move *)
-text {* Legacy theorem names *}
-
-lemmas Lim_ident_at = LIM_ident
-lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
-lemmas Lim_neg = tendsto_minus
-lemmas Lim_add = tendsto_add
-lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = tendsto_scaleR
-lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
-lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
-lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = tendsto_euclidean_component
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
end
--- a/src/HOL/Probability/Borel_Space.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Sat Aug 27 09:02:25 2011 +0200
@@ -11,7 +11,7 @@
section "Generic Borel spaces"
-definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = open\<rparr>"
+definition "borel = sigma \<lparr> space = UNIV::'a::topological_space set, sets = {S. open S}\<rparr>"
abbreviation "borel_measurable M \<equiv> measurable M borel"
interpretation borel: sigma_algebra borel
@@ -19,7 +19,7 @@
lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
- (\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = open\<rparr>).
+ (\<forall>S \<in> sets (sigma \<lparr> space = UNIV, sets = {S. open S}\<rparr>).
f -` S \<inter> space M \<in> sets M)"
by (auto simp add: measurable_def borel_def)
@@ -35,7 +35,7 @@
lemma borel_open[simp]:
assumes "open A" shows "A \<in> sets borel"
proof -
- have "A \<in> open" unfolding mem_def using assms .
+ have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
thus ?thesis unfolding borel_def sigma_def by (auto intro!: sigma_sets.Basic)
qed
@@ -71,8 +71,8 @@
shows "f \<in> borel_measurable M"
unfolding borel_def
proof (rule measurable_sigma, simp_all)
- fix S :: "'x set" assume "S \<in> open" thus "f -` S \<inter> space M \<in> sets M"
- using assms[of S] by (simp add: mem_def)
+ fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M"
+ using assms[of S] by simp
qed
lemma borel_singleton[simp, intro]:
@@ -391,7 +391,8 @@
proof -
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) simp
then interpret sigma_algebra ?SIGMA .
- { fix S :: "'a set" assume "S \<in> open" then have "open S" unfolding mem_def .
+ { fix S :: "'a set" assume "S \<in> {S. open S}"
+ then have "open S" unfolding mem_Collect_eq .
from open_UNION[OF this]
obtain I where *: "S =
(\<Union>(a, b)\<in>I.
@@ -647,8 +648,8 @@
proof -
have "sigma_algebra ?SIGMA" by (rule sigma_algebra_sigma) auto
then interpret sigma_algebra ?SIGMA .
- { fix M :: "'a set" assume "M \<in> open"
- then have "open M" by (simp add: mem_def)
+ { fix M :: "'a set" assume "M \<in> {S. open S}"
+ then have "open M" by simp
have "M \<in> sets ?SIGMA"
apply (subst open_UNION[OF `open M`])
apply (safe intro!: countable_UN)
@@ -784,7 +785,7 @@
"(\<lambda>x::'a::euclidean_space. x $$ i) \<in> borel_measurable borel"
unfolding borel_def[where 'a=real]
proof (rule borel.measurable_sigma, simp_all)
- fix S::"real set" assume "S \<in> open" then have "open S" unfolding mem_def .
+ fix S::"real set" assume "open S"
from open_vimage_euclidean_component[OF this]
show "(\<lambda>x. x $$ i) -` S \<in> sets borel"
by (auto intro: borel_open)
@@ -815,8 +816,8 @@
show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"
proof cases
assume "b \<noteq> 0"
- with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")
- by (auto intro!: open_affinity simp: scaleR_add_right mem_def)
+ with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
+ by (auto intro!: open_affinity simp: scaleR_add_right)
hence "?S \<in> sets borel"
unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)
moreover
@@ -1099,8 +1100,8 @@
"ereal \<in> borel_measurable borel"
unfolding borel_def[where 'a=ereal]
proof (rule borel.measurable_sigma)
- fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open \<rparr>"
- then have "open X" by (auto simp: mem_def)
+ fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>"
+ then have "open X" by simp
then have "open (ereal -` X \<inter> space borel)"
by (simp add: open_ereal_vimage)
then show "ereal -` X \<inter> space borel \<in> sets borel" by auto
@@ -1114,8 +1115,8 @@
"(real :: ereal \<Rightarrow> real) \<in> borel_measurable borel"
unfolding borel_def[where 'a=real]
proof (rule borel.measurable_sigma)
- fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = open \<rparr>"
- then have "open B" by (auto simp: mem_def)
+ fix B :: "real set" assume "B \<in> sets \<lparr>space = UNIV, sets = {S. open S} \<rparr>"
+ then have "open B" by simp
have *: "ereal -` real -` (B - {0}) = B - {0}" by auto
have open_real: "open (real -` (B - {0}) :: ereal set)"
unfolding open_ereal_def * using `open B` by auto
@@ -1190,8 +1191,8 @@
lemma (in sigma_algebra) borel_measurable_uminus_borel_ereal:
"(uminus :: ereal \<Rightarrow> ereal) \<in> borel_measurable borel"
proof (subst borel_def, rule borel.measurable_sigma)
- fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = open\<rparr>"
- then have "open X" by (simp add: mem_def)
+ fix X :: "ereal set" assume "X \<in> sets \<lparr>space = UNIV, sets = {S. open S}\<rparr>"
+ then have "open X" by simp
have "uminus -` X = uminus ` X" by (force simp: image_iff)
then have "open (uminus -` X)" using `open X` ereal_open_uminus by auto
then show "uminus -` X \<inter> space borel \<in> sets borel" by auto
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Sat Aug 27 09:02:25 2011 +0200
@@ -1136,7 +1136,6 @@
| Disj:
"range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
\<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
- monos Pow_mono
definition
@@ -1485,7 +1484,7 @@
using assms dynkin_system_trivial by fastsimp
ultimately show "A \<subseteq> space (dynkin M)"
unfolding dynkin_def using assms
- by simp (metis dynkin_system_def subset_class_def in_mono mem_def)
+ by simp (metis dynkin_system_def subset_class_def in_mono)
next
show "space (dynkin M) \<in> sets (dynkin M)"
unfolding dynkin_def using dynkin_system.space by fastsimp
--- a/src/HOL/Quotient_Examples/FSet.thy Fri Aug 26 23:02:00 2011 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Sat Aug 27 09:02:25 2011 +0200
@@ -196,7 +196,11 @@
lemma member_rsp [quot_respect]:
shows "(op \<approx> ===> op =) List.member List.member"
- by (auto intro!: fun_relI simp add: mem_def)
+proof
+ fix x y assume "x \<approx> y"
+ then show "List.member x = List.member y"
+ unfolding fun_eq_iff by simp
+qed
lemma nil_rsp [quot_respect]:
shows "(op \<approx>) Nil Nil"
--- a/src/Pure/General/linear_set.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/General/linear_set.ML Sat Aug 27 09:02:25 2011 +0200
@@ -14,12 +14,10 @@
val empty: 'a T
val is_empty: 'a T -> bool
val defined: 'a T -> key -> bool
- val lookup: 'a T -> key -> 'a option
+ val lookup: 'a T -> key -> ('a * key option) option
val update: key * 'a -> 'a T -> 'a T
- val fold: key option ->
- ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
- val get_first: key option ->
- ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+ val iterate: key option ->
+ ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
val get_after: 'a T -> key option -> key option
val insert_after: key option -> key * 'a -> 'a T -> 'a T
val delete_after: key option -> 'a T -> 'a T
@@ -70,7 +68,7 @@
fun defined set key = Table.defined (entries_of set) key;
-fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+fun lookup set key = Table.lookup (entries_of set) key;
fun update (key, x) = map_set (fn (start, entries) =>
(start, put_entry (key, (x, next_entry entries key)) entries));
@@ -81,7 +79,7 @@
fun optional_start set NONE = start_of set
| optional_start _ some = some;
-fun fold opt_start f set =
+fun iterate opt_start f set =
let
val entries = entries_of set;
fun apply _ NONE y = y
@@ -89,20 +87,13 @@
let
val (x, next) = the_entry entries key;
val item = ((prev, key), x);
- in apply (SOME key) next (f item y) end;
+ in
+ (case f item y of
+ NONE => y
+ | SOME y' => apply (SOME key) next y')
+ end;
in apply NONE (optional_start set opt_start) end;
-fun get_first opt_start P set =
- let
- val entries = entries_of set;
- fun first _ NONE = NONE
- | first prev (SOME key) =
- let
- val (x, next) = the_entry entries key;
- val item = ((prev, key), x);
- in if P item then SOME item else first (SOME key) next end;
- in first NONE (optional_start set opt_start) end;
-
(* relative addressing *)
--- a/src/Pure/General/markup.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/General/markup.ML Sat Aug 27 09:02:25 2011 +0200
@@ -108,9 +108,7 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val versionN: string
- val execN: string
val assignN: string val assign: int -> T
- val editN: string val edit: int * int -> T
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -353,12 +351,8 @@
(* interactive documents *)
val versionN = "version";
-val execN = "exec";
val (assignN, assign) = markup_int "assign" versionN;
-val editN = "edit";
-fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
-
(* messages *)
--- a/src/Pure/General/markup.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/General/markup.scala Sat Aug 27 09:02:25 2011 +0200
@@ -232,9 +232,7 @@
/* interactive documents */
val VERSION = "version"
- val EXEC = "exec"
val ASSIGN = "assign"
- val EDIT = "edit"
/* prover process */
--- a/src/Pure/Isar/outer_syntax.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sat Aug 27 09:02:25 2011 +0200
@@ -34,10 +34,10 @@
val process_file: Path.T -> theory -> theory
type isar
val isar: TextIO.instream -> bool -> isar
- val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
- val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+ val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
+ val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
(Toplevel.transition * Toplevel.transition list) list
- val prepare_command: Position.T -> string -> Toplevel.transition
+ val read_command: Position.T -> string -> Toplevel.transition
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -251,11 +251,11 @@
|> toplevel_source term (SOME true) lookup_commands_dynamic;
-(* prepare toplevel commands -- fail-safe *)
+(* read toplevel commands -- fail-safe *)
val not_singleton = "Exactly one command expected";
-fun prepare_span outer_syntax span =
+fun read_span outer_syntax span =
let
val commands = lookup_commands outer_syntax;
val range_pos = Position.set_range (Thy_Syntax.span_range span);
@@ -272,19 +272,19 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init {head, proof, proper_proof} =
let
- val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
- val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
+ val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
+ val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
in
if proper_head andalso proper_proof then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
-fun prepare_command pos str =
+fun read_command pos str =
let val (lexs, outer_syntax) = get_syntax () in
(case Thy_Syntax.parse_spans lexs pos str of
- [span] => #1 (prepare_span outer_syntax span)
+ [span] => #1 (read_span outer_syntax span)
| _ => Toplevel.malformed pos not_singleton)
end;
--- a/src/Pure/PIDE/command.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/command.scala Sat Aug 27 09:02:25 2011 +0200
@@ -88,14 +88,22 @@
/* perspective */
- type Perspective = List[Command] // visible commands in canonical order
+ object Perspective
+ {
+ val empty: Perspective = Perspective(Nil)
+ }
- def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+ sealed case class Perspective(commands: List[Command]) // visible commands in canonical order
{
- require(p1.forall(_.is_defined))
- require(p2.forall(_.is_defined))
- p1.length == p2.length &&
- (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ def same(that: Perspective): Boolean =
+ {
+ val cmds1 = this.commands
+ val cmds2 = that.commands
+ require(cmds1.forall(_.is_defined))
+ require(cmds2.forall(_.is_defined))
+ cmds1.length == cmds2.length &&
+ (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ }
}
}
--- a/src/Pure/PIDE/document.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 27 09:02:25 2011 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Document as collection of named nodes, each consisting of an editable
-list of commands, associated with asynchronous execution process.
+list of commands, with asynchronous read/eval/print processes.
*)
signature DOCUMENT =
@@ -28,7 +28,8 @@
val join_commands: state -> unit
val cancel_execution: state -> Future.task list
val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
- val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+ val update: version_id -> version_id -> edit list -> state ->
+ ((command_id * exec_id option) list * (string * command_id option) list) * state
val execute: version_id -> state -> state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -58,7 +59,7 @@
(** document structure **)
type node_header = (string * string list * (string * bool) list) Exn.result;
-type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
+type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
abstype node = Node of
@@ -66,58 +67,62 @@
header: node_header,
perspective: perspective,
entries: exec_id option Entries.T, (*command entries with excecutions*)
+ last_exec: command_id option, (*last command with exec state assignment*)
result: Toplevel.state lazy}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (touched, header, perspective, entries, result) =
+fun make_node (touched, header, perspective, entries, last_exec, result) =
Node {touched = touched, header = header, perspective = perspective,
- entries = entries, result = result};
+ entries = entries, last_exec = last_exec, result = result};
-fun map_node f (Node {touched, header, perspective, entries, result}) =
- make_node (f (touched, header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
+ make_node (f (touched, header, perspective, entries, last_exec, result));
-fun make_perspective ids : perspective =
- (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+fun make_perspective command_ids : perspective =
+ (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
+val no_header = Exn.Exn (ERROR "Bad theory header");
val no_perspective = make_perspective [];
val no_print = Lazy.value ();
val no_result = Lazy.value Toplevel.toplevel;
-val empty_node =
- make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
-
-val clear_node =
- map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
+val clear_node = map_node (fn (_, header, _, _, _, _) =>
+ (false, header, no_perspective, Entries.empty, NONE, no_result));
(* basic components *)
fun is_touched (Node {touched, ...}) = touched;
fun set_touched touched =
- map_node (fn (_, header, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (_, header, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (touched, _, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (touched, _, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
- map_node (fn (touched, header, _, entries, result) =>
- (touched, header, make_perspective ids, entries, result));
+ map_node (fn (touched, header, _, entries, last_exec, result) =>
+ (touched, header, make_perspective ids, entries, last_exec, result));
fun map_entries f =
- map_node (fn (touched, header, perspective, entries, result) =>
- (touched, header, perspective, f entries, result));
-fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
-fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
+ map_node (fn (touched, header, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, f entries, last_exec, result));
+fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
+
+fun get_last_exec (Node {last_exec, ...}) = last_exec;
+fun set_last_exec last_exec =
+ map_node (fn (touched, header, perspective, entries, _, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
fun set_result result =
- map_node (fn (touched, header, perspective, entries, _) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (touched, header, perspective, entries, last_exec, _) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -134,13 +139,26 @@
type edit = string * node_edit;
+fun after_entry (Node {entries, ...}) = Entries.get_after entries;
+
+fun lookup_entry (Node {entries, ...}) id =
+ (case Entries.lookup entries id of
+ NONE => NONE
+ | SOME (exec, _) => exec);
+
fun the_entry (Node {entries, ...}) id =
(case Entries.lookup entries id of
NONE => err_undef "command entry" id
- | SOME entry => entry);
+ | SOME (exec, _) => exec);
+
+fun the_default_entry node (SOME id) = the_default no_id (the_entry node id)
+ | the_default_entry _ NONE = no_id;
-fun update_entry (id, exec_id) =
- map_entries (Entries.update (id, SOME exec_id));
+fun update_entry id exec =
+ map_entries (Entries.update (id, exec));
+
+fun reset_entry id node =
+ if is_some (lookup_entry node id) then update_entry id NONE node else node;
fun reset_after id entries =
(case Entries.get_after entries id of
@@ -197,7 +215,9 @@
in Graph.map_node name (set_header header') nodes3 end
|> touch_node name
| Perspective perspective =>
- update_node name (set_perspective perspective) nodes);
+ nodes
+ |> update_node name (set_perspective perspective)
+ |> touch_node name (* FIXME more precise!?! *));
end;
@@ -254,7 +274,7 @@
val tr =
Future.fork_pri 2 (fn () =>
Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+ (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
val commands' =
Inttab.update_new (id, tr) commands
handle Inttab.DUP dup => err_dup "command" dup;
@@ -344,7 +364,7 @@
-(** editing **)
+(** update **)
(* perspective *)
@@ -356,14 +376,32 @@
in define_version new_id new_version state end;
-(* edit *)
+(* edits *)
local
-fun is_changed node' ((_, id), exec) =
- (case try (the_entry node') id of
- NONE => true
- | SOME exec' => exec' <> exec);
+fun last_common last_visible node0 node =
+ let
+ fun get_common ((prev, id), exec) (found, (result, visible)) =
+ if found then NONE
+ else
+ let val found' = is_none exec orelse exec <> lookup_entry node0 id
+ in SOME (found', (prev, visible andalso prev <> last_visible)) end;
+ in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
+
+fun new_exec state init command_id' (execs, exec) =
+ let
+ val command' = the_command state command_id';
+ val exec_id' = new_id ();
+ val exec' =
+ snd exec |> Lazy.map (fn (st, _) =>
+ let val tr =
+ Future.join command'
+ |> Toplevel.modify_init init
+ |> Toplevel.put_id (print_id exec_id');
+ in run_command tr st end)
+ |> pair command_id';
+ in ((exec_id', exec') :: execs, exec') end;
fun init_theory deps name node =
let
@@ -379,65 +417,74 @@
SOME thy => thy
| NONE =>
get_theory (Position.file_only import)
- (#2 (Future.join (the (AList.lookup (op =) deps import))))));
+ (snd (Future.join (the (AList.lookup (op =) deps import))))));
in Thy_Load.begin_theory dir thy_name imports files parents end;
-fun new_exec state init command_id (assigns, execs, exec) =
- let
- val command = the_command state command_id;
- val exec_id' = new_id ();
- val exec' = exec |> Lazy.map (fn (st, _) =>
- let val tr =
- Future.join command
- |> Toplevel.modify_init init
- |> Toplevel.put_id (print_id exec_id');
- in run_command tr st end);
- in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
-
in
-fun edit (old_id: version_id) (new_id: version_id) edits state =
+fun update (old_id: version_id) (new_id: version_id) edits state =
let
val old_version = the_version state old_id;
val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
val new_version = fold edit_nodes edits old_version;
- val updates =
+ val updated =
nodes_of new_version |> Graph.schedule
(fn deps => fn (name, node) =>
if not (is_touched node) then Future.value (([], [], []), node)
else
- (case first_entry NONE (is_changed (node_of old_version name)) node of
- NONE => Future.value (([], [], []), set_touched false node)
- | SOME ((prev, id), _) =>
- let
- fun init () = init_theory deps name node;
- in
- (singleton o Future.forks)
- {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
- (fn () =>
- let
- val prev_exec =
- (case prev of
- NONE => no_id
- | SOME prev_id => the_default no_id (the_entry node prev_id));
- val (assigns, execs, last_exec) =
- fold_entries (SOME id) (new_exec state init o #2 o #1)
- node ([], [], #2 (the_exec state prev_exec));
- val node' = node
- |> fold update_entry assigns
- |> set_result (Lazy.map #1 last_exec)
- |> set_touched false;
- in ((assigns, execs, [(name, node')]), node') end)
- end))
+ let
+ val node0 = node_of old_version name;
+ fun init () = init_theory deps name node;
+ in
+ (singleton o Future.forks)
+ {name = "Document.update", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+ (fn () =>
+ let
+ val last_visible = #2 (get_perspective node);
+ val (common, visible) = last_common last_visible node0 node;
+ val common_exec = the_exec state (the_default_entry node common);
+
+ val (execs, exec) = ([], common_exec) |>
+ visible ?
+ iterate_entries (after_entry node common)
+ (fn ((prev, id), _) => fn res =>
+ if prev = last_visible then NONE
+ else SOME (new_exec state init id res)) node;
+
+ val no_execs =
+ iterate_entries (after_entry node0 common)
+ (fn ((_, id0), exec0) => fn res =>
+ if is_none exec0 then NONE
+ else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
+ else SOME (id0 :: res)) node0 [];
+
+ val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec);
+ val result =
+ if is_some (after_entry node last_exec) then no_result
+ else Lazy.map #1 (#2 exec);
+
+ val node' = node
+ |> fold reset_entry no_execs
+ |> fold (fn (exec_id, (id, _)) => update_entry id (SOME exec_id)) execs
+ |> set_last_exec last_exec
+ |> set_result result
+ |> set_touched false;
+ in ((no_execs, execs, [(name, node')]), node') end)
+ end)
|> Future.joins |> map #1;
+ val command_execs =
+ map (rpair NONE) (maps #1 updated) @
+ map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
+ val updated_nodes = maps #3 updated;
+ val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
+
val state' = state
- |> fold (fold define_exec o #2) updates
- |> define_version new_id (fold (fold put_node o #3) updates new_version);
-
- in (maps #1 (rev updates), state') end;
+ |> fold (fold define_exec o #2) updated
+ |> define_version new_id (fold put_node updated_nodes new_version);
+ in ((command_execs, last_execs), state') end;
end;
@@ -467,7 +514,7 @@
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
- (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
+ (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/document.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/document.scala Sat Aug 27 09:02:25 2011 +0200
@@ -60,7 +60,8 @@
case exn => exn
}
- val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
+ val empty: Node =
+ Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
@@ -156,7 +157,7 @@
object Change
{
- val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
+ val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
}
sealed case class Change(
@@ -172,7 +173,7 @@
object History
{
- val init = new History(List(Change.init))
+ val init: History = new History(List(Change.init))
}
// FIXME pruning, purging of state
@@ -203,21 +204,42 @@
: Stream[Text.Info[Option[A]]]
}
+ type Assign =
+ (List[(Document.Command_ID, Option[Document.Exec_ID])], // exec state assignment
+ List[(String, Option[Document.Command_ID])]) // last exec
+
+ val no_assign: Assign = (Nil, Nil)
+
object State
{
class Fail(state: State) extends Exception
- val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
+ val init: State =
+ State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
+
+ object Assignment
+ {
+ val init: Assignment = Assignment(Map.empty, Map.empty, false)
+ }
case class Assignment(
- val assignment: Map[Command, Exec_ID],
- val is_finished: Boolean = false)
+ val command_execs: Map[Command_ID, Exec_ID],
+ val last_execs: Map[String, Option[Command_ID]],
+ val is_finished: Boolean)
{
- def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
- def assign(command_execs: List[(Command, Exec_ID)]): Assignment =
+ def check_finished: Assignment = { require(is_finished); this }
+ def unfinished: Assignment = copy(is_finished = false)
+
+ def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
+ add_last_execs: List[(String, Option[Command_ID])]): Assignment =
{
require(!is_finished)
- Assignment(assignment ++ command_execs, true)
+ val command_execs1 =
+ (command_execs /: add_command_execs) {
+ case (res, (command_id, None)) => res - command_id
+ case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
+ }
+ Assignment(command_execs1, last_execs ++ add_last_execs, true)
}
}
}
@@ -232,12 +254,12 @@
{
private def fail[A]: A = throw new State.Fail(this)
- def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
+ def define_version(version: Version, assignment: State.Assignment): State =
{
val id = version.id
if (versions.isDefinedAt(id) || disposed(id)) fail
copy(versions = versions + (id -> version),
- assignments = assignments + (id -> State.Assignment(former_assignment)))
+ assignments = assignments + (id -> assignment.unfinished))
}
def define_command(command: Command): State =
@@ -250,7 +272,7 @@
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
- def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
+ def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
@@ -269,21 +291,22 @@
}
}
- def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
+ def assign(id: Version_ID, arg: Assign): (List[Command], State) =
{
val version = the_version(id)
+ val (command_execs, last_execs) = arg
- var new_execs = execs
- val assigned_execs =
- for ((cmd_id, exec_id) <- edits) yield {
- val st = the_command(cmd_id)
- if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
- new_execs += (exec_id -> st)
- (st.command, exec_id)
+ val (commands, new_execs) =
+ ((Nil: List[Command], execs) /: command_execs) {
+ case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
+ val st = the_command(cmd_id)
+ (st.command :: commands1, execs1 + (exec_id -> st))
+ case (res, (_, None)) => res
}
- val new_assignment = the_assignment(version).assign(assigned_execs)
+ val new_assignment = the_assignment(version).assign(command_execs, last_execs)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
- (assigned_execs.map(_._1), new_state)
+
+ (commands, new_state)
}
def is_assigned(version: Version): Boolean =
@@ -295,8 +318,24 @@
def is_stable(change: Change): Boolean =
change.is_finished && is_assigned(change.version.get_finished)
+ def recent_stable: Option[Change] = history.undo_list.find(is_stable)
def tip_stable: Boolean = is_stable(history.tip)
- def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+ def tip_version: Version = history.tip.version.get_finished
+
+ def last_exec_offset(name: String): Text.Offset =
+ {
+ val version = tip_version
+ the_assignment(version).last_execs.get(name) match {
+ case Some(Some(id)) =>
+ val node = version.nodes(name)
+ val cmd = the_command(id).command
+ node.command_start(cmd) match {
+ case None => 0
+ case Some(start) => start + cmd.length
+ }
+ case _ => 0
+ }
+ }
def continue_history(
previous: Future[Version],
@@ -329,7 +368,10 @@
def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
def state(command: Command): Command.State =
- try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
+ try {
+ the_exec(the_assignment(version).check_finished.command_execs
+ .getOrElse(command.id, fail))
+ }
catch { case _: State.Fail => command.empty_state }
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
--- a/src/Pure/PIDE/isar_document.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Sat Aug 27 09:02:25 2011 +0200
@@ -28,7 +28,7 @@
end));
val _ =
- Isabelle_Process.add_command "Isar_Document.edit_version"
+ Isabelle_Process.add_command "Isar_Document.update"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
val old_id = Document.parse_id old_id_string;
@@ -48,12 +48,15 @@
end;
val running = Document.cancel_execution state;
- val (updates, state') = Document.edit old_id new_id edits state;
+ val (assignment, state') = Document.update old_id new_id edits state;
val _ = Future.join_tasks running;
val _ = Document.join_commands state';
val _ =
Output.status (Markup.markup (Markup.assign new_id)
- (implode (map (Markup.markup_only o Markup.edit) updates)));
+ (assignment |>
+ let open XML.Encode
+ in pair (list (pair int (option int))) (list (pair string (option int))) end
+ |> YXML.string_of_body));
val state'' = Document.execute new_id state';
in state'' end));
--- a/src/Pure/PIDE/isar_document.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Sat Aug 27 09:02:25 2011 +0200
@@ -11,24 +11,20 @@
{
/* document editing */
- object Assign {
- def unapply(msg: XML.Tree)
- : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+ object Assign
+ {
+ def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
msg match {
- case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
- val id_edits = edits.map(Edit.unapply)
- if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
- else None
- case _ => None
- }
- }
-
- object Edit {
- def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
- msg match {
- case XML.Elem(
- Markup(Markup.EDIT,
- List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+ case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
+ try {
+ import XML.Decode._
+ val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
+ Some(id, a)
+ }
+ catch {
+ case _: XML.XML_Atom => None
+ case _: XML.XML_Body => None
+ }
case _ => None
}
}
@@ -144,13 +140,13 @@
{
val ids =
{ import XML.Encode._
- list(long)(perspective.map(_.id)) }
+ list(long)(perspective.commands.map(_.id)) }
input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
YXML.string_of_body(ids))
}
- def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit_Command])
{
val edits_yxml =
@@ -164,10 +160,10 @@
{ case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
(Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
{ case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
- { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
+ { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
YXML.string_of_body(encode(edits)) }
- input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+ input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
}
--- a/src/Pure/PIDE/text.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/PIDE/text.scala Sat Aug 27 09:02:25 2011 +0200
@@ -62,28 +62,39 @@
/* perspective */
- type Perspective = List[Range] // visible text partitioning in canonical order
-
- def perspective(ranges: Seq[Range]): Perspective =
+ object Perspective
{
- val sorted_ranges = ranges.toArray
- Sorting.quickSort(sorted_ranges)(Range.Ordering)
+ val empty: Perspective = Perspective(Nil)
- val result = new mutable.ListBuffer[Text.Range]
- var last: Option[Text.Range] = None
- for (range <- sorted_ranges)
+ def apply(ranges: Seq[Range]): Perspective =
{
- last match {
- case Some(last_range)
- if ((last_range overlaps range) || last_range.stop == range.start) =>
- last = Some(Text.Range(last_range.start, range.stop))
- case _ =>
- result ++= last
- last = Some(range)
+ val sorted_ranges = ranges.toArray
+ Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+ val result = new mutable.ListBuffer[Text.Range]
+ var last: Option[Text.Range] = None
+ for (range <- sorted_ranges)
+ {
+ last match {
+ case Some(last_range)
+ if ((last_range overlaps range) || last_range.stop == range.start) =>
+ last = Some(Text.Range(last_range.start, range.stop))
+ case _ =>
+ result ++= last
+ last = Some(range)
+ }
}
+ result ++= last
+ new Perspective(result.toList)
}
- result ++= last
- result.toList
+ }
+
+ sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
+ {
+ def is_empty: Boolean = ranges.isEmpty
+ def range: Range =
+ if (is_empty) Range(0)
+ else Range(ranges.head.start, ranges.last.stop)
}
--- a/src/Pure/Syntax/syntax_ext.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sat Aug 27 09:02:25 2011 +0200
@@ -231,8 +231,8 @@
val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
val args = filter (fn Argument _ => true | _ => false) raw_symbs;
- val (const', typ', parse_rules) =
- if not (exists is_index args) then (const, typ, [])
+ val (const', typ', syntax_consts, parse_rules) =
+ if not (exists is_index args) then (const, typ, NONE, NONE)
else
let
val indexed_const =
@@ -247,7 +247,7 @@
val lhs = Ast.mk_appl (Ast.Constant indexed_const)
(xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
- in (indexed_const, rangeT, [(lhs, rhs)]) end;
+ in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end;
val (symbs, lhs) = add_args raw_symbs typ' pris;
@@ -273,7 +273,7 @@
else if exists is_terminal symbs' then xprod
else XProd (lhs', map rem_pri symbs', "", chain_pri);
- in (xprod', parse_rules) end;
+ in (xprod', syntax_consts, parse_rules) end;
@@ -298,13 +298,15 @@
val (parse_ast_translation, parse_translation, print_translation,
print_ast_translation) = trfuns;
- val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
- |> split_list |> apsnd (rev o flat);
+ val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
+ val xprods = map #1 xprod_results;
+ val consts' = map_filter #2 xprod_results;
+ val parse_rules' = rev (map_filter #3 xprod_results);
val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
in
Syn_Ext {
xprods = xprods,
- consts = mfix_consts @ consts,
+ consts = mfix_consts @ consts' @ consts,
parse_ast_translation = parse_ast_translation,
parse_rules = parse_rules' @ parse_rules,
parse_translation = parse_translation,
--- a/src/Pure/System/session.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/System/session.scala Sat Aug 27 09:02:25 2011 +0200
@@ -206,7 +206,7 @@
def update_perspective(name: String, text_perspective: Text.Perspective)
{
- val previous = global_state().history.tip.version.get_finished
+ val previous = global_state().tip_version
val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
val text_edits: List[Document.Edit_Text] =
@@ -215,9 +215,9 @@
global_state.change_yield(
_.continue_history(Future.value(previous), text_edits, Future.value(version)))
- val assignment = global_state().the_assignment(previous).get_finished
+ val assignment = global_state().the_assignment(previous).check_finished
global_state.change(_.define_version(version, assignment))
- global_state.change_yield(_.assign(version.id, Nil))
+ global_state.change_yield(_.assign(version.id, Document.no_assign))
prover.get.update_perspective(previous.id, version.id, name, perspective)
}
@@ -248,10 +248,10 @@
/* exec state assignment */
- def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+ def handle_assign(id: Document.Version_ID, assign: Document.Assign)
//{{{
{
- val cmds = global_state.change_yield(_.assign(id, edits))
+ val cmds = global_state.change_yield(_.assign(id, assign))
for (cmd <- cmds) command_change_buffer ! cmd
assignments.event(Session.Assignment)
}
@@ -268,13 +268,6 @@
val name = change.name
val doc_edits = change.doc_edits
- var former_assignment = global_state().the_assignment(previous).get_finished
- for {
- (name, Document.Node.Edits(cmd_edits)) <- doc_edits // FIXME proper coverage!?
- (prev, None) <- cmd_edits
- removed <- previous.nodes(name).commands.get_after(prev)
- } former_assignment -= removed
-
def id_command(command: Command)
{
if (global_state().lookup_command(command.id).isEmpty) {
@@ -287,8 +280,9 @@
edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
}
- global_state.change(_.define_version(version, former_assignment))
- prover.get.edit_version(previous.id, version.id, doc_edits)
+ val assignment = global_state().the_assignment(previous).check_finished
+ global_state.change(_.define_version(version, assignment))
+ prover.get.update(previous.id, version.id, doc_edits)
}
//}}}
@@ -336,8 +330,8 @@
else if (result.is_stdout) { }
else if (result.is_status) {
result.body match {
- case List(Isar_Document.Assign(id, edits)) =>
- try { handle_assign(id, edits) }
+ case List(Isar_Document.Assign(id, assign)) =>
+ try { handle_assign(id, assign) }
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -386,7 +380,8 @@
reply(())
case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
- if (text_edits.isEmpty && global_state().tip_stable)
+ if (text_edits.isEmpty && global_state().tip_stable &&
+ perspective.range.stop <= global_state().last_exec_offset(name))
update_perspective(name, perspective)
else
handle_edits(name, master_dir, header,
--- a/src/Pure/Thy/thy_load.ML Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML Sat Aug 27 09:02:25 2011 +0200
@@ -175,7 +175,7 @@
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val elements =
Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
- |> maps (Outer_Syntax.prepare_element outer_syntax init);
+ |> maps (Outer_Syntax.read_element outer_syntax init);
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sat Aug 27 09:02:25 2011 +0200
@@ -101,7 +101,7 @@
def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
{
- if (perspective.isEmpty) Nil
+ if (perspective.is_empty) Command.Perspective.empty
else {
val result = new mutable.ListBuffer[Command]
@tailrec
@@ -120,9 +120,8 @@
case _ =>
}
}
- val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
- check_ranges(perspective, node.command_range(perspective_range).toStream)
- result.toList
+ check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
+ Command.Perspective(result.toList)
}
}
@@ -132,7 +131,7 @@
val node = nodes(name)
val perspective = command_perspective(node, text_perspective)
val new_nodes =
- if (Command.equal_perspective(node.perspective, perspective)) None
+ if (node.perspective same perspective) None
else Some(nodes + (name -> node.copy(perspective = perspective)))
(perspective, new_nodes)
}
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Aug 27 09:02:25 2011 +0200
@@ -134,11 +134,14 @@
# args
-while [ "$#" -gt 0 ]
-do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
- shift
-done
+if [ "$#" -eq 0 ]; then
+ ARGS["${#ARGS[@]}"]="Scratch.thy"
+else
+ while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+ done
+fi
## dependencies
--- a/src/Tools/jEdit/src/document_model.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sat Aug 27 09:02:25 2011 +0200
@@ -74,10 +74,10 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.perspective(
+ Text.Perspective(
for {
doc_view <- Isabelle.document_views(buffer)
- range <- doc_view.perspective()
+ range <- doc_view.perspective().ranges
} yield range)
}
@@ -88,7 +88,7 @@
{
private val pending = new mutable.ListBuffer[Text.Edit]
private var pending_perspective = false
- private var last_perspective: Text.Perspective = Nil
+ private var last_perspective: Text.Perspective = Text.Perspective.empty
def snapshot(): List[Text.Edit] = pending.toList
@@ -101,7 +101,7 @@
else last_perspective
snapshot() match {
- case Nil if new_perspective == last_perspective =>
+ case Nil if last_perspective == new_perspective =>
case edits =>
pending.clear
last_perspective = new_perspective
--- a/src/Tools/jEdit/src/document_view.scala Fri Aug 26 23:02:00 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Sat Aug 27 09:02:25 2011 +0200
@@ -118,7 +118,7 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.perspective(
+ Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
val start = text_area.getScreenLineStartOffset(i)