# 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"

lemma intpow_spos [simp]: "x > 0 ⟹ x ^⇩Z n > 0"

lemma intpow_one [simp]: "x ^⇩Z 1 = x"

lemma one_intpow [simp]: "1 ^⇩Z n = 1"

lemma intpow_plus: "x > 0 ⟹ x ^⇩Z (m + n) = x ^⇩Z m * x ^⇩Z n"
done

lemma intpow_mult_combine: "x > 0 ⟹ x ^⇩Z m * (x ^⇩Z n * y) = x ^⇩Z (m + n) * y"

lemma intpow_pos [simp]: "n ≥ 0 ⟹ x ^⇩Z n = x ^ nat n"

lemma intpow_uminus: "x ^⇩Z -n = inverse (x ^⇩Z n)"

lemma intpow_uminus_nat: "n ≥ 0 ⟹ x ^⇩Z -n = inverse (x ^ nat n)"

lemma intpow_inverse: "inverse a ^⇩Z n = inverse (a ^⇩Z n)"

lemma intpow_mult_distrib: "(x * y) ^⇩Z m = x ^⇩Z m * y ^⇩Z m"

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)
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 \<^term>‹ENUM('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)"

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
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]

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)"
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)"
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"

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

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)"

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"
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

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

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"

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"

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]"

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 "❙L⋅❙M⋅❙T⇧-⇧2"
term "❙M⋅❙L⇧-⇧3"

value "❙L⋅❙M⋅❙T⇧-⇧2"

lemma "❙L⋅❙M⋅❙T⇧-⇧2 = mk_dimvec [1, 1, - 2, 0, 0, 0, 0]"

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
\<^term>‹1›, 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 \<^term>‹QD('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)"

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) = "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)
type_synonym 'a DimCube = "'a ⋅ 'a ⋅ 'a" ("(_)⇧3"  999)
type_synonym 'a DimQuart = "'a ⋅ 'a ⋅ 'a ⋅ 'a" ("(_)⇧4"  999)
type_synonym 'a DimInvSquare = "('a⇧2)⇧-⇧1" ("(_)⇧-⇧2"  999)
type_synonym 'a DimInvCube = "('a⇧3)⇧-⇧1" ("(_)⇧-⇧3"  999)
type_synonym 'a DimInvQuart = "('a⇧4)⇧-⇧1" ("(_)⇧-⇧4"  999)

translations (type) "'a⇧-⇧2" <= (type) "('a⇧2)⇧-⇧1"
translations (type) "'a⇧-⇧3" <= (type) "('a⇧3)⇧-⇧1"
translations (type) "'a⇧-⇧4" <= (type) "('a⇧4)⇧-⇧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 = "L⇧2" type_synonym Volume = "L⇧3" type_synonym Acceleration = "L⋅T⇧-⇧1" type_synonym Frequency = "T⇧-⇧1" type_synonym Energy = "L⇧2⋅M⋅T⇧-⇧2" type_synonym Power = "L⇧2⋅M⋅T⇧-⇧3" type_synonym Force = "L⋅M⋅T⇧-⇧2" type_synonym Pressure = "L⇧-⇧1⋅M⋅T⇧-⇧2" type_synonym Charge = "I⋅T" type_synonym PotentialDifference = "L⇧2⋅M⋅T⇧-⇧3⋅I⇧-⇧1" type_synonym Capacitance = "L⇧-⇧2⋅M⇧-⇧1⋅T⇧4⋅I⇧2" 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⇧-⇧2⋅M⇧-⇧1⋅T⇧4⋅I⇧2⋅M"}; Dimension_Type.normalise @{typ "L⇧-⇧2⋅M⇧-⇧1⋅T⇧4⋅I⇧2⋅M"}; › 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 \<^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⇩2 itself ⇒ 'a['d⇩1::dim_type, 's::unit_system] ⇒ 'a['d⇩2::dim_type, 's]" where [si_def]: "QD('d⇩1) = QD('d⇩2) ⟹ 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⇩1::dim_type, 's::unit_system]" assumes "QD('d⇩1) = QD('d⇩2::dim_type)" shows "(coerceQuantT TYPE('d⇩2) x) ≅⇩Q x" by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse) lemma coerceQuant_eq_iff2: fixes x :: "'a['d⇩1::dim_type, 's::unit_system]" assumes "QD('d⇩1) = QD('d⇩2::dim_type)" and "y = (coerceQuantT TYPE('d⇩2) 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⇩1::dim_type, 's::unit_system]" fixes y :: "'a['d⇩2::dim_type, 's]" assumes "QD('d⇩1) = QD('d⇩2::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⇩1::dim_type, 's::unit_system]" fixes y :: "'a['d⇩2::dim_type, 's]" assumes "x ≅⇩Q y" shows "QD('d⇩1) = QD('d⇩2)" 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) 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) where "u⇧𝟮 ≡ u❙⋅u" abbreviation qcube ("(_)⇧𝟯"  999) where "u⇧𝟯 ≡ u❙⋅u❙⋅u" abbreviation qquart ("(_)⇧𝟰"  999) where "u⇧𝟰 ≡ u❙⋅u❙⋅u❙⋅u" abbreviation qneq_sq ("(_)⇧-⇧𝟮"  999) where "u⇧-⇧𝟮 ≡ (u⇧𝟮)⇧-⇧𝟭" abbreviation qneq_cube ("(_)⇧-⇧𝟯"  999) where "u⇧-⇧𝟯 ≡ (u⇧𝟯)⇧-⇧𝟭" abbreviation qneq_quart ("(_)⇧-⇧𝟰"  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 # 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 ⟷ ⟦x⟧⇩Q = ⟦y⟧⇩Q" by (auto simp add: magQ_def, transfer, simp add: eq_unit) lemma quant_eqI [si_transfer]: "⟦x⟧⇩Q = ⟦y⟧⇩Q ⟹ x = y" by (simp add: quant_eq_iff_mag_eq) lemma quant_equiv_iff [si_eq]: fixes x :: "'a['u⇩1::dim_type, 's::unit_system]" and y :: "'a['u⇩2::dim_type, 's::unit_system]" shows "x ≅⇩Q y ⟷ ⟦x⟧⇩Q = ⟦y⟧⇩Q ∧ QD('u⇩1) = QD('u⇩2)" proof - have "∀t ta. (ta::'a['u⇩2, '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['u⇩1::dim_type, 's::unit_system]" and y :: "'a['u⇩2::dim_type, 's::unit_system]" assumes "QD('u⇩1) = QD('u⇩2)" "QD('u⇩1) = QD('u⇩2) ⟹ ⟦x⟧⇩Q = ⟦y⟧⇩Q" shows "x ≅⇩Q y" using assms quant_equiv_iff by blast lemma quant_le_iff_magn_le [si_eq]: "x ≤ y ⟷ ⟦x⟧⇩Q ≤ ⟦y⟧⇩Q" by (auto simp add: magQ_def; (transfer, simp)) lemma quant_leI [si_transfer]: "⟦x⟧⇩Q ≤ ⟦y⟧⇩Q ⟹ x ≤ y" by (simp add: quant_le_iff_magn_le) lemma quant_less_iff_magn_less [si_eq]: "x < y ⟷ ⟦x⟧⇩Q < ⟦y⟧⇩Q" by (auto simp add: magQ_def; (transfer, simp)) lemma quant_lessI [si_transfer]: "⟦x⟧⇩Q < ⟦y⟧⇩Q ⟹ x < y" by (simp add: quant_less_iff_magn_less) lemma magQ_zero [si_eq]: "⟦0⟧⇩Q = 0" by (simp add: magQ_def, transfer, simp) lemma magQ_one [si_eq]: "⟦1⟧⇩Q = 1" by (simp add: magQ_def, transfer, simp) lemma magQ_plus [si_eq]: "⟦x + y⟧⇩Q = ⟦x⟧⇩Q + ⟦y⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_minus [si_eq]: "⟦x - y⟧⇩Q = ⟦x⟧⇩Q - ⟦y⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_uminus [si_eq]: "⟦- x⟧⇩Q = - ⟦x⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_scaleQ [si_eq]: "⟦x *⇩Q y⟧⇩Q = x * ⟦y⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_qtimes [si_eq]: "⟦x ❙⋅ y⟧⇩Q = ⟦x⟧⇩Q ⋅ ⟦y⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_qinverse [si_eq]: "⟦x⇧-⇧𝟭⟧⇩Q = inverse ⟦x⟧⇩Q" by (simp add: magQ_def, transfer, simp) lemma magQ_qdivivide [si_eq]: "⟦(x::('a::field)[_,_]) ❙/ y⟧⇩Q = ⟦x⟧⇩Q / ⟦y⟧⇩Q" by (simp add: magQ_def, transfer, simp add: field_class.field_divide_inverse) lemma magQ_numeral [si_eq]: "⟦numeral n⟧⇩Q = 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['d⇩1::dim_type, 's::unit_system]" and t :: "'d⇩2::dim_type itself" assumes "QD('d⇩1) = QD('d⇩2)" shows "⟦coerceQuantT t q⟧⇩Q = ⟦q⟧⇩Q" 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(Θ ⋅ N⇧2)" 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 "x❙⋅z ≅⇩Q y❙⋅z" using assms by si_simp lemma qtimes_weak_cong_right: assumes "x ≅⇩Q y" shows "z❙⋅x ≅⇩Q z❙⋅y" 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 \<^term>‹1›. 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 ('s⇩1::unit_system, 's⇩2::unit_system) Conversion ("(_/ ⇒⇩U _)" [1, 0] 0) = "{c :: ConvSchema. cLengthF c > 0 ∧ cMassF c > 0 ∧ cTimeF c > 0 ∧ cCurrentF c > 0 ∧ cTemperatureF c > 0 ∧ cAmountF c > 0 ∧ cIntensityF c > 0}" by (rule_tac x="⦇ cLengthF = 1, cMassF = 1, cTimeF = 1, cCurrentF = 1 , cTemperatureF = 1, cAmountF = 1, cIntensityF = 1 ⦈" in exI, simp) setup_lifting type_definition_Conversion lift_definition LengthF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cLengthF . lift_definition MassF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cMassF . lift_definition TimeF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cTimeF . lift_definition CurrentF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cCurrentF . lift_definition TemperatureF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cTemperatureF . lift_definition AmountF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cAmountF . lift_definition IntensityF :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ rat" is cIntensityF . lemma Conversion_props [simp]: "LengthF c > 0" "MassF c > 0" "TimeF c > 0" "CurrentF c > 0" "TemperatureF c > 0" "AmountF c > 0" "IntensityF c > 0" by (transfer, simp)+ subsection ‹ Conversion Algebra › lift_definition convid :: "'s::unit_system ⇒⇩U 's" ("id⇩C") is " ⦇ cLengthF = 1 , cMassF = 1 , cTimeF = 1 , cCurrentF = 1 , cTemperatureF = 1 , cAmountF = 1 , cIntensityF = 1 ⦈" by simp lift_definition convcomp :: "('s⇩2 ⇒⇩U 's⇩3::unit_system) ⇒ ('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ ('s⇩1 ⇒⇩U 's⇩3)" (infixl "∘⇩C" 55) is "λ c⇩1 c⇩2. ⦇ cLengthF = cLengthF c⇩1 * cLengthF c⇩2, cMassF = cMassF c⇩1 * cMassF c⇩2 , cTimeF = cTimeF c⇩1 * cTimeF c⇩2, cCurrentF = cCurrentF c⇩1 * cCurrentF c⇩2 , cTemperatureF = cTemperatureF c⇩1 * cTemperatureF c⇩2 , cAmountF = cAmountF c⇩1 * cAmountF c⇩2, cIntensityF = cIntensityF c⇩1 * cIntensityF c⇩2 ⦈" by simp lift_definition convinv :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ ('s⇩2 ⇒⇩U 's⇩1)" ("inv⇩C") is "λ c. ⦇ cLengthF = inverse (cLengthF c), cMassF = inverse (cMassF c), cTimeF = inverse (cTimeF c) , cCurrentF = inverse (cCurrentF c), cTemperatureF = inverse (cTemperatureF c) , cAmountF = inverse (cAmountF c), cIntensityF = inverse (cIntensityF c) ⦈" by simp lemma convinv_inverse [simp]: "convinv (convinv c) = c" by (transfer, simp) lemma convcomp_inv [simp]: "c ∘⇩C inv⇩C c = id⇩C" by (transfer, simp) lemma inv_convcomp [simp]: "inv⇩C c ∘⇩C c = id⇩C" by (transfer, simp) lemma Conversion_invs [simp]: "LengthF (inv⇩C x) = inverse (LengthF x)" "MassF (inv⇩C x) = inverse (MassF x)" "TimeF (inv⇩C x) = inverse (TimeF x)" "CurrentF (inv⇩C x) = inverse (CurrentF x)" "TemperatureF (inv⇩C x) = inverse (TemperatureF x)" "AmountF (inv⇩C x) = inverse (AmountF x)" "IntensityF (inv⇩C x) = inverse (IntensityF x)" by (transfer, simp)+ lemma Conversion_comps [simp]: "LengthF (c⇩1 ∘⇩C c⇩2) = LengthF c⇩1 * LengthF c⇩2" "MassF (c⇩1 ∘⇩C c⇩2) = MassF c⇩1 * MassF c⇩2" "TimeF (c⇩1 ∘⇩C c⇩2) = TimeF c⇩1 * TimeF c⇩2" "CurrentF (c⇩1 ∘⇩C c⇩2) = CurrentF c⇩1 * CurrentF c⇩2" "TemperatureF (c⇩1 ∘⇩C c⇩2) = TemperatureF c⇩1 * TemperatureF c⇩2" "AmountF (c⇩1 ∘⇩C c⇩2) = AmountF c⇩1 * AmountF c⇩2" "IntensityF (c⇩1 ∘⇩C c⇩2) = IntensityF c⇩1 * IntensityF c⇩2" by (transfer, simp)+ subsection ‹ Conversion Functions › definition dconvfactor :: "('s⇩1::unit_system ⇒⇩U 's⇩2::unit_system) ⇒ Dimension ⇒ rat" where "dconvfactor c d = LengthF c ^⇩Z dim_nth d Length * MassF c ^⇩Z dim_nth d Mass * TimeF c ^⇩Z dim_nth d Time * CurrentF c ^⇩Z dim_nth d Current * TemperatureF c ^⇩Z dim_nth d Temperature * AmountF c ^⇩Z dim_nth d Amount * IntensityF c ^⇩Z dim_nth d Intensity" lemma dconvfactor_pos [simp]: "dconvfactor c d > 0" by (simp add: dconvfactor_def) lemma dconvfactor_nz [simp]: "dconvfactor c d ≠ 0" by (metis dconvfactor_pos less_numeral_extra(3)) lemma dconvfactor_convinv: "dconvfactor (convinv c) d = inverse (dconvfactor c d)" by (simp add: dconvfactor_def intpow_inverse[THEN sym]) lemma dconvfactor_id [simp]: "dconvfactor id⇩C d = 1" by (simp add: dconvfactor_def, transfer, simp) lemma dconvfactor_compose: "dconvfactor (c⇩1 ∘⇩C c⇩2) d = dconvfactor c⇩1 d * dconvfactor c⇩2 d" by (simp add: dconvfactor_def, transfer, simp add: mult_ac intpow_mult_distrib) lemma dconvfactor_inverse: "dconvfactor c (inverse d) = inverse (dconvfactor c d)" by (simp add: dconvfactor_def inverse_dimvec_def intpow_uminus) lemma dconvfactor_times: "dconvfactor c (x ⋅ y) = dconvfactor c x ⋅ dconvfactor c y" by (auto simp add: dconvfactor_def mult_ac intpow_mult_combine times_dimvec_def) lift_definition qconv :: "('s⇩1, 's⇩2) Conversion ⇒ ('a::field_char_0)['d::dim_type, 's⇩1::unit_system] ⇒ 'a['d, 's⇩2::unit_system]" is "λ c q. ⦇ mag = of_rat (dconvfactor c (dim q)) * mag q, dim = dim q, unit_sys = unit ⦈" by simp lemma magQ_qconv: "⟦qconv c q⟧⇩Q = of_rat (dconvfactor c (dimQ q)) * ⟦q⟧⇩Q" by (simp add: si_def, transfer, simp) lemma qconv_id [simp]: "qconv id⇩C x = x" by (transfer', simp add: Measurement_System_eq_intro) lemma qconv_comp: "qconv (c⇩1 ∘⇩C c⇩2) x = qconv c⇩1 (qconv c⇩2 x)" by (transfer, simp add: dconvfactor_compose of_rat_mult) lemma qconv_convinv [simp]: "qconv (convinv c) (qconv c x) = x" by (transfer, simp add: dconvfactor_convinv mult.assoc[THEN sym] of_rat_mult[THEN sym] Measurement_System_eq_intro) lemma qconv_scaleQ [simp]: "qconv c (d *⇩Q x) = d *⇩Q qconv c x" by (transfer, simp) lemma qconv_plus [simp]: "qconv c (x + y) = qconv c x + qconv c y" by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs) lemma qconv_minus [simp]: "qconv c (x - y) = qconv c x - qconv c y" by (transfer, auto simp add: plus_Quantity_ext_def mult.commute ring_class.ring_distribs) lemma qconv_qmult [simp]: "qconv c (x ❙⋅ y) = qconv c x ❙⋅ qconv c y" by (transfer, simp add: times_Quantity_ext_def times_Measurement_System_ext_def dconvfactor_times of_rat_mult) lemma qconv_qinverse [simp]: "qconv c (x⇧-⇧𝟭) = (qconv c x)⇧-⇧𝟭" by (transfer, simp add: inverse_Quantity_ext_def inverse_Measurement_System_ext_def dconvfactor_inverse of_rat_inverse) lemma qconv_Length [simp]: "qconv c BUNIT(L, _) = LengthF c *⇩Q BUNIT(L, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Mass [simp]: "qconv c BUNIT(M, _) = MassF c *⇩Q BUNIT(M, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Time [simp]: "qconv c BUNIT(T, _) = TimeF c *⇩Q BUNIT(T, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Current [simp]: "qconv c BUNIT(I, _) = CurrentF c *⇩Q BUNIT(I, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Temperature [simp]: "qconv c BUNIT(Θ, _) = TemperatureF c *⇩Q BUNIT(Θ, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Amount [simp]: "qconv c BUNIT(N, _) = AmountF c *⇩Q BUNIT(N, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) lemma qconv_Intensity [simp]: "qconv c BUNIT(J, _) = IntensityF c *⇩Q BUNIT(J, _)" by (simp add: dconvfactor_def magQ_qconv si_eq mk_BaseDim_def one_dimvec_def) end # 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 \<^term>‹1› 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>‹real⇧3›. 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 \<^term>‹5 :: 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" ("schema⇩C")

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 ::
"'s⇩1 itself ⇒ 's⇩2 itself
⇒ ('a::field_char_0)['d::dim_type, 's⇩1::metrifiable]
⇒ 'a['d::dim_type, 's⇩2::metrifiable]" where
"qmconv s⇩1 s⇩2 x ≡ qconv (inv⇩C (schema⇩C s⇩2) ∘⇩C schema⇩C s⇩1) x"

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

translations
"QMC('s⇩1 → 's⇩2)" == "CONST qmconv TYPE('s⇩1) TYPE('s⇩2)"

lemma qmconv_self: "QMC('s::metrifiable → 's) = id"

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 ⋅ L⇧2 ⋅ T⇧-⇧2, SI]"

abbreviation "watt ≡ kilogram ❙⋅ metre⇧𝟮 ❙⋅ second⇧-⇧𝟯"

type_synonym 'a watt = "'a[M ⋅ L⇧2 ⋅ 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 ⋅ (L⇧2 ⋅ 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]" ("Δv⇩C⇩s") 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 (metre❙⋅second⇧-⇧𝟭)"

text ‹ Planck constant ›

abbreviation Planck :: "'a[M ⋅ L⇧2 ⋅ T⇧-⇧2 ⋅ T,SI]" ("❙h") where
"Planck ≡ (6.62607015 ⋅ 1/(10^34)) *⇩Q (joule❙⋅second)"

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 ⋅ L⇧2 ⋅ T⇧-⇧2 ⋅ Θ⇧-⇧1,SI]" ("❙k") where
"Boltzmann ≡ (1.380649⋅1/(10^23)) *⇩Q (joule ❙/ kelvin)"

text ‹ The Avogadro number ›

abbreviation Avogadro :: "'a[N⇧-⇧1,SI]" ("N⇩A") where

abbreviation max_luminous_frequency :: "'a[T⇧-⇧1,SI]" where
"max_luminous_frequency ≡ (540⋅10^12) *⇩Q hertz"

text ‹ The luminous efficacy of monochromatic radiation of frequency \<^const>‹max_luminous_frequency›. ›

abbreviation luminous_efficacy :: "'a[J ⋅ (L⇧2 ⋅ L⇧-⇧2) ⋅ (M ⋅ L⇧2 ⋅ T⇧-⇧3)⇧-⇧1,SI]" ("K⇩c⇩d") where
"luminous_efficacy ≡ 683 *⇩Q (lumen❙/watt)"

subsection ‹ Checking Foundational Equations of the SI System ›

theorem second_definition:
"1 *⇩Q second ≅⇩Q (9192631770 *⇩Q 𝟭) ❙/ Δv⇩C⇩s"
by si_calc

theorem metre_definition:
"1 *⇩Q metre ≅⇩Q (❙c ❙/ (299792458 *⇩Q 𝟭))❙⋅second"
"1 *⇩Q metre ≅⇩Q (9192631770 / 299792458) *⇩Q (❙c ❙/ Δv⇩C⇩s)"
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 ⋅ L⇧2 ⋅ T⇧-⇧3 ⋅ I⇧-⇧1, SI]"

abbreviation "farad ≡ kilogram⇧-⇧𝟭 ❙⋅ metre⇧-⇧𝟮 ❙⋅ second⇧𝟰 ❙⋅ ampere⇧𝟮"

type_synonym 'a farad = "'a[M⇧-⇧1 ⋅ L⇧-⇧2 ⋅ T⇧4 ⋅ I⇧2, SI]"

abbreviation "ohm ≡ kilogram ❙⋅ metre⇧𝟮 ❙⋅ second⇧-⇧𝟯 ❙⋅ ampere⇧-⇧𝟮"

type_synonym 'a ohm = "'a[M ⋅ L⇧2 ⋅ 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)
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

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) 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)
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_year⟧⇩Q = ⟦❙c ❙⋅ julian_year⟧⇩Q"
using light_year quant_equiv_iff by blast

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

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

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

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

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

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

type_synonym gravitation_field = "real⇧3[L] ⇒ (real⇧3[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)
"_si_cube"        :: "si ⇒ si" ("(_)⇧3"  999)
"_si_quart"       :: "si ⇒ si" ("(_)⇧4"  999)

"_si_inverse"     :: "si ⇒ si" ("(_⇧-⇧1)"  999)
"_si_invsquare"   :: "si ⇒ si" ("(_)⇧-⇧2"  999)
"_si_invcube"     :: "si ⇒ si" ("(_)⇧-⇧3"  999)
"_si_invquart"    :: "si ⇒ si" ("(_)⇧-⇧4"  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('d⇧2)"
(si) "SIPRINT('d)⇧3" == (si) "SIPRINT('d⇧3)"
(si) "SIPRINT('d)⇧4" == (si) "SIPRINT('d⇧4)"
(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('d⇩1) ⋅ SIPRINT('d⇩2)" == (si) "SIPRINT('d⇩1 ⋅ 'd⇩2)"
(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[m⋅s⇧-⇧2]"
typ "real[m⋅s⇧-⇧2⋅A⇧2]"
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, m⇧2]"
term "SI[22, m⋅s⇧-⇧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"
end