Re: [isabelle] Question about sets?

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,

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.


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