Re: [isabelle] Lemma [OF ..] unification with \<And> parts



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"
>>      sorry
>>
>>    lemma l2: "(\<And> E E'. E' \<subseteq> E ==> P E ==> P E')"
>>      sorry
>>
>> writing
>>    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 MHonArc.