src/HOL/Multivariate_Analysis/Euclidean_Space.thy
changeset 34964 4e8be3c04d37
parent 34915 7894c7dab132
child 35028 108662d50512
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Jan 22 16:59:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Jan 25 16:56:24 2010 +0100
@@ -14,9 +14,12 @@
 
 text{* Some common special cases.*}
 
-lemma forall_1: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
+lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
   by (metis num1_eq_iff)
 
+lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
+  by auto (metis num1_eq_iff)
+
 lemma exhaust_2:
   fixes x :: 2 shows "x = 1 \<or> x = 2"
 proof (induct x)
@@ -196,7 +199,6 @@
 instance cart :: (semigroup_add,finite) semigroup_add
   apply (intro_classes) by (vector add_assoc)
 
-
 instance cart :: (monoid_add,finite) monoid_add
   apply (intro_classes) by vector+
 
@@ -2418,87 +2420,65 @@
 
 (* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
 
-definition vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x = (\<chi> i. x)"
-
-definition dest_vec1:: "'a ^1 \<Rightarrow> 'a"
-  where "dest_vec1 x = (x$1)"
+abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
+
+abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
+  where "dest_vec1 x \<equiv> (x$1)"
 
 lemma vec1_component[simp]: "(vec1 x)$1 = x"
-  by (simp add: vec1_def)
+  by (simp add: )
 
 lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
-  by (simp_all add: vec1_def dest_vec1_def Cart_eq forall_1)
+  by (simp_all add:  Cart_eq forall_1)
 
 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)
 
 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)
 
-lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))"  by (metis vec1_dest_vec1)
-
-lemma exists_dest_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(dest_vec1 x))"by (metis vec1_dest_vec1)
-
 lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
 
 lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
 
-lemma vec1_in_image_vec1: "vec1 x \<in> (vec1 ` S) \<longleftrightarrow> x \<in> S" by auto
-
-lemma vec1_vec: "vec1 x = vec x" by (vector vec1_def)
-
-lemma vec1_add: "vec1(x + y) = vec1 x + vec1 y" by (vector vec1_def)
-lemma vec1_sub: "vec1(x - y) = vec1 x - vec1 y" by (vector vec1_def)
-lemma vec1_cmul: "vec1(c* x) = c *s vec1 x " by (vector vec1_def)
-lemma vec1_neg: "vec1(- x) = - vec1 x " by (vector vec1_def)
-
-lemma vec1_0[simp]:"vec1 0 = 0" unfolding vec1_def Cart_eq by auto
+lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
+
+lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
+lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
+lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def)
+lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
 
 lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
   apply(rule_tac x="dest_vec1 x" in bexI) by auto
 
-lemma vec1_setsum: assumes fS: "finite S"
-  shows "vec1(setsum f S) = setsum (vec1 o f) S"
+lemma vec_setsum: assumes fS: "finite S"
+  shows "vec(setsum f S) = setsum (vec o f) S"
   apply (induct rule: finite_induct[OF fS])
-  apply (simp add: vec1_vec)
-  apply (auto simp add: vec1_add)
+  apply (simp)
+  apply (auto simp add: vec_add)
   done
 
 lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
-  by (simp add: dest_vec1_def)
+  by (simp)
 
 lemma dest_vec1_vec: "dest_vec1(vec x) = x"
-  by (simp add: vec1_vec[symmetric])
-
-lemma dest_vec1_add: "dest_vec1(x + y) = dest_vec1 x + dest_vec1 y"
- by (metis vec1_dest_vec1 vec1_add)
-
-lemma dest_vec1_sub: "dest_vec1(x - y) = dest_vec1 x - dest_vec1 y"
- by (metis vec1_dest_vec1 vec1_sub)
-
-lemma dest_vec1_cmul: "dest_vec1(c*sx) = c * dest_vec1 x"
- by (metis vec1_dest_vec1 vec1_cmul)
-
-lemma dest_vec1_neg: "dest_vec1(- x) = - dest_vec1 x"
- by (metis vec1_dest_vec1 vec1_neg)
-
-lemma dest_vec1_0[simp]: "dest_vec1 0 = 0" by (metis vec_0 dest_vec1_vec)
+  by (simp)
 
 lemma dest_vec1_sum: assumes fS: "finite S"
   shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
   apply (induct rule: finite_induct[OF fS])
   apply (simp add: dest_vec1_vec)
-  apply (auto simp add: dest_vec1_add)
+  apply (auto simp add:vector_minus_component)
   done
 
 lemma norm_vec1: "norm(vec1 x) = abs(x)"
-  by (simp add: vec1_def norm_real)
+  by (simp add: vec_def norm_real)
 
 lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
   by (simp only: dist_real vec1_component)
 lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
   by (metis vec1_dest_vec1 norm_vec1)
 
-lemmas vec1_dest_vec1_simps = forall_vec1 vec1_add[THEN sym] dist_vec1 vec1_sub[THEN sym] vec1_dest_vec1 norm_vec1 dest_vec1_cmul
-   vec1_eq vec1_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
+   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
 
 lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
   unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
@@ -2508,7 +2488,6 @@
 lemma linear_vmul_dest_vec1:
   fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
-  unfolding dest_vec1_def
   apply (rule linear_vmul_component)
   by auto
 
@@ -2517,14 +2496,14 @@
   shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
   apply (rule ext)
   apply (subst matrix_works[OF lf, symmetric])
-  apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def  mult_commute UNIV_1)
+  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def  mult_commute UNIV_1)
   done
 
 lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"
   shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
   apply (rule ext)
   apply (subst matrix_works[OF lf, symmetric])
-  apply (simp add: Cart_eq matrix_vector_mult_def vec1_def row_def dot_def mult_commute forall_1)
+  apply (simp add: Cart_eq matrix_vector_mult_def row_def dot_def mult_commute forall_1)
   done
 
 lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
@@ -2532,7 +2511,7 @@
 
 lemma setsum_scalars: assumes fS: "finite S"
   shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
-  unfolding vec1_setsum[OF fS] by simp
+  unfolding vec_setsum[OF fS] by simp
 
 lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
   apply (cases "dest_vec1 x \<le> dest_vec1 y")
@@ -2543,10 +2522,10 @@
 
 text{* Pasting vectors. *}
 
-lemma linear_fstcart: "linear fstcart"
+lemma linear_fstcart[intro]: "linear fstcart"
   by (auto simp add: linear_def Cart_eq)
 
-lemma linear_sndcart: "linear sndcart"
+lemma linear_sndcart[intro]: "linear sndcart"
   by (auto simp add: linear_def Cart_eq)
 
 lemma fstcart_vec[simp]: "fstcart(vec x) = vec x"
@@ -2690,7 +2669,7 @@
 lemma hull_hull: "S hull (S hull s) = S hull s"
   unfolding hull_def by blast
 
-lemma hull_subset: "s \<subseteq> (S hull s)"
+lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
   unfolding hull_def by blast
 
 lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"