[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.