# [isabelle] Arg_cong question

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?
--
Cheers.
Phil Scott
Msc student, University of Edinburgh

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*