author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 48112  b1240319ef15 
permissions  rwrr 
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

1 
(* Title: HOL/Multivariate_Analysis/Norm_Arith.thy 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

3 
*) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

4 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

5 
header {* General linear decision procedure for normed spaces *} 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

6 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

7 
theory Norm_Arith 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

8 
imports "~~/src/HOL/Library/Sum_of_Squares" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

9 
uses ("normarith.ML") 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

10 
begin 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

11 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

12 
lemma norm_cmul_rule_thm: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

13 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

14 
shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

15 
unfolding norm_scaleR 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

16 
apply (erule mult_left_mono) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

17 
apply simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

18 
done 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

19 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

20 
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

21 
lemma norm_add_rule_thm: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

22 
fixes x1 x2 :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

23 
shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

24 
by (rule order_trans [OF norm_triangle_ineq add_mono]) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

25 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

26 
lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a  b \<ge> 0" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

27 
by (simp add: field_simps) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

28 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

29 
lemma pth_1: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

30 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

31 
shows "x == scaleR 1 x" by simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

32 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

33 
lemma pth_2: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

34 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

35 
shows "x  y == x + y" by (atomize (full)) simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

36 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

37 
lemma pth_3: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

38 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

39 
shows " x == scaleR (1) x" by simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

40 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

41 
lemma pth_4: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

42 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

43 
shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

44 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

45 
lemma pth_5: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

46 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

47 
shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

48 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

49 
lemma pth_6: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

50 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

51 
shows "scaleR c (x + y) == scaleR c x + scaleR c y" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

52 
by (simp add: scaleR_right_distrib) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

53 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

54 
lemma pth_7: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

55 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

56 
shows "0 + x == x" and "x + 0 == x" by simp_all 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

57 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

58 
lemma pth_8: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

59 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

60 
shows "scaleR c x + scaleR d x == scaleR (c + d) x" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

61 
by (simp add: scaleR_left_distrib) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

62 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

63 
lemma pth_9: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

64 
fixes x :: "'a::real_normed_vector" shows 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

65 
"(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

66 
"scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

67 
"(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

68 
by (simp_all add: algebra_simps) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

69 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

70 
lemma pth_a: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

71 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

72 
shows "scaleR 0 x + y == y" by simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

73 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

74 
lemma pth_b: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

75 
fixes x :: "'a::real_normed_vector" shows 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

76 
"scaleR c x + scaleR d y == scaleR c x + scaleR d y" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

77 
"(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

78 
"scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

79 
"(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

80 
by (simp_all add: algebra_simps) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

81 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

82 
lemma pth_c: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

83 
fixes x :: "'a::real_normed_vector" shows 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

84 
"scaleR c x + scaleR d y == scaleR d y + scaleR c x" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

85 
"(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

86 
"scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

87 
"(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

88 
by (simp_all add: algebra_simps) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

89 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

90 
lemma pth_d: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

91 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

92 
shows "x + 0 == x" by simp 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

93 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

94 
lemma norm_imp_pos_and_ge: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

95 
fixes x :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

96 
shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

97 
by atomize auto 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

98 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

99 
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> x \<ge> 0" by arith 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

100 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

101 
lemma norm_pths: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

102 
fixes x :: "'a::real_normed_vector" shows 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

103 
"x = y \<longleftrightarrow> norm (x  y) \<le> 0" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

104 
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x  y) \<le> 0)" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

105 
using norm_ge_zero[of "x  y"] by auto 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

106 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

107 
lemmas arithmetic_simps = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

108 
arith_simps 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

109 
add_numeral_special 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

110 
add_neg_numeral_special 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

111 
add_0_left 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

112 
add_0_right 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

113 
mult_zero_left 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

114 
mult_zero_right 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

115 
mult_1_left 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

116 
mult_1_right 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset

117 

44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

118 
use "normarith.ML" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

119 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

120 
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

121 
*} "prove simple linear statements about vector norms" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

122 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

123 
text{* Hence more metric properties. *} 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

124 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

125 
lemma dist_triangle_add: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

126 
fixes x y x' y' :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

127 
shows "dist (x + y) (x' + y') <= dist x x' + dist y y'" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

128 
by norm 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

129 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

130 
lemma dist_triangle_add_half: 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

131 
fixes x x' y y' :: "'a::real_normed_vector" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

132 
shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e" 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

133 
by norm 
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

134 

d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset

135 
end 