Theory ISQ_Quantities

section ‹ Quantities ›

theory ISQ_Quantities
  imports ISQ_Dimensions
begin

subsection ‹ Quantity Semantic Domain ›

text ‹ Here, we give a semantic domain for particular values of physical quantities. A quantity 
  is usually expressed as a number and a measurement unit, and the goal is to support this. First,
  though, we give a more general semantic domain where a quantity has a magnitude and a dimension. ›

record ('a, 'd::enum) Quantity =
  mag  :: 'a                 ― ‹ Magnitude of the quantity. ›
  dim  :: "(int, 'd) dimvec" ― ‹ Dimension of the quantity -- denotes the kind of quantity. ›

text ‹ The quantity type is parametric as we permit the magnitude to be represented using any kind
  of numeric type, such as \<^typ>‹int›, \<^typ>‹rat›, or \<^typ>‹real›, though we usually minimally expect
  a field. ›

lemma Quantity_eq_intro:
  assumes "mag x = mag y" "dim x = dim y" "more x = more y"
  shows "x = y"
  by (simp add: assms eq_unit)

text ‹ We can define several arithmetic operators on quantities. Multiplication takes multiplies
  both the magnitudes and the dimensions. ›

instantiation Quantity_ext :: (times, enum, times) times
begin
definition times_Quantity_ext :: 
    "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" 
    where  [si_def]: "times_Quantity_ext x y = ⦇ mag = mag x ⋅ mag y, dim = dim x ⋅ dim y, 
                                                 … = more x ⋅ more y ⦈"
instance ..
end

lemma mag_times  [simp]: "mag (x ⋅ y) = mag x ⋅ mag y" by (simp add: times_Quantity_ext_def)
lemma dim_times  [simp]: "dim (x ⋅ y) = dim x ⋅ dim y" by (simp add: times_Quantity_ext_def)
lemma more_times [simp]: "more (x ⋅ y) = more x ⋅ more y" by (simp add: times_Quantity_ext_def)

text ‹ The zero and one quantities are both dimensionless quantities with magnitude of \<^term>‹0› and
  \<^term>‹1›, respectively. ›

instantiation Quantity_ext :: (zero, enum, zero) zero
begin
  definition "zero_Quantity_ext = ⦇ mag = 0, dim = 1, … = 0 ⦈"
instance ..
end

lemma mag_zero  [simp]:  "mag 0 = 0" by (simp add: zero_Quantity_ext_def)
lemma dim_zero  [simp]:  "dim 0 = 1" by (simp add: zero_Quantity_ext_def)
lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def)

instantiation Quantity_ext :: (one, enum, one) one
begin
  definition    [si_def]: "one_Quantity_ext = ⦇ mag = 1, dim = 1, … = 1 ⦈"
instance ..
end

lemma mag_one  [simp]: "mag 1 = 1" by (simp add: one_Quantity_ext_def)
lemma dim_one  [simp]: "dim 1 = 1" by (simp add: one_Quantity_ext_def)
lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def)

text ‹ Quantity inversion inverts both the magnitude and the dimension. Similarly, division of
  one quantity by another, divides both the magnitudes and the dimensions. ›

instantiation Quantity_ext :: (inverse, enum, inverse) inverse
begin
definition inverse_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" where 
  [si_def]: "inverse_Quantity_ext x = ⦇ mag = inverse (mag x), dim = inverse (dim x), … = inverse (more x) ⦈"
definition divide_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" where
  [si_def]: "divide_Quantity_ext x y = ⦇ mag = mag x / mag y, dim = dim x / dim y, … = more x / more y ⦈"
instance ..
end

lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)" 
  by (simp add: inverse_Quantity_ext_def)

lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)" 
  by (simp add: inverse_Quantity_ext_def)

lemma more_inverse [simp]: "more (inverse x) = inverse (more x)" 
  by (simp add: inverse_Quantity_ext_def)

lemma mag_divide [simp]: "mag (x / y) = mag x / mag y" 
  by (simp add: divide_Quantity_ext_def)

lemma dim_divide [simp]: "dim (x / y) = dim x / dim y" 
  by (simp add: divide_Quantity_ext_def)

lemma more_divide [simp]: "more (x / y) = more x / more y" 
  by (simp add: divide_Quantity_ext_def)

text ‹ As for dimensions, quantities form a commutative monoid and an abelian group. ›

instance Quantity_ext :: (comm_monoid_mult, enum, comm_monoid_mult) comm_monoid_mult
  by (intro_classes, simp_all add: eq_unit one_Quantity_ext_def times_Quantity_ext_def mult.assoc
     ,simp add: mult.commute)

instance Quantity_ext :: (ab_group_mult, enum, ab_group_mult) ab_group_mult
  by (intro_classes, rule Quantity_eq_intro, simp_all add: eq_unit)

text ‹ We can also define a partial order on quantities. ›

instantiation Quantity_ext :: (ord, enum, ord) ord
begin
  definition less_eq_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ bool"
    where "less_eq_Quantity_ext x y = (mag x ≤ mag y ∧ dim x = dim y ∧ more x ≤ more y)"
  definition less_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ bool"
    where "less_Quantity_ext x y = (x ≤ y ∧ ¬ y ≤ x)"

instance ..

end

instance Quantity_ext :: (order, enum, order) order
  by (intro_classes, auto simp add: less_Quantity_ext_def less_eq_Quantity_ext_def eq_unit)

text ‹ We can define plus and minus as well, but these are partial operators as they are defined
  only when the quantities have the same dimension. ›

instantiation Quantity_ext :: (plus, enum, plus) plus
begin
definition plus_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" 
    where [si_def]:
    "dim x = dim y ⟹ 
     plus_Quantity_ext x y = ⦇ mag = mag x + mag y, dim = dim x, … = more x + more y ⦈"
instance ..
end

instantiation Quantity_ext :: (uminus, enum, uminus) uminus
begin
  definition uminus_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" where 
  [si_def]: "uminus_Quantity_ext x = ⦇ mag = - mag x , dim = dim x, … = - more x ⦈"
instance ..
end

instantiation Quantity_ext :: (minus, enum, minus) minus
begin
  definition minus_Quantity_ext :: "('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme ⇒ ('a, 'b, 'c) Quantity_scheme" where 
  [si_def]:
    "dim x = dim y ⟹ 
      minus_Quantity_ext x y = ⦇ mag = mag x - mag y, dim = dim x, … = more x - more y ⦈"
instance ..
end

subsection ‹ Measurement Systems ›

class unit_system = unitary

lemma unit_system_intro: "(UNIV::'s set) = {a} ⟹ OFCLASS('s, unit_system_class)"
  by (simp add: unit_system_class_def, rule unitary_intro)

record ('a, 'd::enum, 's::unit_system) Measurement_System = "('a, 'd::enum) Quantity" +
  unit_sys  :: 's ― ‹ The system of units being employed ›

definition "mmore = Record.iso_tuple_snd Measurement_System_ext_Tuple_Iso"

lemma mmore [simp]: "mmore ⦇ unit_sys = x, … = y ⦈ = y"
  by (metis Measurement_System.ext_inject Measurement_System.ext_surjective comp_id mmore_def)

lemma mmore_ext [simp]: "⦇unit_sys = unit, … = mmore a⦈ = a"
  apply (case_tac a, rename_tac b, case_tac b)
  apply (simp add: Measurement_System_ext_def mmore_def Measurement_System_ext_Tuple_Iso_def Record.iso_tuple_snd_def Record.iso_tuple_cons_def Abs_Measurement_System_ext_inverse)
  apply (rename_tac x y z)
  apply (subgoal_tac "unit = y")
   apply (simp)
  apply (simp add: eq_unit)
  done

lemma Measurement_System_eq_intro:
  assumes "mag x = mag y" "dim x = dim y" "more x = more y"
  shows "x = y"
  by (rule Quantity_eq_intro, simp_all add: assms)
     (metis Measurement_System.surjective Quantity.select_convs(3) assms(3) mmore mmore_ext)

instantiation Measurement_System_ext :: (unit_system, "zero") "zero"
begin
definition zero_Measurement_System_ext :: "('a, 'b) Measurement_System_ext" 
    where  [si_def]: "zero_Measurement_System_ext = ⦇ unit_sys = unit, … = 0 ⦈"
instance ..
end

instantiation Measurement_System_ext :: (unit_system, "one") "one"
begin
definition one_Measurement_System_ext :: "('a, 'b) Measurement_System_ext"
    where  [si_def]: "one_Measurement_System_ext = ⦇ unit_sys = unit, … = 1 ⦈"
instance ..
end

instantiation Measurement_System_ext :: (unit_system, times) times
begin
definition times_Measurement_System_ext :: 
    "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" 
    where  [si_def]: "times_Measurement_System_ext x y = ⦇ unit_sys = unit, … = mmore x ⋅ mmore y ⦈"
instance ..
end

instantiation Measurement_System_ext :: (unit_system, inverse) inverse
begin
definition inverse_Measurement_System_ext :: "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" where 
  [si_def]: "inverse_Measurement_System_ext x = ⦇ unit_sys = unit, … = inverse (mmore x) ⦈"
definition divide_Measurement_System_ext ::
  "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" 
  where [si_def]: "divide_Measurement_System_ext x y = ⦇ unit_sys = unit, … = mmore x / mmore y ⦈"
instance ..
end

instance Measurement_System_ext :: (unit_system, comm_monoid_mult) comm_monoid_mult
  by (intro_classes, simp_all add: eq_unit one_Measurement_System_ext_def times_Measurement_System_ext_def mult.assoc, simp add: mult.commute)

instance Measurement_System_ext :: (unit_system, ab_group_mult) ab_group_mult
  by (intro_classes, simp_all add: si_def)

instantiation Measurement_System_ext :: (unit_system, ord) ord
begin
  definition less_eq_Measurement_System_ext :: "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ bool"
    where "less_eq_Measurement_System_ext x y = (mmore x ≤ mmore y)"
  definition less_Measurement_System_ext :: "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ bool"
    where "less_Measurement_System_ext x y = (x ≤ y ∧ ¬ y ≤ x)"
instance ..

end

instance Measurement_System_ext :: (unit_system, order) order
  by (intro_classes, simp_all add: less_eq_Measurement_System_ext_def less_Measurement_System_ext_def, metis mmore_ext)

instantiation Measurement_System_ext :: (unit_system, plus) plus
begin
definition plus_Measurement_System_ext :: 
  "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" 
    where [si_def]:
    "plus_Measurement_System_ext x y = ⦇ unit_sys = unit, … = mmore x + mmore y ⦈"
instance ..
end

instantiation Measurement_System_ext :: (unit_system, uminus) uminus
begin
  definition uminus_Measurement_System_ext :: "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" where 
  [si_def]: "uminus_Measurement_System_ext x = ⦇ unit_sys = unit, … = - mmore x ⦈"
instance ..
end

instantiation Measurement_System_ext :: (unit_system, minus) minus
begin
  definition minus_Measurement_System_ext :: 
    "('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext ⇒ ('a, 'b) Measurement_System_ext" where
  [si_def]:
    "minus_Measurement_System_ext x y = ⦇ unit_sys = unit, … = mmore x - mmore y ⦈"
instance ..
end

subsection ‹ Dimension Typed Quantities ›

text ‹ We can now define the type of quantities with parametrised dimension types. ›

typedef (overloaded) ('n, 'd::dim_type, 's::unit_system) QuantT ("_[_, _]" [999,0,0] 999) 
                     = "{x :: ('n, sdim, 's) Measurement_System. dim x = QD('d)}"
  morphisms fromQ toQ by (rule_tac x="⦇ mag = undefined, dim = QD('d), unit_sys = unit ⦈" in exI, simp)

setup_lifting type_definition_QuantT

text ‹ A dimension typed quantity is parameterised by two types: \<^typ>‹'a›, the numeric type for the
  magntitude, and \<^typ>‹'d› for the dimension expression, which is an element of \<^class>‹dim_type›. 
  The type \<^typ>‹('n, 'd, 's) QuantT› is to \<^typ>‹('n, 'd, 's) Measurement_System› as dimension types 
  are to \<^typ>‹Dimension›. Specifically, an element of \<^typ>‹('n', 'd, 's) QuantT› is a quantity whose 
  dimension is \<^typ>‹'d›.

  Intuitively, the formula \<^term>‹x :: 'n['d, 's]› can be read as ``$x$ is a quantity of \<^typ>‹'d›'',
  for example it might be a quantity of length, or a quantity of mass. ›

text ‹ Since quantities can have dimension type expressions that are distinct, but denote the same
  dimension, it is necessary to define the following function for coercion between two dimension
  expressions. This requires that the underlying dimensions are the same. ›

definition coerceQuantT :: "'d⇩₂ itself ⇒ 'a['d⇩₁::dim_type, 's::unit_system] ⇒ 'a['d⇩₂::dim_type, 's]" where
[si_def]: "QD('d⇩₁) = QD('d⇩₂) ⟹ coerceQuantT t x = (toQ (fromQ x))"

syntax
  "_QCOERCE" :: "type ⇒ logic ⇒ logic" ("QCOERCE[_]")

translations
  "QCOERCE['t]" == "CONST coerceQuantT TYPE('t)"

subsection ‹ Predicates on Typed Quantities ›

text ‹ The standard HOL order \<^term>‹(≤)› and equality \<^term>‹(=)› have the homogeneous type
  \<^typ>‹'a ⇒ 'a ⇒ bool› and so they cannot compare values of different types. Consequently,
  we define a heterogeneous order and equivalence on typed quantities. ›

lift_definition qless_eq :: "'n::order['a::dim_type, 's::unit_system] ⇒ 'n['b::dim_type, 's] ⇒ bool" (infix "≲⇩_Q" 50) 
  is "(≤)" .

lift_definition qequiv :: "'n['a::dim_type, 's::unit_system] ⇒ 'n['b::dim_type, 's] ⇒ bool" (infix "≅⇩_Q" 50) 
  is "(=)" .

text ‹ These are both fundamentally the same as the usual order and equality relations, but they
  permit potentially different dimension types, \<^typ>‹'a› and \<^typ>‹'b›. Two typed quantities are
  comparable only when the two dimension types have the same semantic dimension.
›

lemma qequiv_refl [simp]: "a ≅⇩_Q a"
  by (simp add: qequiv_def)

lemma qequiv_sym: "a ≅⇩_Q b ⟹ b ≅⇩_Q a"
  by (simp add: qequiv_def)

lemma qequiv_trans: "⟦ a ≅⇩_Q b; b ≅⇩_Q c ⟧ ⟹ a ≅⇩_Q c"
  by (simp add: qequiv_def)

theorem qeq_iff_same_dim:
  fixes x y :: "'a['d::dim_type, 's::unit_system]"
  shows "x ≅⇩_Q y ⟷ x = y"
  by (transfer, simp)

lemma coerceQuant_eq_iff:
  fixes x :: "'a['d⇩₁::dim_type, 's::unit_system]"
  assumes "QD('d⇩₁) = QD('d⇩₂::dim_type)"
  shows "(coerceQuantT TYPE('d⇩₂) x) ≅⇩_Q x"
  by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)

lemma coerceQuant_eq_iff2:
  fixes x :: "'a['d⇩₁::dim_type, 's::unit_system]"
  assumes "QD('d⇩₁) = QD('d⇩₂::dim_type)" and "y = (coerceQuantT TYPE('d⇩₂) x)"
  shows "x ≅⇩_Q y"
  using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
 
lemma updown_eq_iff:
  fixes x :: "'a['d⇩₁::dim_type, 's::unit_system]" fixes y :: "'a['d⇩₂::dim_type, 's]"
  assumes "QD('d⇩₁) = QD('d⇩₂::dim_type)" and "y = (toQ (fromQ x))"
  shows "x ≅⇩_Q y"
  by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceQuantT_def)

text‹This is more general that ‹y = x ⟹ x ≅⇩_Q y›, since x and y may have different type.›

lemma qeq: 
  fixes x :: "'a['d⇩₁::dim_type, 's::unit_system]" fixes y :: "'a['d⇩₂::dim_type, 's]"
  assumes "x ≅⇩_Q y"
  shows "QD('d⇩₁) = QD('d⇩₂)"
  by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)

subsection‹ Operators on Typed Quantities ›

text ‹ We define several operators on typed quantities. These variously compose the dimension types
  as well. Multiplication composes the two dimension types. Inverse constructs and inverted 
  dimension type. Division is defined in terms of multiplication and inverse. ›

lift_definition 
  qtimes :: "('n::comm_ring_1)['a::dim_type, 's::unit_system] ⇒ 'n['b::dim_type, 's] ⇒ 'n['a ⋅'b, 's]" (infixl "❙⋅" 69) 
  is "(*)" by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def)

lift_definition 
  qinverse :: "('n::field)['a::dim_type, 's::unit_system] ⇒ 'n['a⇧^-⇧¹, 's]" ("(_⇧^-⇧^𝟭)" [999] 999) 
  is "inverse" by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def)

abbreviation (input)
  qdivide :: "('n::field)['a::dim_type, 's::unit_system] ⇒ 'n['b::dim_type, 's] ⇒ 'n['a/'b, 's]" (infixl "❙'/" 70) where
"qdivide x y ≡ x ❙⋅ y⇧^-⇧^𝟭"

text ‹ We also provide some helpful notations for expressing heterogeneous powers. ›

abbreviation qsq         ("(_)⇧^𝟮"  [999] 999) where "u⇧^𝟮 ≡ u❙⋅u"
abbreviation qcube       ("(_)⇧^𝟯"  [999] 999) where "u⇧^𝟯 ≡ u❙⋅u❙⋅u"
abbreviation qquart      ("(_)⇧^𝟰"  [999] 999) where "u⇧^𝟰 ≡ u❙⋅u❙⋅u❙⋅u"

abbreviation qneq_sq     ("(_)⇧^-⇧^𝟮" [999] 999) where "u⇧^-⇧^𝟮 ≡ (u⇧^𝟮)⇧^-⇧^𝟭"
abbreviation qneq_cube   ("(_)⇧^-⇧^𝟯" [999] 999) where "u⇧^-⇧^𝟯 ≡ (u⇧^𝟯)⇧^-⇧^𝟭"
abbreviation qneq_quart  ("(_)⇧^-⇧^𝟰" [999] 999) where "u⇧^-⇧^𝟰 ≡ (u⇧^𝟯)⇧^-⇧^𝟭"

text ‹ Analogous to the \<^const>‹scaleR› operator for vectors, we define the following scalar
  multiplication that scales an existing quantity by a numeric value. This operator is
  especially important for the representation of quantity values, which consist of a numeric
  value and a unit. ›

lift_definition scaleQ :: "'a ⇒ 'a::comm_ring_1['d::dim_type, 's::unit_system] ⇒ 'a['d, 's]" (infixr "*⇩_Q" 63)
  is "λ r x. ⦇ mag = r * mag x, dim = QD('d), unit_sys = unit ⦈" by simp

text ‹ Finally, we instantiate the arithmetic types classes where possible. We do not instantiate
  \<^class>‹times› because this results in a nonsensical homogeneous product on quantities. ›

instantiation QuantT :: (zero, dim_type, unit_system) zero
begin
lift_definition zero_QuantT :: "('a, 'b, 'c) QuantT" is "⦇ mag = 0, dim = QD('b), unit_sys = unit ⦈" 
  by simp
instance ..
end

instantiation QuantT :: (one, dim_type, unit_system) one
begin
lift_definition one_QuantT :: "('a, 'b, 'c) QuantT" is "⦇ mag = 1, dim = QD('b), unit_sys = unit ⦈"
  by simp
instance ..
end

text ‹ The following specialised one element has both magnitude and dimension 1: it is a 
  dimensionless quantity. ›

abbreviation qone :: "'n::one[𝟭, 's::unit_system]" ("𝟭") where "qone ≡ 1"

text ‹ Unlike for semantic quantities, the plus operator on typed quantities is total, since the
  type system ensures that the dimensions (and the dimension types) must be the same. ›

instantiation QuantT :: (plus, dim_type, unit_system) plus
begin
lift_definition plus_QuantT :: "'a['b, 'c] ⇒ 'a['b, 'c] ⇒ 'a['b, 'c]"
  is "λ x y. ⦇ mag = mag x + mag y, dim = QD('b), unit_sys = unit ⦈"
  by (simp)
instance ..
end

text ‹ We can also show that typed quantities are commutative ∗‹additive› monoids. Indeed, addition
  is a much easier operator to deal with in typed quantities, unlike product. ›

instance QuantT :: (semigroup_add,dim_type,unit_system) semigroup_add
  by (intro_classes, transfer, simp add: add.assoc)

instance QuantT :: (ab_semigroup_add,dim_type,unit_system) ab_semigroup_add
  by (intro_classes, transfer, simp add: add.commute)

instance QuantT :: (monoid_add,dim_type,unit_system) monoid_add
  by (intro_classes; (transfer, simp add: eq_unit))
  
instance QuantT :: (comm_monoid_add,dim_type,unit_system) comm_monoid_add
  by (intro_classes; transfer, simp)

instantiation QuantT :: (uminus,dim_type,unit_system) uminus
begin
lift_definition uminus_QuantT :: "'a['b,'c] ⇒ 'a['b,'c]" 
  is "λ x. ⦇ mag = - mag x, dim = dim x, unit_sys = unit ⦈" by (simp)
instance ..
end

instantiation QuantT :: (minus,dim_type,unit_system) minus
begin
lift_definition minus_QuantT :: "'a['b,'c] ⇒ 'a['b,'c] ⇒ 'a['b,'c]"
  is "λ x y. ⦇ mag = mag x - mag y, dim = dim x, unit_sys = unit ⦈" by (simp)

instance ..
end

instance QuantT :: (numeral,dim_type,unit_system) numeral ..

text ‹ Moreover, types quantities also form an additive group. ›

instance QuantT :: (ab_group_add,dim_type,unit_system) ab_group_add
  by (intro_classes, (transfer, simp)+)

text ‹ Typed quantities helpfully can be both partially and a linearly ordered. ›

instantiation QuantT :: (order,dim_type,unit_system) order
begin
  lift_definition less_eq_QuantT :: "'a['b,'c] ⇒ 'a['b,'c] ⇒ bool" is "λ x y. mag x ≤ mag y" .
  lift_definition less_QuantT :: "'a['b,'c] ⇒ 'a['b,'c] ⇒ bool" is "λ x y. mag x < mag y" .
instance by (intro_classes, (transfer, simp add: unit_eq less_le_not_le Measurement_System_eq_intro)+)
end

instance QuantT :: (linorder,dim_type,unit_system) linorder
  by (intro_classes, transfer, auto)

instantiation QuantT :: (scaleR,dim_type,unit_system) scaleR
begin
lift_definition scaleR_QuantT :: "real ⇒ 'a['b,'c] ⇒ 'a['b,'c]"
is "λ n q. ⦇ mag = n *⇩_R mag q, dim = dim q, unit_sys = unit ⦈" by (simp)
instance ..
end

instance QuantT :: (real_vector,dim_type,unit_system) real_vector
  by (intro_classes, (transfer, simp add: eq_unit scaleR_add_left scaleR_add_right)+)

instantiation QuantT :: (norm,dim_type,unit_system) norm
begin
lift_definition norm_QuantT :: "'a['b,'c] ⇒ real" 
is "λ x. norm (mag x)" .
instance ..
end

instantiation QuantT :: (sgn_div_norm,dim_type,unit_system) sgn_div_norm
begin
definition sgn_QuantT :: "'a['b,'c] ⇒ 'a['b,'c]" where
"sgn_QuantT x = x /⇩_R norm x"
instance by (intro_classes, simp add: sgn_QuantT_def)
end

instantiation QuantT :: (dist_norm,dim_type,unit_system) dist_norm
begin
definition dist_QuantT :: "'a['b,'c] ⇒ 'a['b,'c] ⇒ real" where
"dist_QuantT x y = norm (x - y)"
instance
  by (intro_classes, simp add: dist_QuantT_def)
end

instantiation QuantT :: ("{uniformity_dist,dist_norm}",dim_type,unit_system) uniformity_dist
begin
definition uniformity_QuantT :: "('a['b,'c] × 'a['b,'c]) filter" where
"uniformity_QuantT = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"
instance
  by (intro_classes, simp add: uniformity_QuantT_def)
end

instantiation QuantT :: ("{dist_norm,open_uniformity,uniformity_dist}",dim_type,unit_system) 
                        open_uniformity
begin

definition open_QuantT :: "('a['b,'c]) set ⇒ bool" where
"open_QuantT U = (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"
instance by (intro_classes, simp add: open_QuantT_def)
end

text ‹ Quantities form a real normed vector space. ›

instance QuantT :: (real_normed_vector,dim_type,unit_system) real_normed_vector
  by (intro_classes; transfer, auto simp add: eq_unit norm_triangle_ineq)

end