Re: [isabelle] feature request: proof-local datatypes
On Thu, 28 Feb 2013, Dmitriy Traytel wrote:
not quite what you want, but with the new localized datatype package you can
structure your proofs and datatypes definition with locales (with or) without
data 'a list = ...
theorem x: "..."
using list.map ..
Of course, these "local" datatypes may not depend variables fixed by the
locale, since this is already forbidden for typedefs. One could imagine a
proof-local version of the data command with the same restriction.
This is actually the way to go: using the more and more uniform
'localization' of specification mechanisms to delimit scopes in a soft
way. Note that instead of 'locale' above, it could also be 'class' or the
more recent "context begin ... end", which is also nestable to some
extent. (Sometimes some combinations of all that breaks down, but then you
should report it, so it can be amended.)
In the next round of refinements, one could imagine further name space
management to indicate certain specification elements as 'private' like
private data ...
private fun ...
private lemma ...
On 28.02.2013 12:17, John Wickerson wrote:
Something about this strikes me as sub-optimal. The lemmas, definitions
and datatypes x1...x6 are only required *within* this one particular
proof. It seems like a violation of modularity for them to be
globally-available outside of this proof.
I know I can already kind-of define lemmas within a proof (by writing
"have x4: ...") and I know I can already kind-of make definitions
within a proof (by writing "let ..." or "def ..."). But what would be
quite nice would be to have the *full* expressivity that is available
at the "top-level", also available within a proof, so that I can make
proof-local datatypes, typedefs, and so on.
This is very hard, both due to logical foundations and technical
infrastructure. In the hot phase (2006/2007) when the current local
theory concepts where sorted out, we had discussed that question many
The non-uniformity of the theory context (with its polymorphic 'define'
and 'note' elements) and proof context (with its 'fix' and 'assume'
elements and local conclusions) is there at the bottom of Isabelle/Pure
(inherited from the way how Church/Milner/Gordon HOL works.)
In a system like Coq you don't have that restriction, but you have other
problems coming from it. It is this "water bed syndrom": you can push
conceptual complexity from one corner to the other, but it is still there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and