# Re: [isabelle] feature request: proof-local datatypes

On Thu, 28 Feb 2013, Dmitriy Traytel wrote:

Hello John,

`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
``assumptions.
`
theory Scratch
imports "~~/src/HOL/BNF/BNF"
begin
locale A
begin
data 'a list = ...
theorem x: "..."
using list.map ..
end
thm A.x
end

`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
``this:
`
context
begin
private data ...
private fun ...
private lemma ...
theorem ...
end

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
``times.
`

`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.
`
Makarius

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