[isabelle] Bets Practice for local helper lemmas



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




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