[isabelle] Legacy feature?



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.