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



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

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