Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A very strange case

Email Gateway (Aug 18 2022 at 15:21):

From: li yongjian <lyj238@gmail.com>
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

Email Gateway (Aug 18 2022 at 15:21):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Last updated: Apr 30 2024 at 01:06 UTC