Email Gateway (Aug 18 2022 at 13:28): Email Gateway (Aug 18 2022 at 13:28):From: Chris Capel <pdf23ds@gmail.com>
I have this lemma in the format "[| A; B |] ==> ALL x. C x". I want to
apply allI to the rule to get rid of the ALL before applying it with
apply (rule ...), which ought to be a simple task. I was thinking it
would be something like apply (rule myLemma[THEN/OF allI]). However,
that doesn't work, and nothing else I've tried has either. You'd think
there would be a way, but as far as I can tell, there's no
attribute-based analogue of RS or (rule ...). So I have to state the
lemma sans ALL as a new lemma and prove it.
Note, I'm sure there's plenty of nice ways to do it in Isar, but I've
given up on Isar for now because my goals are quite large and I can't
figure out how to get around stating them over and over in full, even
with higher-order-unification-based abbreviation.
Chris Capel
Email Gateway (Aug 18 2022 at 13:28):From: Alexander Krauss <krauss@in.tum.de>
Hi Chris,
Try
apply (rule myLemma[THEN spec])
allI is what you do on goals, but on facts you need elimination.
Alex
Last updated: Nov 21 2024 at 12:39 UTC