Theory SI_Units

chapter ‹ International System of Units ›

section ‹ SI Units Semantics ›

theory SI_Units
  imports ISQ
begin

text ‹ An SI unit is simply a particular kind of quantity with an SI tag. ›

typedef SI = "UNIV :: unit set" by simp

instance SI :: unit_system
  by (rule unit_system_intro[of "Abs_SI ()"], metis (full_types) Abs_SI_cases UNIV_eq_I insert_iff old.unit.exhaust)

abbreviation "SI ≡ unit :: SI"

type_synonym ('n, 'd) SIUnitT = "('n, 'd, SI) QuantT" ("_[_]" [999,0] 999)

text ‹ We now define the seven base units. Effectively, these definitions axiomatise given names
  for the \<^term>‹1› elements of the base quantities. ›

abbreviation "metre    ≡ BUNIT(L, SI)"
abbreviation "kilogram ≡ BUNIT(M, SI)"
abbreviation "ampere   ≡ BUNIT(I, SI)"
abbreviation "kelvin   ≡ BUNIT(Θ, SI)"
abbreviation "mole     ≡ BUNIT(N, SI)"
abbreviation "candela  ≡ BUNIT(J, SI)"

text ‹ The second is commonly used in unit systems other than SI. Consequently, we define it 
  polymorphically, and require that the system type instantiate a type class to use it. ›

class time_second = unit_system

instance SI :: time_second ..
              
abbreviation "second  ≡ BUNIT(T, 'a::time_second)"

text ‹Note that as a consequence of our construction, the term \<^term>‹metre› is a SI Unit constant of 
SI-type \<^typ>‹'a[L, SI]›, so a unit of dimension \<^typ>‹Length› with the magnitude of type \<^typ>‹'a›.
A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of 
type \<^typ>‹real⇧3›. Note than when considering vectors, dimensions refer to the ∗‹norm› of the vector,
not to its components. ›

lemma BaseUnits: 
  "is_base_unit metre" "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_all add: mk_base_unit)

text ‹ 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. ›

type_synonym 'a metre    = "'a[Length, SI]"
type_synonym 'a second   = "'a[Time, SI]"
type_synonym 'a kilogram = "'a[Mass, SI]"
type_synonym 'a ampere   = "'a[Current, SI]"
type_synonym 'a kelvin   = "'a[Temperature, SI]"
type_synonym 'a mole     = "'a[Amount, SI]"
type_synonym 'a candela  = "'a[Intensity, SI]"

text ‹ We can therefore construct a quantity such as \<^term>‹5 :: rat metre›, which unambiguously 
  identifies that the unit of $5$ is metres using the type system. This works because each base
  unit it the one element. ›

subsection ‹ Example Unit Equations ›

lemma "(metre ❙⋅ second⇧-⇧𝟭) ❙⋅ second ≅⇩Q metre"
  by (si_calc)

subsection ‹ Metrification ›

class metrifiable = unit_system +
  fixes convschema :: "'a itself ⇒ ('a, SI) Conversion" ("schema⇩C")

instantiation SI :: metrifiable
begin
lift_definition convschema_SI :: "SI itself ⇒ (SI, SI) Conversion"
is "λ s. 
  ⦇ cLengthF = 1
  , cMassF = 1
  , cTimeF = 1
  , cCurrentF = 1
  , cTemperatureF = 1
  , cAmountF = 1
  , cIntensityF = 1 ⦈" by simp
instance ..
end

abbreviation metrify :: "('a::field_char_0)['d::dim_type, 's::metrifiable] ⇒ 'a['d::dim_type, SI]" where
"metrify ≡ qconv (convschema (TYPE('s)))"

text ‹ Conversion via SI units ›

abbreviation qmconv :: 
  "'s⇩1 itself ⇒ 's⇩2 itself
   ⇒ ('a::field_char_0)['d::dim_type, 's⇩1::metrifiable] 
   ⇒ 'a['d::dim_type, 's⇩2::metrifiable]" where
"qmconv s⇩1 s⇩2 x ≡ qconv (inv⇩C (schema⇩C s⇩2) ∘⇩C schema⇩C s⇩1) x"

syntax
  "_qmconv" :: "type ⇒ type ⇒ logic" ("QMC'(_ → _')")

translations
  "QMC('s⇩1 → 's⇩2)" == "CONST qmconv TYPE('s⇩1) TYPE('s⇩2)"

lemma qmconv_self: "QMC('s::metrifiable → 's) = id"
  by (simp add: fun_eq_iff)

end