Theory SI_Astronomical

section ‹ Astronomical Constants ›

theory SI_Astronomical
  imports SI "HOL-Decision_Procs.Approximation"
begin

text ‹ We create a number of astronomical constants and prove relationships between some of them.
  For this, we use the approximation method that can compute bounds on transcendental functions. ›

definition julian_year :: "'a::field[T]" where
[si_eq]: "julian_year = 365.25 *⇩_Q day"

definition light_year :: "'a::field_char_0[L]" where
"light_year = QCOERCE[L] (❙c ❙⋅ julian_year)"

text ‹ We need to apply a coercion in the definition of light year to convert the dimension type
  from \<^typ>‹L ⋅ T⇧^-⇧¹ ⋅ T› to \<^typ>‹L›. The correctness of this coercion is confirmed by the following
  equivalence theorem. ›

lemma light_year: "light_year ≅⇩_Q ❙c ❙⋅ julian_year"
  unfolding light_year_def by (si_calc)

lemma light_year_eq [si_eq]: "⟦light_year⟧⇩_Q = ⟦❙c ❙⋅ julian_year⟧⇩_Q"
  using light_year quant_equiv_iff by blast

text ‹ HOL can characterise \<^const>‹pi› exactly and so we also give an exact value for the parsec. ›

definition parsec :: "real[L]" where
[si_eq]: "parsec = 648000 / pi *⇩_Q astronomical_unit"

text ‹ We calculate some conservative bounds on the parsec: it is somewhere between 3.26 and 3.27
  light-years. ›

lemma parsec_lb: "3.26 *⇩_Q light_year < parsec"
  by (si_simp, approximation 12)

lemma parsec_ub: "parsec < 3.27 *⇩_Q light_year"
  by (si_simp, approximation 12)

text‹ The full beauty of the approach is perhaps revealed here, with the 
      type of a classical three-dimensional gravitation field:›

type_synonym gravitation_field = "real⇧³[L] ⇒ (real⇧³[L ⋅ T⇧^-⇧²])"

end