Theory BIS

section ‹ British Imperial System (1824/1897) ›

theory BIS
  imports ISQ SI_Units CGS
begin

text ‹ The values in the British Imperial System (BIS) are derived from the UK Weights and Measures 
  Act 1824. ›

subsection ‹ Preliminaries ›

typedef BIS = "UNIV :: unit set" ..
instance BIS :: unit_system
  by (rule unit_system_intro[of "Abs_BIS ()"], 
      metis (full_types) Abs_BIS_cases UNIV_eq_I insert_iff old.unit.exhaust)
instance BIS :: time_second ..
abbreviation "BIS ≡ unit :: BIS"

subsection ‹ Base Units ›

abbreviation "yard     ≡ BUNIT(L, BIS)"
abbreviation "pound    ≡ BUNIT(M, BIS)"
abbreviation "rankine  ≡ BUNIT(Θ, BIS)"

text ‹ We chose Rankine rather than Farenheit as this is more compatible with the SI system and 
  avoids the need for having an offset in conversion functions. ›

subsection ‹ Derived Units ›

definition [si_eq]: "foot = 1/3 *⇩Q yard"

definition [si_eq]: "inch = 1/12 *⇩Q foot"

definition [si_eq]: "furlong = 220 *⇩Q yard"

definition [si_eq]: "mile = 1760 *⇩Q yard"

definition [si_eq]: "acre = 4840 *⇩Q yard⇧𝟯"

definition [si_eq]: "ounce = 1/12 *⇩Q pound"

definition [si_eq]: "gallon = 277.421 *⇩Q inch⇧𝟯"

definition [si_eq]: "quart = 1/4 *⇩Q gallon"

definition [si_eq]: "pint = 1/8 *⇩Q gallon"

definition [si_eq]: "peck = 2 *⇩Q gallon"

definition [si_eq]: "bushel = 8 *⇩Q gallon"

definition [si_eq]: "minute = 60 *⇩Q second"

definition [si_eq]: "hour = 60 *⇩Q minute"

subsection ‹ Conversion to SI ›

instantiation BIS :: metrifiable
begin

lift_definition convschema_BIS :: "BIS itself ⇒ (BIS, SI) Conversion" is
"λ x. ⦇ cLengthF = 0.9143993, cMassF = 0.453592338, cTimeF = 1
      , cCurrentF = 1, cTemperatureF = 5/9, cAmountF = 1, cIntensityF = 1 ⦈" by simp

instance ..
end

lemma BIS_SI_simps [simp]: "LengthF (convschema (a::BIS itself)) = 0.9143993" 
                           "MassF (convschema a) = 0.453592338"
                           "TimeF (convschema a) = 1" 
                           "CurrentF (convschema a) = 1" 
                           "TemperatureF (convschema a) = 5/9"
  by (transfer, simp)+

subsection ‹ Conversion Examples ›

lemma "metrify (foot :: rat[L, BIS]) = 0.9143993 / 3 *⇩Q metre"
  by (simp add: foot_def)

lemma "metrify ((70::rat) *⇩Q mile ❙/ hour) = (704087461 / 22500000) *⇩Q (metre ❙/ second)"
  by (si_simp)

lemma "QMC(CGS → BIS) ((1::rat) *⇩Q centimetre) = 100000 / 9143993 *⇩Q yard"
  by simp



end