Email Gateway (Aug 18 2022 at 09:50): Email Gateway (Aug 18 2022 at 09:50):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello everybody,
in a proof I used the "cases" method and it introduces a new universal
quantification on the variable 'a', but this variable already exists so I
can't fix it. I must fix a new variable 'k' and rewrite the later "assume"
and "show" replacing 'a' with 'k'.
In other words:
(have) P1 ==> P2 (* in P1 and P2 there are some
occurrences of an already fixed variable 'a' *)
apply (cases ad)
(produces) \<And>a. P1 ==> P2
(* now I can't execute "fix a; assume P1; show P2" because this 'a' capture
the already existing 'a' in P1 and P2 *)
There is a way to avoid the introduction of an already existing variable?
Thanks
Gabriele
Email Gateway (Aug 18 2022 at 09:52):From: Makarius <makarius@sketis.net>
On Fri, 27 Oct 2006, Gabriele Pozzani wrote:
in a proof I used the "cases" method and it introduces a new universal
quantification on the variable 'a', but this variable already exists so
I can't fix it. I must fix a new variable 'k' and rewrite the later
"assume" and "show" replacing 'a' with 'k'.
This is a bit hard to follow. Can you produce a more conrete example,
e.g. an Isar proof outline (with 'sorry' steps) that illustrates this?
There is a way to avoid the introduction of an already existing
variable?
Structured proof composition in Isar is oriented towards the actual proof
text, not the internal (hidden) goal state. This means, that a goal like
!!x. A x ==> B x
means that in the proof text one has to show "B x", while "A x" may be
assumed, in the context of a locally fixed x. E.g. your answer to the
above goal could be like this:
fix x
assume "A x"
show "B x" sorry
This piece of proof body is only loosely linked to the pending goal
situation. There is a lot of flexibility in rearrangeing the text (e.g.
assumptions may be permuted, or even ignored; the whole situation may be
generalized etc.). Naturally, local entities are subject to static
scoping and alpha-conversion, e.g. the above "x" can be replaced by
anything more appropriate, but is has to be declared explicitly.
Makarius
Last updated: May 03 2024 at 08:18 UTC