Email Gateway (Aug 22 2022 at 19:57): Email Gateway (Aug 22 2022 at 19:57):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
I defined a type class of operators between real vectors spaces using
typedef. Then I defined a type class consisting of the above-mentioned
operators which are also bounded. When I applied "transfer" in order to
prove that 0 + a = a: it works in the first case, but it does not work in
the second case. I know that it is possible to define both type classes
independently one from the other, but what I did, defining a type class
inside the other one should work as well (this hereditary approach is
typical in mathematical reasoning). The code is below.
Kind Regards,
José M.
theory real_bounded_operators
imports
"HOL-ex.Sketch_and_Explore"
Operator_Norm_Plus
begin
section ‹Linear operators›
(* The operators may be unbounded *)
typedef (overloaded) ('a::real_vector, 'b::real_vector) real_operator
= ‹{ f::'a⇒'b. linear f}›
using linear_zero by blast
setup_lifting type_definition_real_operator
lift_definition bounded_real_operator :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_operator ⇒ bool›
is ‹λ f. bounded_linear_axioms f›.
lift_definition ev_real_operator :: ‹('a::real_vector, 'b::real_vector)
real_operator ⇒ 'a ⇒ 'b›
is ‹λ f. λ x. f x›.
instantiation real_operator :: (real_vector, real_vector) ‹real_vector›
begin
lift_definition uminus_real_operator :: ‹('a, 'b) real_operator ⇒ ('a, 'b)
real_operator›
is ‹λ f. ( λ x. -f x)›
by (rule Real_Vector_Spaces.real_vector.linear_compose_neg)
lift_definition zero_real_operator :: ‹('a, 'b) real_operator› is ‹λ _::'a.
0::'b›
by (rule Real_Vector_Spaces.real_vector.linear_zero)
lift_definition minus_real_operator :: ‹('a, 'b) real_operator ⇒ ('a, 'b)
real_operator ⇒ ('a, 'b) real_operator›
is ‹λ f. λ g. ( λ x. f x - g x)›
by (rule Real_Vector_Spaces.real_vector.module_hom_sub)
lift_definition plus_real_operator :: ‹('a, 'b) real_operator ⇒ ('a, 'b)
real_operator ⇒ ('a, 'b) real_operator›
is ‹λ f. λ g. ( λ x. f x + g x)›
by (rule Real_Vector_Spaces.real_vector.linear_compose_add)
lift_definition scaleR_real_operator :: ‹real ⇒ ('a, 'b) real_operator ⇒
('a, 'b) real_operator›
is ‹λ c. λ f. (λ x. c *⇩R (f x))›
by (rule Real_Vector_Spaces.real_vector.linear_compose_scale_right)
instance
apply intro_classes
apply transfer
apply auto
apply transfer
apply auto
apply transfer
apply auto
apply transfer
apply auto
apply transfer
apply auto
apply transfer
apply (simp add: scaleR_add_right)
apply transfer
apply (simp add: scaleR_add_left)
apply transfer
apply simp
apply transfer
apply auto
done
end
section ‹Bounded linear operators›
typedef (overloaded) ('a::real_normed_vector, 'b::real_normed_vector)
real_bounded
= ‹{ f::('a, 'b) real_operator. bounded_real_operator f}›
apply transfer
using bounded_linear.axioms(2) bounded_linear_zero module_hom_zero by
blast
setup_lifting type_definition_real_bounded
lift_definition ev_real_bounded :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ 'a ⇒ 'b›
is ‹λ f. λ x. ev_real_operator f x›.
instantiation real_bounded :: (real_normed_vector, real_normed_vector)
‹real_vector›
begin
lift_definition uminus_real_bounded :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded›
is ‹λ f. -f›
apply transfer
using bounded_linear_minus bounded_linear.axioms(2) bounded_linear.intro
by auto
lift_definition zero_real_boudned :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_bounded›
is ‹0›
apply transfer
by (simp add: bounded_linear.axioms(2))
lift_definition minus_real_bounded :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded›
is ‹λ f. λ g. f - g›
apply transfer
using bounded_linear_sub bounded_linear_def by blast
lift_definition plus_real_bounded :: ‹('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded›
is ‹λ f g. f + g›
apply transfer
using bounded_linear_add bounded_linear_def by blast
lift_definition scaleR_real_bounded :: ‹real ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded ⇒ ('a::real_normed_vector,
'b::real_normed_vector) real_bounded›
is ‹λ c. λ f. c *⇩R f›
apply transfer
using bounded_linear_const_scaleR bounded_linear_def by blast
instance
apply intro_classes
apply transfer
apply auto
apply transfer
apply auto
apply transfer
sorry
end
end
link to the original file:
https://github.com/dominique-unruh/bounded-operators/blob/master/real_bounded_operators.thy
Last updated: Apr 23 2024 at 04:18 UTC