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
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 -->).
This archive was generated by a fusion of
Pipermail (Mailman edition) and