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
hence "D"

Larry

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"
>>>     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.