Theory SI_Imperial

section ‹ Imperial Units via SI Units ›

theory SI_Imperial
  imports SI_Accepted
begin

subsection ‹ Units of Length ›

default_sort field_char_0

text ‹ The units of length are defined in terms of the international yard, as standardised in 1959. ›

definition yard :: "'a[L]" where
[si_eq]: "yard = 0.9144 *⇩Q metre"

definition foot :: "'a[L]" where
[si_eq]: "foot = 1/3 *⇩Q yard"

lemma foot_alt_def: "foot = 0.3048 *⇩Q metre"
  by (si_simp)

definition inch :: "'a[L]" where
[si_eq]: "inch = (1 / 36) *⇩Q yard"

lemma inch_alt_def: "inch = 25.4 *⇩Q milli *⇩Q metre"
  by (si_simp)

definition mile :: "'a[L]" where
[si_eq]: "mile = 1760 *⇩Q yard"

lemma mile_alt_def: "mile = 1609.344 *⇩Q metre"
  by (si_simp)

definition nautical_mile :: "'a[L]" where
[si_eq]: "nautical_mile = 1852 *⇩Q metre"

subsection ‹ Units of Mass ›

text ‹ The units of mass are defined in terms of the international yard, as standardised in 1959. ›

definition pound :: "'a[M]" where
[si_eq]: "pound = 0.45359237 *⇩Q kilogram"

definition ounce :: "'a[M]" where
[si_eq]: "ounce = 1/16 *⇩Q pound"

definition stone :: "'a[M]" where
[si_eq]: "stone = 14 *⇩Q pound"

subsection ‹ Other Units ›

definition knot :: "'a[L ⋅ T⇧-⇧1]" where
[si_eq]: "knot = 1 *⇩Q (nautical_mile ❙/ hour)"

definition pint :: "'a[Volume]" where
[si_eq]: "pint = 0.56826125 *⇩Q litre"

definition gallon :: "'a[Volume]" where
[si_eq]: "gallon = 8 *⇩Q pint"

definition degrees_farenheit :: "'a ⇒ 'a[Θ]" (‹_°F› [999] 999)
  where [si_eq]: "degrees_farenheit x = (x + 459.67)⋅5/9 *⇩Q kelvin"

default_sort type

subsection ‹ Unit Equations ›
  
lemma miles_to_feet: "mile = 5280 *⇩Q foot"
  by si_simp

lemma mph_to_kmh: "1 *⇩Q (mile ❙/ hour) = 1.609344 *⇩Q ((kilo *⇩Q metre) ❙/ hour)"
  by si_simp

lemma farenheit_to_celcius: "T°F = ((T - 32) ⋅ 5/9)°C"
  by si_simp

end