Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] limiting unfolding using definitions

Email Gateway (Aug 18 2022 at 15:09):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

I have a goal "f <= g" where f, g:: A => B => C.
I want to unfold the goal using le_fun_def only once:
"!! x . f x <= g x"
How can I achieve this goal? If I apply (unfold le_fun_def)
the goal becomes: "!! x y . f x y <= g x y".

I want to avoid re-typing (copying) the expressions f and g.

Best regards,

Viorel

Email Gateway (Aug 18 2022 at 15:09):

From: Alexander Krauss <krauss@in.tum.de>
apply (subst le_fun_def)

or, in this particular case

apply (rule le_funI)

Alex

Last updated: Nov 21 2024 at 12:39 UTC