Re: [isabelle] Introduction rule for quantifiers over sets of pairs



Hi Stephan,

On Fri, 2012-11-16 at 14:14 +0100, Stephan van Staden wrote:
> This one should be simple. I'm looking for the name of the rule that 
> will do the job of RRR below:
> 
> lemma "\<forall> (a,b) \<in> S. P"
> proof (rule RRR)
>    fix a b
>    assume "(a,b) \<in> S"
>    show "P" sorry
> qed

clarify may do more than you want if S or P are compound terms. Here is
another solution:

lemma RRR:
 assumes "⋀a b. (a,b) ∈ S ⟹ P"
 shows "∀ (a,b) ∈ S. P"
by (metis assms splitI2)

Best regards,
Tjark






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