Email Gateway (Aug 19 2022 at 17:04): Email Gateway (Aug 19 2022 at 17:04):From: Sven Schneider <sven.schneider.pub@gmx.de>
Yes of course, I can copy single warnings but how to copy all warnings
at once?
There seem to be no buffer/window which contains these information...
--Sven Schneider
0xF0E2AE90.asc
Email Gateway (Aug 19 2022 at 17:04):From: Sven Schneider <sven.schneider.pub@gmx.de>
Is rename_tac using 'ubiquitious backtracking'? I would not have
expected rename_tac to be so complex.
I had a more simple implementation in mind: a tactic-wrapper which
operates as follows.
(1) obtain the current list of variables
(2) apply rename_tac
(3) obtain the new list of variables
(4) print a warning if old-list = new-list
Then rename_tac could be replaced everywhere by the wrapper-tactic..
--Sven Schneider
0xF0E2AE90.asc
Email Gateway (Aug 19 2022 at 17:04):From: Larry Paulson <lp15@cam.ac.uk>
There must be some confusion here. No backtracking is needed for rename_tac.
The point is to make your proofs independent of names internally generated by the system. It isn’t wrong if the names you choose turn out to be the same as the internal ones.
Larry Paulson
Email Gateway (Aug 19 2022 at 17:04):From: Makarius <makarius@sketis.net>
On Tue, 24 Feb 2015, Sven Schneider wrote:
Is rename_tac using 'ubiquitious backtracking'? I would not have
expected rename_tac to be so complex.I had a more simple implementation in mind: a tactic-wrapper which
operates as follows.
(1) obtain the current list of variables
(2) apply rename_tac
(3) obtain the new list of variables
(4) print a warning if old-list = new-listThen rename_tac could be replaced everywhere by the wrapper-tactic..
Ubiquitious backtracking means you participate in a general situation of
any number of results -- in a compostion of lazy functions that produce
them. This means that in general, warnings or errors don't work without
extra thought and extra machinery.
(The problem is similar in parse translations: sometimes people emit
warnings there, but it merely means some confusing messages pop up out of
nothing, without relation to the actual result.)
A canonical way to get the above effect is to make rename_tac strict, in
the sense that it simply fails on vacous renaming. Thus it would behave
like the "simp" method in that respect, in contrast to the internal
simp_tac.
From the concrete information exposed so far, I am not yet convinced that
it is worth the while to revisit such ancient tactical relics in the Isar
method name space at all.
So just the standard questions:
* What are typical remaining applications of rename_tac?
* Is it feasible to dispose it eventually, e.g. after Eisbach has been
properly established.
Makarius
Email Gateway (Aug 19 2022 at 17:13):From: Sven Schneider <sven.schneider.pub@gmx.de>
Dear experts,
are there best practices to transfer Isabelle2011 (apply-style) code to
Isabelle2014?
For example, a shell-script to execute?
What should be done before the transfer?
The AFP submission guidelines seem to imply that back and isabelle
generated variable names are a source of backwards incompatibilty.
Furthermore, I have encountered renamed/removed lemmas.
Is there a standard way to remove back? (I guess this is mostly the
cases where the allE is used in my proofs; so I can image that the
best way is to explicitly instantiate the P-variable.)
Is there a standard way to remove cases where Isabelle choses variable
names? (I could explicitly set the names using rename_tac in all the
places, but how do I detect such places?)
-- Sven Schneider
0xF0E2AE90.asc
Email Gateway (Aug 19 2022 at 17:13):From: Larry Paulson <lp15@cam.ac.uk>
Have you tried doing this port yet, so that you can report specific things that have been causing you problems? I can imagine many proofs that would go through unaltered.
There are no scripts for porting from one version to another.
I find it useful to run both the old and the new copies of Isabelle during porting. Then you can see where a proof goes wrong. Then the simplest thing is to see whether sledgehammer (greatly improved since 2011) can solve the problematical case.
Try to rewrite some of your proofs in the structured style. That gives you control over variable names and makes future porting much easier.
Larry Paulson
Email Gateway (Aug 19 2022 at 17:13):From: Peter Lammich <lammich@in.tum.de>
Some lemmas from the standard library (HOL) have also been renamed. This
is usually documented in the NEWS-file ... if a lemma is missing, search
for its name in the NEWS-file, and you may find its new name ...
Email Gateway (Aug 19 2022 at 17:17):From: Sven Schneider <sven.schneider.pub@gmx.de>
Thanks for all the hints.
I just tried to translate the first theories. Besides renamed lemmas
which are just annoying I now encountered a serious problem:
(*) clarsimp (more precisely clarify) has changed its default behaviour.
In particular, clarsimp/clarify does not remove (all/any?) useless
assumptions anymore.
In the following example, clarsimp/clarify reduced the goal to "goal (1
subgoal): 1. C" in 2011 but clarsimp/clarify fails at this point in 2014.
Is it possible to change the default clarsimp/clarify behaviour to
remove such assumptions?
lemma "
A=B
\<Longrightarrow> C"
apply(clarsimp)
(*) In 2011 warnings were written to the response buffer. in
Isabelle2014/JEdit: is it possible to copy all these responses to a
certain file?
(*) Is it possible to adapt rename_tac s.t. it produces a warning if it
has not altered the state?
(*) Why is "back" considered bad "style" (according to the AFP
submission guidelines)? I removed all occurrences in my code already but
I am still curious.
(*) Has option_case been removed or has it been renamed? In 2014 it is
interpreted as a (blue) variable when it occurs in a lemma statement?
-- Sven Schneider
0xF0E2AE90.asc
Email Gateway (Aug 19 2022 at 17:17):From: Dmitriy Traytel <traytel@in.tum.de>
Dear Sven,
I (or more precisely the NEWS file) can answer some of your questions.
On 20.02.2015 14:59, Sven Schneider wrote:
Thanks for all the hints.
I just tried to translate the first theories. Besides renamed lemmas
which are just annoying I now encountered a serious problem:(*) clarsimp (more precisely clarify) has changed its default behaviour.
In particular, clarsimp/clarify does not remove (all/any?) useless
assumptions anymore.
In the following example, clarsimp/clarify reduced the goal to "goal (1
subgoal): 1. C" in 2011 but clarsimp/clarify fails at this point in 2014.
Is it possible to change the default clarsimp/clarify behaviour to
remove such assumptions?
lemma "
A=B
\<Longrightarrow> C"
apply(clarsimp)
From the NEWS file:
- Standard tactics and proof methods such as "clarsimp", "auto" and
"safe" now preserve equality hypotheses "x = expr" where x is a free
variable. Locale assumptions and chained facts containing "x"
continue to be useful. The new method "hypsubst_thin" and the
configuration option "hypsubst_thin" (within the attribute name space)
restore the previous behavior. INCOMPATIBILITY, especially where
induction is done after these methods or when the names of free and
bound variables clash. As first approximation, old proofs may be
repaired by "using [[hypsubst_thin = true]]" in the critical spot.
If you have many occurrences, you could also
declare [[hypsubst_thin = true]]
globally.
(*) In 2011 warnings were written to the response buffer. in
Isabelle2014/JEdit: is it possible to copy all these responses to a
certain file?(*) Is it possible to adapt rename_tac s.t. it produces a warning if it
has not altered the state?(*) Why is "back" considered bad "style" (according to the AFP
submission guidelines)? I removed all occurrences in my code already but
I am still curious.
Because it makes your proof rely on the order in which the HO-unifier
produces its results.
(*) Has option_case been removed or has it been renamed? In 2014 it is
interpreted as a (blue) variable when it occurs in a lemma statement?
From the NEWS file:
- The generated constants "xxx_case" and "xxx_rec" have been renamed
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
INCOMPATIBILITY.
Dmitriy
Email Gateway (Aug 19 2022 at 17:18):From: Sven Schneider <sven.schneider.pub@gmx.de>
Thank you very much.
I had a look at the news file but I guess I did not use the right search
strings...
This is what I also believed.
Why is it not required that back always produces an immediate fault,
i.e., always a unique result?
Without 'back' the first result is chosen but if the order changes, this
first element may be a different than before.
Remaining questions:
(*) In 2011 warnings were written to the response buffer. in
Isabelle2014/JEdit: is it possible to copy all these responses to a
certain file?
(*) Is it possible to adapt rename_tac s.t. it produces a warning if it
has not altered the state?
-- Sven Schneider
0xF0E2AE90.asc
Email Gateway (Aug 19 2022 at 17:18):From: Larry Paulson <lp15@cam.ac.uk>
The “back” command is intended to allow interactive exploration of the multiple results delivered by a proof method. But leaving instances of this command in a proof script makes it unusually difficult to read and fragile. You can fix this problem in a number of ways, for example by explicitly instantiating variables in a theorem or by combining a series of proof methods where the last one will fail unless the last choice was made earlier, a bit like constraint satisfaction in Prolog.
Larry Paulson
Email Gateway (Aug 19 2022 at 17:18):From: Makarius <makarius@sketis.net>
The Isabelle/jEdit manual briefly mentions "copy" from "secondary windows"
via the canonical keyboard shortcut C+c. This refers to the "Output"
window, as well as other popup or Info windows.
Makarius
Email Gateway (Aug 19 2022 at 17:18):From: Makarius <makarius@sketis.net>
In really ancient times, the former goal stack package of the ML toplevel
used to issue such a warning for arbitrary tactic applications; thus it
had the above effect for rename_tac. The built-in warning was later
discontinued for the Isar proof state management, because it was unclear
what "not altered" means.
Also note that a tactic or proof method cannot easily provide side-results
as warning (or error) by itself, due to the ubiquitious backtracking,
which was a big thing in Isabelle89. (Backtracking has recently made into
Coq 8.5 as well, with similar consequences on diagnostic tactics.)
After so many years with old-style tactic emulations in Isar (like
rename_tac, rule_tac, erule_tac etc.) it might be time to investigate
possibilities to live without them. Recent developments around the
Eisbach proof method language could allow to remove these old artifacts
eventually.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC