Email Gateway (Aug 18 2022 at 12:17): Email Gateway (Aug 18 2022 at 12:17):From: Phil Scott <philscotted@blueyonder.co.uk>
Hi all.
I'm trying to prove the following in Isar:
F {A, B, C} => F {B, A, C}
where F is a constant I have previously introduced. The tactics auto and blast
will not prove this in a single step. Any ideas what the best way to go about
it is?
For now, I have settled with
from F {A, B, C} have "F {B, A, C}" using arg_cong[of "{A, B, C}" "{B, A,
C}" F] by blast
but I am still having to help blast out by explicitly binding all the
schematic variables of arg_cong. Is this a problem with higher-order
unification? I wonder given that the following does not even go through:
have "{A, B, C} = {B, A, C}" by auto
with arg_cong have "F {A, B, C} = F {B, A, C}" .
unless I supply the ?f argument in arg_cong:
have "{A, B, C} = {B, A, C}" by auto
with arg_cong[where f = F] have "F {A, B, C} = F {B, A, C}" .
Any tips on how to best prove my original fact?
Email Gateway (Aug 18 2022 at 12:18):From: Makarius <makarius@sketis.net>
These rather low-level cong rules for basic equality are rarely needed in
practice -- the automated tools already treat equality in one way or the
other.
Here the Simplifier is used to make use of equations in a different
context:
have "{A, B, C} = {B, A, C}" by auto
then have "F {A, B, C} = F {B, A, C}" by simp
Alternatively, you can tweak the Simplifier context to normalize the
set insert expression like this:
have "F {A, B, C} = F {B, A, C}" by (simp add: insert_commute)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC