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



"What's happening" is a technical question about Isabelle's internals, but the other question is whether you really need to do things this way. The purpose of meta-level connectives such as !! is to create a framework in which proofs can be constructed. If you are doing things with the framework itself, then to some extent you become an implementer and you have to expect things to become very tricky. But there may be a way to conduct your proof within the style shown in the various tutorials.

Larry

On 11 May 2013, at 17:12, "C. Diekmann" <diekmann at in.tum.de> wrote:

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