# Re: [isabelle] Pairs in sets

On Tuesday 21 November 2006 07:29, Peter Lammich wrote:
> 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 ?
The reason fin does not work as a simplification rule is because it loops:
Notice that the right-hand side mentions "f {x}", which is an instance of the
pattern on the left-hand side.
I can think of two workarounds. First, you can use (subst fin); the subst
tactic only applies the rewrite once, not repeatedly like simp does.
Alternatively, you can use (simp add: fin [of X]) or (simp add: fin [where
X=X]). This prevents the simplifier from looping, since the instantiated rule
will not match terms like "f {x}".
- Brian

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