Session Physical_Quantities

Theory Power_int

section ‹ Integer Powers ›

theory Power_int
  imports "HOL.Real"
begin

text ‹ The standard HOL power operator is only for natural powers. This operator allows integers. ›

definition intpow :: "'a::{linordered_field}  int  'a" (infixr "^Z" 80) where
"intpow x n = (if (n < 0) then inverse (x ^ nat (-n)) else (x ^ nat n))"

lemma intpow_zero [simp]: "x ^Z 0 = 1"
  by (simp add: intpow_def)

lemma intpow_spos [simp]: "x > 0  x ^Z n > 0"
  by (simp add: intpow_def)

lemma intpow_one [simp]: "x ^Z 1 = x"
  by (simp add: intpow_def)

lemma one_intpow [simp]: "1 ^Z n = 1"
  by (simp add: intpow_def)

lemma intpow_plus: "x > 0  x ^Z (m + n) = x ^Z m * x ^Z n"
  apply (simp add: intpow_def field_simps power_add)
  apply (metis (no_types, hide_lams) abs_ge_zero add.commute add_diff_cancel_right' nat_add_distrib power_add uminus_add_conv_diff zabs_def)
  done

lemma intpow_mult_combine: "x > 0  x ^Z m * (x ^Z n * y) = x ^Z (m + n) * y"
  by (simp add: intpow_plus)

lemma intpow_pos [simp]: "n  0  x ^Z n = x ^ nat n"
  by (simp add: intpow_def)

lemma intpow_uminus: "x ^Z -n = inverse (x ^Z n)"
  by (simp add: intpow_def)

lemma intpow_uminus_nat: "n  0  x ^Z -n = inverse (x ^ nat n)"
  by (simp add: intpow_def)

lemma intpow_inverse: "inverse a ^Z n = inverse (a ^Z n)"
  by (simp add: intpow_def power_inverse)

lemma intpow_mult_distrib: "(x * y) ^Z m = x ^Z m * y ^Z m"
  by (simp add: intpow_def power_mult_distrib)

end

Theory Enum_extra

section ‹ Enumeration Extras ›

theory Enum_extra
  imports "HOL-Library.Cardinality"
begin

subsection ‹ First Index Function ›

text ‹ The following function extracts the index of the first occurrence of an element in a list, 
  assuming it is indeed an element. ›

fun first_ind :: "'a list  'a  nat  nat" where
"first_ind [] y i = undefined" |
"first_ind (x # xs) y i = (if (x = y) then i else first_ind xs y (Suc i))"

lemma first_ind_length:
  "x  set(xs)  first_ind xs x i < length(xs) + i"
  by (induct xs arbitrary: i, auto, metis add_Suc_right)

lemma nth_first_ind:
  " distinct xs; x  set(xs)   xs ! (first_ind xs x i - i) = x"
  apply (induct xs arbitrary: i)
   apply (auto)
  apply (metis One_nat_def add.right_neutral add_Suc_right add_diff_cancel_left' diff_diff_left empty_iff first_ind.simps(2) list.set(1) nat.simps(3) neq_Nil_conv nth_Cons' zero_diff)
  done

lemma first_ind_nth:
  " distinct xs; i < length xs   first_ind xs (xs ! i) j = i + j"
  apply (induct xs arbitrary: i j)
   apply (auto)
   apply (metis less_Suc_eq_le nth_equal_first_eq)
  using less_Suc_eq_0_disj apply auto
  done

subsection ‹ Enumeration Indices ›

syntax
  "_ENUM" :: "type  logic" ("ENUM'(_')")

translations
  "ENUM('a)" => "CONST Enum.enum :: ('a::enum) list"

text ‹ Extract a unique natural number associated with an enumerated value by using its index
  in the characteristic list termENUM('a). ›

definition enum_ind :: "'a::enum  nat" where
"enum_ind (x :: 'a::enum) = first_ind ENUM('a) x 0"

lemma length_enum_CARD: "length ENUM('a) = CARD('a)"
  by (simp add: UNIV_enum distinct_card enum_distinct)

lemma CARD_length_enum: "CARD('a) = length ENUM('a)"
  by (simp add: length_enum_CARD)

lemma enum_ind_less_CARD [simp]: "enum_ind (x :: 'a::enum) < CARD('a)"
  using first_ind_length[of x, OF in_enum, of 0] by (simp add: enum_ind_def CARD_length_enum)
  
lemma enum_nth_ind [simp]: "Enum.enum ! (enum_ind x) = x"
  using nth_first_ind[of Enum.enum x 0, OF enum_distinct in_enum] by (simp add: enum_ind_def)

lemma enum_distinct_conv_nth:
  assumes "i < CARD('a)" "j < CARD('a)" "ENUM('a) ! i = ENUM('a) ! j"
  shows "i = j"
proof -
  have "(i<length ENUM('a). j<length ENUM('a). i  j  ENUM('a) ! i  ENUM('a) ! j)"
    using distinct_conv_nth[of "ENUM('a)", THEN sym] by (simp add: enum_distinct)
  with assms show ?thesis
    by (auto simp add: CARD_length_enum)
qed

lemma enum_ind_nth [simp]:
  assumes "i < CARD('a::enum)"
  shows "enum_ind (ENUM('a) ! i) = i"
  using assms first_ind_nth[of "ENUM('a)" i 0, OF enum_distinct]
  by (simp add: enum_ind_def CARD_length_enum)

lemma enum_ind_spec:
  "enum_ind (x :: 'a::enum) = (THE i. i < CARD('a)  Enum.enum ! i = x)"
proof (rule sym, rule the_equality, safe)
  show "enum_ind x < CARD('a)"
    by (simp add: enum_ind_less_CARD[of x])
  show "enum_class.enum ! enum_ind x = x"
    by simp
  show "i. i < CARD('a)  x = ENUM('a) ! i  i = enum_ind (ENUM('a) ! i)"
    by (simp add: enum_ind_nth)
qed

lemma enum_ind_inj: "inj (enum_ind :: 'a::enum  nat)"
  by (rule inj_on_inverseI[of _ "λ i. ENUM('a) ! i"], simp)

lemma enum_ind_neq [simp]: "x  y  enum_ind x  enum_ind y"
  by (simp add: enum_ind_inj inj_eq)

end

Theory Groups_mult

section ‹ Multiplication Groups ›

theory Groups_mult
  imports Main
begin

text ‹ The HOL standard library only has groups based on addition. Here, we build one based on
  multiplication. ›

notation times (infixl "" 70)

class group_mult = inverse + monoid_mult +
  assumes left_inverse: "inverse a  a = 1"
  assumes multi_inverse_conv_div [simp]: "a  (inverse b) = a / b"
begin

lemma div_conv_mult_inverse: "a / b = a  (inverse b)"
  by simp

sublocale mult: group times 1 inverse
  by standard (simp_all add: left_inverse)

lemma diff_self [simp]: "a / a = 1"
  using mult.right_inverse by auto

lemma mult_distrib_inverse [simp]: "(a * b) / b = a"
  by (metis local.mult_1_right local.multi_inverse_conv_div mult.right_inverse mult_assoc)

end

class ab_group_mult = comm_monoid_mult + group_mult
begin

lemma mult_distrib_inverse' [simp]: "(a * b) / a = b"
  using local.mult_distrib_inverse mult_commute by fastforce

lemma inverse_distrib: "inverse (a * b)  =  (inverse a) * (inverse b)"
  by (simp add: local.mult.inverse_distrib_swap mult_commute)

lemma inverse_divide [simp]: "inverse (a / b) = b / a"
  by (metis div_conv_mult_inverse inverse_distrib mult.commute mult.inverse_inverse)

end

abbreviation (input) npower :: "'a::{power,inverse}  nat  'a"  ("(_-_)" [1000,999] 999) 
  where "npower x n  inverse (x ^ n)"

end

Theory ISQ_Dimensions

chapter ‹ International System of Quantities ›

section ‹ Quantity Dimensions ›

theory ISQ_Dimensions
  imports Groups_mult Power_int Enum_extra
          HOL.Transcendental
          "HOL-Eisbach.Eisbach"
begin

subsection ‹ Preliminaries ›

class unitary = finite +
  assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
begin

definition "unit = (undefined::'a)"

lemma UNIV_unitary: "UNIV = {a::'a}"
proof -
  have "card(UNIV :: 'a set) = 1"
    by (simp add: local.unitary_unit_pres)
  thus ?thesis
    by (metis (full_types) UNIV_I card_1_singletonE empty_iff insert_iff)
qed

lemma eq_unit: "(a::'a) = b"
  by (metis (full_types) UNIV_unitary iso_tuple_UNIV_I singletonD)

end

lemma unitary_intro: "(UNIV::'s set) = {a}  OFCLASS('s, unitary_class)"
  apply (intro_classes, auto)
  using finite.simps apply blast
  using card_1_singleton_iff apply blast
  done

named_theorems si_def and si_eq

instantiation unit :: comm_monoid_add
begin
  definition "zero_unit = ()"
  definition "plus_unit (x::unit) (y::unit) = ()"
  instance proof qed (simp_all)
end

instantiation unit :: comm_monoid_mult
begin
  definition "one_unit = ()"
  definition "times_unit (x::unit) (y::unit) = ()"
  instance proof qed (simp_all)
end

instantiation unit :: inverse
begin
  definition "inverse_unit (x::unit) = ()"
  definition "divide_unit (x::unit) (y::unit) = ()"
  instance ..
end

instance unit :: ab_group_mult
  by (intro_classes, simp_all)

subsection ‹ Dimension Vectors ›

text ‹ Quantity dimensions are used to distinguish quantities of different kinds. Only quantities
  of the same kind can be compared and combined: it is a mistake to add a length to a mass, for
  example. Dimensions are often expressed in terms of seven base quantities, which can be combined 
  to form derived quantities. Consequently, a dimension associates with each of the base quantities 
  an integer that denotes the power to which it is raised. We use a special vector type to represent
  dimensions, and then specialise this to the seven major dimensions. ›

typedef ('n, 'd) dimvec = "UNIV :: ('d::enum  'n) set"
  morphisms dim_nth dim_lambda ..

declare dim_lambda_inject [simplified, simp]
declare dim_nth_inverse [simp]
declare dim_lambda_inverse [simplified, simp]

instantiation dimvec :: (zero, enum) "one"
begin
definition one_dimvec :: "('a, 'b) dimvec" where "one_dimvec = dim_lambda (λ i. 0)"
instance ..
end

instantiation dimvec :: (plus, enum) times
begin
definition times_dimvec :: "('a, 'b) dimvec  ('a, 'b) dimvec  ('a, 'b) dimvec" where
"times_dimvec x y = dim_lambda (λ i. dim_nth x i + dim_nth y i)"
instance ..
end

instance dimvec :: (comm_monoid_add, enum) comm_monoid_mult
  by ((intro_classes; simp add: times_dimvec_def one_dimvec_def fun_eq_iff add.assoc), simp add: add.commute)
  
text ‹ We also define the inverse and division operations, and an abelian group, which will allow
  us to perform dimensional analysis. ›

instantiation dimvec :: ("{plus,uminus}", enum) inverse
begin
definition inverse_dimvec :: "('a, 'b) dimvec  ('a, 'b) dimvec" where
"inverse_dimvec x = dim_lambda (λ i. - dim_nth x i)"

definition divide_dimvec :: "('a, 'b) dimvec  ('a, 'b) dimvec  ('a, 'b) dimvec" where
[code_unfold]: "divide_dimvec x y = x * (inverse y)"

  instance ..
end

instance dimvec :: (ab_group_add, enum) ab_group_mult
  by (intro_classes, simp_all add: inverse_dimvec_def one_dimvec_def times_dimvec_def divide_dimvec_def)

subsection ‹ Code Generation ›

text ‹ Dimension vectors can be represented using lists, which enables code generation and thus
  efficient proof. ›

definition mk_dimvec :: "'n list  ('n::ring_1, 'd::enum) dimvec" 
  where "mk_dimvec ds = (if (length ds = CARD('d)) then dim_lambda (λ d. ds ! enum_ind d) else 1)"

code_datatype mk_dimvec

lemma mk_dimvec_inj: "inj_on (mk_dimvec :: 'n list  ('n::ring_1, 'd::enum) dimvec) {xs. length xs = CARD('d)}"
proof (rule inj_onI, safe)
  fix x y :: "'n list"
  assume a: "(mk_dimvec x :: ('n, 'd) dimvec) = mk_dimvec y" "length x = CARD('d)" "length y = CARD('d)"
  have "i. i < length x  x ! i = y ! i"
  proof -
    fix i
    assume "i < length x"
    with a have "enum_ind (ENUM('d) ! i) = i"
      by (simp)
    with a show "x ! i = y ! i"
      by (auto simp add: mk_dimvec_def fun_eq_iff, metis)
  qed

  then show "x = y"
    by (metis a(2) a(3) nth_equalityI)
qed

lemma mk_dimvec_eq_iff [simp]: 
  assumes "length x = CARD('d)" "length y = CARD('d)"
  shows "((mk_dimvec x :: ('n::ring_1, 'd::enum) dimvec) = mk_dimvec y)  (x = y)"
  by (rule inj_on_eq_iff[OF mk_dimvec_inj], simp_all add: assms)

lemma one_mk_dimvec [code, si_def]: "(1::('n::ring_1, 'a::enum) dimvec) = mk_dimvec (replicate CARD('a) 0)"
  by (auto simp add: mk_dimvec_def one_dimvec_def)

lemma times_mk_dimvec [code, si_def]:
  "(mk_dimvec xs * mk_dimvec ys :: ('n::ring_1, 'a::enum) dimvec) = 
  (if (length xs = CARD('a)  length ys = CARD('a))
    then mk_dimvec (map (λ (x, y). x + y) (zip xs ys))
    else if length xs = CARD('a) then mk_dimvec xs else mk_dimvec ys)"
  by (auto simp add: times_dimvec_def mk_dimvec_def fun_eq_iff one_dimvec_def)

lemma power_mk_dimvec [si_def]:
  "(power (mk_dimvec xs) n :: ('n::ring_1, 'a::enum) dimvec) = 
    (if (length xs = CARD('a)) then mk_dimvec (map ((*) (of_nat n)) xs) else mk_dimvec xs)"
  by (induct n, simp add: one_dimvec_def mk_dimvec_def)
     (auto simp add: times_mk_dimvec zip_map_map[where f="id", simplified] comp_def split_beta' zip_same_conv_map distrib_right mult.commute)

lemma inverse_mk_dimvec [code, si_def]:
  "(inverse (mk_dimvec xs) :: ('n::ring_1, 'a::enum) dimvec) = 
   (if (length xs = CARD('a)) then mk_dimvec (map uminus xs) else 1)"
  by (auto simp add: inverse_dimvec_def one_dimvec_def mk_dimvec_def fun_eq_iff)  

lemma divide_mk_dimvec [code, si_def]:
  "(mk_dimvec xs / mk_dimvec ys :: ('n::ring_1, 'a::enum) dimvec) = 
  (if (length xs = CARD('a)  length ys = CARD('a))
    then mk_dimvec (map (λ (x, y). x - y) (zip xs ys))
    else if length ys = CARD('a) then mk_dimvec (map uminus ys) else mk_dimvec xs)"
  by (auto simp add: divide_dimvec_def inverse_mk_dimvec times_mk_dimvec zip_map_map[where f="id", simplified] comp_def split_beta')

text ‹ A base dimension is a dimension where precisely one component has power 1: it is the 
  dimension of a base quantity. Here we define the seven base dimensions. ›

definition mk_BaseDim :: "'d::enum  (int, 'd) dimvec" where
"mk_BaseDim d = dim_lambda (λ i. if (i = d) then 1 else 0)"

lemma mk_BaseDim_neq [simp]: "x  y  mk_BaseDim x  mk_BaseDim y"
  by (auto simp add: mk_BaseDim_def fun_eq_iff)

lemma mk_BaseDim_code [code]: "mk_BaseDim (d::'d::enum) = mk_dimvec (list_update (replicate CARD('d) 0) (enum_ind d) 1)"
  by (auto simp add: mk_BaseDim_def mk_dimvec_def fun_eq_iff)

definition is_BaseDim :: "(int, 'd::enum) dimvec  bool" 
  where "is_BaseDim x  ( i. x = dim_lambda ((λ x. 0)(i := 1)))"

lemma is_BaseDim_mk [simp]: "is_BaseDim (mk_BaseDim x)"
  by (auto simp add: mk_BaseDim_def is_BaseDim_def fun_eq_iff)

subsection ‹ Dimension Semantic Domain ›

text ‹ We next specialise dimension vectors to the usual seven place vector. ›

datatype sdim = Length | Mass | Time | Current | Temperature | Amount | Intensity

lemma sdim_UNIV: "(UNIV :: sdim set) = {Length, Mass, Time, Current, Temperature, Amount, Intensity}"
  using sdim.exhaust by blast

lemma CARD_sdim [simp]: "CARD(sdim) = 7"
  by (simp add: sdim_UNIV)

instantiation sdim :: enum
begin
  definition "enum_sdim = [Length, Mass, Time, Current, Temperature, Amount, Intensity]"
  definition "enum_all_sdim P  P Length  P Mass  P Time  P Current  P Temperature  P Amount  P Intensity"
  definition "enum_ex_sdim P  P Length  P Mass  P Time  P Current  P Temperature  P Amount  P Intensity"
  instance
    by (intro_classes, simp_all add: sdim_UNIV enum_sdim_def enum_all_sdim_def enum_ex_sdim_def)
end

instantiation sdim :: card_UNIV 
begin
  definition "finite_UNIV = Phantom(sdim) True"
  definition "card_UNIV = Phantom(sdim) 7"
  instance by (intro_classes, simp_all add: finite_UNIV_sdim_def card_UNIV_sdim_def)
end

lemma sdim_enum [simp]:
  "enum_ind Length = 0" "enum_ind Mass = 1" "enum_ind Time = 2" "enum_ind Current = 3"
  "enum_ind Temperature = 4" "enum_ind Amount = 5" "enum_ind Intensity = 6"
  by (simp_all add: enum_ind_def enum_sdim_def)

type_synonym Dimension = "(int, sdim) dimvec"

abbreviation LengthBD      ("L") where "L  mk_BaseDim Length"
abbreviation MassBD        ("M") where "M  mk_BaseDim Mass"
abbreviation TimeBD        ("T") where "T  mk_BaseDim Time"
abbreviation CurrentBD     ("I") where "I  mk_BaseDim Current"
abbreviation TemperatureBD ("Θ") where "Θ  mk_BaseDim Temperature"
abbreviation AmountBD      ("N") where "N  mk_BaseDim Amount"
abbreviation IntensityBD   ("J") where "J  mk_BaseDim Intensity"

abbreviation "BaseDimensions  {L, M, T, I, Θ, N, J}"

lemma BD_mk_dimvec [si_def]: 
  "L = mk_dimvec [1, 0, 0, 0, 0, 0, 0]"
  "M = mk_dimvec [0, 1, 0, 0, 0, 0, 0]"
  "T = mk_dimvec [0, 0, 1, 0, 0, 0, 0]"
  "I = mk_dimvec [0, 0, 0, 1, 0, 0, 0]"
  "Θ = mk_dimvec [0, 0, 0, 0, 1, 0, 0]"
  "N = mk_dimvec [0, 0, 0, 0, 0, 1, 0]"
  "J = mk_dimvec [0, 0, 0, 0, 0, 0, 1]"
  by (simp_all add: mk_BaseDim_code eval_nat_numeral)

text ‹ The following lemma confirms that there are indeed seven unique base dimensions. ›

lemma seven_BaseDimensions: "card BaseDimensions = 7"
  by simp

text ‹ We can use the base dimensions and algebra to form dimension expressions. Some examples
  are shown below. ›

term "LMT-2"
term "ML-3"

value "LMT-2"

lemma "LMT-2 = mk_dimvec [1, 1, - 2, 0, 0, 0, 0]"
  by (simp add: si_def)

subsection ‹ Dimension Type Expressions ›

subsubsection ‹ Classification ›

text ‹ We provide a syntax for dimension type expressions, which allows representation of 
  dimensions as types in Isabelle. This will allow us to represent quantities that are parametrised 
  by a particular dimension type. We first must characterise the subclass of types that represent a 
  dimension.

  The mechanism in Isabelle to characterize a certain subclass of Isabelle type expressions
  are ‹type classes›. The following type class is used to link particular Isabelle types
  to an instance of the type typ‹Dimension›. It requires that any such type has the cardinality
  term1, since a dimension type is used only to mark a quantity.
  ›

class dim_type = unitary +
  fixes   dim_ty_sem :: "'a itself  Dimension"

syntax
  "_QD" :: "type  logic" ("QD'(_')")

translations
  "QD('a)" == "CONST dim_ty_sem TYPE('a)"

text ‹ The notation termQD('a::dim_type) allows to obtain the dimension of a dimension type
  typ'a. 

  The subset of basic dimension types can be characterized by the following type class: ›

class basedim_type = dim_type +
  assumes is_BaseDim: "is_BaseDim QD('a)"

subsubsection ‹ Base Dimension Type Expressions ›

text ‹ The definition of the basic dimension type constructors is straightforward via a
  one-elementary set, typ‹unit set›. The latter is adequate since we need just an abstract syntax 
  for type expressions, so just one value for the ‹dimension›-type symbols. We define types for
  each of the seven base dimensions, and also for dimensionless quantities. ›

typedef Length      = "UNIV :: unit set" .. setup_lifting type_definition_Length
typedef Mass        = "UNIV :: unit set" .. setup_lifting type_definition_Mass
typedef Time        = "UNIV :: unit set" .. setup_lifting type_definition_Time
typedef Current     = "UNIV :: unit set" .. setup_lifting type_definition_Current
typedef Temperature = "UNIV :: unit set" .. setup_lifting type_definition_Temperature
typedef Amount      = "UNIV :: unit set" .. setup_lifting type_definition_Amount
typedef Intensity   = "UNIV :: unit set" .. setup_lifting type_definition_Intensity
typedef NoDimension = "UNIV :: unit set" .. setup_lifting type_definition_NoDimension

type_synonym M = Mass
type_synonym L = Length
type_synonym T = Time
type_synonym I = Current
type_synonym Θ = Temperature
type_synonym N = Amount
type_synonym J = Intensity
type_notation NoDimension ("𝟭")

translations
  (type) "M" <= (type) "Mass"
  (type) "L" <= (type) "Length"
  (type) "T" <= (type) "Time"
  (type) "I" <= (type) "Current"
  (type) "Θ" <= (type) "Temperature"
  (type) "N" <= (type) "Amount"
  (type) "J" <= (type) "Intensity"

text‹ Next, we embed the base dimensions into the dimension type expressions by instantiating the 
  class class‹basedim_type› with each of the base dimension types. ›

instantiation Length :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Length (_::Length itself) = L"
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def, (transfer, simp)+)
end

instantiation Mass :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Mass (_::Mass itself) = M"
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def, (transfer, simp)+)
end

instantiation Time :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Time (_::Time itself) = T"
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def, (transfer, simp)+)
end

instantiation Current :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Current (_::Current itself) = I"
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def, (transfer, simp)+)
end

instantiation Temperature :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Temperature (_::Temperature itself) = Θ"
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def, (transfer, simp)+)
end

instantiation Amount :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Amount (_::Amount itself) = N"
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def, (transfer, simp)+)
end   

instantiation Intensity :: basedim_type
begin
definition [si_eq]: "dim_ty_sem_Intensity (_::Intensity itself) = J"
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def, (transfer, simp)+)
end

instantiation NoDimension :: dim_type
begin
definition [si_eq]: "dim_ty_sem_NoDimension (_::NoDimension itself) = (1::Dimension)"
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def, (transfer, simp)+)
end

lemma base_dimension_types [simp]: 
  "is_BaseDim QD(Length)" "is_BaseDim QD(Mass)" "is_BaseDim QD(Time)" "is_BaseDim QD(Current)" 
  "is_BaseDim QD(Temperature)" "is_BaseDim QD(Amount)" "is_BaseDim QD(Intensity)" 
  by (simp_all add: is_BaseDim)

subsubsection ‹ Dimension Type Constructors: Inner Product and Inverse ›

text‹ Dimension type expressions can be constructed by multiplication and division of the base
  dimension types above. Consequently, we need to define multiplication and inverse operators
  at the type level as well. On the class of dimension types (in which we have already inserted 
  the base dimension types), the definitions of the type constructors for inner product and inverse is 
  straightforward. ›

typedef ('a::dim_type, 'b::dim_type) DimTimes (infixl "" 69) = "UNIV :: unit set" ..
setup_lifting type_definition_DimTimes

text ‹ The type typ('a,'b) DimTimes› is parameterised by two types, typ'a and typ'b that must
  both be elements of the class‹dim_type› class. As with the base dimensions, it is a unitary type
  as its purpose is to represent dimension type expressions. We instantiate class‹dim_type› with
  this type, where the semantics of a product dimension expression is the product of the underlying
  dimensions. This means that multiplication of two dimension types yields a dimension type. ›

instantiation DimTimes :: (dim_type, dim_type) dim_type
begin
  definition dim_ty_sem_DimTimes :: "('a  'b) itself  Dimension" where
  [si_eq]: "dim_ty_sem_DimTimes x = QD('a) * QD('b)"
  instance by (intro_classes, simp_all add: dim_ty_sem_DimTimes_def, (transfer, simp)+)
end

text ‹ Similarly, we define inversion of dimension types and prove that dimension types are 
  closed under this. ›

typedef 'a DimInv ("(_-1)" [999] 999) = "UNIV :: unit set" ..
setup_lifting type_definition_DimInv
instantiation DimInv :: (dim_type) dim_type
begin
  definition dim_ty_sem_DimInv :: "('a-1) itself  Dimension" where
  [si_eq]: "dim_ty_sem_DimInv x = inverse QD('a)"
  instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
end

subsubsection ‹ Dimension Type Syntax ›

text ‹ A division is expressed, as usual, by multiplication with an inverted dimension. ›

type_synonym ('a, 'b) DimDiv = "'a  ('b-1)" (infixl "'/" 69)

text ‹ A number of further type synonyms allow for more compact notation: ›

type_synonym 'a DimSquare = "'a  'a" ("(_)2" [999] 999)
type_synonym 'a DimCube = "'a  'a  'a" ("(_)3" [999] 999)
type_synonym 'a DimQuart = "'a  'a  'a  'a" ("(_)4" [999] 999)
type_synonym 'a DimInvSquare = "('a2)-1" ("(_)-2" [999] 999)
type_synonym 'a DimInvCube = "('a3)-1" ("(_)-3" [999] 999)
type_synonym 'a DimInvQuart = "('a4)-1" ("(_)-4" [999] 999)

translations (type) "'a-2" <= (type) "('a2)-1"
translations (type) "'a-3" <= (type) "('a3)-1"
translations (type) "'a-4" <= (type) "('a4)-1"

print_translation [(@{type_syntax DimTimes}, 
    fn ctx => fn [a, b] => 
      if (a = b) 
          then Const (@{type_syntax DimSquare}, dummyT) $ a
          else case a of
            Const (@{type_syntax DimTimes}, _) $ a1 $ a2 =>
              if (a1 = a2 andalso a2 = b) 
                then Const (@{type_syntax DimCube}, dummyT) $ a1 
                else case a1 of
                  Const (@{type_syntax DimTimes}, _) $ a11 $ a12 =>
                    if (a11 = a12 andalso a12 = a2 andalso a2 = b)
                      then Const (@{type_syntax DimQuart}, dummyT) $ a11
                      else raise Match |
            _ => raise Match)]

subsubsection ‹ Derived Dimension Types ›

type_synonym Area = "L2"
type_synonym Volume = "L3"
type_synonym Acceleration = "LT-1"
type_synonym Frequency = "T-1"
type_synonym Energy = "L2MT-2"
type_synonym Power = "L2MT-3"
type_synonym Force = "LMT-2"
type_synonym Pressure = "L-1MT-2"
type_synonym Charge = "IT"
type_synonym PotentialDifference = "L2MT-3I-1"
type_synonym Capacitance = "L-2M-1T4I2"

subsection ‹ ML Functions ›

text ‹ We define ML functions for converting a dimension to an integer vector, and vice-versa.
  These are useful for normalising dimension types. ›

ML signature DIMENSION_TYPE = 
sig
  val dim_to_typ: int list -> typ
  val typ_to_dim: typ -> int list
  val normalise: typ -> typ
end

structure Dimension_Type : DIMENSION_TYPE =
struct
  
  val dims = [@{typ L}, @{typ M}, @{typ T}, @{typ I}, @{typ Θ}, @{typ N}, @{typ J}];

  fun typ_to_dim (Type (@{type_name Length}, [])) = [1, 0, 0, 0, 0, 0, 0] |
      typ_to_dim (Type (@{type_name Mass}, []))   = [0, 1, 0, 0, 0, 0, 0] |
      typ_to_dim (Type (@{type_name Time}, []))   = [0, 0, 1, 0, 0, 0, 0] |
      typ_to_dim (Type (@{type_name Current}, []))   = [0, 0, 0, 1, 0, 0, 0] |
      typ_to_dim (Type (@{type_name Temperature}, []))   = [0, 0, 0, 0, 1, 0, 0] |
      typ_to_dim (Type (@{type_name Amount}, []))   = [0, 0, 0, 0, 0, 1, 0] |
      typ_to_dim (Type (@{type_name Intensity}, []))   = [0, 0, 0, 0, 0, 0, 1] |
      typ_to_dim (Type (@{type_name NoDimension}, []))   = [0, 0, 0, 0, 0, 0, 0] |
      typ_to_dim (Type (@{type_name DimInv}, [x])) = map (fn x => 0 - x) (typ_to_dim x) |
      typ_to_dim (Type (@{type_name DimTimes}, [x, y])) 
         = map (fn (x, y) => x + y) (ListPair.zip (typ_to_dim x, typ_to_dim y)) |
      typ_to_dim _ = raise Match;

  fun DimPow 0 _ = Type (@{type_name NoDimension}, []) |
      DimPow 1 t = t |
      DimPow n t = (if (n > 0) then Type (@{type_name DimTimes}, [DimPow (n - 1) t, t]) 
                               else Type (@{type_name DimInv}, [DimPow (0 - n) t]));

  fun dim_to_typ ds = 
    let val dts = map (fn (n, d) => DimPow n d) (filter (fn (n, _) => n <> 0) (ListPair.zip (ds, dims)))
    in if (dts = []) then @{typ NoDimension} else
          foldl1 (fn (x, y) => Type (@{type_name DimTimes}, [x, y])) dts 
    end;

  val normalise = dim_to_typ o typ_to_dim;

end;

Dimension_Type.typ_to_dim @{typ "L-2M-1T4I2M"};
Dimension_Type.normalise @{typ "L-2M-1T4I2M"};

end

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 term0 and
  term1, 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 termx :: '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 :: "'d2 itself  'a['d1::dim_type, 's::unit_system]  'a['d2::dim_type, 's]" where
[si_def]: "QD('d1) = QD('d2)  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['d1::dim_type, 's::unit_system]"
  assumes "QD('d1) = QD('d2::dim_type)"
  shows "(coerceQuantT TYPE('d2) x) Q x"
  by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)

lemma coerceQuant_eq_iff2:
  fixes x :: "'a['d1::dim_type, 's::unit_system]"
  assumes "QD('d1) = QD('d2::dim_type)" and "y = (coerceQuantT TYPE('d2) x)"
  shows "x Q y"
  using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
 
lemma updown_eq_iff:
  fixes x :: "'a['d1::dim_type, 's::unit_system]" fixes y :: "'a['d2::dim_type, 's]"
  assumes "QD('d1) = QD('d2::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['d1::dim_type, 's::unit_system]" fixes y :: "'a['d2::dim_type, 's]"
  assumes "x Q y"
  shows "QD('d1) = QD('d2)"
  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-1, '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𝟮  uu"
abbreviation qcube       ("(_)𝟯"  [999] 999) where "u𝟯  uuu"
abbreviation qquart      ("(_)𝟰"  [999] 999) where "u𝟰  uuuu"

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 = (xU. 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

Theory ISQ_Proof

section ‹ Proof Support for Quantities ›

theory ISQ_Proof
  imports ISQ_Quantities
begin

named_theorems si_transfer

definition magQ :: "'a['u::dim_type, 's::unit_system]  'a" ("_Q") where
[si_def]: "magQ x = mag (fromQ x)"

definition dimQ :: "'a['u::dim_type, 's::unit_system]  Dimension" where
[si_def]: "dimQ x = dim (fromQ x)"

lemma quant_eq_iff_mag_eq [si_eq]:
  "x = y  xQ = yQ"
  by (auto simp add: magQ_def, transfer, simp add: eq_unit)

lemma quant_eqI [si_transfer]:
  "xQ = yQ  x = y"
  by (simp add: quant_eq_iff_mag_eq)

lemma quant_equiv_iff [si_eq]:
  fixes x :: "'a['u1::dim_type, 's::unit_system]" and y :: "'a['u2::dim_type, 's::unit_system]"
  shows "x Q y  xQ = yQ  QD('u1) = QD('u2)"
proof -
  have "t ta. (ta::'a['u2, 's]) = t  mag (fromQ ta)  mag (fromQ t)"
    by (simp add: magQ_def quant_eq_iff_mag_eq)
  then show ?thesis
    by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def)
qed

lemma quant_equivI [si_transfer]:
  fixes x :: "'a['u1::dim_type, 's::unit_system]" and y :: "'a['u2::dim_type, 's::unit_system]"
  assumes "QD('u1) = QD('u2)" "QD('u1) = QD('u2)  xQ = yQ"
  shows "x Q y"
  using assms quant_equiv_iff by blast
  
lemma quant_le_iff_magn_le [si_eq]:
  "x  y  xQ  yQ"
  by (auto simp add: magQ_def; (transfer, simp))

lemma quant_leI [si_transfer]:
  "xQ  yQ  x  y"
  by (simp add: quant_le_iff_magn_le)

lemma quant_less_iff_magn_less [si_eq]:
  "x < y  xQ < yQ"
  by (auto simp add: magQ_def; (transfer, simp))

lemma quant_lessI [si_transfer]:
  "xQ < yQ  x < y"
  by (simp add: quant_less_iff_magn_less)

lemma magQ_zero [si_eq]: "0Q = 0"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_one [si_eq]: "1Q = 1"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_plus [si_eq]: "x + yQ = xQ + yQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_minus [si_eq]: "x - yQ = xQ - yQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_uminus [si_eq]: "- xQ = - xQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_scaleQ [si_eq]: "x *Q yQ = x * yQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qtimes [si_eq]: "x  yQ = xQ  yQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qinverse [si_eq]: "x-𝟭Q = inverse xQ"
  by (simp add: magQ_def, transfer, simp)

lemma magQ_qdivivide [si_eq]: "(x::('a::field)[_,_]) / yQ = xQ / yQ"
  by (simp add: magQ_def, transfer, simp add: field_class.field_divide_inverse)

lemma magQ_numeral [si_eq]: "numeral nQ = numeral n"
  apply (induct n, simp_all add: si_def)
  apply (metis magQ_def magQ_one)
  apply (metis magQ_def magQ_plus numeral_code(2))
  apply (metis magQ_def magQ_one magQ_plus numeral_code(3))
  done

lemma magQ_coerce [si_eq]: 
  fixes q :: "'a['d1::dim_type, 's::unit_system]" and t :: "'d2::dim_type itself"
  assumes "QD('d1) = QD('d2)"
  shows "coerceQuantT t qQ = qQ"
  by (simp add: coerceQuantT_def magQ_def assms, metis assms qequiv.rep_eq updown_eq_iff)

lemma dimQ [simp]: "dimQ(x :: 'a['d::dim_type, 's::unit_system]) = QD('d)"
  by (simp add: dimQ_def, transfer, simp)

text ‹ The following tactic breaks an SI conjecture down to numeric and unit properties ›

method si_simp uses add =
  (rule_tac si_transfer; simp add: add si_eq field_simps)

text ‹ The next tactic additionally compiles the semantics of the underlying units ›

method si_calc uses add = 
  (si_simp add: add; simp add: si_def add)

lemma "QD(N  Θ  N) = QD(Θ  N2)" by (simp add: si_eq si_def)
  
end

Theory ISQ_Algebra

section ‹ Algebraic Laws ›

theory ISQ_Algebra
  imports ISQ_Proof
begin

subsection ‹ Quantity Scale ›

lemma scaleQ_add_right: "a *Q x + y = (a *Q x) + (a *Q y)"
  by (si_simp add: distrib_left)

lemma scaleQ_add_left: "a + b *Q x = (a *Q x) + (b *Q x)"
  by (si_simp add: distrib_right)

lemma scaleQ_scaleQ [simp]: "a *Q b *Q x = a  b *Q x"
  by si_simp

lemma scaleQ_one [simp]: "1 *Q x = x"
  by si_simp

lemma scaleQ_zero [simp]: "0 *Q x = 0"
  by si_simp

lemma scaleQ_inv: "-a *Q x = a *Q -x"
  by si_calc

lemma scaleQ_as_qprod: "a *Q x Q (a *Q 𝟭)  x"
  by si_simp

lemma mult_scaleQ_left [simp]: "(a *Q x)  y = a *Q x  y"
  by si_simp

lemma mult_scaleQ_right [simp]: "x  (a *Q y) = a *Q x  y"
  by si_simp

subsection ‹ Field Laws ›

lemma qtimes_commute: "x  y Q y  x"
  by si_calc

lemma qtimes_assoc: "(x  y)  z  Q  x  (y  z)"
  by (si_calc)

lemma qtimes_left_unit: "𝟭  x Q x"
  by (si_calc)

lemma qtimes_right_unit: "x  𝟭 Q x"
  by (si_calc)

text‹The following weak congruences will allow for replacing equivalences in contexts
     built from product and inverse. ›

lemma qtimes_weak_cong_left:
  assumes "x Q y"
  shows  "xz Q yz"
  using assms by si_simp

lemma qtimes_weak_cong_right:
  assumes "x Q y"
  shows  "zx Q zy"
  using assms by si_calc

lemma qinverse_weak_cong:
  assumes "x Q y"
  shows   "x-𝟭 Q y-𝟭"
  using assms by si_calc

lemma scaleQ_cong:
  assumes "y Q z"
  shows "x *Q y Q x *Q z"
  using assms by si_calc

lemma qinverse_qinverse: "x-𝟭-𝟭 Q x"
  by si_calc

lemma qinverse_nonzero_iff_nonzero: "x-𝟭 = 0  x = 0"
  by (auto, si_calc+)

lemma qinverse_qtimes: "(x  y)-𝟭 Q x-𝟭  y-𝟭"
  by (si_simp add: inverse_distrib)

lemma qinverse_qdivide: "(x / y)-𝟭 Q y / x"
  by si_simp

lemma qtimes_cancel: "x  0  x / x Q 𝟭"
  by si_calc

end

Theory ISQ_Units

section ‹ Units ›

theory ISQ_Units
  imports ISQ_Proof
begin

text ‹ Parallel to the base quantities, there are base units. In the implementation of
  the SI unit system, we fix these to be precisely those quantities that have a base dimension
  and a magnitude of term1. Consequently, a base unit corresponds to a unit in the algebraic
  sense. ›

lift_definition is_base_unit :: "'a::one['d::dim_type, 's::unit_system]  bool" 
  is "λ x. mag x = 1  is_BaseDim (dim x)" . 

definition mk_base_unit :: "'u itself  's itself  ('a::one)['u::basedim_type, 's::unit_system]" 
  where "mk_base_unit t s = 1"

syntax "_mk_base_unit" :: "type  type  logic" ("BUNIT'(_, _')")
translations "BUNIT('a, 's)" == "CONST mk_base_unit TYPE('a) TYPE('s)"

lemma mk_base_unit: "is_base_unit (mk_base_unit a s)"
  by (simp add: mk_base_unit_def si_eq, transfer, simp add: is_BaseDim)

lemma magQ_mk [si_eq]: "BUNIT('u::basedim_type, 's::unit_system)Q = 1"
  by (simp add: mk_base_unit_def magQ_def si_eq, transfer, simp)

end

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 ('s1::unit_system, 's2::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      :: "('s1::unit_system U 's2::unit_system)  rat" is cLengthF .
lift_definition MassF        :: "('s1::unit_system U 's2::unit_system)  rat" is cMassF .
lift_definition TimeF        :: "('s1::unit_system U 's2::unit_system)  rat" is cTimeF .
lift_definition CurrentF     :: "('s1::unit_system U 's2::unit_system)  rat" is cCurrentF .
lift_definition TemperatureF :: "('s1::unit_system U 's2::unit_system)  rat" is cTemperatureF .
lift_definition AmountF      :: "('s1::unit_system U 's2::unit_system)  rat" is cAmountF .
lift_definition IntensityF   :: "('s1::unit_system U 's2::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" ("idC")
is "
   cLengthF = 1
  , cMassF = 1
  , cTimeF = 1
  , cCurrentF = 1
  , cTemperatureF = 1
  , cAmountF = 1
  , cIntensityF = 1 " by simp

lift_definition convcomp :: 
  "('s2 U 's3::unit_system)  ('s1::unit_system U 's2::unit_system)  ('s1 U 's3)" (infixl "C" 55) is
"λ c1 c2.  cLengthF = cLengthF c1 * cLengthF c2, cMassF = cMassF c1 * cMassF c2
         , cTimeF = cTimeF c1 * cTimeF c2, cCurrentF = cCurrentF c1 * cCurrentF c2
         , cTemperatureF = cTemperatureF c1 * cTemperatureF c2
         , cAmountF = cAmountF c1 * cAmountF c2, cIntensityF = cIntensityF c1 * cIntensityF c2 "
  by simp

lift_definition convinv :: "('s1::unit_system U 's2::unit_system)  ('s2 U 's1)" ("invC") 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 invC c = idC"
  by (transfer, simp)

lemma inv_convcomp [simp]: "invC c C c = idC"
  by (transfer, simp)

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

lemma Conversion_comps [simp]: "LengthF (c1 C c2) = LengthF c1 * LengthF c2"
  "MassF (c1 C c2) = MassF c1 * MassF c2"
  "TimeF (c1 C c2) = TimeF c1 * TimeF c2"
  "CurrentF (c1 C c2) = CurrentF c1 * CurrentF c2"
  "TemperatureF (c1 C c2) = TemperatureF c1 * TemperatureF c2"
  "AmountF (c1 C c2) = AmountF c1 * AmountF c2"
  "IntensityF (c1 C c2) = IntensityF c1 * IntensityF c2"
  by (transfer, simp)+

subsection ‹ Conversion Functions ›

definition dconvfactor :: "('s1::unit_system U 's2::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 idC d = 1"
  by (simp add: dconvfactor_def, transfer, simp)

lemma dconvfactor_compose:
  "dconvfactor (c1 C c2) d = dconvfactor c1 d * dconvfactor c2 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 :: "('s1, 's2) Conversion  ('a::field_char_0)['d::dim_type, 's1::unit_system]  'a['d, 's2::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 qQ = of_rat (dconvfactor c (dimQ q)) * qQ"
  by (simp add: si_def, transfer, simp)

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

lemma qconv_comp: "qconv (c1 C c2) x = qconv c1 (qconv c2 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

Theory ISQ

section ‹ Meta-Theory for ISQ ›

theory ISQ
  imports ISQ_Dimensions ISQ_Quantities ISQ_Proof ISQ_Algebra ISQ_Units ISQ_Conversion
begin end

Theory SI_Units

chapter ‹ International System of Units ›

section ‹ SI Units Semantics ›

theory SI_Units
  imports ISQ
begin

text ‹ An SI unit is simply a particular kind of quantity with an SI tag. ›

typedef SI = "UNIV :: unit set" by simp

instance SI :: unit_system
  by (rule unit_system_intro[of "Abs_SI ()"], metis (full_types) Abs_SI_cases UNIV_eq_I insert_iff old.unit.exhaust)

abbreviation "SI  unit :: SI"

type_synonym ('n, 'd) SIUnitT = "('n, 'd, SI) QuantT" ("_[_]" [999,0] 999)

text ‹ We now define the seven base units. Effectively, these definitions axiomatise given names
  for the term1 elements of the base quantities. ›

abbreviation "metre     BUNIT(L, SI)"
abbreviation "kilogram  BUNIT(M, SI)"
abbreviation "ampere    BUNIT(I, SI)"
abbreviation "kelvin    BUNIT(Θ, SI)"
abbreviation "mole      BUNIT(N, SI)"
abbreviation "candela   BUNIT(J, SI)"

text ‹ The second is commonly used in unit systems other than SI. Consequently, we define it 
  polymorphically, and require that the system type instantiate a type class to use it. ›

class time_second = unit_system

instance SI :: time_second ..
              
abbreviation "second   BUNIT(T, 'a::time_second)"

text ‹Note that as a consequence of our construction, the term term‹metre› is a SI Unit constant of 
SI-type typ'a[L, SI], so a unit of dimension typ‹Length› with the magnitude of type typ'a.
A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of 
type typ‹real3. Note than when considering vectors, dimensions refer to the ‹norm› of the vector,
not to its components. ›

lemma BaseUnits: 
  "is_base_unit metre" "is_base_unit second" "is_base_unit kilogram" "is_base_unit ampere"
  "is_base_unit kelvin" "is_base_unit mole" "is_base_unit candela"
  by (simp_all add: mk_base_unit)

text ‹ The effect of the above encoding is that we can use the SI base units as synonyms for their
  corresponding dimensions at the type level. ›

type_synonym 'a metre    = "'a[Length, SI]"
type_synonym 'a second   = "'a[Time, SI]"
type_synonym 'a kilogram = "'a[Mass, SI]"
type_synonym 'a ampere   = "'a[Current, SI]"
type_synonym 'a kelvin   = "'a[Temperature, SI]"
type_synonym 'a mole     = "'a[Amount, SI]"
type_synonym 'a candela  = "'a[Intensity, SI]"

text ‹ We can therefore construct a quantity such as term5 :: rat metre›, which unambiguously 
  identifies that the unit of $5$ is metres using the type system. This works because each base
  unit it the one element. ›

subsection ‹ Example Unit Equations ›

lemma "(metre  second-𝟭)  second Q metre"
  by (si_calc)

subsection ‹ Metrification ›

class metrifiable = unit_system +
  fixes convschema :: "'a itself  ('a, SI) Conversion" ("schemaC")

instantiation SI :: metrifiable
begin
lift_definition convschema_SI :: "SI itself  (SI, SI) Conversion"
is "λ s. 
   cLengthF = 1
  , cMassF = 1
  , cTimeF = 1
  , cCurrentF = 1
  , cTemperatureF = 1
  , cAmountF = 1
  , cIntensityF = 1 " by simp
instance ..
end

abbreviation metrify :: "('a::field_char_0)['d::dim_type, 's::metrifiable]  'a['d::dim_type, SI]" where
"metrify  qconv (convschema (TYPE('s)))"

text ‹ Conversion via SI units ›

abbreviation qmconv :: 
  "'s1 itself  's2 itself
    ('a::field_char_0)['d::dim_type, 's1::metrifiable] 
    'a['d::dim_type, 's2::metrifiable]" where
"qmconv s1 s2 x  qconv (invC (schemaC s2) C schemaC s1) x"

syntax
  "_qmconv" :: "type  type  logic" ("QMC'(_  _')")

translations
  "QMC('s1  's2)" == "CONST qmconv TYPE('s1) TYPE('s2)"

lemma qmconv_self: "QMC('s::metrifiable  's) = id"
  by (simp add: fun_eq_iff)

end

Theory CGS

section ‹ Centimetre-Gram-Second System ›

theory CGS
  imports SI_Units
begin

subsection ‹ Preliminaries ›

typedef CGS = "UNIV :: unit set" ..
instance CGS :: unit_system
  by (rule unit_system_intro[of "Abs_CGS ()"], metis (full_types) 
           Abs_CGS_cases UNIV_eq_I insert_iff old.unit.exhaust)
instance CGS :: time_second ..
abbreviation "CGS  unit :: CGS"

subsection ‹ Base Units ›

abbreviation "centimetre   BUNIT(L, CGS)"
abbreviation "gram         BUNIT(M, CGS)"

subsection ‹ Conversion to SI ›

instantiation CGS :: metrifiable
begin

lift_definition convschema_CGS :: "CGS itself  (CGS, SI) Conversion" is
"λ x.  cLengthF = 0.01, cMassF = 0.001, cTimeF = 1
      , cCurrentF = 1, cTemperatureF = 1, cAmountF = 1, cIntensityF = 1 " by simp

instance ..
end

lemma CGS_SI_simps [simp]: "LengthF (convschema (a::CGS itself)) = 0.01" "MassF (convschema a) = 0.001"
  "TimeF (convschema a) = 1" "CurrentF (convschema a) = 1" "TemperatureF (convschema a) = 1"
  by (transfer, simp)+

subsection ‹ Conversion Examples ›

lemma "metrify ((100::rat) *Q centimetre) = 1 *Q metre"
  by (si_simp)

end

Theory SI_Constants

section ‹ Physical Constants ›

theory SI_Constants
  imports SI_Units
begin

subsection ‹ Core Derived Units ›

abbreviation (input) "hertz  second-𝟭"

abbreviation "radian  metre  metre-𝟭"

abbreviation "steradian  metre𝟮  metre-𝟮"

abbreviation "joule  kilogram  metre𝟮   second-𝟮"

type_synonym 'a joule = "'a[M  L2  T-2, SI]"

abbreviation "watt  kilogram  metre𝟮  second-𝟯"

type_synonym 'a watt = "'a[M  L2  T-3, SI]"

abbreviation "coulomb  ampere  second"

type_synonym 'a coulomb = "'a[I  T, SI]"

abbreviation "lumen  candela  steradian"

type_synonym 'a lumen = "'a[J  (L2  L-2), SI]"

subsection ‹ Constants ›

text ‹ The most general types we support must form a field into which the natural numbers can 
  be injected. ›

default_sort field_char_0

text ‹ Hyperfine transition frequency of frequency of Cs ›

abbreviation caesium_frequency:: "'a[T-1,SI]" ("ΔvCs") where
  "caesium_frequency  9192631770 *Q hertz"

text ‹ Speed of light in vacuum ›

abbreviation speed_of_light :: "'a[L  T-1,SI]" ("c") where
  "speed_of_light  299792458 *Q (metresecond-𝟭)"

text ‹ Planck constant ›

abbreviation Planck :: "'a[M  L2  T-2  T,SI]" ("h") where
  "Planck  (6.62607015  1/(10^34)) *Q (joulesecond)"

text ‹ Elementary charge ›

abbreviation elementary_charge :: "'a[I  T,SI]" ("e") where
  "elementary_charge  (1.602176634  1/(10^19)) *Q coulomb"

text ‹ The Boltzmann constant ›

abbreviation Boltzmann :: "'a[M  L2  T-2  Θ-1,SI]" ("k") where
  "Boltzmann  (1.3806491/(10^23)) *Q (joule / kelvin)"

text ‹ The Avogadro number ›

abbreviation Avogadro :: "'a[N-1,SI]" ("NA") where
"Avogadro  6.02214076(10^23) *Q (mole-𝟭)"

abbreviation max_luminous_frequency :: "'a[T-1,SI]" where
"max_luminous_frequency  (54010^12) *Q hertz"

text ‹ The luminous efficacy of monochromatic radiation of frequency const‹max_luminous_frequency›. ›

abbreviation luminous_efficacy :: "'a[J  (L2  L-2)  (M  L2  T-3)-1,SI]" ("Kcd") where
"luminous_efficacy  683 *Q (lumen/watt)"

subsection ‹ Checking Foundational Equations of the SI System ›

theorem second_definition: 
  "1 *Q second Q (9192631770 *Q 𝟭) / ΔvCs"
  by si_calc

theorem metre_definition: 
  "1 *Q metre Q (c / (299792458 *Q 𝟭))second"
  "1 *Q metre Q (9192631770 / 299792458) *Q (c / ΔvCs)"
  by si_calc+

theorem kilogram_definition:
  "((1 *Q kilogram)::'a kilogram) Q (h / (6.62607015  1/(10^34) *Q 𝟭))metre-𝟮second" 
  by si_calc


abbreviation "approx_ice_point  273.15 *Q kelvin"

default_sort type

end

Theory SI_Prefix

section ‹ SI Prefixes ›

theory SI_Prefix
  imports SI_Constants
begin

subsection ‹ Definitions ›

text ‹ Prefixes are simply numbers that can be composed with units using the scalar 
  multiplication operator const‹scaleQ›. ›

default_sort ring_char_0

definition deca :: "'a" where [si_eq]: "deca = 10^1"

definition hecto :: "'a" where [si_eq]: "hecto = 10^2"

definition kilo :: "'a" where [si_eq]: "kilo = 10^3"

definition mega :: "'a" where [si_eq]: "mega = 10^6"

definition giga :: "'a" where [si_eq]: "giga = 10^9"

definition tera :: "'a" where [si_eq]: "tera = 10^12"

definition peta :: "'a" where [si_eq]: "peta = 10^15"

definition exa :: "'a" where [si_eq]: "exa = 10^18"

definition zetta :: "'a" where [si_eq]: "zetta = 10^21"

definition yotta :: "'a" where [si_eq]: "yotta = 10^24"

default_sort field_char_0

definition deci :: "'a" where [si_eq]: "deci = 1/10^1"

definition centi :: "'a" where [si_eq]: "centi = 1/10^2"

definition milli :: "'a" where [si_eq]: "milli = 1/10^3"

definition micro :: "'a" where [si_eq]: "micro = 1/10^6"

definition nano :: "'a" where [si_eq]: "nano = 1/10^9"

definition pico :: "'a" where [si_eq]: "pico = 1/10^12"

definition femto :: "'a" where [si_eq]: "femto = 1/10^15"

definition atto :: "'a" where [si_eq]: "atto = 1/10^18"

definition zepto :: "'a" where [si_eq]: "zepto = 1/10^21"

definition yocto :: "'a" where [si_eq]: "yocto = 1/10^24"

subsection ‹ Examples ›

lemma "2.3 *Q (centi *Q metre)𝟯 = 2.3  1/10^6 *Q metre𝟯"
  by (si_simp)

lemma "1 *Q (centi *Q metre)-𝟭 = 100 *Q metre-𝟭"
  by (si_simp)

subsection ‹ Binary Prefixes ›

text ‹ Although not in general applicable to physical quantities, we include these prefixes
  for completeness. ›

default_sort ring_char_0

definition kibi :: "'a" where [si_eq]: "kibi = 2^10"

definition mebi :: "'a" where [si_eq]: "mebi = 2^20"

definition gibi :: "'a" where [si_eq]: "gibi = 2^30"

definition tebi :: "'a" where [si_eq]: "tebi = 2^40"

definition pebi :: "'a" where [si_eq]: "pebi = 2^50"

definition exbi :: "'a" where [si_eq]: "exbi = 2^60"

definition zebi :: "'a" where [si_eq]: "zebi = 2^70"

definition yobi :: "'a" where [si_eq]: "yobi = 2^80"

default_sort type

end

Theory SI_Derived

section ‹ Derived SI-Units›

theory SI_Derived
  imports SI_Prefix
begin                                  

subsection ‹ Definitions ›

abbreviation "newton  kilogram  metre  second-𝟮"

type_synonym 'a newton = "'a[M  L  T-2, SI]"

abbreviation "pascal  kilogram  metre-𝟭  second-𝟮"

type_synonym 'a pascal = "'a[M  L-1  T-2, SI]"

abbreviation "volt  kilogram  metre𝟮  second-𝟯  ampere-𝟭"

type_synonym 'a volt = "'a[M  L2  T-3  I-1, SI]"

abbreviation "farad  kilogram-𝟭  metre-𝟮  second𝟰  ampere𝟮"

type_synonym 'a farad = "'a[M-1  L-2  T4  I2, SI]"

abbreviation "ohm  kilogram  metre𝟮  second-𝟯  ampere-𝟮"

type_synonym 'a ohm = "'a[M  L2  T-3  I-2, SI]"

abbreviation "siemens  kilogram-𝟭  metre-𝟮  second𝟯  ampere𝟮"

abbreviation "weber  kilogram  metre𝟮  second-𝟮  ampere-𝟭"

abbreviation "tesla  kilogram  second-𝟮  ampere-𝟭"

abbreviation "henry  kilogram  metre𝟮  second-𝟮  ampere-𝟮"

abbreviation "lux  candela  steradian  metre-𝟮"

abbreviation (input) "becquerel  second-𝟭"

abbreviation "gray  metre𝟮  second-𝟮"

abbreviation "sievert  metre𝟮  second-𝟮"

abbreviation "katal  mole  second-𝟭"

definition degrees_celcius :: "'a::field_char_0  'a[Θ]" ("_°C" [999] 999) 
  where [si_eq]: "degrees_celcius x = (x *Q kelvin) + approx_ice_point"

definition [si_eq]: "gram = milli *Q kilogram"

subsection ‹ Equivalences ›

lemma joule_alt_def: "joule Q newton  metre" 
  by si_calc

lemma watt_alt_def: "watt Q joule / second"
  by si_calc

lemma volt_alt_def: "volt = watt / ampere"
  by simp
  
lemma farad_alt_def: "farad Q coulomb / volt"
  by si_calc

lemma ohm_alt_def: "ohm Q volt / ampere"
  by si_calc

lemma siemens_alt_def: "siemens Q ampere / volt"
  by si_calc

lemma weber_alt_def: "weber Q volt  second"
  by si_calc

lemma tesla_alt_def: "tesla Q weber / metre𝟮"
  by si_calc

lemma henry_alt_def: "henry Q weber / ampere"
  by si_calc

lemma lux_alt_def: "lux = lumen / metre𝟮"
  by simp

lemma gray_alt_def: "gray Q joule / kilogram"
  by si_calc

lemma sievert_alt_def: "sievert Q joule / kilogram"
  by si_calc

subsection ‹ Properties ›

lemma kilogram: "kilo *Q gram = kilogram"
  by (si_simp)

lemma celcius_to_kelvin: "T°C = (T *Q kelvin) + (273.15 *Q kelvin)"
  by (si_simp)

end

Theory SI_Accepted

section ‹ Non-SI Units Accepted for SI use ›

theory SI_Accepted
  imports SI_Derived
begin

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

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

definition [si_def, si_eq]: "day = 24 *Q hour"

definition [si_def, si_eq]: "astronomical_unit = 149597870700 *Q metre"

definition degree :: "'a::real_field[L/L]" where
[si_def, si_eq]: "degree = (2(of_real pi) / 180) *Q radian"

abbreviation degrees ("_°" [999] 999) where "n°  n *Q degree"

definition [si_def, si_eq]: "litre = 1/1000 *Q metre𝟯"

definition [si_def, si_eq]: "tonne = 10^3 *Q kilogram"

definition [si_def, si_eq]: "dalton = 1.66053906660 * (1 / 10^27) *Q kilogram"

subsection ‹ Example Unit Equations ›

lemma "1 *Q hour = 3600 *Q second"
  by (si_simp)

lemma "watt  hour Q 3600 *Q joule"   by (si_calc)

lemma "25 *Q metre / second = 90 *Q (kilo *Q metre) / hour"
  by (si_calc)

end

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

Theory SI

section ‹ Meta-Theory for SI Units ›

theory SI
  imports SI_Units SI_Constants SI_Prefix SI_Derived SI_Accepted SI_Imperial
begin end

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-1  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_yearQ = c  julian_yearQ"
  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 = "real3[L]  (real3[L  T-2])"

end

Theory SI_Pretty

section ‹ Parsing and Pretty Printing of SI Units ›

theory SI_Pretty
  imports SI
begin

subsection ‹ Syntactic SI Units ›

text ‹ The following syntactic representation can apply at both the type and value level. ›

nonterminal si

syntax
  "_si_metre"    :: "si" ("m")
  "_si_kilogram" :: "si" ("kg")
  "_si_second"   :: "si" ("s")
  "_si_ampere"   :: "si" ("A")
  "_si_kelvin"   :: "si" ("K")
  "_si_mole"     :: "si" ("mol")
  "_si_candela"  :: "si" ("cd")

  "_si_square"      :: "si  si" ("(_)2" [999] 999)
  "_si_cube"        :: "si  si" ("(_)3" [999] 999)
  "_si_quart"       :: "si  si" ("(_)4" [999] 999)

  "_si_inverse"     :: "si  si" ("(_-1)" [999] 999)
  "_si_invsquare"   :: "si  si" ("(_)-2" [999] 999)
  "_si_invcube"     :: "si  si" ("(_)-3" [999] 999)
  "_si_invquart"    :: "si  si" ("(_)-4" [999] 999)

  "_si_times"    :: "si  si  si" (infixl "" 70)

subsection ‹ Type Notation ›

text ‹ Pretty notation for SI units at the type level. ›

no_type_notation SIUnitT ("_[_]" [999,0] 999)

syntax
  "_si_unit"        :: "type  si  type" ("_[_]" [999,0] 999)
  "_si_print"       :: "type  si" ("SIPRINT'(_')")

translations
  (type) "'a[SIPRINT('d)]" == (type) "'a['d, SI]"
  (si) "SIPRINT('d)2" == (si) "SIPRINT('d2)"
  (si) "SIPRINT('d)3" == (si) "SIPRINT('d3)"
  (si) "SIPRINT('d)4" == (si) "SIPRINT('d4)"
  (si) "SIPRINT('d)-1" == (si) "SIPRINT('d-1)"
  (si) "SIPRINT('d)-2" == (si) "SIPRINT('d-2)"
  (si) "SIPRINT('d)-3" == (si) "SIPRINT('d-3)"
  (si) "SIPRINT('d)-4" == (si) "SIPRINT('d-4)"
  (si) "SIPRINT('d1)  SIPRINT('d2)" == (si) "SIPRINT('d1  'd2)"
  (si) "m"   == (si) "SIPRINT(L)"
  (si) "kg"  == (si) "SIPRINT(M)"
  (si) "s"   == (si) "SIPRINT(T)"
  (si) "A"   == (si) "SIPRINT(I)"
  (si) "K"   == (si) "SIPRINT(Θ)"
  (si) "mol" == (si) "SIPRINT(N)"
  (si) "cd"  == (si) "SIPRINT(J)"

  "_si_invsquare x" <= "_si_inverse (_si_square x)"
  "_si_invcube x" <= "_si_inverse (_si_cube x)"
  "_si_invquart x" <= "_si_inverse (_si_quart x)"

  "_si_invsquare x" <= "_si_square (_si_inverse x)"
  "_si_invcube x" <= "_si_cube (_si_inverse  x)"
  "_si_invquart x" <= "_si_quart (_si_inverse x)"

typ "real[ms-2]"
typ "real[ms-2A2]"
term "5 *Q joule"

subsection ‹ Value Notations ›

text ‹ Pretty notation for SI units at the type level. Currently, it is not possible to support
  prefixes, as this would require a more sophisticated cartouche parser. ›

definition "SIQ n u = n *Q u"

syntax
  "_si_term"        :: "si  logic" ("SI'(_')")
  "_siq_term"       :: "logic  si  logic" ("SI[_, _]")
  "_siq_print"      :: "logic  si"

translations
  "_siq_term n u" => "CONST SIQ n (_si_term u)"
  "_siq_term n (_siq_print u)" <= "CONST SIQ n u"
  "_si_term (_si_times x y)" == "(_si_term x)  (_si_term y)"
  "_si_term (_si_inverse x)" == "(_si_term x)-𝟭"
  "_si_term (_si_square x)" == "(_si_term x)𝟮"
  "_si_term (_si_cube x)" == "(_si_term x)𝟮"
  "SI(m)"   => "CONST metre"
  "SI(kg)"  => "CONST kilogram"
  "SI(s)"   => "CONST second"
  "SI(A)"   => "CONST ampere"
  "SI(K)"   => "CONST kelvin"
  "SI(mol)" => "CONST mole"
  "SI(cd)"  => "CONST candela"

  "_si_inverse (_siq_print x)" <= "_siq_print (x-𝟭)"
  "_si_invsquare (_siq_print x)" <= "_siq_print (x-𝟮)"
  "_si_invcube (_siq_print x)" <= "_siq_print (x-𝟯)"
  "_si_invquart (_siq_print x)" <= "_siq_print (x-𝟰)"

  "_si_square (_siq_print x)" <= "_siq_print (x𝟮)"
  "_si_cube (_siq_print x)" <= "_siq_print (x𝟯)"
  "_si_quart (_siq_print x)" <= "_siq_print (x𝟰)"
  "_si_times (_siq_print x) (_siq_print y)" <= "_siq_print (x  y)"

  "_si_metre" <= "_siq_print (CONST metre)"
  "_si_kilogram" <= "_siq_print (CONST kilogram)"
  "_si_second" <= "_siq_print (CONST second)"
  "_si_ampere" <= "_siq_print (CONST ampere)"
  "_si_kelvin" <= "_siq_print (CONST kelvin)"
  "_si_mole" <= "_siq_print (CONST mole)"
  "_si_candela" <= "_siq_print (CONST candela)"

term "SI[5, m2]"
term "SI[22, ms-1]"

end

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