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.