[isabelle-dev] pretty-printing of DIM('a)

[Lawrence Paulson]

The DIM('a) notation is introduced in Multivariate_Analysis/Euclidean_Space, for referring to the dimension of the Euclidean space designated by type ‘a. (See code snippet below.) Unfortunately, DIM(‘a) pretty-prints as card Basis, and the type reference is lost. We need to fix this somehow.

Larry

class euclidean_space = real_inner +
  fixes Basis :: "'a set"
  assumes nonempty_Basis [simp]: "Basis ≠ {}"
  assumes finite_Basis [simp]: "finite Basis"
  assumes inner_Basis:
    "⟦u ∈ Basis; v ∈ Basis⟧ ⟹ inner u v = (if u = v then 1 else 0)"
  assumes euclidean_all_zero_iff:
    "(∀u∈Basis. inner x u = 0) ⟷ (x = 0)"

abbreviation dimension :: "('a::euclidean_space) itself ⇒ nat" where
  "dimension TYPE('a) ≡ card (Basis :: 'a set)"

syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")

translations "DIM('t)" == "CONST dimension (TYPE('t))"