Commented on the relationship between units and quantities, and added several supporting definitions and types.

src/SI/ISQ_Dimensions.thy

@@ -171,7 +171,7 @@ text \<open> The notation \<^term>\<open>QD('a::dim_type)\<close> allows to obta
 
   The subset of basic dimension types can be characterized by the following type class: \<close>
 
-class si_basedim = dim_type +
+class basedim_type = dim_type +
   assumes is_BaseDim: "is_BaseDim QD('a)"
 
 subsubsection \<open> Base Dimension Type Expressions \<close>
@@ -209,45 +209,45 @@ translations
   (type) "J" <= (type) "Intensity"
 
 text\<open> Next, we embed the base dimensions into the dimension type expressions by instantiating the 
-  class \<^class>\<open>si_basedim\<close> with each of the base dimension types. \<close>
+  class \<^class>\<open>basedim_type\<close> with each of the base dimension types. \<close>
 
-instantiation Length :: si_basedim
+instantiation Length :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Length (_::Length itself) = \<^bold>L"
 instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
 end
 
-instantiation Mass :: si_basedim
+instantiation Mass :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Mass (_::Mass itself) = \<^bold>M"
 instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
 end
 
-instantiation Time :: si_basedim
+instantiation Time :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Time (_::Time itself) = \<^bold>T"
 instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
 end
 
-instantiation Current :: si_basedim
+instantiation Current :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Current (_::Current itself) = \<^bold>I"
 instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
 end
 
-instantiation Temperature :: si_basedim
+instantiation Temperature :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\<Theta>"
 instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
 end
 
-instantiation Amount :: si_basedim
+instantiation Amount :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Amount (_::Amount itself) = \<^bold>N"
 instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
 end   
 
-instantiation Intensity :: si_basedim
+instantiation Intensity :: basedim_type
 begin
 definition [si_def]: "dim_ty_sem_Intensity (_::Intensity itself) = \<^bold>J"
 instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)

src/SI/SI_Prefix.thy

@@ -6,6 +6,9 @@ begin
 
 subsection \<open> Definitions \<close>
 
+text \<open> Prefixes are simply numbers that can be composed with units using the scalar 
+  multiplication operator \<^const>\<open>scaleQ\<close>. \<close>
+
 default_sort ring_char_0
 
 definition deca :: "'a" where [si_eq]: "deca = 10^1"
@@ -60,6 +63,9 @@ lemma "1 \<odot> (centi \<odot> meter)\<^sup>-\<^sup>\<one> = 100 \<odot> meter\
 
 subsection \<open> Binary Prefixes \<close>
 
+text \<open> Although not in general applicable to physical quantities, we include these prefixes
+  for completeness. \<close>
+
 default_sort ring_char_0
 
 definition kibi :: "'a" where [si_eq]: "kibi = 2^10"

src/SI/SI_Units.thy

@@ -13,21 +13,23 @@ text \<open> Parallel to the seven base quantities, there are seven base units.
   and a magnitude of \<^term>\<open>1\<close>. Consequently, a base unit corresponds to a unit in the algebraic
   sense. \<close>
 
-lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool" 
-  is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
+lift_definition is_base_unit :: "'a::one['d::dim_type] \<Rightarrow> bool" 
+  is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" . 
 
-
-lift_definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]" 
-  is "\<lambda> u. \<lparr> mag = 1, dim = QD('u) \<rparr>" by simp
+definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::basedim_type]" 
+  where [si_eq]: "mk_base_unit t = 1"
 
 syntax "_mk_base_unit" :: "type \<Rightarrow> logic" ("BUNIT'(_')")
 translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)"
 
-lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
-  by (simp add: magQuant_def, transfer, simp)
+lemma mk_base_unit: "is_base_unit (mk_base_unit a)"
+  by (simp add: si_eq, transfer, simp add: is_BaseDim)
 
-text \<open> We now define the seven base units. Effectively, these definitions axiomatise give names
-  to the \<^term>\<open>1\<close> elements of the base quantities. \<close>
+lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::basedim_type)\<rbrakk>\<^sub>Q = 1"
+  by (simp add: magQuant_def si_eq, transfer, simp)
+
+text \<open> We now define the seven base units. Effectively, these definitions axiomatise given names
+  for the \<^term>\<open>1\<close> elements of the base quantities. \<close>
 
 definition [si_eq]: "meter    = BUNIT(L)"
 definition [si_eq]: "second   = BUNIT(T)"
@@ -37,15 +39,31 @@ definition [si_eq]: "kelvin   = BUNIT(\<Theta>)"
 definition [si_eq]: "mole     = BUNIT(N)"
 definition [si_eq]: "candela  = BUNIT(J)"
 
-text\<open>Note that as a consequence of our construction, the term @{term meter} is a SI Unit constant of 
-SI-type @{typ "'a[L]"}, so a unit of dimension @{typ "Length"} with the magnitude of type @{typ"'a"}.
+text\<open>Note that as a consequence of our construction, the term \<^term>\<open>meter\<close> is a SI Unit constant of 
+SI-type \<^typ>\<open>'a[L]\<close>, so a unit of dimension \<^typ>\<open>Length\<close> with the magnitude of type \<^typ>\<open>'a\<close>.
 A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of 
-type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer to the \<^emph>\<open>norm\<close> of the vector,
-not to its components.
-\<close>
+type \<^typ>\<open>real\<^sup>3\<close>. Note than when considering vectors, dimensions refer to the \<^emph>\<open>norm\<close> of the vector,
+not to its components. \<close>
 
-lemma meter_is_BaseUnit: "is_BaseUnit meter"
-  by (simp add: si_eq, transfer, simp)
+lemma BaseUnits: 
+  "is_base_unit meter" "is_base_unit second" "is_base_unit kilogram" "is_base_unit ampere"
+  "is_base_unit kelvin" "is_base_unit mole" "is_base_unit candela"
+  by (simp add: si_eq, transfer, simp)+
+
+text \<open> The effect of the above encoding is that we can use the SI base units as synonyms for their
+  corresponding dimensions at the type level. \<close>
+
+type_synonym meter = Length
+type_synonym second = Time
+type_synonym kilogram = Mass
+type_synonym ampere = Current
+type_synonym kelvin = Temperature
+type_synonym mole = Amount
+type_synonym candela = Intensity
+
+text \<open> We can therefore construct a quantity such as \<^term>\<open>5 :: rat[meter]\<close>, which unambiguously 
+  identifies that the unit of $5$ is meters using the type system. This works because each base
+  unit it the one element. \<close>
 
 subsection \<open> Example Unit Equations \<close>