# Re: [isabelle] A quick question about fixing variables in a proof

In your example, func is fixed and therefore it cannot be unified with anything.
It isn't easy to introduce unifiable variables in Isar.
Larry Paulson
On 14 Dec 2009, at 02:56, munddr at googlemail.com wrote:
> Hi,
>
> I'm trying to just fix a functional variable in a proof as follows:
>
> typedecl S
> typedecl T
>
> consts
> G :: "S * T => real"
> s :: T
> f :: T
>
> locale A =
> fixes p :: Obj
> assumes cons: "!! t1 t2. G(p,t1) = G(p,t2)"
>
> locale B =
> ...
>
> lemma A_B_inconsistent:
> assumes "A p"
> shows "False"
> proof -
> fix func
> interpret localA: A p
> by fact
> interpret localB: B p
> by fact
> show "False"
> proof -
> have "func(p,s) = func(p,f)"
> using localA.cons
> by auto
> qed
> next
> ...
>
> Does anyone know how to unify 'func' to G and s/f to the second argument? Why can't auto unify them?
>
> Any help will be much appreciated.
>
> Thank you
> John

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