Email Gateway (Aug 18 2022 at 10:44): Email Gateway (Aug 18 2022 at 10:44):From: Randy Pollack <rpollack@inf.ed.ac.uk>
I frequently use the forms:
case (constr v1 v2 ...)
hence j1:"..." and j2:"..." ... by auto
or
case (constr v1 v2 ...)
have j1:"..." and j2:"..." ... by fact
Both of these now give a warning:
### Legacy feature: implicit use of prems in assumption proof
I would not like to see these forms eliminated. It seems natural to
set out the known facts before working on the proof.
What is the intended replacement for this style? If users are
intended to use the names such as constr.hyps and constr.prems, could
these names be shown along with "this" in the goal window?
This naming scheme, constr.hyps and constr.prems, could be improved.
In my old system LEGO, when defining an inductive type/relation you
could (optionally) give names to side conditions/premises. When you
did induction on that type/relation, the assumptions were given names
derived from the premises they came from, and the induction hypotheses
were also given names derived from the premises they came from.
E.g. we might have beta_app.leftPrem and beta_app.leftPrem.ih, where
beta_app is the rule name, leftPrem the name of the premise, and
beta_app.leftPrem.ih the induction hypothesis derived from the left
premise of thet rule.
At the least, Isar could name the induction hypotheses something like
constr.ih instead of mixing them up in constr.hyps.
Best,
Randy
Email Gateway (Aug 18 2022 at 10:44):From: Makarius <makarius@sketis.net>
On Fri, 17 Aug 2007, Randy Pollack wrote:
I frequently use the forms:
case (constr v1 v2 ...)
hence j1:"..." and j2:"..." ... by autoor
case (constr v1 v2 ...)
have j1:"..." and j2:"..." ... by factBoth of these now give a warning:
### Legacy feature: implicit use of prems in assumption proof
I would not like to see these forms eliminated. It seems natural to
set out the known facts before working on the proof.
This warning indicates that the above 'by' steps are actually "deceptive",
meaning that both auto and fact failed to solve the atomic sub-proofs
completely.
In the second case you just need to say "fact+" to produce multiple facts.
The first case needs to be debugged by looking at the internal goal state,
after turning by auto'' into apply auto'' temporarily. You will then
see that some subgoals are left over, which happen to be solvable by
referring to prems that are not indicated explicitly in the text. I.e.
``by auto'' was actually wrong as a description of how the proof works.
This naming scheme, constr.hyps and constr.prems, could be improved.
Yes, this will happen at some later stage. At the moment we are glad
enough to have gotten rid of alphabetically sorted bound variables.
Makarius
Last updated: May 03 2024 at 08:18 UTC