[isabelle] Blast behaves strangely with free schematic variables



I downloaded Isabelle2005 just now following the installation
instructions at

   http://www.cl.cam.ac.uk/Research/HVG/Isabelle/installation.html

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

   theory ToyList
   imports PreList
   begin

   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.

-- 
Tim Freeman               http://www.fungible.com           tim at fungible.com
Pass it on: The Integral Fast Reactor can provide safe, clean
energy.  Politically motivated misrepresentation stopped the research.
Check it out at: http://en.wikipedia.org/wiki/Integral_Fast_Reactor






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