[isabelle] Several questions about coding style/best practices



Dear All,

I would like to clarify certain aspects related to the coding style best
suited for Isabelle2019. The question combines both my concerns about the
changes associated with the new release and, also, some of my previous
concerns. Unfortunately, I was not able to find an explicit Isabelle coding
style guide - please accept my apologies for asking this question if a
document that answers it already exists somewhere.

1. Should ⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T) be preferred over S ⊆ 𝔘
⟹ T ⊆ 𝔘 ⟹ τ S ⟹ τ T  ⟹ τ (S ∩ T)?
2. Should ['a set, ('a set ⇒ bool), 'a set] ⇒ bool be preferred over 'a set
⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool?
3. Should lemma ‹⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)› be preferred
over lemma "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"?
4. Should definition closed_ow :: ‹['a set, ('a set ⇒ bool), 'a set] ⇒
bool› be preferred over definition closed_ow :: "['a set, ('a set ⇒ bool),
'a set] ⇒ bool"?
5. In general, when should I use double quotation marks over cartouches if
both options are available?
6. The reference manual states that 'hence' and 'thus' are, effectively,
legacy features. Nevertheless, they are used consistently throughout the
Isabelle sources and there does not seem to be too much effort devoted to
their elimination. Somehow, I always preferred my code to be as concise as
possible and I find it difficult to understand why the readability is
sacrificed when using, for example, 'thus' instead of 'then show'.
Therefore, my question is whether there is a good chance that 'hence' and
'thus' will become obsolete in the future releases.
7. I would like to understand if it is recommended to use locale structures
for the definition of algebraic structures and abstract spaces. Somehow, I
always found it easier and more natural to state all definitional elements
as explicit locale parameters (also, the main HOL library does not use
structures). Nevertheless, this feature was introduced for a good reason
and there are certain libraries that rely on it (e.g. HOL-Algebra). I would
like to make sure that it is not considered to be bad style not to use it
for the development of new theories/libraries about algebraic structures or
abstract spaces (of course, provided, that these theories/libraries are not
meant to extend one of the existing libraries that already uses structures).

Thank you

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



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