Re: [isabelle] Lemma [OF ..] unification with \<And> parts
Another possibility might be to structure your proof something like this:
have "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')" sorry
On 14 May 2013, at 13:40, C. Diekmann <diekmann at in.tum.de> wrote:
> 2013/5/13 Makarius <makarius at sketis.net>:
>> On Sat, 11 May 2013, C. Diekmann wrote:
>>> given these two lemmata
>>> lemma l1: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E') ==> D"
>>> lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
>>> thm l1[OF l2]
>>> I expected to get D. However, I get something very strange.
>> As already pointed out by Larry, rule composition via "OF" (or "THEN" with
>> different argument order), or "rule" as a proof method works exactly like
>> that. You should study relevant Isabelle documentation until you expect the
>> correct outcome and don't consider it to be strange. This is about
>> higher-order natural deduction in Isabelle/Pure. Applications should not
>> step out of that comfortable environment without good reason (which means
>> you need to understand first what is its very purpose).
> Thank you all for your answers. Today I learned that I want to use !
> (∀), the ordinary FOL all quantifier.
This archive was generated by a fusion of
Pipermail (Mailman edition) and