Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
wgt_digraphs_props.prf
Sprache: Unknown
(* Title: HOL/Real_Vector_Spaces.thy
Author: Brian Huffman
Author: Johannes Hölzl
*)
section \<open>Vector Spaces and Algebras over the Reals\<close>
theory Real_Vector_Spaces
imports Real Topological_Spaces Vector_Spaces
begin
subsection \<open>Real vector spaces\<close>
class scaleR =
fixes scaleR :: "real \ 'a \ 'a" (infixr "*\<^sub>R" 75)
begin
abbreviation divideR :: "'a \ real \ 'a" (infixl "'/\<^sub>R" 70)
where "x /\<^sub>R r \ inverse r *\<^sub>R x"
end
class real_vector = scaleR + ab_group_add +
assumes scaleR_add_right: "a *\<^sub>R (x + y) = a *\<^sub>R x + a *\<^sub>R y"
and scaleR_add_left: "(a + b) *\<^sub>R x = a *\<^sub>R x + b *\<^sub>R x"
and scaleR_scaleR: "a *\<^sub>R b *\<^sub>R x = (a * b) *\<^sub>R x"
and scaleR_one: "1 *\<^sub>R x = x"
class real_algebra = real_vector + ring +
assumes mult_scaleR_left [simp]: "a *\<^sub>R x * y = a *\<^sub>R (x * y)"
and mult_scaleR_right [simp]: "x * a *\<^sub>R y = a *\<^sub>R (x * y)"
class real_algebra_1 = real_algebra + ring_1
class real_div_algebra = real_algebra_1 + division_ring
class real_field = real_div_algebra + field
instantiation real :: real_field
begin
definition real_scaleR_def [simp]: "scaleR a x = a * x"
instance
by standard (simp_all add: algebra_simps)
end
locale linear = Vector_Spaces.linear "scaleR::_\_\'a::real_vector" "scaleR::_\_\'b::real_vector"
begin
lemmas scaleR = scale
end
global_interpretation real_vector?: vector_space "scaleR :: real \ 'a \ 'a :: real_vector"
rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines dependent_raw_def: dependent = real_vector.dependent
and representation_raw_def: representation = real_vector.representation
and subspace_raw_def: subspace = real_vector.subspace
and span_raw_def: span = real_vector.span
and extend_basis_raw_def: extend_basis = real_vector.extend_basis
and dim_raw_def: dim = real_vector.dim
proof unfold_locales
show "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
by (force simp: linear_def real_scaleR_def[abs_def])+
qed (use scaleR_add_right scaleR_add_left scaleR_scaleR scaleR_one in auto)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.dependent
real_vector.independent
real_vector.representation
real_vector.subspace
real_vector.span
real_vector.extend_basis
real_vector.dim
abbreviation "independent x \ \ dependent x"
global_interpretation real_vector?: vector_space_pair "scaleR::_\_\'a::real_vector" "scaleR::_\_\'b::real_vector"
rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines construct_raw_def: construct = real_vector.construct
proof unfold_locales
show "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
unfolding linear_def real_scaleR_def by auto
qed (auto simp: linear_def)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.construct
lemma linear_compose: "linear f \ linear g \ linear (g \ f)"
unfolding linear_def by (rule Vector_Spaces.linear_compose)
text \<open>Recover original theorem names\<close>
lemmas scaleR_left_commute = real_vector.scale_left_commute
lemmas scaleR_zero_left = real_vector.scale_zero_left
lemmas scaleR_minus_left = real_vector.scale_minus_left
lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib
lemmas scaleR_sum_left = real_vector.scale_sum_left
lemmas scaleR_zero_right = real_vector.scale_zero_right
lemmas scaleR_minus_right = real_vector.scale_minus_right
lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib
lemmas scaleR_sum_right = real_vector.scale_sum_right
lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff
lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq
lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq
lemmas scaleR_cancel_left = real_vector.scale_cancel_left
lemmas scaleR_cancel_right = real_vector.scale_cancel_right
lemma [field_simps]:
"c \ 0 \ a = b /\<^sub>R c \ c *\<^sub>R a = b"
"c \ 0 \ b /\<^sub>R c = a \ b = c *\<^sub>R a"
"c \ 0 \ a + b /\<^sub>R c = (c *\<^sub>R a + b) /\<^sub>R c"
"c \ 0 \ a /\<^sub>R c + b = (a + c *\<^sub>R b) /\<^sub>R c"
"c \ 0 \ a - b /\<^sub>R c = (c *\<^sub>R a - b) /\<^sub>R c"
"c \ 0 \ a /\<^sub>R c - b = (a - c *\<^sub>R b) /\<^sub>R c"
"c \ 0 \ - (a /\<^sub>R c) + b = (- a + c *\<^sub>R b) /\<^sub>R c"
"c \ 0 \ - (a /\<^sub>R c) - b = (- a - c *\<^sub>R b) /\<^sub>R c"
for a b :: "'a :: real_vector"
by (auto simp add: scaleR_add_right scaleR_add_left scaleR_diff_right scaleR_diff_left)
text \<open>Legacy names\<close>
lemmas scaleR_left_distrib = scaleR_add_left
lemmas scaleR_right_distrib = scaleR_add_right
lemmas scaleR_left_diff_distrib = scaleR_diff_left
lemmas scaleR_right_diff_distrib = scaleR_diff_right
lemmas linear_injective_0 = linear_inj_iff_eq_0
and linear_injective_on_subspace_0 = linear_inj_on_iff_eq_0
and linear_cmul = linear_scale
and linear_scaleR = linear_scale_self
and subspace_mul = subspace_scale
and span_linear_image = linear_span_image
and span_0 = span_zero
and span_mul = span_scale
and injective_scaleR = injective_scale
lemma scaleR_minus1_left [simp]: "scaleR (-1) x = - x"
for x :: "'a::real_vector"
using scaleR_minus_left [of 1 x] by simp
lemma scaleR_2:
fixes x :: "'a::real_vector"
shows "scaleR 2 x = x + x"
unfolding one_add_one [symmetric] scaleR_left_distrib by simp
lemma scaleR_half_double [simp]:
fixes a :: "'a::real_vector"
shows "(1 / 2) *\<^sub>R (a + a) = a"
proof -
have "\r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a"
by (metis scaleR_2 scaleR_scaleR)
then show ?thesis
by simp
qed
lemma linear_scale_real:
fixes r::real shows "linear f \ f (r * b) = r * f b"
using linear_scale by fastforce
interpretation scaleR_left: additive "(\a. scaleR a x :: 'a::real_vector)"
by standard (rule scaleR_left_distrib)
interpretation scaleR_right: additive "(\x. scaleR a x :: 'a::real_vector)"
by standard (rule scaleR_right_distrib)
lemma nonzero_inverse_scaleR_distrib:
"a \ 0 \ x \ 0 \ inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
for x :: "'a::real_div_algebra"
by (rule inverse_unique) simp
lemma inverse_scaleR_distrib: "inverse (scaleR a x) = scaleR (inverse a) (inverse x)"
for x :: "'a::{real_div_algebra,division_ring}"
by (metis inverse_zero nonzero_inverse_scaleR_distrib scale_eq_0_iff)
lemmas sum_constant_scaleR = real_vector.sum_constant_scale\<comment> \<open>legacy name\<close>
named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
lemma [vector_add_divide_simps]:
"v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
"a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
"(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)"
"(a / z) *\<^sub>R v + b *\<^sub>R w = (if z = 0 then b *\<^sub>R w else (a *\<^sub>R v + (b * z) *\<^sub>R w) /\<^sub>R z)"
"v - (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
"a *\<^sub>R v - (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
"(a / z) *\<^sub>R v - w = (if z = 0 then -w else (a *\<^sub>R v - z *\<^sub>R w) /\<^sub>R z)"
"(a / z) *\<^sub>R v - b *\<^sub>R w = (if z = 0 then -b *\<^sub>R w else (a *\<^sub>R v - (b * z) *\<^sub>R w) /\<^sub>R z)"
for v :: "'a :: real_vector"
by (simp_all add: divide_inverse_commute scaleR_add_right scaleR_diff_right)
lemma eq_vector_fraction_iff [vector_add_divide_simps]:
fixes x :: "'a :: real_vector"
shows "(x = (u / v) *\<^sub>R a) \ (if v=0 then x = 0 else v *\<^sub>R x = u *\<^sub>R a)"
by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleR_one scaleR_scaleR)
lemma vector_fraction_eq_iff [vector_add_divide_simps]:
fixes x :: "'a :: real_vector"
shows "((u / v) *\<^sub>R a = x) \ (if v=0 then x = 0 else u *\<^sub>R a = v *\<^sub>R x)"
by (metis eq_vector_fraction_iff)
lemma real_vector_affinity_eq:
fixes x :: "'a :: real_vector"
assumes m0: "m \ 0"
shows "m *\<^sub>R x + c = y \ x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
(is "?lhs \ ?rhs")
proof
assume ?lhs
then have "m *\<^sub>R x = y - c" by (simp add: field_simps)
then have "inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp
then show "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
using m0
by (simp add: scaleR_diff_right)
next
assume ?rhs
with m0 show "m *\<^sub>R x + c = y"
by (simp add: scaleR_diff_right)
qed
lemma real_vector_eq_affinity: "m \ 0 \ y = m *\<^sub>R x + c \ inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x"
for x :: "'a::real_vector"
using real_vector_affinity_eq[where m=m and x=x and y=y and c=c]
by metis
lemma scaleR_eq_iff [simp]: "b + u *\<^sub>R a = a + u *\<^sub>R b \ a = b \ u = 1"
for a :: "'a::real_vector"
proof (cases "u = 1")
case True
then show ?thesis by auto
next
case False
have "a = b" if "b + u *\<^sub>R a = a + u *\<^sub>R b"
proof -
from that have "(u - 1) *\<^sub>R a = (u - 1) *\<^sub>R b"
by (simp add: algebra_simps)
with False show ?thesis
by auto
qed
then show ?thesis by auto
qed
lemma scaleR_collapse [simp]: "(1 - u) *\<^sub>R a + u *\<^sub>R a = a"
for a :: "'a::real_vector"
by (simp add: algebra_simps)
subsection \<open>Embedding of the Reals into any \<open>real_algebra_1\<close>: \<open>of_real\<close>\<close>
definition of_real :: "real \ 'a::real_algebra_1"
where "of_real r = scaleR r 1"
lemma scaleR_conv_of_real: "scaleR r x = of_real r * x"
by (simp add: of_real_def)
lemma of_real_0 [simp]: "of_real 0 = 0"
by (simp add: of_real_def)
lemma of_real_1 [simp]: "of_real 1 = 1"
by (simp add: of_real_def)
lemma of_real_add [simp]: "of_real (x + y) = of_real x + of_real y"
by (simp add: of_real_def scaleR_left_distrib)
lemma of_real_minus [simp]: "of_real (- x) = - of_real x"
by (simp add: of_real_def)
lemma of_real_diff [simp]: "of_real (x - y) = of_real x - of_real y"
by (simp add: of_real_def scaleR_left_diff_distrib)
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
by (simp add: of_real_def)
lemma of_real_sum[simp]: "of_real (sum f s) = (\x\s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
lemma of_real_prod[simp]: "of_real (prod f s) = (\x\s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
lemma nonzero_of_real_inverse:
"x \ 0 \ of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)"
by (simp add: of_real_def nonzero_inverse_scaleR_distrib)
lemma of_real_inverse [simp]:
"of_real (inverse x) = inverse (of_real x :: 'a::{real_div_algebra,division_ring})"
by (simp add: of_real_def inverse_scaleR_distrib)
lemma nonzero_of_real_divide:
"y \ 0 \ of_real (x / y) = (of_real x / of_real y :: 'a::real_field)"
by (simp add: divide_inverse nonzero_of_real_inverse)
lemma of_real_divide [simp]:
"of_real (x / y) = (of_real x / of_real y :: 'a::real_div_algebra)"
by (simp add: divide_inverse)
lemma of_real_power [simp]:
"of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
by (induct n) simp_all
lemma of_real_power_int [simp]:
"of_real (power_int x n) = power_int (of_real x :: 'a :: {real_div_algebra,division_ring}) n"
by (auto simp: power_int_def)
lemma of_real_eq_iff [simp]: "of_real x = of_real y \ x = y"
by (simp add: of_real_def)
lemma inj_of_real: "inj of_real"
by (auto intro: injI)
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
lemma minus_of_real_eq_of_real_iff [simp]: "-of_real x = of_real y \ -x = y"
using of_real_eq_iff[of "-x" y] by (simp only: of_real_minus)
lemma of_real_eq_minus_of_real_iff [simp]: "of_real x = -of_real y \ x = -y"
using of_real_eq_iff[of x "-y"] by (simp only: of_real_minus)
lemma of_real_eq_id [simp]: "of_real = (id :: real \ real)"
by (rule ext) (simp add: of_real_def)
text \<open>Collapse nested embeddings.\<close>
lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n"
by (induct n) auto
lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z"
by (cases z rule: int_diff_cases) simp
lemma of_real_numeral [simp]: "of_real (numeral w) = numeral w"
using of_real_of_int_eq [of "numeral w"] by simp
lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w"
using of_real_of_int_eq [of "- numeral w"] by simp
lemma numeral_power_int_eq_of_real_cancel_iff [simp]:
"power_int (numeral x) n = (of_real y :: 'a :: {real_div_algebra, division_ring}) \
power_int (numeral x) n = y"
proof -
have "power_int (numeral x) n = (of_real (power_int (numeral x) n) :: 'a)"
by simp
also have "\ = of_real y \ power_int (numeral x) n = y"
by (subst of_real_eq_iff) auto
finally show ?thesis .
qed
lemma of_real_eq_numeral_power_int_cancel_iff [simp]:
"(of_real y :: 'a :: {real_div_algebra, division_ring}) = power_int (numeral x) n \
y = power_int (numeral x) n"
by (subst (1 2) eq_commute) simp
lemma of_real_eq_of_real_power_int_cancel_iff [simp]:
"power_int (of_real b :: 'a :: {real_div_algebra, division_ring}) w = of_real x \
power_int b w = x"
by (metis of_real_power_int of_real_eq_iff)
lemma of_real_in_Ints_iff [simp]: "of_real x \ \ \ x \ \"
proof safe
fix x assume "(of_real x :: 'a) \ \"
then obtain n where "(of_real x :: 'a) = of_int n"
by (auto simp: Ints_def)
also have "of_int n = of_real (real_of_int n)"
by simp
finally have "x = real_of_int n"
by (subst (asm) of_real_eq_iff)
thus "x \ \"
by auto
qed (auto simp: Ints_def)
lemma Ints_of_real [intro]: "x \ \ \ of_real x \ \"
by simp
text \<open>Every real algebra has characteristic zero.\<close>
instance real_algebra_1 < ring_char_0
proof
from inj_of_real inj_of_nat have "inj (of_real \ of_nat)"
by (rule inj_compose)
then show "inj (of_nat :: nat \ 'a)"
by (simp add: comp_def)
qed
lemma fraction_scaleR_times [simp]:
fixes a :: "'a::real_algebra_1"
shows "(numeral u / numeral v) *\<^sub>R (numeral w * a) = (numeral u * numeral w / numeral v) *\<^sub>R a"
by (metis (no_types, lifting) of_real_numeral scaleR_conv_of_real scaleR_scaleR times_divide_eq_left)
lemma inverse_scaleR_times [simp]:
fixes a :: "'a::real_algebra_1"
shows "(1 / numeral v) *\<^sub>R (numeral w * a) = (numeral w / numeral v) *\<^sub>R a"
by (metis divide_inverse_commute inverse_eq_divide of_real_numeral scaleR_conv_of_real scaleR_scaleR)
lemma scaleR_times [simp]:
fixes a :: "'a::real_algebra_1"
shows "(numeral u) *\<^sub>R (numeral w * a) = (numeral u * numeral w) *\<^sub>R a"
by (simp add: scaleR_conv_of_real)
instance real_field < field_char_0 ..
subsection \<open>The Set of Real Numbers\<close>
definition Reals :: "'a::real_algebra_1 set" ("\")
where "\ = range of_real"
lemma Reals_of_real [simp]: "of_real r \ \"
by (simp add: Reals_def)
lemma Reals_of_int [simp]: "of_int z \ \"
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
lemma Reals_of_nat [simp]: "of_nat n \ \"
by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
lemma Reals_numeral [simp]: "numeral w \ \"
by (subst of_real_numeral [symmetric], rule Reals_of_real)
lemma Reals_0 [simp]: "0 \ \" and Reals_1 [simp]: "1 \ \"
by (simp_all add: Reals_def)
lemma Reals_add [simp]: "a \ \ \ b \ \ \ a + b \ \"
by (metis (no_types, hide_lams) Reals_def Reals_of_real imageE of_real_add)
lemma Reals_minus [simp]: "a \ \ \ - a \ \"
by (auto simp: Reals_def)
lemma Reals_minus_iff [simp]: "- a \ \ \ a \ \"
using Reals_minus by fastforce
lemma Reals_diff [simp]: "a \ \ \ b \ \ \ a - b \ \"
by (metis Reals_add Reals_minus_iff add_uminus_conv_diff)
lemma Reals_mult [simp]: "a \ \ \ b \ \ \ a * b \ \"
by (metis (no_types, lifting) Reals_def Reals_of_real imageE of_real_mult)
lemma nonzero_Reals_inverse: "a \ \ \ a \ 0 \ inverse a \ \"
for a :: "'a::real_div_algebra"
by (metis Reals_def Reals_of_real imageE of_real_inverse)
lemma Reals_inverse: "a \ \ \ inverse a \ \"
for a :: "'a::{real_div_algebra,division_ring}"
using nonzero_Reals_inverse by fastforce
lemma Reals_inverse_iff [simp]: "inverse x \ \ \ x \ \"
for x :: "'a::{real_div_algebra,division_ring}"
by (metis Reals_inverse inverse_inverse_eq)
lemma nonzero_Reals_divide: "a \ \ \ b \ \ \ b \ 0 \ a / b \ \"
for a b :: "'a::real_field"
by (simp add: divide_inverse)
lemma Reals_divide [simp]: "a \ \ \ b \ \ \ a / b \ \"
for a b :: "'a::{real_field,field}"
using nonzero_Reals_divide by fastforce
lemma Reals_power [simp]: "a \ \ \ a ^ n \ \"
for a :: "'a::real_algebra_1"
by (metis Reals_def Reals_of_real imageE of_real_power)
lemma Reals_cases [cases set: Reals]:
assumes "q \ \"
obtains (of_real) r where "q = of_real r"
unfolding Reals_def
proof -
from \<open>q \<in> \<real>\<close> have "q \<in> range of_real" unfolding Reals_def .
then obtain r where "q = of_real r" ..
then show thesis ..
qed
lemma sum_in_Reals [intro,simp]: "(\i. i \ s \ f i \ \) \ sum f s \ \"
proof (induct s rule: infinite_finite_induct)
case infinite
then show ?case by (metis Reals_0 sum.infinite)
qed simp_all
lemma prod_in_Reals [intro,simp]: "(\i. i \ s \ f i \ \) \ prod f s \ \"
proof (induct s rule: infinite_finite_induct)
case infinite
then show ?case by (metis Reals_1 prod.infinite)
qed simp_all
lemma Reals_induct [case_names of_real, induct set: Reals]:
"q \ \ \ (\r. P (of_real r)) \ P q"
by (rule Reals_cases) auto
subsection \<open>Ordered real vector spaces\<close>
class ordered_real_vector = real_vector + ordered_ab_group_add +
assumes scaleR_left_mono: "x \ y \ 0 \ a \ a *\<^sub>R x \ a *\<^sub>R y"
and scaleR_right_mono: "a \ b \ 0 \ x \ a *\<^sub>R x \ b *\<^sub>R x"
begin
lemma scaleR_mono:
"a \ b \ x \ y \ 0 \ b \ 0 \ x \ a *\<^sub>R x \ b *\<^sub>R y"
by (meson order_trans scaleR_left_mono scaleR_right_mono)
lemma scaleR_mono':
"a \ b \ c \ d \ 0 \ a \ 0 \ c \ a *\<^sub>R c \ b *\<^sub>R d"
by (rule scaleR_mono) (auto intro: order.trans)
lemma pos_le_divideR_eq [field_simps]:
"a \ b /\<^sub>R c \ c *\<^sub>R a \ b" (is "?P \ ?Q") if "0 < c"
proof
assume ?P
with scaleR_left_mono that have "c *\<^sub>R a \ c *\<^sub>R (b /\<^sub>R c)"
by simp
with that show ?Q
by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
next
assume ?Q
with scaleR_left_mono that have "c *\<^sub>R a /\<^sub>R c \ b /\<^sub>R c"
by simp
with that show ?P
by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
qed
lemma pos_less_divideR_eq [field_simps]:
"a < b /\<^sub>R c \ c *\<^sub>R a < b" if "c > 0"
using that pos_le_divideR_eq [of c a b]
by (auto simp add: le_less scaleR_scaleR scaleR_one)
lemma pos_divideR_le_eq [field_simps]:
"b /\<^sub>R c \ a \ b \ c *\<^sub>R a" if "c > 0"
using that pos_le_divideR_eq [of "inverse c" b a] by simp
lemma pos_divideR_less_eq [field_simps]:
"b /\<^sub>R c < a \ b < c *\<^sub>R a" if "c > 0"
using that pos_less_divideR_eq [of "inverse c" b a] by simp
lemma pos_le_minus_divideR_eq [field_simps]:
"a \ - (b /\<^sub>R c) \ c *\<^sub>R a \ - b" if "c > 0"
using that by (metis add_minus_cancel diff_0 left_minus minus_minus neg_le_iff_le
scaleR_add_right uminus_add_conv_diff pos_le_divideR_eq)
lemma pos_less_minus_divideR_eq [field_simps]:
"a < - (b /\<^sub>R c) \ c *\<^sub>R a < - b" if "c > 0"
using that by (metis le_less less_le_not_le pos_divideR_le_eq
pos_divideR_less_eq pos_le_minus_divideR_eq)
lemma pos_minus_divideR_le_eq [field_simps]:
"- (b /\<^sub>R c) \ a \ - b \ c *\<^sub>R a" if "c > 0"
using that by (metis pos_divideR_le_eq pos_le_minus_divideR_eq that
inverse_positive_iff_positive le_imp_neg_le minus_minus)
lemma pos_minus_divideR_less_eq [field_simps]:
"- (b /\<^sub>R c) < a \ - b < c *\<^sub>R a" if "c > 0"
using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)
lemma scaleR_image_atLeastAtMost: "c > 0 \ scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)
end
lemma neg_le_divideR_eq [field_simps]:
"a \ b /\<^sub>R c \ b \ c *\<^sub>R a" (is "?P \ ?Q") if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_le_divideR_eq [of "- c" a "- b"] by simp
lemma neg_less_divideR_eq [field_simps]:
"a < b /\<^sub>R c \ b < c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that neg_le_divideR_eq [of c a b] by (auto simp add: le_less)
lemma neg_divideR_le_eq [field_simps]:
"b /\<^sub>R c \ a \ c *\<^sub>R a \ b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_divideR_le_eq [of "- c" "- b" a] by simp
lemma neg_divideR_less_eq [field_simps]:
"b /\<^sub>R c < a \ c *\<^sub>R a < b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that neg_divideR_le_eq [of c b a] by (auto simp add: le_less)
lemma neg_le_minus_divideR_eq [field_simps]:
"a \ - (b /\<^sub>R c) \ - b \ c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_le_minus_divideR_eq [of "- c" a "- b"] by (simp add: minus_le_iff)
lemma neg_less_minus_divideR_eq [field_simps]:
"a < - (b /\<^sub>R c) \ - b < c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
proof -
have *: "- b = c *\<^sub>R a \ b = - (c *\<^sub>R a)"
by (metis add.inverse_inverse)
from that neg_le_minus_divideR_eq [of c a b]
show ?thesis by (auto simp add: le_less *)
qed
lemma neg_minus_divideR_le_eq [field_simps]:
"- (b /\<^sub>R c) \ a \ c *\<^sub>R a \ - b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_minus_divideR_le_eq [of "- c" "- b" a] by (simp add: le_minus_iff)
lemma neg_minus_divideR_less_eq [field_simps]:
"- (b /\<^sub>R c) < a \ c *\<^sub>R a < - b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that by (simp add: less_le_not_le neg_le_minus_divideR_eq neg_minus_divideR_le_eq)
lemma [field_split_simps]:
"a = b /\<^sub>R c \ (if c = 0 then a = 0 else c *\<^sub>R a = b)"
"b /\<^sub>R c = a \ (if c = 0 then a = 0 else b = c *\<^sub>R a)"
"a + b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a + b) /\<^sub>R c)"
"a /\<^sub>R c + b = (if c = 0 then b else (a + c *\<^sub>R b) /\<^sub>R c)"
"a - b /\<^sub>R c = (if c = 0 then a else (c *\<^sub>R a - b) /\<^sub>R c)"
"a /\<^sub>R c - b = (if c = 0 then - b else (a - c *\<^sub>R b) /\<^sub>R c)"
"- (a /\<^sub>R c) + b = (if c = 0 then b else (- a + c *\<^sub>R b) /\<^sub>R c)"
"- (a /\<^sub>R c) - b = (if c = 0 then - b else (- a - c *\<^sub>R b) /\<^sub>R c)"
for a b :: "'a :: real_vector"
by (auto simp add: field_simps)
lemma [field_split_simps]:
"0 < c \ a \ b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a \ b else if c < 0 then b \ c *\<^sub>R a else a \ 0)"
"0 < c \ a < b /\<^sub>R c \ (if c > 0 then c *\<^sub>R a < b else if c < 0 then b < c *\<^sub>R a else a < 0)"
"0 < c \ b /\<^sub>R c \ a \ (if c > 0 then b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ b else a \ 0)"
"0 < c \ b /\<^sub>R c < a \ (if c > 0 then b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < b else a > 0)"
"0 < c \ a \ - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a \ - b else if c < 0 then - b \ c *\<^sub>R a else a \ 0)"
"0 < c \ a < - (b /\<^sub>R c) \ (if c > 0 then c *\<^sub>R a < - b else if c < 0 then - b < c *\<^sub>R a else a < 0)"
"0 < c \ - (b /\<^sub>R c) \ a \ (if c > 0 then - b \ c *\<^sub>R a else if c < 0 then c *\<^sub>R a \ - b else a \ 0)"
"0 < c \ - (b /\<^sub>R c) < a \ (if c > 0 then - b < c *\<^sub>R a else if c < 0 then c *\<^sub>R a < - b else a > 0)"
for a b :: "'a :: ordered_real_vector"
by (clarsimp intro!: field_simps)+
lemma scaleR_nonneg_nonneg: "0 \ a \ 0 \ x \ 0 \ a *\<^sub>R x"
for x :: "'a::ordered_real_vector"
using scaleR_left_mono [of 0 x a] by simp
lemma scaleR_nonneg_nonpos: "0 \ a \ x \ 0 \ a *\<^sub>R x \ 0"
for x :: "'a::ordered_real_vector"
using scaleR_left_mono [of x 0 a] by simp
lemma scaleR_nonpos_nonneg: "a \ 0 \ 0 \ x \ a *\<^sub>R x \ 0"
for x :: "'a::ordered_real_vector"
using scaleR_right_mono [of a 0 x] by simp
lemma split_scaleR_neg_le: "(0 \ a \ x \ 0) \ (a \ 0 \ 0 \ x) \ a *\<^sub>R x \ 0"
for x :: "'a::ordered_real_vector"
by (auto simp: scaleR_nonneg_nonpos scaleR_nonpos_nonneg)
lemma le_add_iff1: "a *\<^sub>R e + c \ b *\<^sub>R e + d \ (a - b) *\<^sub>R e + c \ d"
for c d e :: "'a::ordered_real_vector"
by (simp add: algebra_simps)
lemma le_add_iff2: "a *\<^sub>R e + c \ b *\<^sub>R e + d \ c \ (b - a) *\<^sub>R e + d"
for c d e :: "'a::ordered_real_vector"
by (simp add: algebra_simps)
lemma scaleR_left_mono_neg: "b \ a \ c \ 0 \ c *\<^sub>R a \ c *\<^sub>R b"
for a b :: "'a::ordered_real_vector"
by (drule scaleR_left_mono [of _ _ "- c"], simp_all)
lemma scaleR_right_mono_neg: "b \ a \ c \ 0 \ a *\<^sub>R c \ b *\<^sub>R c"
for c :: "'a::ordered_real_vector"
by (drule scaleR_right_mono [of _ _ "- c"], simp_all)
lemma scaleR_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a *\<^sub>R b"
for b :: "'a::ordered_real_vector"
using scaleR_right_mono_neg [of a 0 b] by simp
lemma split_scaleR_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a *\<^sub>R b"
for b :: "'a::ordered_real_vector"
by (auto simp: scaleR_nonneg_nonneg scaleR_nonpos_nonpos)
lemma zero_le_scaleR_iff:
fixes b :: "'a::ordered_real_vector"
shows "0 \ a *\<^sub>R b \ 0 < a \ 0 \ b \ a < 0 \ b \ 0 \ a = 0"
(is "?lhs = ?rhs")
proof (cases "a = 0")
case True
then show ?thesis by simp
next
case False
show ?thesis
proof
assume ?lhs
from \<open>a \<noteq> 0\<close> consider "a > 0" | "a < 0" by arith
then show ?rhs
proof cases
case 1
with \<open>?lhs\<close> have "inverse a *\<^sub>R 0 \<le> inverse a *\<^sub>R (a *\<^sub>R b)"
by (intro scaleR_mono) auto
with 1 show ?thesis
by simp
next
case 2
with \<open>?lhs\<close> have "- inverse a *\<^sub>R 0 \<le> - inverse a *\<^sub>R (a *\<^sub>R b)"
by (intro scaleR_mono) auto
with 2 show ?thesis
by simp
qed
next
assume ?rhs
then show ?lhs
by (auto simp: not_le \<open>a \<noteq> 0\<close> intro!: split_scaleR_pos_le)
qed
qed
lemma scaleR_le_0_iff: "a *\<^sub>R b \ 0 \ 0 < a \ b \ 0 \ a < 0 \ 0 \ b \ a = 0"
for b::"'a::ordered_real_vector"
by (insert zero_le_scaleR_iff [of "-a" b]) force
lemma scaleR_le_cancel_left: "c *\<^sub>R a \ c *\<^sub>R b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)"
for b :: "'a::ordered_real_vector"
by (auto simp: neq_iff scaleR_left_mono scaleR_left_mono_neg
dest: scaleR_left_mono[where a="inverse c"] scaleR_left_mono_neg[where c="inverse c"])
lemma scaleR_le_cancel_left_pos: "0 < c \ c *\<^sub>R a \ c *\<^sub>R b \ a \ b"
for b :: "'a::ordered_real_vector"
by (auto simp: scaleR_le_cancel_left)
lemma scaleR_le_cancel_left_neg: "c < 0 \ c *\<^sub>R a \ c *\<^sub>R b \ b \ a"
for b :: "'a::ordered_real_vector"
by (auto simp: scaleR_le_cancel_left)
lemma scaleR_left_le_one_le: "0 \ x \ a \ 1 \ a *\<^sub>R x \ x"
for x :: "'a::ordered_real_vector" and a :: real
using scaleR_right_mono[of a 1 x] by simp
subsection \<open>Real normed vector spaces\<close>
class dist =
fixes dist :: "'a \ 'a \ real"
class norm =
fixes norm :: "'a \ real"
class sgn_div_norm = scaleR + norm + sgn +
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)"
class uniformity_dist = dist + uniformity +
assumes uniformity_dist: "uniformity = (INF e\{0 <..}. principal {(x, y). dist x y < e})"
begin
lemma eventually_uniformity_metric:
"eventually P uniformity \ (\e>0. \x y. dist x y < e \ P (x, y))"
unfolding uniformity_dist
by (subst eventually_INF_base)
(auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
end
class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
assumes norm_eq_zero [simp]: "norm x = 0 \ x = 0"
and norm_triangle_ineq: "norm (x + y) \ norm x + norm y"
and norm_scaleR [simp]: "norm (scaleR a x) = \a\ * norm x"
begin
lemma norm_ge_zero [simp]: "0 \ norm x"
proof -
have "0 = norm (x + -1 *\<^sub>R x)"
using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
also have "\ \ norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
finally show ?thesis by simp
qed
end
class real_normed_algebra = real_algebra + real_normed_vector +
assumes norm_mult_ineq: "norm (x * y) \ norm x * norm y"
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
assumes norm_one [simp]: "norm 1 = 1"
lemma (in real_normed_algebra_1) scaleR_power [simp]: "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
by (induct n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
class real_normed_div_algebra = real_div_algebra + real_normed_vector +
assumes norm_mult: "norm (x * y) = norm x * norm y"
class real_normed_field = real_field + real_normed_div_algebra
instance real_normed_div_algebra < real_normed_algebra_1
proof
show "norm (x * y) \ norm x * norm y" for x y :: 'a
by (simp add: norm_mult)
next
have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)"
by (rule norm_mult)
then show "norm (1::'a) = 1" by simp
qed
context real_normed_vector begin
lemma norm_zero [simp]: "norm (0::'a) = 0"
by simp
lemma zero_less_norm_iff [simp]: "norm x > 0 \ x \ 0"
by (simp add: order_less_le)
lemma norm_not_less_zero [simp]: "\ norm x < 0"
by (simp add: linorder_not_less)
lemma norm_le_zero_iff [simp]: "norm x \ 0 \ x = 0"
by (simp add: order_le_less)
lemma norm_minus_cancel [simp]: "norm (- x) = norm x"
proof -
have "- 1 *\<^sub>R x = - (1 *\<^sub>R x)"
unfolding add_eq_0_iff2[symmetric] scaleR_add_left[symmetric]
using norm_eq_zero
by fastforce
then have "norm (- x) = norm (scaleR (- 1) x)"
by (simp only: scaleR_one)
also have "\ = \- 1\ * norm x"
by (rule norm_scaleR)
finally show ?thesis by simp
qed
lemma norm_minus_commute: "norm (a - b) = norm (b - a)"
proof -
have "norm (- (b - a)) = norm (b - a)"
by (rule norm_minus_cancel)
then show ?thesis by simp
qed
lemma dist_add_cancel [simp]: "dist (a + b) (a + c) = dist b c"
by (simp add: dist_norm)
lemma dist_add_cancel2 [simp]: "dist (b + a) (c + a) = dist b c"
by (simp add: dist_norm)
lemma norm_uminus_minus: "norm (- x - y) = norm (x + y)"
by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
lemma norm_triangle_ineq2: "norm a - norm b \ norm (a - b)"
proof -
have "norm (a - b + b) \ norm (a - b) + norm b"
by (rule norm_triangle_ineq)
then show ?thesis by simp
qed
lemma norm_triangle_ineq3: "\norm a - norm b\ \ norm (a - b)"
proof -
have "norm a - norm b \ norm (a - b)"
by (simp add: norm_triangle_ineq2)
moreover have "norm b - norm a \ norm (a - b)"
by (metis norm_minus_commute norm_triangle_ineq2)
ultimately show ?thesis
by (simp add: abs_le_iff)
qed
lemma norm_triangle_ineq4: "norm (a - b) \ norm a + norm b"
proof -
have "norm (a + - b) \ norm a + norm (- b)"
by (rule norm_triangle_ineq)
then show ?thesis by simp
qed
lemma norm_triangle_le_diff: "norm x + norm y \ e \ norm (x - y) \ e"
by (meson norm_triangle_ineq4 order_trans)
lemma norm_diff_ineq: "norm a - norm b \ norm (a + b)"
proof -
have "norm a - norm (- b) \ norm (a - - b)"
by (rule norm_triangle_ineq2)
then show ?thesis by simp
qed
lemma norm_triangle_sub: "norm x \ norm y + norm (x - y)"
using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
lemma norm_triangle_le: "norm x + norm y \ e \ norm (x + y) \ e"
by (rule norm_triangle_ineq [THEN order_trans])
lemma norm_triangle_lt: "norm x + norm y < e \ norm (x + y) < e"
by (rule norm_triangle_ineq [THEN le_less_trans])
lemma norm_add_leD: "norm (a + b) \ c \ norm b \ norm a + c"
by (metis ab_semigroup_add_class.add.commute add_commute diff_le_eq norm_diff_ineq order_trans)
lemma norm_diff_triangle_ineq: "norm ((a + b) - (c + d)) \ norm (a - c) + norm (b - d)"
proof -
have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
by (simp add: algebra_simps)
also have "\ \ norm (a - c) + norm (b - d)"
by (rule norm_triangle_ineq)
finally show ?thesis .
qed
lemma norm_diff_triangle_le: "norm (x - z) \ e1 + e2"
if "norm (x - y) \ e1" "norm (y - z) \ e2"
proof -
have "norm (x - (y + z - y)) \ norm (x - y) + norm (y - z)"
using norm_diff_triangle_ineq that diff_diff_eq2 by presburger
with that show ?thesis by simp
qed
lemma norm_diff_triangle_less: "norm (x - z) < e1 + e2"
if "norm (x - y) < e1" "norm (y - z) < e2"
proof -
have "norm (x - z) \ norm (x - y) + norm (y - z)"
by (metis norm_diff_triangle_ineq add_diff_cancel_left' diff_diff_eq2)
with that show ?thesis by auto
qed
lemma norm_triangle_mono:
"norm a \ r \ norm b \ s \ norm (a + b) \ r + s"
by (metis (mono_tags) add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
lemma norm_sum: "norm (sum f A) \ (\i\A. norm (f i))"
for f::"'b \ 'a"
by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
lemma sum_norm_le: "norm (sum f S) \ sum g S"
if "\x. x \ S \ norm (f x) \ g x"
for f::"'b \ 'a"
by (rule order_trans [OF norm_sum sum_mono]) (simp add: that)
lemma abs_norm_cancel [simp]: "\norm a\ = norm a"
by (rule abs_of_nonneg [OF norm_ge_zero])
lemma sum_norm_bound:
"norm (sum f S) \ of_nat (card S)*K"
if "\x. x \ S \ norm (f x) \ K"
for f :: "'b \ 'a"
using sum_norm_le[OF that] sum_constant[symmetric]
by simp
lemma norm_add_less: "norm x < r \ norm y < s \ norm (x + y) < r + s"
by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
end
lemma dist_scaleR [simp]: "dist (x *\<^sub>R a) (y *\<^sub>R a) = \x - y\ * norm a"
for a :: "'a::real_normed_vector"
by (metis dist_norm norm_scaleR scaleR_left.diff)
lemma norm_mult_less: "norm x < r \ norm y < s \ norm (x * y) < r * s"
for x y :: "'a::real_normed_algebra"
by (rule order_le_less_trans [OF norm_mult_ineq]) (simp add: mult_strict_mono')
lemma norm_of_real [simp]: "norm (of_real r :: 'a::real_normed_algebra_1) = \r\"
by (simp add: of_real_def)
lemma norm_numeral [simp]: "norm (numeral w::'a::real_normed_algebra_1) = numeral w"
by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
lemma norm_neg_numeral [simp]: "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
lemma norm_of_real_add1 [simp]: "norm (of_real x + 1 :: 'a :: real_normed_div_algebra) = \x + 1\"
by (metis norm_of_real of_real_1 of_real_add)
lemma norm_of_real_addn [simp]:
"norm (of_real x + numeral b :: 'a :: real_normed_div_algebra) = \x + numeral b\"
by (metis norm_of_real of_real_add of_real_numeral)
lemma norm_of_int [simp]: "norm (of_int z::'a::real_normed_algebra_1) = \of_int z\"
by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
lemma norm_of_nat [simp]: "norm (of_nat n::'a::real_normed_algebra_1) = of_nat n"
by (metis abs_of_nat norm_of_real of_real_of_nat_eq)
lemma nonzero_norm_inverse: "a \ 0 \ norm (inverse a) = inverse (norm a)"
for a :: "'a::real_normed_div_algebra"
by (metis inverse_unique norm_mult norm_one right_inverse)
lemma norm_inverse: "norm (inverse a) = inverse (norm a)"
for a :: "'a::{real_normed_div_algebra,division_ring}"
by (metis inverse_zero nonzero_norm_inverse norm_zero)
lemma nonzero_norm_divide: "b \ 0 \ norm (a / b) = norm a / norm b"
for a b :: "'a::real_normed_field"
by (simp add: divide_inverse norm_mult nonzero_norm_inverse)
lemma norm_divide: "norm (a / b) = norm a / norm b"
for a b :: "'a::{real_normed_field,field}"
by (simp add: divide_inverse norm_mult norm_inverse)
lemma norm_inverse_le_norm:
fixes x :: "'a::real_normed_div_algebra"
shows "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r"
by (simp add: le_imp_inverse_le norm_inverse)
lemma norm_power_ineq: "norm (x ^ n) \ norm x ^ n"
for x :: "'a::real_normed_algebra_1"
proof (induct n)
case 0
show "norm (x ^ 0) \ norm x ^ 0" by simp
next
case (Suc n)
have "norm (x * x ^ n) \ norm x * norm (x ^ n)"
by (rule norm_mult_ineq)
also from Suc have "\ \ norm x * norm x ^ n"
using norm_ge_zero by (rule mult_left_mono)
finally show "norm (x ^ Suc n) \ norm x ^ Suc n"
by simp
qed
lemma norm_power: "norm (x ^ n) = norm x ^ n"
for x :: "'a::real_normed_div_algebra"
by (induct n) (simp_all add: norm_mult)
lemma norm_power_int: "norm (power_int x n) = power_int (norm x) n"
for x :: "'a::real_normed_div_algebra"
by (cases n rule: int_cases4) (auto simp: norm_power power_int_minus norm_inverse)
lemma power_eq_imp_eq_norm:
fixes w :: "'a::real_normed_div_algebra"
assumes eq: "w ^ n = z ^ n" and "n > 0"
shows "norm w = norm z"
proof -
have "norm w ^ n = norm z ^ n"
by (metis (no_types) eq norm_power)
then show ?thesis
using assms by (force intro: power_eq_imp_eq_base)
qed
lemma power_eq_1_iff:
fixes w :: "'a::real_normed_div_algebra"
shows "w ^ n = 1 \ norm w = 1 \ n = 0"
by (metis norm_one power_0_left power_eq_0_iff power_eq_imp_eq_norm power_one)
lemma norm_mult_numeral1 [simp]: "norm (numeral w * a) = numeral w * norm a"
for a b :: "'a::{real_normed_field,field}"
by (simp add: norm_mult)
lemma norm_mult_numeral2 [simp]: "norm (a * numeral w) = norm a * numeral w"
for a b :: "'a::{real_normed_field,field}"
by (simp add: norm_mult)
lemma norm_divide_numeral [simp]: "norm (a / numeral w) = norm a / numeral w"
for a b :: "'a::{real_normed_field,field}"
by (simp add: norm_divide)
lemma norm_of_real_diff [simp]:
"norm (of_real b - of_real a :: 'a::real_normed_algebra_1) \ \b - a\"
by (metis norm_of_real of_real_diff order_refl)
text \<open>Despite a superficial resemblance, \<open>norm_eq_1\<close> is not relevant.\<close>
lemma square_norm_one:
fixes x :: "'a::real_normed_div_algebra"
assumes "x\<^sup>2 = 1"
shows "norm x = 1"
by (metis assms norm_minus_cancel norm_one power2_eq_1_iff)
lemma norm_less_p1: "norm x < norm (of_real (norm x) + 1 :: 'a)"
for x :: "'a::real_normed_algebra_1"
proof -
have "norm x < norm (of_real (norm x + 1) :: 'a)"
by (simp add: of_real_def)
then show ?thesis
by simp
qed
lemma prod_norm: "prod (\x. norm (f x)) A = norm (prod f A)"
for f :: "'a \ 'b::{comm_semiring_1,real_normed_div_algebra}"
by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
lemma norm_prod_le:
"norm (prod f A) \ (\a\A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))"
proof (induct A rule: infinite_finite_induct)
case empty
then show ?case by simp
next
case (insert a A)
then have "norm (prod f (insert a A)) \ norm (f a) * norm (prod f A)"
by (simp add: norm_mult_ineq)
also have "norm (prod f A) \ (\a\A. norm (f a))"
by (rule insert)
finally show ?case
by (simp add: insert mult_left_mono)
next
case infinite
then show ?case by simp
qed
lemma norm_prod_diff:
fixes z w :: "'i \ 'a::{real_normed_algebra_1, comm_monoid_mult}"
shows "(\i. i \ I \ norm (z i) \ 1) \ (\i. i \ I \ norm (w i) \ 1) \
norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
proof (induction I rule: infinite_finite_induct)
case empty
then show ?case by simp
next
case (insert i I)
note insert.hyps[simp]
have "norm ((\i\insert i I. z i) - (\i\insert i I. w i)) =
norm ((\<Prod>i\<in>I. z i) * (z i - w i) + ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * w i)"
(is "_ = norm (?t1 + ?t2)")
by (auto simp: field_simps)
also have "\ \ norm ?t1 + norm ?t2"
by (rule norm_triangle_ineq)
also have "norm ?t1 \ norm (\i\I. z i) * norm (z i - w i)"
by (rule norm_mult_ineq)
also have "\ \ (\i\I. norm (z i)) * norm(z i - w i)"
by (rule mult_right_mono) (auto intro: norm_prod_le)
also have "(\i\I. norm (z i)) \ (\i\I. 1)"
by (intro prod_mono) (auto intro!: insert)
also have "norm ?t2 \ norm ((\i\I. z i) - (\i\I. w i)) * norm (w i)"
by (rule norm_mult_ineq)
also have "norm (w i) \ 1"
by (auto intro: insert)
also have "norm ((\i\I. z i) - (\i\I. w i)) \ (\i\I. norm (z i - w i))"
using insert by auto
finally show ?case
by (auto simp: ac_simps mult_right_mono mult_left_mono)
next
case infinite
then show ?case by simp
qed
lemma norm_power_diff:
fixes z w :: "'a::{real_normed_algebra_1, comm_monoid_mult}"
assumes "norm z \ 1" "norm w \ 1"
shows "norm (z^m - w^m) \ m * norm (z - w)"
proof -
have "norm (z^m - w^m) = norm ((\ i < m. z) - (\ i < m. w))"
by simp
also have "\ \ (\i
by (intro norm_prod_diff) (auto simp: assms)
also have "\ = m * norm (z - w)"
by simp
finally show ?thesis .
qed
subsection \<open>Metric spaces\<close>
class metric_space = uniformity_dist + open_uniformity +
assumes dist_eq_0_iff [simp]: "dist x y = 0 \ x = y"
and dist_triangle2: "dist x y \ dist x z + dist y z"
begin
lemma dist_self [simp]: "dist x x = 0"
by simp
lemma zero_le_dist [simp]: "0 \ dist x y"
using dist_triangle2 [of x x y] by simp
lemma zero_less_dist_iff: "0 < dist x y \ x \ y"
by (simp add: less_le)
lemma dist_not_less_zero [simp]: "\ dist x y < 0"
by (simp add: not_less)
lemma dist_le_zero_iff [simp]: "dist x y \ 0 \ x = y"
by (simp add: le_less)
lemma dist_commute: "dist x y = dist y x"
proof (rule order_antisym)
show "dist x y \ dist y x"
using dist_triangle2 [of x y x] by simp
show "dist y x \ dist x y"
using dist_triangle2 [of y x y] by simp
qed
lemma dist_commute_lessI: "dist y x < e \ dist x y < e"
by (simp add: dist_commute)
lemma dist_triangle: "dist x z \ dist x y + dist y z"
using dist_triangle2 [of x z y] by (simp add: dist_commute)
lemma dist_triangle3: "dist x y \ dist a x + dist a y"
using dist_triangle2 [of x y a] by (simp add: dist_commute)
lemma abs_dist_diff_le: "\dist a b - dist b c\ \ dist a c"
using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
lemma dist_pos_lt: "x \ y \ 0 < dist x y"
by (simp add: zero_less_dist_iff)
lemma dist_nz: "x \ y \ 0 < dist x y"
by (simp add: zero_less_dist_iff)
declare dist_nz [symmetric, simp]
lemma dist_triangle_le: "dist x z + dist y z \ e \ dist x y \ e"
by (rule order_trans [OF dist_triangle2])
lemma dist_triangle_lt: "dist x z + dist y z < e \ dist x y < e"
by (rule le_less_trans [OF dist_triangle2])
lemma dist_triangle_less_add: "dist x1 y < e1 \ dist x2 y < e2 \ dist x1 x2 < e1 + e2"
by (rule dist_triangle_lt [where z=y]) simp
lemma dist_triangle_half_l: "dist x1 y < e / 2 \ dist x2 y < e / 2 \ dist x1 x2 < e"
by (rule dist_triangle_lt [where z=y]) simp
lemma dist_triangle_half_r: "dist y x1 < e / 2 \ dist y x2 < e / 2 \ dist x1 x2 < e"
by (rule dist_triangle_half_l) (simp_all add: dist_commute)
lemma dist_triangle_third:
assumes "dist x1 x2 < e/3" "dist x2 x3 < e/3" "dist x3 x4 < e/3"
shows "dist x1 x4 < e"
proof -
have "dist x1 x3 < e/3 + e/3"
by (metis assms(1) assms(2) dist_commute dist_triangle_less_add)
then have "dist x1 x4 < (e/3 + e/3) + e/3"
by (metis assms(3) dist_commute dist_triangle_less_add)
then show ?thesis
by simp
qed
subclass uniform_space
proof
fix E x
assume "eventually E uniformity"
then obtain e where E: "0 < e" "\x y. dist x y < e \ E (x, y)"
by (auto simp: eventually_uniformity_metric)
then show "E (x, x)" "\\<^sub>F (x, y) in uniformity. E (y, x)"
by (auto simp: eventually_uniformity_metric dist_commute)
show "\D. eventually D uniformity \ (\x y z. D (x, y) \ D (y, z) \ E (x, z))"
using E dist_triangle_half_l[where e=e]
unfolding eventually_uniformity_metric
by (intro exI[of _ "\(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
(auto simp: dist_commute)
qed
lemma open_dist: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)"
by (simp add: dist_commute open_uniformity eventually_uniformity_metric)
lemma open_ball: "open {y. dist x y < d}"
unfolding open_dist
proof (intro ballI)
fix y
assume *: "y \ {y. dist x y < d}"
then show "\e>0. \z. dist z y < e \ z \ {y. dist x y < d}"
by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt)
qed
subclass first_countable_topology
proof
fix x
show "\A::nat \ 'a set. (\i. x \ A i \ open (A i)) \ (\S. open S \ x \ S \ (\i. A i \ S))"
proof (safe intro!: exI[of _ "\n. {y. dist x y < inverse (Suc n)}"])
fix S
assume "open S" "x \ S"
then obtain e where e: "0 < e" and "{y. dist x y < e} \ S"
by (auto simp: open_dist subset_eq dist_commute)
moreover
from e obtain i where "inverse (Suc i) < e"
by (auto dest!: reals_Archimedean)
then have "{y. dist x y < inverse (Suc i)} \ {y. dist x y < e}"
by auto
ultimately show "\i. {y. dist x y < inverse (Suc i)} \ S"
by blast
qed (auto intro: open_ball)
qed
end
instance metric_space \<subseteq> t2_space
proof
fix x y :: "'a::metric_space"
assume xy: "x \ y"
let ?U = "{y'. dist x y' < dist x y / 2}"
let ?V = "{x'. dist y x' < dist x y / 2}"
have *: "d x z \ d x y + d y z \ d y z = d z y \ \ (d x y * 2 < d x z \ d z y * 2 < d x z)"
for d :: "'a \ 'a \ real" and x y z :: 'a
by arith
have "open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}"
using dist_pos_lt[OF xy] *[of dist, OF dist_triangle dist_commute]
using open_ball[of _ "dist x y / 2"] by auto
then show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}"
by blast
qed
text \<open>Every normed vector space is a metric space.\<close>
instance real_normed_vector < metric_space
proof
fix x y z :: 'a
show "dist x y = 0 \ x = y"
by (simp add: dist_norm)
show "dist x y \ dist x z + dist y z"
using norm_triangle_ineq4 [of "x - z" "y - z"] by (simp add: dist_norm)
qed
subsection \<open>Class instances for real numbers\<close>
instantiation real :: real_normed_field
begin
definition dist_real_def: "dist x y = \x - y\"
definition uniformity_real_def [code del]:
"(uniformity :: (real \ real) filter) = (INF e\{0 <..}. principal {(x, y). dist x y < e})"
definition open_real_def [code del]:
"open (U :: real set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)"
definition real_norm_def [simp]: "norm r = \r\"
instance
by intro_classes (auto simp: abs_mult open_real_def dist_real_def sgn_real_def uniformity_real_def)
end
declare uniformity_Abort[where 'a=real, code]
lemma dist_of_real [simp]: "dist (of_real x :: 'a) (of_real y) = dist x y"
for a :: "'a::real_normed_div_algebra"
by (metis dist_norm norm_of_real of_real_diff real_norm_def)
declare [[code abort: "open :: real set \ bool"]]
instance real :: linorder_topology
proof
show "(open :: real set \ bool) = generate_topology (range lessThan \ range greaterThan)"
proof (rule ext, safe)
fix S :: "real set"
assume "open S"
then obtain f where "\x\S. 0 < f x \ (\y. dist y x < f x \ y \ S)"
unfolding open_dist bchoice_iff ..
then have *: "(\x\S. {x - f x <..} \ {..< x + f x}) = S" (is "?S = S")
by (fastforce simp: dist_real_def)
moreover have "generate_topology (range lessThan \ range greaterThan) ?S"
by (force intro: generate_topology.Basis generate_topology_Union generate_topology.Int)
ultimately show "generate_topology (range lessThan \ range greaterThan) S"
by simp
next
fix S :: "real set"
assume "generate_topology (range lessThan \ range greaterThan) S"
moreover have "\a::real. open {..
unfolding open_dist dist_real_def
proof clarify
fix x a :: real
assume "x < a"
then have "0 < a - x \ (\y. \y - x\ < a - x \ y \ {..
then show "\e>0. \y. \y - x\ < e \ y \ {..
qed
moreover have "\a::real. open {a <..}"
unfolding open_dist dist_real_def
proof clarify
fix x a :: real
assume "a < x"
then have "0 < x - a \ (\y. \y - x\ < x - a \ y \ {a<..})" by auto
then show "\e>0. \y. \y - x\ < e \ y \ {a<..}" ..
qed
ultimately show "open S"
by induct auto
qed
qed
instance real :: linear_continuum_topology ..
lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
lemmas open_real_lessThan = open_lessThan[where 'a=real]
lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
lemmas closed_real_atMost = closed_atMost[where 'a=real]
lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
instance real :: ordered_real_vector
by standard (auto intro: mult_left_mono mult_right_mono)
subsection \<open>Extra type constraints\<close>
text \<open>Only allow \<^term>\<open>open\<close> in class \<open>topological_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
(\<^const_name>\<open>open\<close>, SOME \<^typ>\<open>'a::topological_space set \<Rightarrow> bool\<close>)\<close>
text \<open>Only allow \<^term>\<open>uniformity\<close> in class \<open>uniform_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
(\<^const_name>\<open>uniformity\<close>, SOME \<^typ>\<open>('a::uniformity \<times> 'a) filter\<close>)\<close>
text \<open>Only allow \<^term>\<open>dist\<close> in class \<open>metric_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
(\<^const_name>\<open>dist\<close>, SOME \<^typ>\<open>'a::metric_space \<Rightarrow> 'a \<Rightarrow> real\<close>)\<close>
text \<open>Only allow \<^term>\<open>norm\<close> in class \<open>real_normed_vector\<close>.\<close>
setup \<open>Sign.add_const_constraint
(\<^const_name>\<open>norm\<close>, SOME \<^typ>\<open>'a::real_normed_vector \<Rightarrow> real\<close>)\<close>
subsection \<open>Sign function\<close>
lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
for x :: "'a::real_normed_vector"
by (simp add: sgn_div_norm)
lemma sgn_zero [simp]: "sgn (0::'a::real_normed_vector) = 0"
by (simp add: sgn_div_norm)
lemma sgn_zero_iff: "sgn x = 0 \ x = 0"
for x :: "'a::real_normed_vector"
by (simp add: sgn_div_norm)
lemma sgn_minus: "sgn (- x) = - sgn x"
for x :: "'a::real_normed_vector"
by (simp add: sgn_div_norm)
lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
for x :: "'a::real_normed_vector"
by (simp add: sgn_div_norm ac_simps)
lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
by (simp add: sgn_div_norm)
lemma sgn_of_real: "sgn (of_real r :: 'a::real_normed_algebra_1) = of_real (sgn r)"
unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y"
for x y :: "'a::real_normed_div_algebra"
by (simp add: sgn_div_norm norm_mult)
hide_fact (open) sgn_mult
lemma real_sgn_eq: "sgn x = x / \x\"
for x :: real
by (simp add: sgn_div_norm divide_inverse)
lemma zero_le_sgn_iff [simp]: "0 \ sgn x \ 0 \ x"
for x :: real
by (cases "0::real" x rule: linorder_cases) simp_all
lemma sgn_le_0_iff [simp]: "sgn x \ 0 \ x \ 0"
for x :: real
by (cases "0::real" x rule: linorder_cases) simp_all
lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp
declare norm_conv_dist [symmetric, simp]
lemma dist_0_norm [simp]: "dist 0 x = norm x"
for x :: "'a::real_normed_vector"
by (simp add: dist_norm)
lemma dist_diff [simp]: "dist a (a - b) = norm b" "dist (a - b) a = norm b"
by (simp_all add: dist_norm)
lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \m - n\"
proof -
have "dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))"
by simp
also have "\ = of_int \m - n\" by (subst dist_diff, subst norm_of_int) simp
finally show ?thesis .
qed
lemma dist_of_nat:
"dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \int m - int n\"
by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
subsection \<open>Bounded Linear and Bilinear Operators\<close>
lemma linearI: "linear f"
if "\b1 b2. f (b1 + b2) = f b1 + f b2"
"\r b. f (r *\<^sub>R b) = r *\<^sub>R f b"
using that
by unfold_locales (auto simp: algebra_simps)
lemma linear_iff:
"linear f \ (\x y. f (x + y) = f x + f y) \ (\c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
(is "linear f \ ?rhs")
proof
assume "linear f"
then interpret f: linear f .
show "?rhs" by (simp add: f.add f.scale)
next
assume "?rhs"
then show "linear f" by (intro linearI) auto
qed
lemmas linear_scaleR_left = linear_scale_left
lemmas linear_imp_scaleR = linear_imp_scale
corollary real_linearD:
fixes f :: "real \ real"
assumes "linear f" obtains c where "f = (*) c"
by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
lemma linear_times_of_real: "linear (\x. a * of_real x)"
by (auto intro!: linearI simp: distrib_left)
(metis mult_scaleR_right scaleR_conv_of_real)
locale bounded_linear = linear f for f :: "'a::real_normed_vector \ 'b::real_normed_vector" +
assumes bounded: "\K. \x. norm (f x) \ norm x * K"
begin
lemma pos_bounded: "\K>0. \x. norm (f x) \ norm x * K"
proof -
obtain K where K: "\x. norm (f x) \ norm x * K"
using bounded by blast
show ?thesis
proof (intro exI impI conjI allI)
show "0 < max 1 K"
by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
next
fix x
have "norm (f x) \ norm x * K" using K .
also have "\ \ norm x * max 1 K"
by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
finally show "norm (f x) \ norm x * max 1 K" .
qed
qed
lemma nonneg_bounded: "\K\0. \x. norm (f x) \ norm x * K"
using pos_bounded by (auto intro: order_less_imp_le)
lemma linear: "linear f"
by (fact local.linear_axioms)
end
lemma bounded_linear_intro:
assumes "\x y. f (x + y) = f x + f y"
and "\r x. f (scaleR r x) = scaleR r (f x)"
and "\x. norm (f x) \ norm x * K"
shows "bounded_linear f"
by standard (blast intro: assms)+
locale bounded_bilinear =
fixes prod :: "'a::real_normed_vector \ 'b::real_normed_vector \ 'c::real_normed_vector"
(infixl "**" 70)
assumes add_left: "prod (a + a') b = prod a b + prod a' b"
and add_right: "prod a (b + b') = prod a b + prod a b'"
and scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
and scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)"
and bounded: "\K. \a b. norm (prod a b) \ norm a * norm b * K"
begin
lemma pos_bounded: "\K>0. \a b. norm (a ** b) \ norm a * norm b * K"
proof -
obtain K where "\a b. norm (a ** b) \ norm a * norm b * K"
using bounded by blast
then have "norm (a ** b) \ norm a * norm b * (max 1 K)" for a b
by (rule order.trans) (simp add: mult_left_mono)
then show ?thesis
by force
qed
lemma nonneg_bounded: "\K\0. \a b. norm (a ** b) \ norm a * norm b * K"
using pos_bounded by (auto intro: order_less_imp_le)
lemma additive_right: "additive (\b. prod a b)"
by (rule additive.intro, rule add_right)
lemma additive_left: "additive (\a. prod a b)"
by (rule additive.intro, rule add_left)
lemma zero_left: "prod 0 b = 0"
by (rule additive.zero [OF additive_left])
lemma zero_right: "prod a 0 = 0"
by (rule additive.zero [OF additive_right])
lemma minus_left: "prod (- a) b = - prod a b"
by (rule additive.minus [OF additive_left])
lemma minus_right: "prod a (- b) = - prod a b"
by (rule additive.minus [OF additive_right])
lemma diff_left: "prod (a - a') b = prod a b - prod a' b"
by (rule additive.diff [OF additive_left])
lemma diff_right: "prod a (b - b') = prod a b - prod a b'"
by (rule additive.diff [OF additive_right])
lemma sum_left: "prod (sum g S) x = sum ((\i. prod (g i) x)) S"
by (rule additive.sum [OF additive_left])
lemma sum_right: "prod x (sum g S) = sum ((\i. (prod x (g i)))) S"
by (rule additive.sum [OF additive_right])
lemma bounded_linear_left: "bounded_linear (\a. a ** b)"
proof -
obtain K where "\a b. norm (a ** b) \ norm a * norm b * K"
using pos_bounded by blast
then show ?thesis
by (rule_tac K="norm b * K" in bounded_linear_intro) (auto simp: algebra_simps scaleR_left add_left)
qed
lemma bounded_linear_right: "bounded_linear (\b. a ** b)"
proof -
obtain K where "\a b. norm (a ** b) \ norm a * norm b * K"
using pos_bounded by blast
then show ?thesis
by (rule_tac K="norm a * K" in bounded_linear_intro) (auto simp: algebra_simps scaleR_right add_right)
qed
lemma prod_diff_prod: "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)"
by (simp add: diff_left diff_right)
lemma flip: "bounded_bilinear (\x y. y ** x)"
proof
show "\K. \a b. norm (b ** a) \ norm a * norm b * K"
by (metis bounded mult.commute)
qed (simp_all add: add_right add_left scaleR_right scaleR_left)
lemma comp1:
assumes "bounded_linear g"
shows "bounded_bilinear (\x. (**) (g x))"
proof unfold_locales
interpret g: bounded_linear g by fact
show "\a a' b. g (a + a') ** b = g a ** b + g a' ** b"
"\a b b'. g a ** (b + b') = g a ** b + g a ** b'"
"\r a b. g (r *\<^sub>R a) ** b = r *\<^sub>R (g a ** b)"
"\a r b. g a ** (r *\<^sub>R b) = r *\<^sub>R (g a ** b)"
by (auto simp: g.add add_left add_right g.scaleR scaleR_left scaleR_right)
from g.nonneg_bounded nonneg_bounded obtain K L
where nn: "0 \ K" "0 \ L"
and K: "\x. norm (g x) \ norm x * K"
and L: "\a b. norm (a ** b) \ norm a * norm b * L"
by auto
have "norm (g a ** b) \ norm a * K * norm b * L" for a b
by (auto intro!: order_trans[OF K] order_trans[OF L] mult_mono simp: nn)
then show "\K. \a b. norm (g a ** b) \ norm a * norm b * K"
by (auto intro!: exI[where x="K * L"] simp: ac_simps)
qed
lemma comp: "bounded_linear f \ bounded_linear g \ bounded_bilinear (\x y. f x ** g y)"
by (rule bounded_bilinear.flip[OF bounded_bilinear.comp1[OF bounded_bilinear.flip[OF comp1]]])
end
lemma bounded_linear_ident[simp]: "bounded_linear (\x. x)"
by standard (auto intro!: exI[of _ 1])
lemma bounded_linear_zero[simp]: "bounded_linear (\x. 0)"
by standard (auto intro!: exI[of _ 1])
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 0.359 Sekunden
(vorverarbeitet)
]
|
|
