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

On Mon, Dec 14, 2009 at 4:04 PM, Makarius <makarius at sketis.net> wrote:
> On Mon, 14 Dec 2009, munddr at googlemail.com wrote:
>
>
>
> Anyway, I couldn't see what you where trying to do. Can you explain the
> reasoning informally?
>
I see. What I'm trying to do is the following:
Given the following locales (formalising some (possibly wrong) physics
theories and (possibly wrong) experiments:
typedecl Obj
typedecl Energy
typedecl Time
consts
Vel :: "Obj * Time => real"
Height :: "Obj * Time => real"
TE :: "Obj * Time => real"
PE :: "Obj * Time => real"
KE :: "Obj * Time => real"
Mass :: "Obj => real"
G :: real
start :: Time
finish :: Time
locale A =
fixes p :: Obj
assumes te: "!!t. TE(p,t) = PE(p,t) + KE(p,t)"
and pe: "!!t. PE(p,t) = Mass(p)*G*Height(p,t)"
and ke: "!!t. KE(p,t) = Mass(p)*Vel(p,t)*Vel(p,t)"
and cons: "!! t1 t2. TE(p,t1) = TE(p,t2)"
locale B =
fixes p :: Obj
assumes vstart: "Vel(p,start) = 0"
and vfinish: "Vel(p,finish) = 0"
and hfinish: "Height(p,finish) = 0"
and mass: "Mass(p) > 0"
and height: "Height(p,start) > 0"
I want to prove a theorem that relates the two, e.g., there's a
function such that it equals to v1 in locale A but equals to v2 in
locale B, and v1 ~= v2. The two locales can't be merged because
together they would be inconsistent. Is it possible to do it with
Isar?
Any help will be much appreciated.
Thank you
John

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