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.