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

[C. Diekmann]

Hello,

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. I get
(\<And>E E'. E' \<subseteq> E ==> ?P E ==> ?E'1 E E' \<subseteq> ?E1 E E')
==> (\<And>E E'. E' ⊆ E ==> ?P E ==> ?P1 E E' (?E1 E E')) ==> ?D
[%E E'. ?P1 E E' (?E'1 E E') =?= %E. ?P]

What am I doing wrong, what is happening? In lemma l1, I conclude D
from some (anti-monotonicity) of P. In lemma l2 I show this
anti-monotonicity. Is there a better way to express this?

Symbols: \<And> corresponds to /\, or !! written in ASCII.

Regards
Cornelius

[Tobias Nipkow]

Am 11/05/2013 18:12, schrieb C. Diekmann:
> Hello,
>
> 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. I get
> (\<And>E E'. E' \<subseteq> E ==> ?P E ==> ?E'1 E E' \<subseteq> ?E1 E E')
> ==> (\<And>E E'. E' ⊆ E ==> ?P E ==> ?P1 E E' (?E1 E E')) ==> ?D
> [%E E'. ?P1 E E' (?E'1 E E') =?= %E. ?P]

OF treats !! and ==> specially and lifts l2 over l1. The same thing happens when
you apply a rule to a proof state with !! and ==>. In the latter situation you
can prevent that by using `fact' instead of rule, but I don't know if there is
an analogue for OF. Would like to have that from time to time, too.

Tobias

[Lawrence Paulson]

"What's happening" is a technical question about Isabelle's internals, but the other question is whether you really need to do things this way. The purpose of meta-level connectives such as !! is to create a framework in which proofs can be constructed. If you are doing things with the framework itself, then to some extent you become an implementer and you have to expect things to become very tricky. But there may be a way to conduct your proof within the style shown in the various tutorials.

Larry

[Makarius]

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

Since contemporary Isabelle has a bit too many manuals to keep an
overview, it might help to look at the "Old Introduction to Isabelle"
manual -- where "Isabelle" means Isabelle/Pure, not Isabelle/HOL -- or the
paper "The next 700 theorem provers" by Larry Paulson, 1990.


Makarius

[C. Diekmann]

2013/5/13 Makarius <maka...@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.

[Lawrence Paulson]

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