author  huffman 
Sat, 21 Feb 2009 09:55:32 0800  
changeset 30039  7208c88df507 
parent 29906  80369da39838 
child 30040  e2cd1acda1ab 
permissions  rwrr 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1 
(* Title: Library/Euclidean_Space 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

2 
ID: $Id: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

3 
Author: Amine Chaieb, University of Cambridge 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

4 
*) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

5 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

6 
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

7 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

8 
theory Euclidean_Space 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

9 
imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

10 
Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

11 
uses ("normarith.ML") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

12 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

13 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

14 
text{* Some common special cases.*} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

15 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

16 
lemma forall_1: "(\<forall>(i::'a::{order,one}). 1 <= i \<and> i <= 1 > P i) \<longleftrightarrow> P 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

17 
by (metis order_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

18 
lemma forall_dimindex_1: "(\<forall>i \<in> {1..dimindex(UNIV:: 1 set)}. P i) \<longleftrightarrow> P 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

19 
by (simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

20 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

21 
lemma forall_2: "(\<forall>(i::nat). 1 <= i \<and> i <= 2 > P i) \<longleftrightarrow> P 1 \<and> P 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

22 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

23 
have "\<And>i::nat. 1 <= i \<and> i <= 2 \<longleftrightarrow> i = 1 \<or> i = 2" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

24 
thus ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

25 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

26 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

27 
lemma forall_3: "(\<forall>(i::nat). 1 <= i \<and> i <= 3 > P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

28 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

29 
have "\<And>i::nat. 1 <= i \<and> i <= 3 \<longleftrightarrow> i = 1 \<or> i = 2 \<or> i = 3" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

30 
thus ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

31 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

32 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

33 
lemma setsum_singleton[simp]: "setsum f {x} = f x" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

34 
lemma setsum_1: "setsum f {(1::'a::{order,one})..1} = f 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

35 
by (simp add: atLeastAtMost_singleton) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

36 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

37 
lemma setsum_2: "setsum f {1::nat..2} = f 1 + f 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

38 
by (simp add: nat_number atLeastAtMostSuc_conv add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

39 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

40 
lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

41 
by (simp add: nat_number atLeastAtMostSuc_conv add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

42 

29906  43 
subsection{* Basic componentwise operations on vectors. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

44 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

45 
instantiation "^" :: (plus,type) plus 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

46 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

47 
definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

48 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

49 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

50 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

51 
instantiation "^" :: (times,type) times 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

52 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

53 
definition vector_mult_def : "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

54 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

55 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

56 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

57 
instantiation "^" :: (minus,type) minus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

58 
definition vector_minus_def : "op  \<equiv> (\<lambda> x y. (\<chi> i. (x$i)  (y$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

59 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

60 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

61 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

62 
instantiation "^" :: (uminus,type) uminus begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

63 
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i.  (x$i)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

64 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

65 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

66 
instantiation "^" :: (zero,type) zero begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

67 
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

68 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

69 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

70 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

71 
instantiation "^" :: (one,type) one begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

72 
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

73 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

74 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

75 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

76 
instantiation "^" :: (ord,type) ord 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

77 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

78 
definition vector_less_eq_def: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

79 
"less_eq (x :: 'a ^'b) y = (ALL i : {1 .. dimindex (UNIV :: 'b set)}. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

80 
x$i <= y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

81 
definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i : {1 .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

82 
dimindex (UNIV :: 'b set)}. x$i < y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

83 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

84 
instance by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

85 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

86 

30039  87 
instantiation "^" :: (scaleR, type) scaleR 
88 
begin 

89 
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" 

90 
instance .. 

91 
end 

92 

93 
text{* Also the scalarvector multiplication. *} 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

94 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

95 
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

96 
where "c *s x = (\<chi> i. c * (x$i))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

97 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

98 
text{* Constant Vectors *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

99 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

100 
definition "vec x = (\<chi> i. x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

101 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

102 
text{* Dot products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

103 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

104 
definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

105 
"x \<bullet> y = setsum (\<lambda>i. x$i * y$i) {1 .. dimindex (UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

106 
lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

107 
by (simp add: dot_def dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

108 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

109 
lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

110 
by (simp add: dot_def dimindex_def nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

111 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

112 
lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

113 
by (simp add: dot_def dimindex_def nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

114 

29906  115 
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

116 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

117 
lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

118 
method_setup vector = {* 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

119 
let 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

120 
val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

121 
@{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

122 
@{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

123 
val ss2 = @{simpset} addsimps 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

124 
[@{thm vector_add_def}, @{thm vector_mult_def}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

125 
@{thm vector_minus_def}, @{thm vector_uminus_def}, 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

126 
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, 
30039  127 
@{thm vector_scaleR_def}, 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

128 
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

129 
fun vector_arith_tac ths = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

130 
simp_tac ss1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

131 
THEN' (fn i => rtac @{thm setsum_cong2} i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

132 
ORELSE rtac @{thm setsum_0'} i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

133 
ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

134 
(* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

135 
THEN' asm_full_simp_tac (ss2 addsimps ths) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

136 
in 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

137 
Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

138 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

139 
*} "Lifts trivial vector statements to real arith statements" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

140 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

141 
lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

142 
lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

143 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

144 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

145 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

146 
text{* Obvious "componentpushing". *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

147 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

148 
lemma vec_component: " i \<in> {1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (vec x :: 'a ^ 'n)$i = x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

149 
by (vector vec_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

150 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

151 
lemma vector_add_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

152 
fixes x y :: "'a::{plus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

153 
shows "(x + y)$i = x$i + y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

154 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

155 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

156 
lemma vector_minus_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

157 
fixes x y :: "'a::{minus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

158 
shows "(x  y)$i = x$i  y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

159 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

160 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

161 
lemma vector_mult_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

162 
fixes x y :: "'a::{times} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

163 
shows "(x * y)$i = x$i * y$i" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

164 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

165 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

166 
lemma vector_smult_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

167 
fixes y :: "'a::{times} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

168 
shows "(c *s y)$i = c * (y$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

169 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

170 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

171 
lemma vector_uminus_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

172 
fixes x :: "'a::{uminus} ^ 'n" assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

173 
shows "( x)$i =  (x$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

174 
using i by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

175 

30039  176 
lemma vector_scaleR_component: 
177 
fixes x :: "'a::scaleR ^ 'n" 

178 
assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}" 

179 
shows "(scaleR r x)$i = scaleR r (x$i)" 

180 
using i by vector 

181 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

182 
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

183 

30039  184 
lemmas vector_component = 
185 
vec_component vector_add_component vector_mult_component 

186 
vector_smult_component vector_minus_component vector_uminus_component 

187 
vector_scaleR_component cond_component 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

188 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

189 
subsection {* Some frequently useful arithmetic lemmas over vectors. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

190 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

191 
instance "^" :: (semigroup_add,type) semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

192 
apply (intro_classes) by (vector add_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

193 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

194 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

195 
instance "^" :: (monoid_add,type) monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

196 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

197 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

198 
instance "^" :: (group_add,type) group_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

199 
apply (intro_classes) by (vector algebra_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

200 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

201 
instance "^" :: (ab_semigroup_add,type) ab_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

202 
apply (intro_classes) by (vector add_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

203 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

204 
instance "^" :: (comm_monoid_add,type) comm_monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

205 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

206 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

207 
instance "^" :: (ab_group_add,type) ab_group_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

208 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

209 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

210 
instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

211 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

212 
by (vector Cart_eq)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

213 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

214 
instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

215 
apply (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

216 
by (vector Cart_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

217 

30039  218 
instance "^" :: (real_vector, type) real_vector 
219 
by default (vector scaleR_left_distrib scaleR_right_distrib)+ 

220 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

221 
instance "^" :: (semigroup_mult,type) semigroup_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

222 
apply (intro_classes) by (vector mult_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

223 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

224 
instance "^" :: (monoid_mult,type) monoid_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

225 
apply (intro_classes) by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

226 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

227 
instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

228 
apply (intro_classes) by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

229 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

230 
instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

231 
apply (intro_classes) by (vector mult_idem) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

232 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

233 
instance "^" :: (comm_monoid_mult,type) comm_monoid_mult 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

234 
apply (intro_classes) by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

235 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

236 
fun vector_power :: "('a::{one,times} ^'n) \<Rightarrow> nat \<Rightarrow> 'a^'n" where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

237 
"vector_power x 0 = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

238 
 "vector_power x (Suc n) = x * vector_power x n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

239 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

240 
instantiation "^" :: (recpower,type) recpower 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

241 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

242 
definition vec_power_def: "op ^ \<equiv> vector_power" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

243 
instance 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

244 
apply (intro_classes) by (simp_all add: vec_power_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

245 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

246 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

247 
instance "^" :: (semiring,type) semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

248 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

249 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

250 
instance "^" :: (semiring_0,type) semiring_0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

251 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

252 
instance "^" :: (semiring_1,type) semiring_1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

253 
apply (intro_classes) apply vector using dimindex_ge_1 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

254 
instance "^" :: (comm_semiring,type) comm_semiring 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

255 
apply (intro_classes) by (vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

256 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

257 
instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) 
29905  258 
instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

259 
instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

260 
instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

261 
instance "^" :: (ring,type) ring by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

262 
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

263 
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes) 
30039  264 

265 
instance "^" :: (ring_1,type) ring_1 .. 

266 

267 
instance "^" :: (real_algebra,type) real_algebra 

268 
apply intro_classes 

269 
apply (simp_all add: vector_scaleR_def ring_simps) 

270 
apply vector 

271 
apply vector 

272 
done 

273 

274 
instance "^" :: (real_algebra_1,type) real_algebra_1 .. 

275 

29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

276 
lemma of_nat_index: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

277 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

278 
apply (induct n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

279 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

280 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

281 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

282 
lemma zero_index[simp]: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

283 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (0 :: 'a::zero ^'n)$i = 0" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

284 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

285 
lemma one_index[simp]: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

286 
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (1 :: 'a::one ^'n)$i = 1" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

287 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

288 
lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

289 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

290 
have "(1::'a) + of_nat n = 0 \<longleftrightarrow> of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

291 
also have "\<dots> \<longleftrightarrow> 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

292 
finally show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

293 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

294 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

295 
instance "^" :: (semiring_char_0,type) semiring_char_0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

296 
proof (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

297 
fix m n ::nat 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

298 
show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

299 
proof(induct m arbitrary: n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

300 
case 0 thus ?case apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

301 
apply (induct n,auto simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

302 
using dimindex_ge_1 apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

303 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

304 
by (auto simp add: of_nat_index one_plus_of_nat_neq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

305 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

306 
case (Suc n m) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

307 
thus ?case apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

308 
apply (induct m, auto simp add: ring_simps of_nat_index zero_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

309 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

310 
apply (simp add: one_plus_of_nat_neq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

311 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

312 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

313 
apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

314 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

315 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

316 
apply (simp only: of_nat.simps(2)[where ?'a = 'a, symmetric] of_nat_eq_iff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

317 
using dimindex_ge_1 apply simp apply blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

318 
apply (simp add: vector_component one_index of_nat_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

319 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

320 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

321 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

322 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

323 
instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes 
30039  324 
instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

325 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

326 
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

327 
by (vector mult_assoc) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

328 
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

329 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

330 
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

331 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

332 
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

333 
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

334 
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x  y) = c *s x  c *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

335 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

336 
lemma vector_smult_rneg: "(c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

337 
lemma vector_smult_lneg: " (c::'a::ring) *s x = (c *s x)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

338 
lemma vector_sneg_minus1: "x = ( (1::'a::ring_1)) *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

339 
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

340 
lemma vector_sub_rdistrib: "((a::'a::ring)  b) *s x = a *s x  b *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

341 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

342 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

343 
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

344 
apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

345 
using dimindex_ge_1 apply auto done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

346 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

347 
subsection{* Properties of the dot product. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

348 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

349 
lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

350 
by (vector mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

351 
lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

352 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

353 
lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

354 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

355 
lemma dot_lsub: "((x::'a::ring ^ 'n)  y) \<bullet> z = (x \<bullet> z)  (y \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

356 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

357 
lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y  z) = (x \<bullet> y)  (x \<bullet> z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

358 
by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

359 
lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

360 
lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

361 
lemma dot_lneg: "(x) \<bullet> (y::'a::ring ^ 'n) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

362 
lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (y) = (x \<bullet> y)" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

363 
lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

364 
lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

365 
lemma dot_pos_le[simp]: "(0::'a\<Colon>ordered_ring_strict) <= x \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

366 
by (simp add: dot_def setsum_nonneg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

367 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

368 
lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::pordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

369 
using fS fp setsum_nonneg[OF fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

370 
proof (induct set: finite) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

371 
case empty thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

372 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

373 
case (insert x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

374 
from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

375 
from insert.hyps Fp setsum_nonneg[OF Fp] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

376 
have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

377 
from sum_nonneg_eq_zero_iff[OF Fx setsum_nonneg[OF Fp]] insert.hyps(1,2) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

378 
show ?case by (simp add: h) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

379 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

380 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

381 
lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

382 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

383 
{assume f: "finite (UNIV :: 'n set)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

384 
let ?S = "{Suc 0 .. card (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

385 
have fS: "finite ?S" using f by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

386 
have fp: "\<forall> i\<in> ?S. x$i * x$i>= 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

387 
have ?thesis by (vector dimindex_def f setsum_squares_eq_0_iff[OF fS fp])} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

388 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

389 
{assume "\<not> finite (UNIV :: 'n set)" then have ?thesis by (vector dimindex_def)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

390 
ultimately show ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

391 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

392 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

393 
lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

394 
by (auto simp add: le_less) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

395 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

396 
subsection {* Introduce norms, but defer many properties till we get square roots. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

397 
text{* FIXME : This is ugly *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

398 
defs (overloaded) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

399 
real_of_real_def [code inline, simp]: "real == id" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

400 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

401 
instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

402 
definition real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

403 
instance .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

404 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

405 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

406 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

407 
subsection{* The collapse of the general concepts to dimention one. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

408 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

409 
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

410 
by (vector dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

411 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

412 
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

413 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

414 
apply (erule_tac x= "x$1" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

415 
apply (simp only: vector_one[symmetric]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

416 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

417 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

418 
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

419 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

420 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

421 
text{* Metric *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

422 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

423 
definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

424 
"dist x y = norm (x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

425 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

426 
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1)  (y$1))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

427 
using dimindex_ge_1[of "UNIV :: 1 set"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

428 
by (auto simp add: norm_real dist_def vector_component Cart_lambda_beta[where ?'a = "1"] ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

429 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

430 
subsection {* A connectedness or intermediate value lemma with several applications. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

431 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

432 
lemma connected_real_lemma: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

433 
fixes f :: "real \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

434 
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

435 
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y  x) < d \<longrightarrow> dist(f y) (f x) < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

436 
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

437 
and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

438 
and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

439 
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

440 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

441 
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

442 
have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

443 
have Sub: "\<exists>y. isUb UNIV ?S y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

444 
apply (rule exI[where x= b]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

445 
using ab fb e12 by (auto simp add: isUb_def setle_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

446 
from reals_complete[OF Se Sub] obtain l where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

447 
l: "isLub UNIV ?S l"by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

448 
have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

449 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

450 
by (metis linorder_linear) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

451 
have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

452 
apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

453 
by (metis linorder_linear not_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

454 
have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z  x) < d" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

455 
have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

456 
have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

457 
{assume le2: "f l \<in> e2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

458 
from le2 fa fb e12 alb have la: "l \<noteq> a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

459 
hence lap: "l  a > 0" using alb by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

460 
from e2[rule_format, OF le2] obtain e where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

461 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

462 
from dst[OF alb e(1)] obtain d where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

463 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

464 
have "\<exists>d'. d' < d \<and> d' >0 \<and> l  d' > a" using lap d(1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

465 
apply ferrack by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

466 
then obtain d' where d': "d' > 0" "d' < d" "l  d' > a" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

467 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e2" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

468 
from th0[rule_format, of "l  d'"] d' have "f (l  d') \<in> e2" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

469 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

470 
have "f (l  d') \<in> e1" using ale1[rule_format, of "l d'"] d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

471 
ultimately have False using e12 alb d' by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

472 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

473 
{assume le1: "f l \<in> e1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

474 
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

475 
hence blp: "b  l > 0" using alb by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

476 
from e1[rule_format, OF le1] obtain e where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

477 
e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

478 
from dst[OF alb e(1)] obtain d where 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

479 
d: "d > 0" "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

480 
have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

481 
then obtain d' where d': "d' > 0" "d' < d" by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

482 
from d e have th0: "\<forall>y. \<bar>y  l\<bar> < d \<longrightarrow> f y \<in> e1" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

483 
hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

484 
with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

485 
with l d' have False 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

486 
by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

487 
ultimately show ?thesis using alb by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

488 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

489 

29881  490 
text{* One immediately useful corollary is the existence of square roots!  Should help to get rid of all the development of squareroot for reals as a special case @{typ "real^1"} *} 
29842
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

491 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

492 
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

493 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

494 
have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

495 
thus ?thesis by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

496 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

497 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

498 
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y  x) < d \<longrightarrow> abs(y * y  x * x) < e)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

499 
using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_def, rule_format, of e x] apply (auto simp add: power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

500 
apply (rule_tac x="s" in exI) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

501 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

502 
apply (erule_tac x=y in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

503 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

504 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

505 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

506 
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

507 
using real_sqrt_le_iff[of x "y^2"] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

508 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

509 
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

510 
using real_sqrt_le_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

511 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

512 
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

513 
using real_sqrt_less_mono[of "x^2" y] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

514 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

515 
lemma sqrt_even_pow2: assumes n: "even n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

516 
shows "sqrt(2 ^ n) = 2 ^ (n div 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

517 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

518 
from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

519 
by (auto simp add: nat_number) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

520 
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

521 
by (simp only: power_mult[symmetric] mult_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

522 
then show ?thesis using m by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

523 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

524 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

525 
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

526 
apply (cases "x = 0", simp_all) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

527 
using sqrt_divide_self_eq[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

528 
apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

529 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

530 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

531 
text{* Hence derive more interesting properties of the norm. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

532 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

533 
lemma norm_0: "norm (0::real ^ 'n) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

534 
by (simp add: real_vector_norm_def dot_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

535 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

536 
lemma norm_pos_le: "0 <= norm (x::real^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

537 
by (simp add: real_vector_norm_def dot_pos_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

538 
lemma norm_neg: " norm(x) = norm (x:: real ^ 'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

539 
by (simp add: real_vector_norm_def dot_lneg dot_rneg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

540 
lemma norm_sub: "norm(x  y) = norm(y  (x::real ^ 'n))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

541 
by (metis norm_neg minus_diff_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

542 
lemma norm_mul: "norm(a *s x) = abs(a) * norm x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

543 
by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

544 
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

545 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

546 
lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

547 
by (simp add: real_vector_norm_def dot_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

548 
lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

549 
by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

550 
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

551 
by (simp add: real_vector_norm_def dot_pos_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

552 
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

553 
lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

554 
by (metis norm_eq_0 norm_pos_le order_antisym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

555 
lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

556 
by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

557 
lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

558 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

559 
lemma vector_mul_rcancel: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

560 
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

561 
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

562 
by (metis vector_mul_lcancel) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

563 
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

564 
by (metis vector_mul_rcancel) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

565 
lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

566 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

567 
{assume "norm x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

568 
hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

569 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

570 
{assume "norm y = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

571 
hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

572 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

573 
{assume h: "norm x \<noteq> 0" "norm y \<noteq> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

574 
let ?z = "norm y *s x  norm x *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

575 
from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

576 
from dot_pos_le[of ?z] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

577 
have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

578 
apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

579 
by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

580 
hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

581 
by (simp add: field_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

582 
hence ?thesis using h by (simp add: power2_eq_square)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

583 
ultimately show ?thesis by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

584 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

585 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

586 
lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

587 
using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

588 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

589 
lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

590 
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "y"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

591 
by (simp add: real_abs_def dot_rneg norm_neg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

592 
lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

593 
unfolding real_vector_norm_def 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

594 
apply (rule real_le_lsqrt) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

595 
apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

596 
apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

597 
apply (simp add: dot_ladd dot_radd dot_sym ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

598 
by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

599 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

600 
lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

601 
using norm_triangle[of "y" "x  y"] by (simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

602 
lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

603 
by (metis order_trans norm_triangle) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

604 
lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

605 
by (metis basic_trans_rules(21) norm_triangle) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

606 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

607 
lemma setsum_delta: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

608 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

609 
shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

610 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

611 
let ?f = "(\<lambda>k. if k=a then b k else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

612 
{assume a: "a \<notin> S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

613 
hence "\<forall> k\<in> S. ?f k = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

614 
hence ?thesis using a by simp} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

615 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

616 
{assume a: "a \<in> S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

617 
let ?A = "S  {a}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

618 
let ?B = "{a}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

619 
have eq: "S = ?A \<union> ?B" using a by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

620 
have dj: "?A \<inter> ?B = {}" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

621 
from fS have fAB: "finite ?A" "finite ?B" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

622 
have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

623 
using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

624 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

625 
then have ?thesis using a by simp} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

626 
ultimately show ?thesis by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

627 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

628 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

629 
lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

630 
proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

631 
assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

632 
let ?S = "{1 .. dimindex(UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

633 
let ?f = "(\<lambda>k. if k = i then x$i ^2 else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

634 
have fS: "finite ?S" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

635 
from i setsum_delta[OF fS, of i "\<lambda>k. x$i ^ 2"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

636 
have th: "x$i^2 = setsum ?f ?S" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

637 
let ?g = "\<lambda>k. x$k * x$k" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

638 
{fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

639 
with setsum_mono[of ?S ?f ?g] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

640 
have "setsum ?f ?S \<le> setsum ?g ?S" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

641 
then show "x$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

642 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

643 
lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

644 
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> <= e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

645 
by (metis component_le_norm order_trans) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

646 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

647 
lemma norm_bound_component_lt: "norm(x::real ^ 'n) < e 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

648 
==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x$i\<bar> < e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

649 
by (metis component_le_norm basic_trans_rules(21)) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

650 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

651 
lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

652 
proof (simp add: real_vector_norm_def, rule real_le_lsqrt,simp add: dot_pos_le, simp add: setsum_mono, simp add: dot_def, induct "dimindex(UNIV::'n set)") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

653 
case 0 thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

654 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

655 
case (Suc n) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

656 
have th: "2 * (\<bar>x$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x$i\<bar>)) \<ge> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

657 
apply simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

658 
apply (rule mult_nonneg_nonneg) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

659 
by (simp_all add: setsum_abs_ge_zero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

660 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

661 
from Suc 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

662 
show ?case using th by (simp add: power2_eq_square ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

663 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

664 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

665 
lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

666 
by (simp add: norm_pos_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

667 
lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n)  norm y\<bar> <= norm(x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

668 
apply (simp add: abs_le_iff ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

669 
by (metis norm_triangle_sub norm_sub) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

670 
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

671 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

672 
lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

673 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

674 
lemma norm_eq: "norm (x::real ^'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

675 
by (simp add: order_eq_iff norm_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

676 
lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

677 
by (simp add: real_vector_norm_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

678 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

679 
text{* Squaring equations and inequalities involving norms. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

680 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

681 
lemma dot_square_norm: "x \<bullet> x = norm(x)^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

682 
by (simp add: real_vector_norm_def dot_pos_le ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

683 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

684 
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

685 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

686 
have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = y" by algebra 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

687 
show ?thesis using norm_pos_le[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

688 
apply (simp add: dot_square_norm th) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

689 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

690 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

691 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

692 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

693 
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

694 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

695 
have "x^2 \<le> y^2 \<longleftrightarrow> (x y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

696 
also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

697 
finally show ?thesis .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

698 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

699 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

700 
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

701 
using norm_pos_le[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

702 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

703 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

704 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

705 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

706 
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

707 
using norm_pos_le[of x] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

708 
apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

709 
apply arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

710 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

711 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

712 
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

713 
by (metis not_le norm_ge_square) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

714 
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

715 
by (metis norm_le_square not_less) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

716 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

717 
text{* Dot product in terms of the norm rather than conversely. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

718 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

719 
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2  norm x ^ 2  norm y ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

720 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

721 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

722 
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2)  norm(x  y) ^ 2) / 2" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

723 
by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

724 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

725 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

726 
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

727 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

728 
lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

729 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

730 
assume "?lhs" then show ?rhs by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

731 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

732 
assume ?rhs 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

733 
then have "x \<bullet> x  x \<bullet> y = 0 \<and> x \<bullet> y  y\<bullet> y = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

734 
hence "x \<bullet> (x  y) = 0 \<and> y \<bullet> (x  y) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

735 
by (simp add: dot_rsub dot_lsub dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

736 
then have "(x  y) \<bullet> (x  y) = 0" by (simp add: ring_simps dot_lsub dot_rsub) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

737 
then show "x = y" by (simp add: dot_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

738 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

739 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

740 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

741 
subsection{* General linear decision procedure for normed spaces. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

742 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

743 
lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

744 
apply (clarsimp simp add: norm_mul) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

745 
apply (rule mult_mono1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

746 
apply simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

747 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

748 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

749 
lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

750 
apply (rule norm_triangle_le) by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

751 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

752 
lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a  b \<ge> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

753 
by (simp add: ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

754 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

755 
lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

756 
lemma pth_2: "x  (y::real^'n) == x + y" by (atomize (full)) simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

757 
lemma pth_3: "(x::real^'n) == 1 *s x" by vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

758 
lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

759 
lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

760 
lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

761 
lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

762 
lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

763 
lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

764 
"c *s x + (d *s x + z) == (c + d) *s x + z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

765 
"(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

766 
lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

767 
lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

768 
"(c *s x + z) + d *s y == c *s x + (z + d *s y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

769 
"c *s x + (d *s y + z) == c *s x + (d *s y + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

770 
"(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

771 
by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

772 
lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

773 
"(c *s x + z) + d *s y == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

774 
"c *s x + (d *s y + z) == d *s y + (c *s x + z)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

775 
"(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

776 
lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

777 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

778 
lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

779 
by (atomize) (auto simp add: norm_pos_le) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

780 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

781 
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> x \<ge> 0" by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

782 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

783 
lemma norm_pths: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

784 
"(x::real ^'n) = y \<longleftrightarrow> norm (x  y) \<le> 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

785 
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x  y) \<le> 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

786 
using norm_pos_le[of "x  y"] by (auto simp add: norm_0 norm_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

787 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

788 
use "normarith.ML" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

789 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

790 
method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

791 
*} "Proves simple linear statements about vector norms" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

792 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

793 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

794 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

795 
text{* Hence more metric properties. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

796 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

797 
lemma dist_refl: "dist x x = 0" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

798 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

799 
lemma dist_sym: "dist x y = dist y x"by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

800 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

801 
lemma dist_pos_le: "0 <= dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

802 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

803 
lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

804 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

805 
lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

806 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

807 
lemma dist_eq_0: "dist x y = 0 \<longleftrightarrow> x = y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

808 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

809 
lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

810 
lemma dist_nz: "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

811 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

812 
lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

813 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

814 
lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

815 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

816 
lemma dist_triangle_half_l: "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 ==> dist x1 x2 < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

817 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

818 
lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 ==> dist x1 x2 < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

819 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

820 
lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

821 
by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

822 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

823 
lemma dist_mul: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

824 
unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

825 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

826 
lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

827 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

828 
lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

829 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

830 
instantiation "^" :: (monoid_add,type) monoid_add 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

831 
begin 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

832 
instance by (intro_classes) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

833 
end 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

834 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

835 
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

836 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

837 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

838 
apply (cases "finite S") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

839 
apply (rule finite_induct[of S]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

840 
apply (auto simp add: vector_component zero_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

841 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

842 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

843 
lemma setsum_clauses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

844 
shows "setsum f {} = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

845 
and "finite S \<Longrightarrow> setsum f (insert x S) = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

846 
(if x \<in> S then setsum f S else f x + setsum f S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

847 
by (auto simp add: insert_absorb) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

848 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

849 
lemma setsum_cmul: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

850 
fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

851 
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

852 
by (simp add: setsum_eq Cart_eq Cart_lambda_beta vector_component setsum_right_distrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

853 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

854 
lemma setsum_component: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

855 
fixes f:: " 'a \<Rightarrow> ('b::semiring_1) ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

856 
assumes i: "i \<in> {1 .. dimindex(UNIV:: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

857 
shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

858 
using i by (simp add: setsum_eq Cart_lambda_beta) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

859 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

860 
(* This needs finiteness assumption due to the definition of fold!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

861 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

862 
lemma setsum_superset: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

863 
assumes fb: "finite B" and ab: "A \<subseteq> B" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

864 
and f0: "\<forall>x \<in> B  A. f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

865 
shows "setsum f B = setsum f A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

866 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

867 
from ab fb have fa: "finite A" by (metis finite_subset) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

868 
from fb have fba: "finite (B  A)" by (metis finite_Diff) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

869 
have d: "A \<inter> (B  A) = {}" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

870 
from ab have b: "B = A \<union> (B  A)" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

871 
from setsum_Un_disjoint[OF fa fba d, of f] b 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

872 
setsum_0'[OF f0] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

873 
show "setsum f B = setsum f A" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

874 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

875 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

876 
lemma setsum_restrict_set: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

877 
assumes fA: "finite A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

878 
shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

879 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

880 
from fA have fab: "finite (A \<inter> B)" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

881 
have aba: "A \<inter> B \<subseteq> A" by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

882 
let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

883 
from setsum_superset[OF fA aba, of ?g] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

884 
show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

885 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

886 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

887 
lemma setsum_cases: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

888 
assumes fA: "finite A" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

889 
shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

890 
setsum f (A \<inter> B) + setsum g (A \<inter>  B)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

891 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

892 
have a: "A = A \<inter> B \<union> A \<inter> B" "(A \<inter> B) \<inter> (A \<inter> B) = {}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

893 
by blast+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

894 
from fA 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

895 
have f: "finite (A \<inter> B)" "finite (A \<inter> B)" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

896 
let ?g = "\<lambda>x. if x \<in> B then f x else g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

897 
from setsum_Un_disjoint[OF f a(2), of ?g] a(1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

898 
show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

899 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

900 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

901 
lemma setsum_norm: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

902 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

903 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

904 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

905 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

906 
case 1 thus ?case by (simp add: norm_zero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

907 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

908 
case (2 x S) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

909 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

910 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

911 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

912 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

913 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

914 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

915 
lemma real_setsum_norm: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

916 
fixes f :: "'a \<Rightarrow> real ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

917 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

918 
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

919 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

920 
case 1 thus ?case by simp norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

921 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

922 
case (2 x S) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

923 
from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" apply (simp add: norm_triangle_ineq) by norm 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

924 
also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

925 
using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

926 
finally show ?case using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

927 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

928 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

929 
lemma setsum_norm_le: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

930 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

931 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

932 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

933 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

934 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

935 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

936 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

937 
then show ?thesis using setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

938 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

939 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

940 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

941 
lemma real_setsum_norm_le: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

942 
fixes f :: "'a \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

943 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

944 
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

945 
shows "norm (setsum f S) \<le> setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

946 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

947 
from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

948 
by  (rule setsum_mono, simp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

949 
then show ?thesis using real_setsum_norm[OF fS, of f] fg 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

950 
by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

951 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

952 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

953 
lemma setsum_norm_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

954 
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

955 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

956 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

957 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

958 
using setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

959 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

960 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

961 
lemma real_setsum_norm_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

962 
fixes f :: "'a \<Rightarrow> real ^ 'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

963 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

964 
and K: "\<forall>x \<in> S. norm (f x) \<le> K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

965 
shows "norm (setsum f S) \<le> of_nat (card S) * K" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

966 
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

967 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

968 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

969 
lemma setsum_vmul: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

970 
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

971 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

972 
shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

973 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

974 
case 1 then show ?case by (simp add: vector_smult_lzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

975 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

976 
case (2 x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

977 
from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

978 
by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

979 
also have "\<dots> = f x *s v + setsum f F *s v" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

980 
by (simp add: vector_sadd_rdistrib) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

981 
also have "\<dots> = setsum (\<lambda>x. f x *s v) (insert x F)" using "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

982 
finally show ?case . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

983 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

984 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

985 
(* FIXME : Problem thm setsum_vmul[of _ "f:: 'a \<Rightarrow> real ^'n"]  
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

986 
Get rid of *s and use real_vector instead! Also prove that ^ creates a real_vector !! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

987 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

988 
lemma setsum_add_split: assumes mn: "(m::nat) \<le> n + 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

989 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

990 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

991 
let ?A = "{m .. n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

992 
let ?B = "{n + 1 .. n + p}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

993 
have eq: "{m .. n+p} = ?A \<union> ?B" using mn by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

994 
have d: "?A \<inter> ?B = {}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

995 
from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

996 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

997 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

998 
lemma setsum_reindex_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

999 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1000 
and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1001 
shows "setsum h (f ` S) = setsum (h o f) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1002 
using nz 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1003 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1004 
case 1 thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1005 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1006 
case (2 x F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1007 
{assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1008 
then obtain y where y: "y \<in> F" "f x = f y" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1009 
from "2.hyps" y have xy: "x \<noteq> y" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1010 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1011 
from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1012 
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1013 
also have "\<dots> = setsum (h o f) (insert x F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1014 
using "2.hyps" "2.prems" h0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1015 
finally have ?case .} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1016 
moreover 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1017 
{assume fxF: "f x \<notin> f ` F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1018 
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1019 
using fxF "2.hyps" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1020 
also have "\<dots> = setsum (h o f) (insert x F)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1021 
using "2.hyps" "2.prems" fxF 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1022 
apply auto apply metis done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1023 
finally have ?case .} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1024 
ultimately show ?case by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1025 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1026 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1027 
lemma setsum_Un_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1028 
assumes fS: "finite S" and fF: "finite F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1029 
and f: "\<forall> x\<in> S \<inter> F . f x = (0::'a::ab_group_add)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1030 
shows "setsum f (S \<union> F) = setsum f S + setsum f F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1031 
using setsum_Un[OF fS fF, of f] setsum_0'[OF f] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1032 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1033 
lemma setsum_natinterval_left: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1034 
assumes mn: "(m::nat) <= n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1035 
shows "setsum f {m..n} = f m + setsum f {m + 1..n}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1036 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1037 
from mn have "{m .. n} = insert m {m+1 .. n}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1038 
then show ?thesis by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1039 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1040 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1041 
lemma setsum_natinterval_difff: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1042 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1043 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1044 
(if m <= n then f m  f(n + 1) else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1045 
by (induct n, auto simp add: ring_simps not_le le_Suc_eq) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1046 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1047 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1048 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1049 
lemma setsum_setsum_restrict: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1050 
"finite S \<Longrightarrow> finite T \<Longrightarrow> setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y\<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1051 
apply (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1052 
by (rule setsum_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1053 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1054 
lemma setsum_image_gen: assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1055 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1056 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1057 
{fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1058 
note th0 = this 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1059 
have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1060 
apply (rule setsum_cong2) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1061 
by (simp add: th0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1062 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1063 
apply (rule setsum_setsum_restrict[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1064 
by (rule finite_imageI[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1065 
finally show ?thesis . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1066 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1067 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1068 
(* FIXME: Here too need stupid finiteness assumption on T!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1069 
lemma setsum_group: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1070 
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1071 
shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1072 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1073 
apply (subst setsum_image_gen[OF fS, of g f]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1074 
apply (rule setsum_superset[OF fT fST]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1075 
by (auto intro: setsum_0') 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1076 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1077 
(* FIXME: Change the name to fold_image\<dots> *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1078 
lemma (in comm_monoid_mult) fold_1': "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1079 
apply (induct set: finite) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1080 
apply simp by (auto simp add: fold_image_insert) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1081 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1082 
lemma (in comm_monoid_mult) fold_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1083 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1084 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1085 
shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1086 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1087 
have "fold_image op * f 1 (S \<inter> T) = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1088 
apply (rule fold_1') 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1089 
using fS fT I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1090 
with fold_image_Un_Int[OF fS fT] show ?thesis by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1091 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1092 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1093 
lemma setsum_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1094 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1095 
and I0: "\<forall>x \<in> S\<inter>T. f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1096 
shows "setsum f (S \<union> T) = setsum f S + setsum f T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1097 
using fS fT 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1098 
apply (simp add: setsum_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1099 
apply (rule comm_monoid_add.fold_union_nonzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1100 
using I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1101 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1102 
lemma setprod_union_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1103 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1104 
and I0: "\<forall>x \<in> S\<inter>T. f x = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1105 
shows "setprod f (S \<union> T) = setprod f S * setprod f T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1106 
using fS fT 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1107 
apply (simp add: setprod_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1108 
apply (rule fold_union_nonzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1109 
using I0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1110 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1111 
lemma setsum_unions_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1112 
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1113 
and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1114 
shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1115 
using fSS f0 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1116 
proof(induct rule: finite_induct[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1117 
case 1 thus ?case by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1118 
next 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1119 
case (2 T F) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1120 
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1121 
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1122 
from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1123 
from "2.prems" TF fTF 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1124 
show ?case 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1125 
by (auto simp add: H[symmetric] intro: setsum_union_nonzero[OF fTF(1) fUF, of f]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1126 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1127 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1128 
(* FIXME : Copied from Pocklington  should be moved to Finite_Set!!!!!!!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1129 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1130 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1131 
lemma (in comm_monoid_mult) fold_related: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1132 
assumes Re: "R e e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1133 
and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1134 
and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1135 
shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1136 
using fS by (rule finite_subset_induct) (insert assms, auto) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1137 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1138 
(* FIXME: I think we can get rid of the finite assumption!! *) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1139 
lemma (in comm_monoid_mult) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1140 
fold_eq_general: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1141 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1142 
and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1143 
and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1144 
shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1145 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1146 
from h f12 have hS: "h ` S = S'" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1147 
{fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1148 
from f12 h H have "x = y" by auto } 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1149 
hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1150 
from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1151 
from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1152 
also have "\<dots> = fold_image (op *) (f2 o h) e S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1153 
using fold_image_reindex[OF fS hinj, of f2 e] . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1154 
also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1155 
by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1156 
finally show ?thesis .. 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1157 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1158 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1159 
lemma (in comm_monoid_mult) fold_eq_general_inverses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1160 
assumes fS: "finite S" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1161 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1162 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1163 
shows "fold_image (op *) f e S = fold_image (op *) g e T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1164 
using fold_eq_general[OF fS, of T h g f e] kh hk by metis 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1165 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1166 
lemma setsum_eq_general_reverses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1167 
assumes fS: "finite S" and fT: "finite T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1168 
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1169 
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1170 
shows "setsum f S = setsum g T" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1171 
apply (simp add: setsum_def fS fT) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1172 
apply (rule comm_monoid_add.fold_eq_general_inverses[OF fS]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1173 
apply (erule kh) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1174 
apply (erule hk) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1175 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1176 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1177 
lemma vsum_norm_allsubsets_bound: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1178 
fixes f:: "'a \<Rightarrow> real ^'n" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1179 
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1180 
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real (dimindex(UNIV :: 'n set)) * e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1181 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1182 
let ?d = "real (dimindex (UNIV ::'n set))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1183 
let ?nf = "\<lambda>x. norm (f x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1184 
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1185 
have th0: "setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P = setsum (\<lambda>i. setsum (\<lambda>x. \<bar>f x $ i\<bar>) P) ?U" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1186 
by (rule setsum_commute) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1187 
have th1: "2 * ?d * e = of_nat (card ?U) * (2 * e)" by (simp add: real_of_nat_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1188 
have "setsum ?nf P \<le> setsum (\<lambda>x. setsum (\<lambda>i. \<bar>f x $ i\<bar>) ?U) P" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1189 
apply (rule setsum_mono) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1190 
by (rule norm_le_l1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1191 
also have "\<dots> \<le> 2 * ?d * e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1192 
unfolding th0 th1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1193 
proof(rule setsum_bounded) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1194 
fix i assume i: "i \<in> ?U" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1195 
let ?Pp = "{x. x\<in> P \<and> f x $ i \<ge> 0}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1196 
let ?Pn = "{x. x \<in> P \<and> f x $ i < 0}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1197 
have thp: "P = ?Pp \<union> ?Pn" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1198 
have thp0: "?Pp \<inter> ?Pn ={}" by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1199 
have PpP: "?Pp \<subseteq> P" and PnP: "?Pn \<subseteq> P" by blast+ 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1200 
have Ppe:"setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp \<le> e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1201 
using i component_le_norm[OF i, of "setsum (\<lambda>x. f x) ?Pp"] fPs[OF PpP] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1202 
by (auto simp add: setsum_component intro: abs_le_D1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1203 
have Pne: "setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn \<le> e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1204 
using i component_le_norm[OF i, of "setsum (\<lambda>x.  f x) ?Pn"] fPs[OF PnP] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1205 
by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1206 
have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1207 
apply (subst thp) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1208 
apply (rule setsum_Un_nonzero) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1209 
using fP thp0 by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1210 
also have "\<dots> \<le> 2*e" using Pne Ppe by arith 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1211 
finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1212 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1213 
finally show ?thesis . 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1214 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1215 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1216 
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S " 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1217 
by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1218 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1219 
lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S " 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1220 
by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1221 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1222 
subsection{* Basis vectors in coordinate directions. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1223 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1224 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1225 
definition "basis k = (\<chi> i. if i = k then 1 else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1226 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1227 
lemma delta_mult_idempotent: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1228 
"(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1229 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1230 
lemma norm_basis: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1231 
assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1232 
shows "norm (basis k :: real ^'n) = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1233 
using k 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1234 
apply (simp add: basis_def real_vector_norm_def dot_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1235 
apply (vector delta_mult_idempotent) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1236 
using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "k" "\<lambda>k. 1::real"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1237 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1238 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1239 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1240 
lemma norm_basis_1: "norm(basis 1 :: real ^'n) = 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1241 
apply (simp add: basis_def real_vector_norm_def dot_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1242 
apply (vector delta_mult_idempotent) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1243 
using setsum_delta[of "{1 .. dimindex (UNIV :: 'n set)}" "1" "\<lambda>k. 1::real"] dimindex_nonzero[of "UNIV :: 'n set"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1244 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1245 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1246 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1247 
lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1248 
apply (rule exI[where x="c *s basis 1"]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1249 
by (simp only: norm_mul norm_basis_1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1250 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1251 
lemma vector_choose_dist: assumes e: "0 <= e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1252 
shows "\<exists>(y::real^'n). dist x y = e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1253 
proof 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1254 
from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1255 
by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1256 
then have "dist x (x  c) = e" by (simp add: dist_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1257 
then show ?thesis by blast 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1258 
qed 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1259 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1260 
lemma basis_inj: "inj_on (basis :: nat \<Rightarrow> real ^'n) {1 .. dimindex (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1261 
by (auto simp add: inj_on_def basis_def Cart_eq Cart_lambda_beta) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1262 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1263 
lemma basis_component: "i \<in> {1 .. dimindex(UNIV:: 'n set)} ==> (basis k ::('a::semiring_1)^'n)$i = (if k=i then 1 else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1264 
by (simp add: basis_def Cart_lambda_beta) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1265 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1266 
lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1267 
by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1268 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1269 
lemma basis_expansion: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1270 
"setsum (\<lambda>i. (x$i) *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1271 
by (auto simp add: Cart_eq basis_component[where ?'n = "'n"] setsum_component vector_component cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1272 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1273 
lemma basis_expansion_unique: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1274 
"setsum (\<lambda>i. f i *s basis i) {1 .. dimindex (UNIV :: 'n set)} = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i\<in>{1 .. dimindex(UNIV:: 'n set)}. f i = x$i)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1275 
by (simp add: Cart_eq setsum_component vector_component basis_component setsum_delta cond_value_iff cong del: if_weak_cong) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1276 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1277 
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1278 
by auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1279 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1280 
lemma dot_basis: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1281 
assumes i: "i \<in> {1 .. dimindex (UNIV :: 'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1282 
shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1283 
using i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1284 
by (auto simp add: dot_def basis_def Cart_lambda_beta cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1285 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1286 
lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> i \<notin> {1..dimindex(UNIV ::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1287 
by (auto simp add: Cart_eq basis_component zero_index) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1288 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1289 
lemma basis_nonzero: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1290 
assumes k: "k \<in> {1 .. dimindex(UNIV ::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1291 
shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1292 
using k by (simp add: basis_eq_0) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1293 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1294 
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1295 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1296 
apply (erule_tac x="basis i" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1297 
apply (simp add: dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1298 
apply (subgoal_tac "y = z") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1299 
apply simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1300 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1301 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1302 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1303 
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1304 
apply (auto simp add: Cart_eq dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1305 
apply (erule_tac x="basis i" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1306 
apply (simp add: dot_basis) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1307 
apply (subgoal_tac "x = y") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1308 
apply simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1309 
apply vector 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1310 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1311 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1312 
subsection{* Orthogonality. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1313 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1314 
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1315 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1316 
lemma orthogonal_basis: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1317 
assumes i:"i \<in> {1 .. dimindex(UNIV ::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1318 
shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x$i = (0::'a::ring_1)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1319 
using i 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1320 
by (auto simp add: orthogonal_def dot_def basis_def Cart_lambda_beta cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1321 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1322 
lemma orthogonal_basis_basis: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1323 
assumes i:"i \<in> {1 .. dimindex(UNIV ::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1324 
and j: "j \<in> {1 .. dimindex(UNIV ::'n set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1325 
shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1326 
unfolding orthogonal_basis[OF i] basis_component[OF i] by simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1327 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1328 
(* FIXME : Maybe some of these require less than comm_ring, but not all*) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1329 
lemma orthogonal_clauses: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1330 
"orthogonal a (0::'a::comm_ring ^'n)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1331 
"orthogonal a x ==> orthogonal a (c *s x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1332 
"orthogonal a x ==> orthogonal a (x)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1333 
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1334 
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x  y)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1335 
"orthogonal 0 a" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1336 
"orthogonal x a ==> orthogonal (c *s x) a" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1337 
"orthogonal x a ==> orthogonal (x) a" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1338 
"orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x + y) a" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1339 
"orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x  y) a" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1340 
unfolding orthogonal_def dot_rneg dot_rmult dot_radd dot_rsub 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1341 
dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1342 
by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1343 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1344 
lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1345 
by (simp add: orthogonal_def dot_sym) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1346 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1347 
subsection{* Explicit vector construction from lists. *} 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1348 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1349 
lemma Cart_lambda_beta_1[simp]: "(Cart_lambda g)$1 = g 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1350 
apply (rule Cart_lambda_beta[rule_format]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1351 
using dimindex_ge_1 apply auto done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1352 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1353 
lemma Cart_lambda_beta_1'[simp]: "(Cart_lambda g)$(Suc 0) = g 1" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1354 
by (simp only: One_nat_def[symmetric] Cart_lambda_beta_1) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1355 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1356 
definition "vector l = (\<chi> i. if i <= length l then l ! (i  1) else 0)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1357 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1358 
lemma vector_1: "(vector[x]) $1 = x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1359 
using dimindex_ge_1 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1360 
by (auto simp add: vector_def Cart_lambda_beta[rule_format]) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1361 
lemma dimindex_2[simp]: "2 \<in> {1 .. dimindex (UNIV :: 2 set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1362 
by (auto simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1363 
lemma dimindex_2'[simp]: "2 \<in> {Suc 0 .. dimindex (UNIV :: 2 set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1364 
by (auto simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1365 
lemma dimindex_3[simp]: "2 \<in> {1 .. dimindex (UNIV :: 3 set)}" "3 \<in> {1 .. dimindex (UNIV :: 3 set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1366 
by (auto simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1367 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1368 
lemma dimindex_3'[simp]: "2 \<in> {Suc 0 .. dimindex (UNIV :: 3 set)}" "3 \<in> {Suc 0 .. dimindex (UNIV :: 3 set)}" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1369 
by (auto simp add: dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1370 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1371 
lemma vector_2: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1372 
"(vector[x,y]) $1 = x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1373 
"(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1374 
apply (simp add: vector_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1375 
using Cart_lambda_beta[rule_format, OF dimindex_2, of "\<lambda>i. if i \<le> length [x,y] then [x,y] ! (i  1) else (0::'a)"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1376 
apply (simp only: vector_def ) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1377 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1378 
done 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1379 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1380 
lemma vector_3: 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1381 
"(vector [x,y,z] ::('a::zero)^3)$1 = x" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1382 
"(vector [x,y,z] ::('a::zero)^3)$2 = y" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1383 
"(vector [x,y,z] ::('a::zero)^3)$3 = z" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1384 
apply (simp_all add: vector_def Cart_lambda_beta dimindex_3) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1385 
using Cart_lambda_beta[rule_format, OF dimindex_3(1), of "\<lambda>i. if i \<le> length [x,y,z] then [x,y,z] ! (i  1) else (0::'a)"] using Cart_lambda_beta[rule_format, OF dimindex_3(2), of "\<lambda>i. if i \<le> length [x,y,z] then [x,y,z] ! (i  1) else (0::'a)"] 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1386 
by simp_all 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1387 

4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1388 
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))" 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1389 
apply auto 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1390 
apply (erule_tac x="v$1" in allE) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1391 
apply (subgoal_tac "vector [v$1] = v") 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1392 
apply simp 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
chaieb
parents:
diff
changeset

1393 
by (vector vector_def dimindex_def) 
4ac60c7d9b78
(Real) Vectors in Euclidean space, and elementary linear algebra.
< 