Re: [isabelle] A very strange case



When this sort of thing happens, it is a good idea to enable "show types". You then discover that these two variables have got different types. 

goal (1 subgoal):
 1. single_valued (set (zip L ?L0.0)) ==> single_valued (set (zip L L0))
variables:
  L0 :: 'c list
  ?L0.0 :: 'a list
  L :: 'b list

You can correct the situation by constraining their types explicitly.

lemma test:"[|\<forall> L0::'a list. (single_valued   (set (zip L L0 ))) |]
==> (single_valued (set (zip L (L0::'a list))))"

The polymorphism of the predicate single_valued allows your situation to occur. The abstract predicate P is not polymorphic.

Larry Paulson


On 25 May 2010, at 15:37, li yongjian wrote:

> 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.






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