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.