Email Gateway (Aug 18 2022 at 09:43): Email Gateway (Aug 18 2022 at 09:43):From: Vaidas Gasiunas <gasiunas@informatik.tu-darmstadt.de>
In Isabelle there is a nice property, that from "f a = x" "f b = y" it
automatically concludes that "x = y".
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?
Greetings,
Vaidas
smime.p7s
Email Gateway (Aug 18 2022 at 09:43):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 09:44):From: Vaidas Gasiunas <gasiunas@informatik.tu-darmstadt.de>
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
Last updated: May 06 2024 at 20:16 UTC