Re: [isabelle] Pairs in sets



Peter Lammich wrote:
Hello all,

I have the following lemma:
consts f:: "'a set => 'a set"
lemma fin: "f X = \<Union> { f {x} | x . x : X }" sorry

And in a proof, I have to solve the following subgoal:

"f X = \<Union> { f {(a,b)} | a b . (a,b) : X }"

How to do this elegantly using lemma fin ?? Things like (simp add: fin) or (auto iff add: fin) do not work ?

Greetings and thanks in advance
 Peter Lammich


Peter,

If all else fails, try using the following lemma:


Goal "{ f {x} | x . x : X } = { f {(a,b)} | a b . (a,b) : X }";
### Obsolete goal command encountered
Level 0 (1 subgoal)
{f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
 1. {f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
val it = [] : Thm.thm list
> auto();
Level 1
{f {x} |x. x : X} = {f {(a, b)} |a b. (a, b) : X}
No subgoals!
val it = () : unit


Jeremy





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