adapted to changes in Cset.thy
authorhaftmann
Sat, 27 Aug 2011 09:02:25 +0200
changeset 44557 9ab8c88449a4
parent 44539 ddfd934e19bb (diff)
parent 44556 c0fd385a41f4 (current diff)
child 44558 cc878a312673
adapted to changes in Cset.thy
--- 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)