Theory SI_Derived

section ‹ Derived SI-Units›

theory SI_Derived
  imports SI_Prefix
begin                                  

subsection ‹ Definitions ›

abbreviation "newton ≡ kilogram ❙⋅ metre ❙⋅ second⇧^-⇧^𝟮"

type_synonym 'a newton = "'a[M ⋅ L ⋅ T⇧^-⇧², SI]"

abbreviation "pascal ≡ kilogram ❙⋅ metre⇧^-⇧^𝟭 ❙⋅ second⇧^-⇧^𝟮"

type_synonym 'a pascal = "'a[M ⋅ L⇧^-⇧¹ ⋅ T⇧^-⇧², SI]"

abbreviation "volt ≡ kilogram ❙⋅ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟯 ❙⋅ ampere⇧^-⇧^𝟭"

type_synonym 'a volt = "'a[M ⋅ L⇧² ⋅ T⇧^-⇧³ ⋅ I⇧^-⇧¹, SI]"

abbreviation "farad ≡ kilogram⇧^-⇧^𝟭 ❙⋅ metre⇧^-⇧^𝟮 ❙⋅ second⇧^𝟰 ❙⋅ ampere⇧^𝟮"

type_synonym 'a farad = "'a[M⇧^-⇧¹ ⋅ L⇧^-⇧² ⋅ T⇧⁴ ⋅ I⇧², SI]"

abbreviation "ohm ≡ kilogram ❙⋅ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟯 ❙⋅ ampere⇧^-⇧^𝟮"

type_synonym 'a ohm = "'a[M ⋅ L⇧² ⋅ T⇧^-⇧³ ⋅ I⇧^-⇧², SI]"

abbreviation "siemens ≡ kilogram⇧^-⇧^𝟭 ❙⋅ metre⇧^-⇧^𝟮 ❙⋅ second⇧^𝟯 ❙⋅ ampere⇧^𝟮"

abbreviation "weber ≡ kilogram ❙⋅ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟮 ❙⋅ ampere⇧^-⇧^𝟭"

abbreviation "tesla ≡ kilogram ❙⋅ second⇧^-⇧^𝟮 ❙⋅ ampere⇧^-⇧^𝟭"

abbreviation "henry ≡ kilogram ❙⋅ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟮 ❙⋅ ampere⇧^-⇧^𝟮"

abbreviation "lux ≡ candela ❙⋅ steradian ❙⋅ metre⇧^-⇧^𝟮"

abbreviation (input) "becquerel ≡ second⇧^-⇧^𝟭"

abbreviation "gray ≡ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟮"

abbreviation "sievert ≡ metre⇧^𝟮 ❙⋅ second⇧^-⇧^𝟮"

abbreviation "katal ≡ mole ❙⋅ second⇧^-⇧^𝟭"

definition degrees_celcius :: "'a::field_char_0 ⇒ 'a[Θ]" ("_°C" [999] 999) 
  where [si_eq]: "degrees_celcius x = (x *⇩_Q kelvin) + approx_ice_point"

definition [si_eq]: "gram = milli *⇩_Q kilogram"

subsection ‹ Equivalences ›

lemma joule_alt_def: "joule ≅⇩_Q newton ❙⋅ metre" 
  by si_calc

lemma watt_alt_def: "watt ≅⇩_Q joule ❙/ second"
  by si_calc

lemma volt_alt_def: "volt = watt ❙/ ampere"
  by simp
  
lemma farad_alt_def: "farad ≅⇩_Q coulomb ❙/ volt"
  by si_calc

lemma ohm_alt_def: "ohm ≅⇩_Q volt ❙/ ampere"
  by si_calc

lemma siemens_alt_def: "siemens ≅⇩_Q ampere ❙/ volt"
  by si_calc

lemma weber_alt_def: "weber ≅⇩_Q volt ❙⋅ second"
  by si_calc

lemma tesla_alt_def: "tesla ≅⇩_Q weber ❙/ metre⇧^𝟮"
  by si_calc

lemma henry_alt_def: "henry ≅⇩_Q weber ❙/ ampere"
  by si_calc

lemma lux_alt_def: "lux = lumen ❙/ metre⇧^𝟮"
  by simp

lemma gray_alt_def: "gray ≅⇩_Q joule ❙/ kilogram"
  by si_calc

lemma sievert_alt_def: "sievert ≅⇩_Q joule ❙/ kilogram"
  by si_calc

subsection ‹ Properties ›

lemma kilogram: "kilo *⇩_Q gram = kilogram"
  by (si_simp)

lemma celcius_to_kelvin: "T°C = (T *⇩_Q kelvin) + (273.15 *⇩_Q kelvin)"
  by (si_simp)

end