Theory CGS

section ‹ Centimetre-Gram-Second System ›

theory CGS
  imports SI_Units
begin

subsection ‹ Preliminaries ›

typedef CGS = "UNIV :: unit set" ..
instance CGS :: unit_system
  by (rule unit_system_intro[of "Abs_CGS ()"], metis (full_types) 
           Abs_CGS_cases UNIV_eq_I insert_iff old.unit.exhaust)
instance CGS :: time_second ..
abbreviation "CGS ≡ unit :: CGS"

subsection ‹ Base Units ›

abbreviation "centimetre  ≡ BUNIT(L, CGS)"
abbreviation "gram        ≡ BUNIT(M, CGS)"

subsection ‹ Conversion to SI ›

instantiation CGS :: metrifiable
begin

lift_definition convschema_CGS :: "CGS itself ⇒ (CGS, SI) Conversion" is
"λ x. ⦇ cLengthF = 0.01, cMassF = 0.001, cTimeF = 1
      , cCurrentF = 1, cTemperatureF = 1, cAmountF = 1, cIntensityF = 1 ⦈" by simp

instance ..
end

lemma CGS_SI_simps [simp]: "LengthF (convschema (a::CGS itself)) = 0.01" "MassF (convschema a) = 0.001"
  "TimeF (convschema a) = 1" "CurrentF (convschema a) = 1" "TemperatureF (convschema a) = 1"
  by (transfer, simp)+

subsection ‹ Conversion Examples ›

lemma "metrify ((100::rat) *⇩Q centimetre) = 1 *⇩Q metre"
  by (si_simp)

end