Re: [isabelle] Types for variables


> It can infer the types of all func, x and y and blast resolves it. However,
> if I change the LHS to a free variable:
> lemma lem1: "EX func x y.func x y = v"
> using ax
> by blast
> I wasn't so lucky. How come it can't unify v with B x y + C x y? What more
> do I need?

The free variable is to become a free/schematic variable of the theorem.
Hence its logically some arbitrary but fixed value which need not be
related to B and C.

On the other hand the claim is trivially true since there is the
constant v function (% is a lambda)

lemma lem2: "EX func x y. func x y = v"
apply (rule exI[where x="% x y . v"])
by simp

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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