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

On Mon, Dec 14, 2009 at 4:04 PM, Makarius <makarius at> wrote:
> On Mon, 14 Dec 2009, munddr at 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

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

Any help will be much appreciated.

Thank you

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