Re: [isabelle] Lemma [OF ..] unification with \<And> parts
Am 11/05/2013 18:12, schrieb C. Diekmann:
> 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]
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.
> 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