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



Peter,

On Sunday 19 February 2006 11:36, Peter wrote:
>   lemma bug: "?A & ?B & ?XYZZY --> ?XYZZY" by blast
>
> outputs:
> lemma bug: ?A & ?B & [] \<in> lists ?Aa --> [] \<in> lists ?Aa

as Larry already wrote, schematic variables can be replaced by any well-formed 
term.  If you find the above behavior surprising, maybe you just want to 
input your lemma using free variables (without the question marks), e.g.

  lemma foo: "A & B & XYZZY --> XYZZY" by blast

NB: Isabelle issues a warning "Goal statement contains unbound schematic 
variable(s)" for the "bug" lemma.

Best,
Tjark





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