*To*: John Munroe <munddr at googlemail.com>*Subject*: Re: [isabelle] Types for variables*From*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Date*: Thu, 03 Sep 2009 10:41:33 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <e4d7be570909020439p3f178de4sb94d331dfbb7794@mail.gmail.com>*References*: <e4d7be570909012125u67b7fc7n5a2c125e00aa6c57@mail.gmail.com> <4A9E34EF.9010801@uni-muenster.de> <e4d7be570909020439p3f178de4sb94d331dfbb7794@mail.gmail.com>

Hello > 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 -- Regards Christian Doczkal

**Attachment:
smime.p7s**

**References**:**[isabelle] Types for variables***From:*John Munroe

**Re: [isabelle] Types for variables***From:*Peter Lammich

**Re: [isabelle] Types for variables***From:*John Munroe

- Previous by Date: Re: [isabelle] Proving formulae from separate sets of axioms
- Next by Date: Re: [isabelle] Types for variables
- Previous by Thread: Re: [isabelle] Types for variables
- Next by Thread: Re: [isabelle] Types for variables
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list