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.