Theory SI_Accepted

section ‹ Non-SI Units Accepted for SI use ›

theory SI_Accepted
  imports SI_Derived
begin

definition [si_def, si_eq]: "minute = 60 *⇩Q second"

definition [si_def, si_eq]: "hour = 60 *⇩Q minute"

definition [si_def, si_eq]: "day = 24 *⇩Q hour"

definition [si_def, si_eq]: "astronomical_unit = 149597870700 *⇩Q metre"

definition degree :: "'a::real_field[L/L]" where
[si_def, si_eq]: "degree = (2⋅(of_real pi) / 180) *⇩Q radian"

abbreviation degrees (‹_°› [999] 999) where "n° ≡ n *⇩Q degree"

definition [si_def, si_eq]: "litre = 1/1000 *⇩Q metre⇧𝟯"

definition [si_def, si_eq]: "tonne = 10^3 *⇩Q kilogram"

definition [si_def, si_eq]: "dalton = 1.66053906660 * (1 / 10^27) *⇩Q kilogram"

subsection ‹ Example Unit Equations ›

lemma "1 *⇩Q hour = 3600 *⇩Q second"
  by (si_simp)

lemma "watt ❙⋅ hour ≅⇩Q 3600 *⇩Q joule"   by (si_calc)

lemma "25 *⇩Q metre ❙/ second = 90 *⇩Q (kilo *⇩Q metre) ❙/ hour"
  by (si_calc)

end