Email Gateway (Aug 22 2022 at 09:49): Email Gateway (Aug 22 2022 at 09:49):From: Makarius <makarius@sketis.net>
It might be surprising, but it is according to the documented meaning of
'private' (or 'qualified'). Only name space accesses are affected,
everything else is unchanged, e.g. fact declarations in the context.
Makarius
Email Gateway (Aug 22 2022 at 09:49):From: Makarius <makarius@sketis.net>
This excessive "local." prefix in the output has always been there in
"context begin ... end" blocks since their introduction in 2013, but it is
not necessary.
I've refined that detail in
https://bitbucket.org/isabelle_project/isabelle-release/commits/014b86186c49
which will be in the next release candidate.
Makarius
Email Gateway (Aug 22 2022 at 10:05):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Isabelle List,
what is the best practice to state some temporary helper lemmas? I
don't want to pollute the global namespace.
For example, I want to have a collection of lemmas about foo and bar
(called foobar).
Try 1)
lemma help1: "foo X"
lemma help2: "bar X"
lemmas foobar = help1 help2
hide_const help1 help2
It is rather unpleasant to list help1 and help2 in hide_const again.
Try 2)
context
begin
private lemma help1: "foo X"
private lemma help2: "bar X"
lemmas foobar = help1 help2
end
Are there any downsides with this approach? Do help1 and help2 exist
outside of the context?
For me as a user, are approach 1 and 2 equivalent?
If so, why does a theory file not introduce a context by default so
that I can use the private keyword everywhere?
Are hide_cost(open) and qualified equivalent?
Try 3)
lemma foobar shows "foo X" and "bar X"
proof -
show "foo X"
show "bar X"
qed
Two downsides of this approach: Only applicable if those two X are of
the same type and I need to repeat the two theses again.
Are there better possibilities? Which one is preferred?
Cheers,
Cornelius
Email Gateway (Aug 22 2022 at 10:05):From: Makarius <makarius@sketis.net>
On Mon, 4 May 2015, C. Diekmann wrote:
what is the best practice to state some temporary helper lemmas? I don't
want to pollute the global namespace.For example, I want to have a collection of lemmas about foo and bar
(called foobar).Try 1)
lemma help1: "foo X"
lemma help2: "bar X"
lemmas foobar = help1 help2
hide_const help1 help2It is rather unpleasant to list help1 and help2 in hide_const again.
Try 2)
context
begin
private lemma help1: "foo X"
private lemma help2: "bar X"
lemmas foobar = help1 help2
end
You probably mean hide_fact instead of hide_const above -- Isabelle is not
Coq.
For the coming Isabelle2015 release, form 2) is considered canonical. At
least it had been virutally canonical over a long time in the pipeline.
The implementation suddendly popped out as a result of the work on the
Eisbach release, just before the Isabelle2015-RC phase started. This also
means there might be fine points to be reconsidered later.
E.g. there is a slightly different notion of "concealed" name space
entries that is used internally. Its relation to "private" still needs to
be clarified.
Do help1 and help2 exist outside of the context?
The 'private' keyword only affects name space entries. Everything else is
as before. E.g. in
private lemma help [simp]: ...
the [simp] declaration is unchanged, it is not subject to name space
management.
There is also a new 'experimentation' target, which combines a private
context with an anonymous locale. Thus it is as private and local as
possible, but nothing can be exported from it (at least not without
special tricks).
For me as a user, are approach 1 and 2 equivalent?
No. The 'hide' variants are old workarounds: the system first produces
name space entries, and the user marks them as hidden later. The
'private' keyword suppresses the name space entries from the outset, there
is no hiding happening at all. There are certain corner cases where this
can make a difference, e.g. with merges of name spaces.
Moreover, 'private' affects all name space bindings of the specification
command in question, not just the isolated entities that are hidden by
separate hide_type / hide_const / hide_fact etc. This makes a difference
for more complex specifications, e.g. 'definition', 'inductive',
'function'.
Note that 'datatype' does not work with 'private' yet: something to be
refined for the next release.
If so, why does a theory file not introduce a context by default so
that I can use the private keyword everywhere?
Here is some more text from the isar-ref manual:
Neither a global @{command theory} nor a @{command locale} target provides
a local scope by itself: an extra unnamed context is required to use
@{keyword "private"} or @{keyword "qualified"} here.
It means that the new notion of a formal "scope" is missing. It is
unclear how that would interact with theory imports or locale
interpretation. So instead of making a mess of features in the last
moment before the release, I made a conceptually clear thing.
In fact, the relatively new "context begin ... end" form made the new
'private' / 'concealed' very easy to provide, bypassing many historic
problems.
Are hide_cost(open) and qualified equivalent?
Similar, but not equivalent. Like full 'hide' and 'private'.
In practice, it should be possible to replace most uses of "hide (open)"
by "qualified" and "hide" by "private", together with an enclosing context
block, at least that is the plan.
Try 3)
lemma foobar shows "foo X" and "bar X"
proof -
show "foo X"
show "bar X"
qedTwo downsides of this approach: Only applicable if those two X are of
the same type and I need to repeat the two theses again.
There are more disadvantages of putting local things into the proof body:
you don't get the full flexibility of specification mechanisms like
'inductive', 'function', etc.
There are logical and technical obstacles, and I am very glad that we have
such a relatively simple logical framework. In Coq you can do arbitrary
things inside a proof (I think), and it bogs down the whole system a lot.
Are there better possibilities? Which one is preferred?
Users of Isabelle2015-RC versions are welcome to post further
observations. This is new and might need further polishing (after the
release).
Makarius
Email Gateway (Aug 22 2022 at 10:07):From: "C. Diekmann" <diekmann@in.tum.de>
2015-05-04 22:39 GMT+02:00 Makarius <makarius@sketis.net>:
On Mon, 4 May 2015, C. Diekmann wrote:
what is the best practice to state some temporary helper lemmas? I don't
want to pollute the global namespace.For example, I want to have a collection of lemmas about foo and bar
(called foobar).Try 1)
lemma help1: "foo X"
lemma help2: "bar X"
lemmas foobar = help1 help2
hide_const help1 help2It is rather unpleasant to list help1 and help2 in hide_const again.
Try 2)
context
begin
private lemma help1: "foo X"
private lemma help2: "bar X"
lemmas foobar = help1 help2
endYou probably mean hide_fact instead of hide_const above -- Isabelle is not
Coq.For the coming Isabelle2015 release, form 2) is considered canonical. At
least it had been virutally canonical over a long time in the pipeline. The
implementation suddendly popped out as a result of the work on the Eisbach
release, just before the Isabelle2015-RC phase started. This also means
there might be fine points to be reconsidered later.
Very nice, I like 2).
However, sometimes the current proof obligation appears a bit
unnecessarily crowded (in my opinion) if local definitions are
prefixed with "local."
E.g. there is a slightly different notion of "concealed" name space entries
that is used internally. Its relation to "private" still needs to be
clarified.Do help1 and help2 exist outside of the context?
The 'private' keyword only affects name space entries. Everything else is
as before. E.g. inprivate lemma help [simp]: ...
the [simp] declaration is unchanged, it is not subject to name space
management.
I found a behavior (2015-RC3) which I found rather surprising:
context
begin
private fun give0 :: "nat ⇒ nat" where
"give0 _ = 0"
fun is_zero :: "nat ⇒ bool" where
"is_zero n ⟷ n = give0 8"
lemma "is_zero 0" by simp
declare is_zero.simps[simp del]
lemma "is_zero 0" by simp (fails)
lemma "is_zero 0" using is_zero.simps by simp (success)
end
lemma "is_zero 0" by simp (fails)
lemma "is_zero 0" using is_zero.simps by simp (success)
Why does the proof of the final lemma succeed? Now I understand that
the give0.simps are in the global simp set and hence the proof
succeeds. Doesn't this somehow pollute the simp set with facts about
things which are private?
Regards,
Cornelius
Email Gateway (Aug 22 2022 at 10:08):From: Manuel Eberl <eberlm@in.tum.de>
I currently have the following problem:
i have a helper lemma A and a locale in which I use that lemma. The
lemma, however, is of no interest other than the use in that locale, so
I would like to make it private. However, the following fails with an
error message:
context
begin
private lemma A: "..."
locale foo = ...
begin
end
end
Do I /have/ to put A inside the locale to make this work or is there
another way?
Cheers,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC