Email Gateway (Aug 18 2022 at 14:25): 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
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
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
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: Nov 21 2024 at 12:39 UTC