Re: [PVS-HELP] Choose Function

["SongFu" <fsong@xxxxxxxxxxxxxxx>]

----- Original Message ----- 
From: "schoppekloppe" <schoppekloppe@yahoo.de>
To: <pvs-help@csl.sri.com>
Sent: Monday, April 20, 2009 11:29 PM
Subject: Re: [PVS-HELP] Choose Function


> SongFu schrieb:
>> I want know how to proof the following:
>>
>> choose({x: nat| x=1}) =1
> 
> Use the lemma "choose_singleton[nat]" and then expand "singleton".
> -- 
> Christian Henkel
> 
>


----- Original Message ----- 
From: John Rushby 
To: SongFu 
Cc: pvs-help@csl.sri.com 
Sent: Monday, April 20, 2009 11:31 PM
Subject: Re: [PVS-HELP] Choose Function


SongFu wrote:
> Dear everyone:
> I want know how to proof the following:
>  
> choose({x: nat| x=1}) =1
>  
> Thanks
> Song

If you look at the definition of choose (in the prelude), you'll see
its type makes this easy.

 (typepred "choose({x: nat | x = 1})")
then
 (hide 2) (grind)

John


Dear  Sir or Madam:

Both your method can fix this problem. Thank you!

Song