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.