Re: [isabelle] Blast behaves strangely with free schematic variables

Tim Freeman wrote:

I downloaded Isabelle2005 just now following the installation
instructions at

and if I start my "ToyList.thy" file with

  theory ToyList
  imports PreList

  lemma bug: "?A & ?B & ?XYZZY \<longrightarrow> ?XYZZY" by blast

and go to the end and press control-c control-enter, I see this in the
response window:

  lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n

I had expected it to say:

  lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY

I was surprised by the intruction of the "gcd" operator. If I change
"blast" to "auto", I do get the output I expected.

I'm getting similiar results, with Main imported instead of PreList:

theory Scratch
imports Main

 lemma bug: "?A & ?B & ?XYZZY --> ?XYZZY" by blast

lemma bug: ?A & ?B & [] \<in> lists ?Aa --> [] \<in> lists ?Aa

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