# Re: [isabelle] Arg_cong question

On Sun, 3 Aug 2008, Phil Scott wrote:
> 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
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

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