Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] The-operator


view this post on Zulip 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: Mar 29 2024 at 12:28 UTC