Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about sets?

Email Gateway (Aug 18 2022 at 12:58):

From: Amine Chaieb <ac638@cam.ac.uk>
Your goal can be solved e.g. like this:

unfolding Collect_def
by blast

The key is to get the Collect away. It is somehow strange to write goals
like this, so I guess it is an intermediate goal where you in a previous
state used mem_def

Hope it helps,
Amine.

TIMOTHY KREMANN wrote:

Email Gateway (Aug 18 2022 at 13:04):

From: TIMOTHY KREMANN <twksoa262@verizon.net>
I have the following subgoal:

\<And> (n::nat) (f::nat=>'a) (x::'a).
{y. \<exists> j < n . y = f j} x ==>
\<exists> i < n . f i = x

I need to get the j where x = f j and then instantiate the i to that value.
I am such a neophyte that I do not know how to do this.
Any suggestions would be appreciated.

Tim

Last updated: May 03 2024 at 12:27 UTC