Email Gateway (Aug 22 2022 at 20:02): Email Gateway (Aug 22 2022 at 20:02):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
I tried to import the nonstandard analysis libraries but there is a
problem with "apply transfer" in the instantiation below. More concretely,
when I add to "import" the library
"HOL-Nonstandard_Analysis.HSEQ"
I obtain the following error message:
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(bounded_clinear ?aa2) ⟹
(bounded_clinear ?ba2) ⟹
(bounded_clinear ?ca2) ⟹
Abs_bounded (λt. Rep_bounded (Abs_bounded (λt. ?aa2 t + ?ba2 t)) t + ?ca2
t) =
Abs_bounded (λt. ?aa2 t + Rep_bounded (Abs_bounded (λt. ?ba2 t + ?ca2 t))
t)
Without importing this library, the proof was fine. This is the code where
the problem appeared:
instantiation bounded :: (complex_normed_vector, complex_normed_vector)
"semigroup_add"
begin
lift_definition plus_bounded :: "('a,'b) bounded ⇒ ('a,'b) bounded ⇒
('a,'b) bounded" is
‹λ f g. Abs_bounded (λ t. (Rep_bounded f) t + (Rep_bounded g) t)›.
instance
proof
fix a b c :: ‹('a::complex_normed_vector, 'b::complex_normed_vector)
bounded›
show ‹a + b + c = a + (b + c)›
apply transfer
proof transfer
fix a b c::‹'a ⇒ 'b›
assume ‹bounded_clinear a›
and ‹bounded_clinear b›
and ‹bounded_clinear c›
have ‹(λt. ( (λt. a t + b t)) t + c t)
= (λt. a t + ( (λt. b t + c t)) t)›
by (simp add: ordered_field_class.sign_simps(1))
hence ‹(λt. ( (λt. a t + b t)) t + c t)
= (λt. a t + Rep_bounded (Abs_bounded (λt. b t + c t)) t)›
by (simp add: Abs_bounded_inverse ‹bounded_clinear b›
‹bounded_clinear c› bounded_clinear_add)
hence ‹(λt. Rep_bounded (Abs_bounded (λt. a t + b t)) t + c t)
= (λt. a t + Rep_bounded (Abs_bounded (λt. b t + c t)) t)›
using Abs_bounded_inverse
by (simp add: Abs_bounded_inverse ‹bounded_clinear a›
‹bounded_clinear b› bounded_clinear_add)
thus ‹Abs_bounded
(λt. Rep_bounded (Abs_bounded (λt. a t + b t)) t + c t) =
Abs_bounded
(λt. a t + Rep_bounded (Abs_bounded (λt. b t + c t)) t)›
by simp
qed
qed
end
Link:
https://github.com/dominique-unruh/bounded-operators/blob/master/Bounded_Operators.thy
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 20:02):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Jose,
Non-standard analysis defines its own proof method "transfer", which transfers first-order
statements about the standard numbers to the non-standard numbers. So the "transfer" proof
method from the Transfer package is shadowed. You can still access it by its full name
"Transfer.transfer".
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 20:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,
it could be worth thinking about giving that particular nonstandard
analysis transfer machinery qualified names, but so far I did not come
up with a suitable prefix.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 20:03):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I agree with Florian’s proposal for changing some names in the library of Nonstandard Analysis (see below). Another problem with the compatibility is that in this library, the Greek letter epsilon is used in a rather unfamiliar way and the role of the traditional epsilon in Analysis is played by the letter e, which collapses with the notation for Euler’s number.
It is important to remark that nonstandard numbers play an important role in model theory, e.g., in the proof that Goodstein theorem cannot be proved using just Peano Axioms. There is a project to formalize that in Coq by Prof. Pierre Casteran.
Kind Regards,
José M.
Sent from my iPhone
Email Gateway (Aug 22 2022 at 20:04):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Florian,
What about "nsa_transfer"? Non-standard analysis used to be abbreviated as NSA for a long
time in Isabelle.
Andreas
Email Gateway (Aug 22 2022 at 20:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
What about "nsa_transfer"? Non-standard analysis used to be abbreviated
as NSA for a long time in Isabelle.
Did we ever consider »hyper«?
I.e. »hyper.transfer«, »»hyper.transfer_intro« etc.
Florian
Andreas
On 23/06/2019 11:25, Florian Haftmann wrote:
Dear all,
Non-standard analysis defines its own proof method "transfer", which
transfers first-order statements about the standard numbers to the
non-standard numbers. So the "transfer" proof method from the Transfer
package is shadowed. You can still access it by its full name
"Transfer.transfer".it could be worth thinking about giving that particular nonstandard
analysis transfer machinery qualified names, but so far I did not come
up with a suitable prefix.Cheers,
Florian
Email Gateway (Aug 22 2022 at 20:04):From: Jacques Fleuriot <jdf@inf.ed.ac.uk>
NSA is a standard acronym for nonstandard analysis, so nsa.transfer would make sense.
Jacques
Email Gateway (Aug 22 2022 at 20:04):From: Lawrence Paulson <lp15@cam.ac.uk>
That’s interesting to know. I hope that somebody will feel inspired to do something with this library.
Larry
Last updated: Apr 25 2024 at 12:23 UTC