Email Gateway (Aug 18 2022 at 17:39): Email Gateway (Aug 18 2022 at 17:39):From: Jeremy Dawson <jlcaadawson@netspeed.com.au>
Because of exactly this situation some years ago I enquired if it could
be possible to turn off higher order unification (ie, leaving
first-order unification), so then one could simply use arg_cong2
(which would in effect look like
... ==> app (app f a) c = ..., so would unify unambiguously with your goal)
Jeremy
Email Gateway (Aug 18 2022 at 17:42):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I have a goal of the form:
I a b ==> I a' b'
how to transform this goal into
a=a' &&& b=b'
which can (in my case) be easily solved by auto.
Optimal would be a proof like this:
by (auto {intro,elim,dest,simp}: some_rule)
I tried to find an adequate rule via find_thms, but had no success.
Best,
Peter
Email Gateway (Aug 18 2022 at 17:43):From: Lars Noschinski <noschinl@in.tum.de>
Have a look at the rules app_cong and app_cong2. You may need to
instantiate them first.
-- Lars
Email Gateway (Aug 18 2022 at 17:44):From: Peter Lammich <peter.lammich@uni-muenster.de>
Probably, you mean arg_cong and arg_cong2 ??? A theorem named app_cong
does not exist.
An
apply (subst arg_cong2[where f=I]) by auto
does the job, but introduces some odd-looking schematic variables in
between.
Thanks
Peter
Lars Noschinski schrieb:
Email Gateway (Aug 18 2022 at 17:45):From: Lars Noschinski <noschinl@in.tum.de>
On 03.05.2011 15:58, Peter Lammich wrote:
Probably, you mean arg_cong and arg_cong2 ??? A theorem named app_cong
does not exist.
Yes, sorry.
An
apply (subst arg_cong2[where f=I]) by auto
does the job, but introduces some odd-looking schematic variables in
between.
In your case, this rule is more suitable as an introduction rule, i.e.
by (rule arg_cong2[where f=I]) auto
-- Lars
Email Gateway (Aug 18 2022 at 17:46):From: Peter Lammich <peter.lammich@uni-muenster.de>
This does not work.
thm arg_cong2[where f=I]
yields
[|?a = ?b; ?c = ?d|] ==> I ?a ?c = I ?b ?d
and the conclusion of this rule (topmost operator is =) does not unify
with "I a' b'", so you cannot use it as introduction rule.
Indeed, apply (rule arg_cong2[where f=I]) fails.
However, a (lengthy)
apply (erule rev_iffD2[OF _ arg_cong2[where f=I]])
does the job, and yields a'=a &&& b'=b
I have defined a shortcut for rev_iffD2[OF _ arg_cong2], and use this.
Best and thanks again,
Peter
Last updated: Nov 21 2024 at 12:39 UTC