Email Gateway (Aug 19 2022 at 10:22): Email Gateway (Aug 19 2022 at 10:22):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
I have a theorem.
theorem t: "......"
To state my theorem is quite straightforward, but to prove it I require a whole bunch of other lemmas, definitions and datatypes. My theory file, therefore, looks like this:
definition x1: "......"
datatype x2 = ......
definition x3: "......"
lemma x4: "......"
datatype x5 = ......
lemma x6: "......"
theorem t: "......."
proof ......
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. So I would prefer my theory file to look like this:
theorem t: "......."
proofdefinition x1: "......"
datatype x2 = ......
definition x3: "......"
lemma x4: "......"
datatype x5 = ......
lemma x6: "......"
......
qed
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.
cheers,
john
Email Gateway (Aug 19 2022 at 10:23):From: Dmitriy Traytel <traytel@in.tum.de>
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.
Best,
Dmitriy
Email Gateway (Aug 19 2022 at 10:43):From: Makarius <makarius@sketis.net>
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"
beginlocale A
begindata '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
Last updated: Apr 26 2024 at 08:19 UTC