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. ›