Re: [isabelle] Functional Relations



I have experimented with various formulations of the lemma, for example 
I tried to make an elimination rule like:

"[| (a, b) in myrel; (a, b') in myrel; [| (a, b) in myrel; b = b' |] ==> 
P |] ==> P"

Indeed "[| (a, b) in myrel; (a, b') in myrel |] ==> b = b'" works best 
as destruction rule. I can even mark it with [dest] and then it is 
applied successfully automatically.

Thanks,
Vaidas

----- Original Message ----- 
From: "Tobias Nipkow" <nipkow at in.tum.de>
To: "Vaidas Gasiunas" <gasiunas at informatik.tu-darmstadt.de>
Cc: <isabelle-users at cl.cam.ac.uk>
Sent: Thursday, September 28, 2006 10:05 AM
Subject: Re: [isabelle] Functional Relations


>
>
> Vaidas Gasiunas schrieb:
>> In Isabelle there is a nice property, that from "f a = x" "f b = y" 
>> it automatically concludes that "x = y".
>
> I hope not! That is, only if a=b. Then this is just rewriting.
>
>> Sometimes I define functions as inductive relations and prove that 
>> they are functional, e.g. "[| (a, b) in myrel; (a, b') in myrel |] 
>> ==> b = b'". How to achieve that such lemmas were applied 
>> automatically?
>
> If you give them to blast/fast/fastsimp/auto as dstruction rules, ie 
> via "dest: ..." (or "dest!: ...") they may help. In the case of 
> blast/fast only if one of b or b' is just a variable.
>
> Tobias 







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