[isabelle] A very strange case



Dear Isabelle Expert,

I meet a very strange case (in Isabelle2009):

I can not prove the following simple lemma:

lemma test:"[|\<forall> L0. (single_valued   (set (zip L L0 ))) |]
==> (single_valued (set (zip L L0)))"
  by(drule spec,simp)
  ----after using the command, Isabelle says failure.

But I can prove a more general lemma;

lemma test1:"[|\<forall> L0. (P   (set (zip L L0 ))) |]
\<Longrightarrow>( P (set (zip L L0)))"
  by(drule spec,simp)
  ---the command passes in Isabelle.

  I really can not understand this problem, is it a bug?

Yongjian Li




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