[isabelle-dev] NEWS: 'subgoal' command

[Daniel Matichuk]

I like the dots notation, it resolves the issue of having to always think about the parameters in reverse order.

I've found a few small issues related to clashing/fresh names.

First, It looks like the suffix naming doesn't quite work if there are clashing existing goal params.

e.g.

lemma "⋀x y. A x y"
  subgoal for … x

Results in "x" being named "xa" instead of x. This works as expected in prefix naming, however.

Additionally, fresh names are chosen for any free variables that appear in the subgoal

e.g.

lemma "⋀x y. A x y"
  subgoal for A

Results in "x" being named "Aa". In this case I would expect either an error ("Free name clash") or for the new fixed term to shadow the free A.
The second choice is a bit strange, however, because you end up with two different coloured "A"s in the goal.

Finally, duplicate for-fixes should be disallowed. Currently this results in fresh names being chosen for the duplicates.

This was as of Isabelle/22830a64358f.

-Dan


________________________________________
From: isabelle-dev [isabelle-dev-bounces at mailbroy.informatik.tu-muenchen.de] on behalf of Makarius [makarius at sketis.net]
Sent: Thursday, July 02, 2015 10:30 PM
To: isabelle-dev at in.tum.de
Subject: [isabelle-dev] NEWS: 'subgoal' command

* Command 'subgoal' allows to impose some structure on backward
refinements, to avoid proof scripts degenerating into long of 'apply'
sequences. Further explanations and examples are given in the isar-ref
manual.


This refers to Isabelle/441fdbfbb2d3, which also contains the
documentation and examples.

Practical experience will show what are the full consequences.  E.g. how
close do we get to a situation without the need for rule_tac, case_tac
etc. with their implicit access to hidden goal paramaters.

It should also solve certain indentation problems in long apply scripts.


       Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.