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 term1 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 termmetre is a SI Unit constant of 
SI-type typ'a[L, SI], so a unit of dimension typLength 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 typreal3. 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 term5 :: 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" ("schemaC")

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 :: 
  "'s1 itself  's2 itself
    ('a::field_char_0)['d::dim_type, 's1::metrifiable] 
    'a['d::dim_type, 's2::metrifiable]" where
"qmconv s1 s2 x  qconv (invC (schemaC s2) C schemaC s1) x"

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

translations
  "QMC('s1  's2)" == "CONST qmconv TYPE('s1) TYPE('s2)"

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

end