# Re: [isabelle] [isabelle-dev] The-operator

On Wed, May 22, 2013 at 8:14 AM, Roger H. <s57076 at hotmail.com> wrote:
> Hello,
>
>
> how can i prove the following:
>
>
> ( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) = {c1, c2, c3} ?
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,
- Brian

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