Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 11:04):

From: "C. Diekmann" <diekmann@in.tum.de>
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

Last updated: Apr 26 2024 at 12:28 UTC