Theory ISQ_Conversion

section ‹ Conversion Between Unit Systems ›

theory ISQ_Conversion
  imports ISQ_Units
begin
                                          
subsection ‹ Conversion Schemas ›

text ‹  A conversion schema provides factors for each of the base units for converting between
  two systems of units. We currently only support conversion between systems that can meaningfully
  characterise a subset of the seven SI dimensions. ›

record ConvSchema =
  cLengthF      :: rat
  cMassF        :: rat
  cTimeF        :: rat
  cCurrentF     :: rat 
  cTemperatureF :: rat
  cAmountF      :: rat
  cIntensityF   :: rat

text ‹ We require that all the factors of greater than zero. ›

typedef ('s⇩1::unit_system, 's⇩2::unit_system) Conversion ("(_/ ⇒⇩U _)" [1, 0] 0) =
  "{c :: ConvSchema. cLengthF c > 0 ∧ cMassF c > 0 ∧ cTimeF c > 0 ∧ cCurrentF c > 0
         ∧ cTemperatureF c > 0 ∧ cAmountF c > 0 ∧ cIntensityF c > 0}"
  by (rule_tac x="⦇ cLengthF = 1, cMassF = 1, cTimeF = 1, cCurrentF = 1
                  , cTemperatureF = 1, cAmountF = 1, cIntensityF = 1 ⦈" in exI, simp)

setup_lifting type_definition_Conversion

lift_definition LengthF      :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cLengthF .
lift_definition MassF        :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cMassF .
lift_definition TimeF        :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cTimeF .
lift_definition CurrentF     :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cCurrentF .
lift_definition TemperatureF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cTemperatureF .
lift_definition AmountF      :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cAmountF .
lift_definition IntensityF   :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cIntensityF .

lemma Conversion_props [simp]: "LengthF c > 0" "MassF c > 0" "TimeF c > 0" "CurrentF c > 0"
  "TemperatureF c > 0" "AmountF c > 0" "IntensityF c > 0"
  by (transfer, simp)+

subsection ‹ Conversion Algebra ›

lift_definition convid :: "'s::unit_system ⇒⇩U 's" ("id⇩C")
is "
  ⦇ cLengthF = 1
  , cMassF = 1
  , cTimeF = 1
  , cCurrentF = 1
  , cTemperatureF = 1
  , cAmountF = 1
  , cIntensityF = 1 ⦈" by simp

lift_definition convcomp :: 
  "('s⇩2 ⇒⇩U 's⇩3::unit_system) ⇒ ('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ ('s⇩1 ⇒⇩U 's⇩3)" (infixl "∘⇩C" 55) is
"λ c⇩1 c⇩2. ⦇ cLengthF = cLengthF c⇩1 * cLengthF c⇩2, cMassF = cMassF c⇩1 * cMassF c⇩2
         , cTimeF = cTimeF c⇩1 * cTimeF c⇩2, cCurrentF = cCurrentF c⇩1 * cCurrentF c⇩2
         , cTemperatureF = cTemperatureF c⇩1 * cTemperatureF c⇩2
         , cAmountF = cAmountF c⇩1 * cAmountF c⇩2, cIntensityF = cIntensityF c⇩1 * cIntensityF c⇩2 ⦈"
  by simp

lift_definition convinv :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ ('s⇩2 ⇒⇩U 's⇩1)" ("inv⇩C") is
"λ c. ⦇ cLengthF = inverse (cLengthF c), cMassF = inverse (cMassF c), cTimeF = inverse (cTimeF c)
      , cCurrentF = inverse (cCurrentF c), cTemperatureF = inverse (cTemperatureF c)
      , cAmountF = inverse (cAmountF c), cIntensityF = inverse (cIntensityF c) ⦈" by simp

lemma convinv_inverse [simp]: "convinv (convinv c) = c"
  by (transfer, simp)

lemma convcomp_inv [simp]: "c ∘⇩C inv⇩C c = id⇩C"
  by (transfer, simp)

lemma inv_convcomp [simp]: "inv⇩C c ∘⇩C c = id⇩C"
  by (transfer, simp)

lemma Conversion_invs [simp]: "LengthF (inv⇩C x) = inverse (LengthF x)" "MassF (inv⇩C x) = inverse (MassF x)"
  "TimeF (inv⇩C x) = inverse (TimeF x)" "CurrentF (inv⇩C x) = inverse (CurrentF x)"
  "TemperatureF (inv⇩C x) = inverse (TemperatureF x)" "AmountF (inv⇩C x) = inverse (AmountF x)"
  "IntensityF (inv⇩C x) = inverse (IntensityF x)"
  by (transfer, simp)+

lemma Conversion_comps [simp]: "LengthF (c⇩1 ∘⇩C c⇩2) = LengthF c⇩1 * LengthF c⇩2"
  "MassF (c⇩1 ∘⇩C c⇩2) = MassF c⇩1 * MassF c⇩2"
  "TimeF (c⇩1 ∘⇩C c⇩2) = TimeF c⇩1 * TimeF c⇩2"
  "CurrentF (c⇩1 ∘⇩C c⇩2) = CurrentF c⇩1 * CurrentF c⇩2"
  "TemperatureF (c⇩1 ∘⇩C c⇩2) = TemperatureF c⇩1 * TemperatureF c⇩2"
  "AmountF (c⇩1 ∘⇩C c⇩2) = AmountF c⇩1 * AmountF c⇩2"
  "IntensityF (c⇩1 ∘⇩C c⇩2) = IntensityF c⇩1 * IntensityF c⇩2"
  by (transfer, simp)+

subsection ‹ Conversion Functions ›

definition dconvfactor :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ Dimension ⇒ rat" where
"dconvfactor c d = 
  LengthF c ^⇩Z dim_nth d Length
  * MassF c ^⇩Z dim_nth d Mass 
  * TimeF c ^⇩Z dim_nth d Time 
  * CurrentF c ^⇩Z dim_nth d Current 
  * TemperatureF c ^⇩Z dim_nth d Temperature
  * AmountF c ^⇩Z dim_nth d Amount
  * IntensityF c ^⇩Z dim_nth d Intensity"

lemma dconvfactor_pos [simp]: "dconvfactor c d > 0"
  by (simp add: dconvfactor_def)

lemma dconvfactor_nz [simp]: "dconvfactor c d ≠ 0"
  by (metis dconvfactor_pos less_numeral_extra(3))
  
lemma dconvfactor_convinv: "dconvfactor (convinv c) d = inverse (dconvfactor c d)"
  by (simp add: dconvfactor_def intpow_inverse[THEN sym])

lemma dconvfactor_id [simp]: "dconvfactor id⇩C d = 1"
  by (simp add: dconvfactor_def, transfer, simp)

lemma dconvfactor_compose:
  "dconvfactor (c⇩1 ∘⇩C c⇩2) d = dconvfactor c⇩1 d * dconvfactor c⇩2 d"
  by (simp add: dconvfactor_def, transfer, simp add: mult_ac intpow_mult_distrib)

lemma dconvfactor_inverse:
  "dconvfactor c (inverse d) = inverse (dconvfactor c d)"
  by (simp add: dconvfactor_def inverse_dimvec_def intpow_uminus)

lemma dconvfactor_times:
  "dconvfactor c (x ⋅ y) = dconvfactor c x ⋅ dconvfactor c y"
  by (auto simp add: dconvfactor_def  mult_ac intpow_mult_combine times_dimvec_def)
                                                                                                                                           
lift_definition qconv :: "('s⇩1, 's⇩2) Conversion ⇒ ('a::field_char_0)['d::dim_type, 's⇩1::unit_system] ⇒ 'a['d, 's⇩2::unit_system]"
is "λ c q. ⦇ mag = of_rat (dconvfactor c (dim q)) * mag q, dim = dim q, unit_sys = unit ⦈" by simp

lemma magQ_qconv: "⟦qconv c q⟧⇩Q = of_rat (dconvfactor c (dimQ q)) * ⟦q⟧⇩Q"
  by (simp add: si_def, transfer, simp)

lemma qconv_id [simp]: "qconv id⇩C x = x"
  by (transfer', simp add: Measurement_System_eq_intro)

lemma qconv_comp: "qconv (c⇩1 ∘⇩C c⇩2) x = qconv c⇩1 (qconv c⇩2 x)"
  by (transfer, simp add: dconvfactor_compose of_rat_mult)

lemma qconv_convinv [simp]: "qconv (convinv c) (qconv c x) = x"
  by (transfer, simp add: dconvfactor_convinv mult.assoc[THEN sym] of_rat_mult[THEN sym] Measurement_System_eq_intro)

lemma qconv_scaleQ [simp]: "qconv c (d *⇩Q x) = d *⇩Q qconv c x"
  by (transfer, simp)

lemma qconv_plus [simp]: "qconv c (x + y) = qconv c x + qconv c y"
  by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs)

lemma qconv_minus [simp]: "qconv c (x - y) = qconv c x - qconv c y"
  by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs)

lemma qconv_qmult [simp]: "qconv c (x ❙⋅ y) = qconv c x ❙⋅ qconv c y"
  by (transfer, simp add: times_Quantity_ext_def times_Measurement_System_ext_def dconvfactor_times of_rat_mult)

lemma qconv_qinverse [simp]: "qconv c (x⇧-⇧𝟭) = (qconv c x)⇧-⇧𝟭"
  by (transfer, simp add: inverse_Quantity_ext_def inverse_Measurement_System_ext_def dconvfactor_inverse of_rat_inverse)

lemma qconv_Length [simp]: "qconv c BUNIT(L, _) = LengthF c *⇩Q BUNIT(L, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Mass [simp]: "qconv c BUNIT(M, _) = MassF c *⇩Q BUNIT(M, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Time [simp]: "qconv c BUNIT(T, _) = TimeF c *⇩Q BUNIT(T, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Current [simp]: "qconv c BUNIT(I, _) = CurrentF c *⇩Q BUNIT(I, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Temperature [simp]: "qconv c BUNIT(Θ, _) = TemperatureF c *⇩Q BUNIT(Θ, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Amount [simp]: "qconv c BUNIT(N, _) = AmountF c *⇩Q BUNIT(N, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

lemma qconv_Intensity [simp]: "qconv c BUNIT(J, _) = IntensityF c *⇩Q BUNIT(J, _)" 
  by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def)

end