Email Gateway (Aug 19 2022 at 11:11): Email Gateway (Aug 19 2022 at 11:11):From: Brian Huffman <huffman@in.tum.de>
Hi Roger,
I'm responding to the isabelle-users list, which is a better venue for
this question.
You will want to start your proof with rule the_equality, and then try
to discharge the remaining goals.
During a proof, you can find rules that match the current goal using the command
find_theorems intro
or to limit the list to rules involving THE, try:
find_theorems intro "THE _. _"
By the way, for your particular goal, you will probably need to assume
also that there exists "a" such that f a = {c1, c2, c3}; otherwise "A"
is not uniquely determined.
Hope this helps,
Last updated: Nov 21 2024 at 12:39 UTC