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.