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  L2  T-3  I-1, SI]"

abbreviation "farad  kilogram-𝟭  metre-𝟮  second𝟰  ampere𝟮"

type_synonym 'a farad = "'a[M-1  L-2  T4  I2, SI]"

abbreviation "ohm  kilogram  metre𝟮  second-𝟯  ampere-𝟮"

type_synonym 'a ohm = "'a[M  L2  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