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-boun...@mailbroy.informatik.tu-muenchen.de] on
behalf of Makarius [makar...@sketis.net]
Sent: Thursday, July 02, 2015 10:30 PM
To: isabelle-...@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-...@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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
