Theory SI_Constants

section ‹ Physical Constants ›

theory SI_Constants
  imports SI_Units
begin

subsection ‹ Core Derived Units ›

abbreviation (input) "hertz ≡ second-𝟭"

abbreviation "radian ≡ metre ⋅ metre-𝟭"

abbreviation "steradian ≡ metre𝟮 ⋅ metre-𝟮"

abbreviation "joule ≡ kilogram ⋅ metre𝟮 ⋅  second-𝟮"

type_synonym 'a joule = "'a[M ⋅ L2 ⋅ T-2, SI]"

abbreviation "watt ≡ kilogram ⋅ metre𝟮 ⋅ second-𝟯"

type_synonym 'a watt = "'a[M ⋅ L2 ⋅ T-3, SI]"

abbreviation "coulomb ≡ ampere ⋅ second"

type_synonym 'a coulomb = "'a[I ⋅ T, SI]"

abbreviation "lumen ≡ candela ⋅ steradian"

type_synonym 'a lumen = "'a[J ⋅ (L2 ⋅ L-2), SI]"

subsection ‹ Constants ›

text ‹ The most general types we support must form a field into which the natural numbers can 
  be injected. ›

default_sort field_char_0

text ‹ Hyperfine transition frequency of frequency of Cs ›

abbreviation caesium_frequency:: "'a[T-1,SI]" (‹ΔvCs›) where
  "caesium_frequency ≡ 9192631770 *Q hertz"

text ‹ Speed of light in vacuum ›

abbreviation speed_of_light :: "'a[L ⋅ T-1,SI]" (‹c›) where
  "speed_of_light ≡ 299792458 *Q (metre⋅second-𝟭)"

text ‹ Planck constant ›

abbreviation Planck :: "'a[M ⋅ L2 ⋅ T-2 ⋅ T,SI]" (‹h›) where
  "Planck ≡ (6.62607015 ⋅ 1/(10^34)) *Q (joule⋅second)"

text ‹ Elementary charge ›

abbreviation elementary_charge :: "'a[I ⋅ T,SI]" (‹e›) where
  "elementary_charge ≡ (1.602176634 ⋅ 1/(10^19)) *Q coulomb"

text ‹ The Boltzmann constant ›

abbreviation Boltzmann :: "'a[M ⋅ L2 ⋅ T-2 ⋅ Θ-1,SI]" (‹k›) where
  "Boltzmann ≡ (1.380649⋅1/(10^23)) *Q (joule / kelvin)"

text ‹ The Avogadro number ›

abbreviation Avogadro :: "'a[N-1,SI]" (‹NA›) where
"Avogadro ≡ 6.02214076⋅(10^23) *Q (mole-𝟭)"

abbreviation max_luminous_frequency :: "'a[T-1,SI]" where
"max_luminous_frequency ≡ (540⋅10^12) *Q hertz"

text ‹ The luminous efficacy of monochromatic radiation of frequency const‹max_luminous_frequency›. ›

abbreviation luminous_efficacy :: "'a[J ⋅ (L2 ⋅ L-2) ⋅ (M ⋅ L2 ⋅ T-3)-1,SI]" (‹Kcd›) where
"luminous_efficacy ≡ 683 *Q (lumen/watt)"

subsection ‹ Checking Foundational Equations of the SI System ›

theorem second_definition: 
  "1 *Q second ≅Q (9192631770 *Q 𝟭) / ΔvCs"
  by si_calc

theorem metre_definition: 
  "1 *Q metre ≅Q (c / (299792458 *Q 𝟭))⋅second"
  "1 *Q metre ≅Q (9192631770 / 299792458) *Q (c / ΔvCs)"
  by si_calc+

theorem kilogram_definition:
  "((1 *Q kilogram)::'a kilogram) ≅Q (h / (6.62607015 ⋅ 1/(10^34) *Q 𝟭))⋅metre-𝟮⋅second" 
  by si_calc


abbreviation "approx_ice_point ≡ 273.15 *Q kelvin"

default_sort type

end