# HG changeset patch
# User hoelzl
# Date 1258627897 -3600
# Node ID 53078b0d21f5ae61c61bb39e9f20894786e4a35a
# Parent  bc75dbbbf3e6c5dbc4d70502bbac69469daa0798
Renamed vector_less_eq_def to the more usual name vector_le_def.

diff -r bc75dbbbf3e6 -r 53078b0d21f5 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 19 10:49:43 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 19 11:51:37 2009 +0100
@@ -1562,12 +1562,12 @@
   obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
   fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
 next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
-  hence "a \<le> b" unfolding interval_eq_empty vector_less_eq_def by(auto simp add: not_less)
-  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_less_eq_def forall_2 by auto
+  hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
+  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto
 next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
     apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
-    unfolding pathstart_def by(auto simp add: vector_less_eq_def) then guess z .. note z=this
+    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
   have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
   hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
     using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
@@ -1576,7 +1576,7 @@
 next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
     apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
     unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
-    unfolding pathstart_def by(auto simp add: vector_less_eq_def) then guess z .. note z=this
+    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
   have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
   hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
     using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
@@ -1693,7 +1693,7 @@
       path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
       path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
       by(auto simp add: pathstart_join pathfinish_join path_image_join path_image_linepath path_join path_linepath) 
-  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_less_eq_def forall_2 vector_2)
+  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
   guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
     show "path ?P1" "path ?P2" using assms by(auto simp add: pathstart_join pathfinish_join path_join)
diff -r bc75dbbbf3e6 -r 53078b0d21f5 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Nov 19 10:49:43 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Nov 19 11:51:37 2009 +0100
@@ -23,7 +23,7 @@
 
 lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto
 
-lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_less_eq_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
+lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component
 
 lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id
 
@@ -61,7 +61,7 @@
 lemma mem_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def all_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1)
 
 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =
   (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
@@ -77,7 +77,7 @@
   apply(rule_tac [!] allI)apply(rule_tac [!] impI)
   apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
   apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
-  by (auto simp add: vector_less_def vector_less_eq_def all_1 dest_vec1_def
+  by (auto simp add: vector_less_def vector_le_def all_1 dest_vec1_def
     vec1_dest_vec1[unfolded dest_vec1_def One_nat_def])
 
 lemma dest_vec1_setsum: assumes "finite S"
@@ -2354,7 +2354,7 @@
   assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
 proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI) 
-    using assms(1) by(auto simp add: vector_less_eq_def dest_vec1_def)
+    using assms(1) by(auto simp add: vector_le_def dest_vec1_def)
   thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
     using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
     using assms by(auto intro!: imageI) qed
@@ -2415,10 +2415,10 @@
       show ?thesis proof(cases "x$i=1")
         case True have "\<forall>j\<in>{i. x$i \<noteq> 0}. x$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof-
           fix j assume "x $ j \<noteq> 0" "x $ j \<noteq> 1"
-          hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_less_eq_def elim!:allE[where x=j])
+          hence j:"x$j \<in> {0<..<1}" using Suc(2) by(auto simp add: vector_le_def elim!:allE[where x=j])
           hence "x$j \<in> op $ x ` {i. x $ i \<noteq> 0}" by auto 
           hence "x$j \<ge> x$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
-          thus False using True Suc(2) j by(auto simp add: vector_less_eq_def elim!:ballE[where x=j]) qed
+          thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed
         thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
           by(auto simp add: Cart_lambda_beta)
       next let ?y = "\<lambda>j. if x$j = 0 then 0 else (x$j - x$i) / (1 - x$i)"
@@ -2439,7 +2439,7 @@
   show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule 
     apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
     unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
-    by(auto simp add: vector_less_eq_def mem_def[of _ convex]) qed
+    by(auto simp add: vector_le_def mem_def[of _ convex]) qed
 
 subsection {* And this is a finite set of vertices. *}
 
@@ -2469,7 +2469,7 @@
     hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms
       by(auto simp add: Cart_eq vector_component_simps field_simps)
     thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI) 
-      using assms by(auto simp add: Cart_eq vector_less_eq_def Cart_lambda_beta)
+      using assms by(auto simp add: Cart_eq vector_le_def Cart_lambda_beta)
   next
     fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z" 
     have "\<And>i. 0 \<le> d * z $ i \<and> d * z $ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
@@ -2911,7 +2911,7 @@
 lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" proof-
   have *:"\<And>g. path_image(reversepath g) \<subseteq> path_image g"
     unfolding path_image_def subset_eq reversepath_def Ball_def image_iff apply(rule,rule,erule bexE)  
-    apply(rule_tac x="1 - xa" in bexI) by(auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+    apply(rule_tac x="1 - xa" in bexI) by(auto simp add:vector_le_def vector_component_simps elim!:ballE)
   show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
 
 lemma path_reversepath[simp]: "path(reversepath g) \<longleftrightarrow> path g" proof-
@@ -2919,7 +2919,7 @@
     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(rule continuous_on_subset[of "{0..1}"], assumption)
-    by (auto, auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+    by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
   show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed
 
 lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath
@@ -2930,7 +2930,7 @@
   have *:"g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)" 
          "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" unfolding o_def by auto
   have "op *\<^sub>R (1 / 2) ` {0::real^1..1} \<subseteq> {0..1}"  "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real^1)..1} \<subseteq> {0..1}"
-    unfolding image_smult_interval by (auto, auto simp add:vector_less_eq_def vector_component_simps elim!:ballE)
+    unfolding image_smult_interval by (auto, auto simp add:vector_le_def vector_component_simps elim!:ballE)
   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
diff -r bc75dbbbf3e6 -r 53078b0d21f5 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Nov 19 10:49:43 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Nov 19 11:51:37 2009 +0100
@@ -627,7 +627,7 @@
 subsection {* The traditional Rolle theorem in one dimension. *}
 
 lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
-  unfolding vector_less_eq_def by auto
+  unfolding vector_le_def by auto
 lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
   unfolding vector_less_def by auto 
 
diff -r bc75dbbbf3e6 -r 53078b0d21f5 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Nov 19 10:49:43 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Nov 19 11:51:37 2009 +0100
@@ -94,7 +94,7 @@
 
 instantiation "^" :: (ord,type) ord
  begin
-definition vector_less_eq_def:
+definition vector_le_def:
   "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
 definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
 
diff -r bc75dbbbf3e6 -r 53078b0d21f5 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 19 10:49:43 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 19 11:51:37 2009 +0100
@@ -4619,17 +4619,17 @@
 lemma interval: fixes a :: "'a::ord^'n::finite" shows
   "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
   "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
-  by (auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+  by (auto simp add: expand_set_eq vector_less_def vector_le_def)
 
 lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows
   "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
   "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
-  using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_less_eq_def)
+  using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
 
 lemma mem_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def forall_1)
 
 lemma vec1_interval:fixes a::"real" shows
   "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
@@ -4690,7 +4690,7 @@
 
 lemma interval_sing: fixes a :: "'a::linorder^'n::finite" shows
  "{a .. a} = {a} \<and> {a<..<a} = {}"
-apply(auto simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
 apply (simp add: order_eq_iff)
 apply (auto simp add: not_less less_imp_le)
 done
@@ -4703,17 +4703,17 @@
   { fix i
     have "a $ i \<le> x $ i"
       using x order_less_imp_le[of "a$i" "x$i"]
-      by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   }
   moreover
   { fix i
     have "x $ i \<le> b $ i"
       using x order_less_imp_le[of "x$i" "b$i"]
-      by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   }
   ultimately
   show "a \<le> x \<and> x \<le> b"
-    by(simp add: expand_set_eq vector_less_def vector_less_eq_def Cart_eq)
+    by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
 qed
 
 lemma subset_interval: fixes a :: "real^'n::finite" shows
@@ -5026,12 +5026,12 @@
 
 lemma interval_cases_1: fixes x :: "real^1" shows
  "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
-  by(simp add:  Cart_eq vector_less_def vector_less_eq_def all_1, auto)
+  by(simp add:  Cart_eq vector_less_def vector_le_def all_1, auto)
 
 lemma in_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
   (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp add: Cart_eq vector_less_def vector_less_eq_def all_1 dest_vec1_def)
+by(simp add: Cart_eq vector_less_def vector_le_def all_1 dest_vec1_def)
 
 lemma interval_eq_empty_1: fixes a :: "real^1" shows
   "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
@@ -5067,10 +5067,10 @@
 
 lemma open_closed_interval_1: fixes a :: "real^1" shows
  "{a<..<b} = {a .. b} - {a, b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
 
 lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_less_eq_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and all_1 and dest_vec1_eq[THEN sym] and dest_vec1_def by auto
 
 (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
 
@@ -5742,30 +5742,30 @@
             else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
 proof(cases "m=0")
   { fix x assume "x \<le> c" "c \<le> x"
-    hence "x=c" unfolding vector_less_eq_def and Cart_eq by (auto intro: order_antisym) }
+    hence "x=c" unfolding vector_le_def and Cart_eq by (auto intro: order_antisym) }
   moreover case True
-  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: vector_less_eq_def)
+  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: vector_le_def)
   ultimately show ?thesis by auto
 next
   case False
   { fix y assume "a \<le> y" "y \<le> b" "m > 0"
     hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
-      unfolding vector_less_eq_def by(auto simp add: vector_smult_component vector_add_component)
+      unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component)
   } moreover
   { fix y assume "a \<le> y" "y \<le> b" "m < 0"
     hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
-      unfolding vector_less_eq_def by(auto simp add: vector_smult_component vector_add_component mult_left_mono_neg elim!:ballE)
+      unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component mult_left_mono_neg elim!:ballE)
   } moreover
   { 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 vector_less_eq_def
+      unfolding image_iff Bex_def mem_interval vector_le_def
       apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
       by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_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 vector_less_eq_def
+      unfolding image_iff Bex_def mem_interval vector_le_def
       apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
       by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)