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



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.