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



Tim Freeman wrote:

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.

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

theory Scratch
imports Main
begin


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

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








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