[isabelle] Overriding reason not to use single quote or camelcase in identifiers?


I try not to ask these simple questions when I know so little, but I'd need to ask this eventually. It's better to ask now, than later with a couple thousand lines of code.

I've read the style guide in implementation.pdf, so I've read and seen that the preferred identifier naming scheme uses the underscore character "_". However, I don't like how it looks, but a bigger issue is that I have to escape it in Latex. Right now, I'm not using the Isabelle Latex processing.

I'm kind of settling on a combination of limited camelcase use, and using the single quote character, ( ' ), to separate words in an identifier.

For example, I have the identifer "emS'is'unique". Below, I include a very fledgling theory where I don't know what I'm doing. It's to show some of my identifier naming.

I haven't seen any naming like "emS'is'unique". Is this just a matter of preference, or would doing a lot of that come back to haunt me? I'm assuming if I don't get errors in jEdit when doing that kind of thing, it's not going to come back to haunt me.

(I haven't figured out if the unicode characters in an email like this show up correctly in other's email readers.)


theory sTs
imports Main
(*sT....The set type.*)
typedecl sT
(*scP...Axiom schema of comprehension property.*)
type_synonym scP = "sT ⇒ bool"

(*inS...Set membership predicate.*)
inS:: "sT ⇒ sT ⇒ bool" and
(*emS...The empty set.*)
emS:: sT
(*emE...The empty set is empty.*)
emE: "∀a::sT. ¬(inS a emS)" and
(*upS...Unordered pair set.*)
upS: "∀(a::sT)(b::sT). (∃c::sT. ∀x. (inS x c) ⟷ (x = a) ∨ (x = b))" and
(*scS...Schema set: axiom schema of comprehension.*)
scS: "∀(a::sT)(P::scP). (∃b::sT. ∀x. (inS x b) ⟷ ((inS x a) ∧ (P x)))"

(*Meaningless. It's merely a result of names.*)
theorem emS'unique'meaningless : "(a = emS) ∧ (b = emS) ⟹ a = b"

theorem emS'is'unique: "a = emS ⟷ (∀x::sT. ¬(inS x a))"

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