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



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.