author huffman Thu, 04 Jun 2009 14:32:00 -0700 changeset 31445 c8a474a919a7 parent 31440 ee1d5bec4ce3 child 31446 2d91b2416de8
generalize norm method to work over class real_normed_vector
```--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu Jun 04 14:32:00 2009 -0700
@@ -39,7 +39,9 @@

lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto

-lemma vector_unminus_smult[simp]: "(-1::real) *s x = -x" unfolding pth_3[symmetric] by simp
+lemma vector_unminus_smult[simp]: "(-1::real) *s x = -x"
+  unfolding vector_sneg_minus1 by simp
+  (* TODO: move to Euclidean_Space.thy *)

lemma setsum_delta_notmem: assumes "x\<notin>s"
shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
@@ -302,7 +304,7 @@
apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
unfolding setsum_clauses(2)[OF `?as`]  apply simp
-	unfolding vu and * and pth_4(1)
+	unfolding vu and * and vector_smult_lzero
by (auto simp add: setsum_delta[OF `?as`])
next
case False
@@ -1178,7 +1180,8 @@
unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto
moreover have "(\<Sum>v\<in>s. u v *s v + (t * w v) *s v) - (u a *s a + (t * w a) *s a) = y"
unfolding setsum_addf obt(6) vector_smult_assoc[THEN sym] setsum_cmul wv(4)
-      by (metis diff_0_right a(2) pth_5 pth_8 pth_d vector_mul_eq_0)
+      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]]
ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(1-3) and t and a by (auto simp add: *)
thus False using smallest[THEN spec[where x="n - 1"]] by auto qed```
```--- a/src/HOL/Library/Euclidean_Space.thy	Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Thu Jun 04 14:32:00 2009 -0700
@@ -1060,54 +1060,103 @@

subsection{* General linear decision procedure for normed spaces. *}

-lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)"
-  apply (clarsimp simp add: norm_mul)
-  apply (rule mult_mono1)
-  apply simp_all
+lemma norm_cmul_rule_thm:
+  fixes x :: "'a::real_normed_vector"
+  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+  unfolding norm_scaleR
+  apply (erule mult_mono1)
+  apply simp
done

(* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"
-  apply (rule norm_triangle_le) by simp
+  fixes x1 x2 :: "'a::real_normed_vector"
+  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+  by (rule order_trans [OF norm_triangle_ineq add_mono])

lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"

-lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid)
-lemma pth_2: "x - (y::real^'n) == x + -y" by (atomize (full)) simp
-lemma pth_3: "(-x::real^'n) == -1 *s x" by vector
-lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+
-lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector
-lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps)
-lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all
-lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps)
-lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z"
-  "c *s x + (d *s x + z) == (c + d) *s x + z"
-  "(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+
-lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector
-lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y"
-  "(c *s x + z) + d *s y == c *s x + (z + d *s y)"
-  "c *s x + (d *s y + z) == c *s x + (d *s y + z)"
-  "(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))"
-  by ((atomize (full)), vector)+
-lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x"
-  "(c *s x + z) + d *s y == d *s y + (c *s x + z)"
-  "c *s x + (d *s y + z) == d *s y + (c *s x + z)"
-  "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+
-lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
-
-lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
-  by (atomize) (auto simp add: norm_ge_zero)
+lemma pth_1:
+  fixes x :: "'a::real_normed_vector"
+  shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+  fixes x :: "'a::real_normed_vector"
+  shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+  fixes x :: "'a::real_normed_vector"
+  shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+
+lemma pth_7:
+  fixes x :: "'a::real_normed_vector"
+  shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+
+lemma pth_9:
+  fixes x :: "'a::real_normed_vector" shows
+  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+
+lemma pth_a:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+
+lemma pth_c:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+
+lemma pth_d:
+  fixes x :: "'a::real_normed_vector"
+  shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+  fixes x :: "'a::real_normed_vector"
+  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+  by atomize auto

lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith

lemma norm_pths:
-  "(x::real ^'n::finite) = y \<longleftrightarrow> norm (x - y) \<le> 0"
+  fixes x :: "'a::real_normed_vector" shows
+  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
"x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
using norm_ge_zero[of "x - y"] by auto

lemma vector_dist_norm:
-  fixes x y :: "real ^ _"
+  fixes x :: "'a::real_normed_vector"
shows "dist x y = norm (x - y)"
by (rule dist_norm)

@@ -1117,7 +1166,6 @@
*} "Proves simple linear statements about vector norms"

-
text{* Hence more metric properties. *}

lemma dist_triangle_alt:
@@ -1158,7 +1206,7 @@
fixes x y x' y' :: "'a::real_normed_vector"
shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-unfolding dist_norm by (rule norm_diff_triangle_ineq)
+  by norm

lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
@@ -1166,7 +1214,7 @@
fixes x x' y y' :: "'a::real_normed_vector"
shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
-by (rule le_less_trans [OF dist_triangle_add], simp)
+  by norm

lemma setsum_component [simp]:
fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"```
```--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 14:32:00 2009 -0700
@@ -3401,11 +3401,16 @@
thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
qed

+lemma dist_minus:
+  fixes x y :: "'a::real_normed_vector"
+  shows "dist (- x) (- y) = dist x y"
+  unfolding dist_norm minus_diff_minus norm_minus_cancel ..
+
lemma uniformly_continuous_on_neg:
fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
shows "uniformly_continuous_on s f
==> uniformly_continuous_on s (\<lambda>x. -(f x))"
-  using uniformly_continuous_on_cmul[of s f "-1"] unfolding pth_3 by auto
+  unfolding uniformly_continuous_on_def dist_minus .

fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -3735,9 +3740,15 @@
thus ?thesis unfolding open_dist by auto
qed

+lemma minus_image_eq_vimage:
+  fixes A :: "'a::ab_group_add set"
+  shows "(\<lambda>x. - x) ` A = (\<lambda>x. - x) -` A"
+  by (auto intro!: image_eqI [where f="\<lambda>x. - x"])
+
lemma open_negations:
fixes s :: "(real ^ _) set" (* FIXME: generalize *)
-  shows "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
+  shows "open s ==> open ((\<lambda> x. -x) ` s)"
+  unfolding vector_sneg_minus1 by auto

lemma open_translation:
fixes s :: "(real ^ _) set" (* FIXME: generalize *)
@@ -4261,7 +4272,8 @@
fixes s :: "(real ^ _) set"
assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
proof-
-  have "uminus ` s = (\<lambda>x. -1 *s x) ` s" apply auto unfolding image_iff pth_3 by auto
+  have "(\<lambda>x. - x) ` s = (\<lambda>x. (- 1) *s x) ` s"
+    unfolding vector_sneg_minus1 ..
thus ?thesis using compact_scaling[OF assms, of "-1"] by auto
qed

@@ -4401,7 +4413,8 @@
lemma closed_negations:
fixes s :: "(real ^ _) set" (* FIXME: generalize *)
assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaling[OF assms, of "-1"] unfolding  pth_3 by auto
+  using closed_scaling[OF assms, of "- 1"]
+  unfolding vector_sneg_minus1 by auto

lemma compact_closed_sums:
fixes s :: "(real ^ _) set"```
```--- a/src/HOL/Library/normarith.ML	Thu Jun 04 15:00:44 2009 +0200
+++ b/src/HOL/Library/normarith.ML	Thu Jun 04 14:32:00 2009 -0700
@@ -49,21 +49,23 @@
fun int_lincomb_eq l r = Intfunc.is_undefined (int_lincomb_sub l r)

fun vector_lincomb t = case term_of t of
-   Const(@{const_name plus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) \$ _ \$ _ =>
+   Const(@{const_name plus}, _) \$ _ \$ _ =>
cterm_lincomb_add (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name minus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) \$ _ \$ _ =>
+ | Const(@{const_name minus}, _) \$ _ \$ _ =>
cterm_lincomb_sub (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name vector_scalar_mult},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))\$_\$_ =>
+ | Const(@{const_name scaleR}, _)\$_\$_ =>
cterm_lincomb_cmul (dest_ratconst (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name uminus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))\$_ =>
+ | Const(@{const_name uminus}, _)\$_ =>
cterm_lincomb_neg (vector_lincomb (dest_arg t))
- | Const(@{const_name vec},_)\$_ =>
+(* FIXME: how should we handle numerals?
+ | Const(@ {const_name vec},_)\$_ =>
let
val b = ((snd o HOLogic.dest_number o term_of o dest_arg) t = 0
handle TERM _=> false)
in if b then Ctermfunc.onefunc (t,Rat.one)
else Ctermfunc.undefined
end
+*)
| _ => Ctermfunc.onefunc (t,Rat.one)

fun vector_lincombs ts =
@@ -188,7 +190,7 @@
val apply_pth5 = rewr_conv @{thm pth_5};
val apply_pth6 = rewr_conv @{thm pth_6};
val apply_pth7 = rewrs_conv @{thms pth_7};
- val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm vector_smult_lzero})));
+ val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv);
val apply_ptha = rewr_conv @{thm pth_a};
val apply_pthb = rewrs_conv @{thms pth_b};
@@ -196,9 +198,9 @@
val apply_pthd = try_conv (rewr_conv @{thm pth_d});

fun headvector t = case t of
-  Const(@{const_name plus}, Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))\$
-   (Const(@{const_name vector_scalar_mult}, _)\$l\$v)\$r => v
- | Const(@{const_name vector_scalar_mult}, _)\$l\$v => v
+  Const(@{const_name plus}, _)\$
+   (Const(@{const_name scaleR}, _)\$l\$v)\$r => v
+ | Const(@{const_name scaleR}, _)\$l\$v => v
| _ => error "headvector: non-canonical term"

fun vector_cmul_conv ct =
@@ -234,7 +236,7 @@
val th = Drule.binop_cong_rule p lth rth
in fconv_rule (arg_conv vector_add_conv) th end

-| Const(@{const_name vector_scalar_mult}, _)\$_\$_ =>
+| Const(@{const_name scaleR}, _)\$_\$_ =>
let
val (p,r) = Thm.dest_comb ct
val rth = Drule.arg_cong_rule p (vector_canon_conv r)
@@ -245,12 +247,13 @@

| Const(@{const_name uminus},_)\$_ => (apply_pth3 then_conv vector_canon_conv) ct

+(* FIXME
| Const(@{const_name vec},_)\$n =>
let val n = Thm.dest_arg ct
in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
then reflexive ct else apply_pth1 ct
end
-
+*)
| _ => apply_pth1 ct

fun norm_canon_conv ct = case term_of ct of
@@ -266,8 +269,8 @@
then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq;

local
- val pth_zero = @{thm "norm_0"}
- val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
+ val pth_zero = @{thm norm_zero}
+ val tv_n = (ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
pth_zero
val concl = dest_arg o cprop_of
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
@@ -327,7 +330,7 @@
(fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)

in RealArith.real_linear_prover translator
-        (map (fn t => instantiate ([(tv_n,(hd o tl o dest_ctyp o ctyp_of_term) t)],[]) pth_zero)
+        (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
@@ -391,7 +394,7 @@

fun init_conv ctxt =
Simplifier.rewrite (Simplifier.context ctxt
-     (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
then_conv field_comp_conv
then_conv nnf_conv

@@ -409,4 +412,4 @@
ObjectLogic.full_atomize_tac THEN'
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);

-end;
\ No newline at end of file
+end;```