Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Questions regarding endomorphisms of real norm...


view this post on Zulip Email Gateway (May 12 2021 at 20:58):

From: "Luckhardt, Daniel" <daniel.luckhardt@mathematik.uni-goettingen.de>
Hi,

I want to tell Isabelle that the bounded linear functions from a real normed vector space to itself form a real normed algebra. My approach is to formalize it parallel to and basing on what is already in the theory Bounded_Linear_Function, namely

typedef ‹tag important› (overloaded) ('a, 'b) blinfun ("(_ ⇒⇩L /_)" [22, 21] 21) =
"{f::'a::real_normed_vector⇒'b::real_normed_vector. bounded_linear f}"
morphisms blinfun_apply Blinfun
by (blast intro: bounded_linear_intros)

So my attempt is

typedef ‹tag important› (overloaded) ('a) blinalg =
"UNIV :: ('a ⇒⇩L 'a) set"
morphisms blinalg_apply Blinalg
by simp

But unfortunately, when I want to do the instantiation

instantiation blinalg :: (real_normed_vector) real_normed_algebra
begin
lift_definition times_blinalg :: "('a ⇒⇩L 'a) ⇒ ('a ⇒⇩L 'a) ⇒ ('a ⇒⇩L 'a)" is "λ a b x. a (b x)" by (rule bounded_linear_compose)

lift_definition norm_blinalg :: "'a ⇒⇩L 'a ⇒ real" is onorm .
...
end

there is a conflict with the instantiation of blinfun as real_normed_vector. The error message is

Clash of specifications for norm:
"Play_type.norm_blinfun_inst.norm_blinfun_def"⌂
"Bounded_Linear_Function.norm_blinfun_inst.norm_blinfun_def"⌂
The error(s) above occurred in definition "norm_blinfun_def":
"norm ≡ Play_type.norm_blinfun_inst.norm_blinfun"

How do I get around this?

Secondary questions:

1. What is the function of "setup_lifting type_definition_blinfun" where is it documented?
2. What is the difference (if it exists) between "definition" and "lift_definition" (besides that the syntax is a bit different)
3. What is the "morphisms" doing, where is it documented?

Daniel

view this post on Zulip Email Gateway (May 14 2021 at 15:28):

From: Fabian Immler via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Daniel,

The AFP already contains such a formalisation, very similar to your approach:
https://www.isa-afp.org/browser_info/current/AFP/Ordinary_Differential_Equations/Bounded_Linear_Operator.html <https://www.isa-afp.org/browser_info/current/AFP/Ordinary_Differential_Equations/Bounded_Linear_Operator.html>

setup_lifting is documented in the Isabelle/Isar Reference Manual (11.9.2 Lifting Package).
https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf <https://isabelle.in.tum.de/dist/Isabelle2021/doc/isar-ref.pdf>

In your example, "setup_lifting type_definition_blinalg" sets up the Lifting Package such that you can define constants involving the type “‘a blinalg” in terms of constants involving the concrete type “(‘a, ‘a) blinfun”.

For the instantiation of “norm_blinalg", you have to provide a definition for the type that you want to instantiate ("‘a blinalg”), i.e., the following should work (with "setup_lifting type_definition_blinalg” after your typedef):

lift_definition norm_blinalg :: "'a blinalg ⇒ real" is norm .

Hope this helps,
Fabian


Last updated: Sep 25 2021 at 09:17 UTC