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⇧-⇧2, SI]"
abbreviation "pascal ≡ kilogram ❙⋅ metre⇧-⇧𝟭 ❙⋅ second⇧-⇧𝟮"
type_synonym 'a pascal = "'a[M ⋅ L⇧-⇧1 ⋅ T⇧-⇧2, SI]"
abbreviation "volt ≡ kilogram ❙⋅ metre⇧𝟮 ❙⋅ second⇧-⇧𝟯 ❙⋅ ampere⇧-⇧𝟭"
type_synonym 'a volt = "'a[M ⋅ L⇧2 ⋅ T⇧-⇧3 ⋅ I⇧-⇧1, SI]"
abbreviation "farad ≡ kilogram⇧-⇧𝟭 ❙⋅ metre⇧-⇧𝟮 ❙⋅ second⇧𝟰 ❙⋅ ampere⇧𝟮"
type_synonym 'a farad = "'a[M⇧-⇧1 ⋅ L⇧-⇧2 ⋅ T⇧4 ⋅ I⇧2, SI]"
abbreviation "ohm ≡ kilogram ❙⋅ metre⇧𝟮 ❙⋅ second⇧-⇧𝟯 ❙⋅ ampere⇧-⇧𝟮"
type_synonym 'a ohm = "'a[M ⋅ L⇧2 ⋅ T⇧-⇧3 ⋅ I⇧-⇧2, 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