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.


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