Re: [isabelle] Why does "also" fail in this proof?



On Sun, 7 May 2006, Robin Green wrote:

> I'm using Isabelle 2005, and I've picked up how to do some calculational 
> proofs in a "monkey-see, monkey-do" kind of way - i.e. not really 
> understanding the connecting commands like "also" and "have" and "show".

'also' merely composes the background calculation with the last fact. 
Several rules are tried in turn, cf. print_trans_rules.


> Can someone explain why, in the attached theory file, I get this error
> on the last line:

Because the calculational step does not make any progress -- your first 
step is reflexivity.  Such redundant cases are filtered out in order to 
achieve more robust guessing of rule instances.  Try this to see what 
happens internally:

  thm  calculation  this  transitive [OF calculation this]

Also note that equality reasoning is usually performed at the 
object-level, using "=" instead of "==".  (This is in contrast to the 
other connectives !! and ==>, which usually work better than ALL and -->).


	Makarius





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