Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A quick question about fixing variables in a p...


view this post on Zulip Email Gateway (Aug 18 2022 at 14:25):

From: munddr@googlemail.com
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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:25):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:25):

From: Makarius <makarius@sketis.net>
Because auto (and the Isar proof language in general) observe the logical
scopes of abstract entities. In the context of your proof, "func", "G",
"s", "f" are all fixed, to there is no way to instantiate them (via
unification or other means). While global "consts" can never be
instantiated without leaving the background theory itself, a locally fixed
entity like "func" becomes arbitrary after leaving it scope. Cf. the
following canonical Isar pattern:

{
fix x
have "B x" sorry
}
have "B a" by fact

Anyway, I couldn't see what you where trying to do. Can you explain the
reasoning informally?

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 14:25):

From: John Munroe <munddr@googlemail.com>
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)GHeight(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


Last updated: Mar 28 2024 at 16:17 UTC