[isabelle] Lemma [OF ..] unification with \<And> parts
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. 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and