Re: [isabelle] Introduction rule for quantifiers over sets of pairs
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
clarify may do more than you want if S or P are compound terms. Here is
assumes "⋀a b. (a,b) ∈ S ⟹ P"
shows "∀ (a,b) ∈ S. P"
by (metis assms splitI2)
This archive was generated by a fusion of
Pipermail (Mailman edition) and