author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 53717 | 6eb85a1cb406 |
child 58877 | 262572d90bc6 |
permissions | -rw-r--r-- |
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 |
begin |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
10 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
11 |
lemma norm_cmul_rule_thm: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
12 |
fixes x :: "'a::real_normed_vector" |
53717 | 13 |
shows "b \<ge> norm x \<Longrightarrow> \<bar>c\<bar> * b \<ge> norm (scaleR c x)" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
14 |
unfolding norm_scaleR |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
15 |
apply (erule mult_left_mono) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
16 |
apply simp |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
17 |
done |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
18 |
|
53717 | 19 |
(* FIXME: Move all these theorems into the ML code using lemma antiquotation *) |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
20 |
lemma norm_add_rule_thm: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
|
53717 | 25 |
lemma ge_iff_diff_ge_0: |
26 |
fixes a :: "'a::linordered_ring" |
|
27 |
shows "a \<ge> b \<equiv> a - b \<ge> 0" |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
28 |
by (simp add: field_simps) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
29 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
30 |
lemma pth_1: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
31 |
fixes x :: "'a::real_normed_vector" |
53717 | 32 |
shows "x \<equiv> scaleR 1 x" by simp |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
33 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
34 |
lemma pth_2: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
35 |
fixes x :: "'a::real_normed_vector" |
53717 | 36 |
shows "x - y \<equiv> x + -y" |
37 |
by (atomize (full)) simp |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
38 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
39 |
lemma pth_3: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
40 |
fixes x :: "'a::real_normed_vector" |
53717 | 41 |
shows "- x \<equiv> scaleR (-1) x" |
42 |
by simp |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
43 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
44 |
lemma pth_4: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
45 |
fixes x :: "'a::real_normed_vector" |
53717 | 46 |
shows "scaleR 0 x \<equiv> 0" |
47 |
and "scaleR c 0 = (0::'a)" |
|
48 |
by simp_all |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
49 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
50 |
lemma pth_5: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
51 |
fixes x :: "'a::real_normed_vector" |
53717 | 52 |
shows "scaleR c (scaleR d x) \<equiv> scaleR (c * d) x" |
53 |
by simp |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
54 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
55 |
lemma pth_6: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
56 |
fixes x :: "'a::real_normed_vector" |
53717 | 57 |
shows "scaleR c (x + y) \<equiv> scaleR c x + scaleR c y" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
58 |
by (simp add: scaleR_right_distrib) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
59 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
60 |
lemma pth_7: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
61 |
fixes x :: "'a::real_normed_vector" |
53717 | 62 |
shows "0 + x \<equiv> x" |
63 |
and "x + 0 \<equiv> x" |
|
64 |
by simp_all |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
65 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
66 |
lemma pth_8: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
67 |
fixes x :: "'a::real_normed_vector" |
53717 | 68 |
shows "scaleR c x + scaleR d x \<equiv> scaleR (c + d) x" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
69 |
by (simp add: scaleR_left_distrib) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
70 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
71 |
lemma pth_9: |
53717 | 72 |
fixes x :: "'a::real_normed_vector" |
73 |
shows "(scaleR c x + z) + scaleR d x \<equiv> scaleR (c + d) x + z" |
|
74 |
and "scaleR c x + (scaleR d x + z) \<equiv> scaleR (c + d) x + z" |
|
75 |
and "(scaleR c x + w) + (scaleR d x + z) \<equiv> scaleR (c + d) x + (w + z)" |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
76 |
by (simp_all add: algebra_simps) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
77 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
78 |
lemma pth_a: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
79 |
fixes x :: "'a::real_normed_vector" |
53717 | 80 |
shows "scaleR 0 x + y \<equiv> y" |
81 |
by simp |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
82 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
83 |
lemma pth_b: |
53717 | 84 |
fixes x :: "'a::real_normed_vector" |
85 |
shows "scaleR c x + scaleR d y \<equiv> scaleR c x + scaleR d y" |
|
86 |
and "(scaleR c x + z) + scaleR d y \<equiv> scaleR c x + (z + scaleR d y)" |
|
87 |
and "scaleR c x + (scaleR d y + z) \<equiv> scaleR c x + (scaleR d y + z)" |
|
88 |
and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR c x + (w + (scaleR d y + z))" |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
89 |
by (simp_all add: algebra_simps) |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
90 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
91 |
lemma pth_c: |
53717 | 92 |
fixes x :: "'a::real_normed_vector" |
93 |
shows "scaleR c x + scaleR d y \<equiv> scaleR d y + scaleR c x" |
|
94 |
and "(scaleR c x + z) + scaleR d y \<equiv> scaleR d y + (scaleR c x + z)" |
|
95 |
and "scaleR c x + (scaleR d y + z) \<equiv> scaleR d y + (scaleR c x + z)" |
|
96 |
and "(scaleR c x + w) + (scaleR d y + z) \<equiv> scaleR d y + ((scaleR c x + w) + z)" |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
97 |
by (simp_all add: algebra_simps) |
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 pth_d: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
100 |
fixes x :: "'a::real_normed_vector" |
53717 | 101 |
shows "x + 0 \<equiv> x" |
102 |
by simp |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
103 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
104 |
lemma norm_imp_pos_and_ge: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
105 |
fixes x :: "'a::real_normed_vector" |
53717 | 106 |
shows "norm x \<equiv> n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
107 |
by atomize auto |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
108 |
|
53717 | 109 |
lemma real_eq_0_iff_le_ge_0: |
110 |
fixes x :: real |
|
111 |
shows "x = 0 \<equiv> x \<ge> 0 \<and> - x \<ge> 0" |
|
112 |
by arith |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
113 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
114 |
lemma norm_pths: |
53717 | 115 |
fixes x :: "'a::real_normed_vector" |
116 |
shows "x = y \<longleftrightarrow> norm (x - y) \<le> 0" |
|
117 |
and "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)" |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
118 |
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
|
119 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
120 |
lemmas arithmetic_simps = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
121 |
arith_simps |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
122 |
add_numeral_special |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
123 |
add_neg_numeral_special |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
124 |
mult_1_left |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
125 |
mult_1_right |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44516
diff
changeset
|
126 |
|
48891 | 127 |
ML_file "normarith.ML" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
128 |
|
53717 | 129 |
method_setup norm = {* |
130 |
Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
131 |
*} "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
|
132 |
|
53717 | 133 |
|
134 |
text {* Hence more metric properties. *} |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
135 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
136 |
lemma dist_triangle_add: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
137 |
fixes x y x' y' :: "'a::real_normed_vector" |
53717 | 138 |
shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'" |
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
139 |
by norm |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
140 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
141 |
lemma dist_triangle_add_half: |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
142 |
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
|
143 |
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
|
144 |
by norm |
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
145 |
|
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
diff
changeset
|
146 |
end |