Compare commits
2 Commits
3fa136ec72
...
1ee0a1610f
Author | SHA1 | Date |
---|---|---|
Simon Foster | 1ee0a1610f | |
Simon Foster | 75e62c7356 |
|
@ -36,4 +36,7 @@ lemma inverse_distrib: "inverse (a * b) = (inverse a) * (inverse b)"
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
abbreviation npower :: "'a::{power,inverse} \<Rightarrow> nat \<Rightarrow> 'a" ("(_\<^sup>-\<^sup>_)" [1000,999] 999)
|
||||||
|
where "npower x n \<equiv> inverse (x ^ n)"
|
||||||
|
|
||||||
end
|
end
|
|
@ -1,19 +1,47 @@
|
||||||
section \<open> SI Dimensions \<close>
|
section \<open> Dimensions \<close>
|
||||||
|
|
||||||
theory SI_Dimensions
|
theory ISQ_Dimensions
|
||||||
imports Groups_mult
|
imports Groups_mult
|
||||||
HOL.Transcendental
|
HOL.Transcendental
|
||||||
"HOL-Eisbach.Eisbach"
|
"HOL-Eisbach.Eisbach"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
subsection \<open> Preliminaries \<close>
|
||||||
|
|
||||||
named_theorems si_def and si_eq
|
named_theorems si_def and si_eq
|
||||||
|
|
||||||
section\<open>The Semantic Domain of Dimensions\<close>
|
instantiation unit :: comm_monoid_add
|
||||||
|
begin
|
||||||
|
definition "zero_unit = ()"
|
||||||
|
definition "plus_unit (x::unit) (y::unit) = ()"
|
||||||
|
instance proof qed (simp_all)
|
||||||
|
end
|
||||||
|
|
||||||
subsection \<open> The Dimension-type and its operations \<close>
|
instantiation unit :: comm_monoid_mult
|
||||||
|
begin
|
||||||
|
definition "one_unit = ()"
|
||||||
|
definition "times_unit (x::unit) (y::unit) = ()"
|
||||||
|
instance proof qed (simp_all)
|
||||||
|
end
|
||||||
|
|
||||||
text \<open> An SI unit associates with each of the seven base unit an integer that denotes the power
|
instantiation unit :: inverse
|
||||||
to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \<close>
|
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 \<open> Dimensions Semantic Domain \<close>
|
||||||
|
|
||||||
|
text \<open> 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 expressed in terms of seven base quantities, which can be combined to form
|
||||||
|
derived quantities. Consequently, a dimension associates with each of the seven base quantities an
|
||||||
|
integer that denotes the power to which it is raised. We use a record to represent this 7-tuple,
|
||||||
|
to enable code generation and thus efficient proof. \<close>
|
||||||
|
|
||||||
record Dimension =
|
record Dimension =
|
||||||
Length :: int
|
Length :: int
|
||||||
|
@ -24,7 +52,8 @@ record Dimension =
|
||||||
Amount :: int
|
Amount :: int
|
||||||
Intensity :: int
|
Intensity :: int
|
||||||
|
|
||||||
text \<open> We define a commutative monoid for SI units. \<close>
|
text \<open> Next, we define dimension multiplication, and its unit, which corresponds to a dimensionless
|
||||||
|
quantity. These are then shown to form a commutative monoid. \<close>
|
||||||
|
|
||||||
instantiation Dimension_ext :: (one) one
|
instantiation Dimension_ext :: (one) one
|
||||||
begin
|
begin
|
||||||
|
@ -58,7 +87,8 @@ proof
|
||||||
by (simp add: times_Dimension_ext_def one_Dimension_ext_def)
|
by (simp add: times_Dimension_ext_def one_Dimension_ext_def)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
text \<open> We also define the inverse and division operations, and an abelian group. \<close>
|
text \<open> We also define the inverse and division operations, and an abelian group, which will allow
|
||||||
|
us to perform dimensional analysis. \<close>
|
||||||
|
|
||||||
instantiation Dimension_ext :: ("{times,inverse}") inverse
|
instantiation Dimension_ext :: ("{times,inverse}") inverse
|
||||||
begin
|
begin
|
||||||
|
@ -84,49 +114,39 @@ proof
|
||||||
by (simp add: divide_Dimension_ext_def)
|
by (simp add: divide_Dimension_ext_def)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
text \<open> It makes no sense to define a plus operator for SI units because we can only add together
|
|
||||||
identical units, and this makes for a useless function. \<close>
|
|
||||||
|
|
||||||
instantiation unit :: comm_monoid_add
|
text \<open> A base dimension is a dimension where precisely one component has power 1: it is the
|
||||||
begin
|
dimension of a base quantity. \<close>
|
||||||
definition "zero_unit = ()"
|
|
||||||
definition "plus_unit (x::unit) (y::unit) = ()"
|
|
||||||
instance proof qed (simp_all)
|
|
||||||
end
|
|
||||||
|
|
||||||
instantiation unit :: comm_monoid_mult
|
definition LengthBD ("\<^bold>L") where [si_def]: "\<^bold>L = (1::Dimension)\<lparr>Length := 1\<rparr>"
|
||||||
begin
|
definition MassBD ("\<^bold>M") where [si_def]: "\<^bold>M = (1::Dimension)\<lparr>Mass := 1\<rparr>"
|
||||||
definition "one_unit = ()"
|
definition TimeBD ("\<^bold>T") where [si_def]: "\<^bold>T = (1::Dimension)\<lparr>Time := 1\<rparr>"
|
||||||
definition "times_unit (x::unit) (y::unit) = ()"
|
definition CurrentBD ("\<^bold>I") where [si_def]: "\<^bold>I = (1::Dimension)\<lparr>Current := 1\<rparr>"
|
||||||
instance proof qed (simp_all)
|
definition TemperatureBD ("\<^bold>\<Theta>") where [si_def]: "\<^bold>\<Theta> = (1::Dimension)\<lparr>Temperature := 1\<rparr>"
|
||||||
end
|
definition AmountBD ("\<^bold>N") where [si_def]: "\<^bold>N = (1::Dimension)\<lparr>Amount := 1\<rparr>"
|
||||||
|
definition IntensityBD ("\<^bold>J") where [si_def]: "\<^bold>J = (1::Dimension)\<lparr>Intensity := 1\<rparr>"
|
||||||
|
|
||||||
instantiation unit :: inverse
|
abbreviation "BaseDimensions \<equiv> {\<^bold>L, \<^bold>M, \<^bold>T, \<^bold>I, \<^bold>\<Theta>, \<^bold>N, \<^bold>J}"
|
||||||
begin
|
|
||||||
definition "inverse_unit (x::unit) = ()"
|
|
||||||
definition "divide_unit (x::unit) (y::unit) = ()"
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instance unit :: ab_group_mult
|
text \<open> The following lemma confirms that there are indeed seven unique base dimensions. \<close>
|
||||||
by (intro_classes, simp_all)
|
|
||||||
|
|
||||||
text \<open> A base unit is an unit where precisely one component has power 1. \<close>
|
lemma seven_BaseDimensions: "card BaseDimensions = 7"
|
||||||
|
by (simp add: si_def)
|
||||||
|
|
||||||
definition is_BaseDim :: "Dimension \<Rightarrow> bool" where
|
definition is_BaseDim :: "Dimension \<Rightarrow> bool" where [si_def]: "is_BaseDim x \<equiv> x \<in> BaseDimensions"
|
||||||
"is_BaseDim u = (\<exists> n. u = 1\<lparr>Length := n\<rparr> \<or> u = 1\<lparr>Mass := n\<rparr> \<or> u = 1\<lparr>Time := n\<rparr>
|
|
||||||
\<or> u = 1\<lparr>Current := n\<rparr> \<or> u = 1\<lparr>Temperature := n\<rparr> \<or> u = 1\<lparr>Amount := n\<rparr>
|
|
||||||
\<or> u = 1\<lparr>Intensity := n\<rparr>)"
|
|
||||||
|
|
||||||
section\<open>The Syntax and Semantics of Dimension Types\<close>
|
text \<open> We can use the base dimensions and algebra to form dimension expressions. Some examples
|
||||||
|
are shown below \<close>
|
||||||
|
|
||||||
subsection \<open> Basic Dimensions as Types (Basic SI-types)\<close>
|
term "\<^bold>L\<cdot>\<^bold>M\<cdot>\<^bold>T\<^sup>-\<^sup>2"
|
||||||
|
term "\<^bold>M\<cdot>\<^bold>L\<^sup>-\<^sup>3"
|
||||||
|
|
||||||
text \<open> We provide a syntax for type-expressions; The definition of
|
subsection \<open> Dimensions as Types \<close>
|
||||||
the basic type constructors is straight-forward via a one-elementary set.
|
|
||||||
The latter is adequate since we need just an abstract syntax for type-expressions,
|
text \<open> We provide a syntax for type expressions, which allows representation of dimensions as
|
||||||
so just one value for the \<^verbatim>\<open>dimension\<close>-type symbols.
|
types in Isabelle. The definition of the basic type constructors is straightforward via a
|
||||||
\<close>
|
one-elementary set. The latter is adequate since we need just an abstract syntax for
|
||||||
|
type expressions, so just one value for the \<^verbatim>\<open>dimension\<close>-type symbols. \<close>
|
||||||
|
|
||||||
typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length
|
typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length
|
||||||
typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass
|
typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass
|
||||||
|
@ -172,18 +192,17 @@ class dim_type = finite +
|
||||||
fixes dim_ty_sem :: "'a itself \<Rightarrow> Dimension"
|
fixes dim_ty_sem :: "'a itself \<Rightarrow> Dimension"
|
||||||
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
||||||
|
|
||||||
|
|
||||||
syntax
|
syntax
|
||||||
"_SI" :: "type \<Rightarrow> logic" ("SI'(_')")
|
"_QD" :: "type \<Rightarrow> logic" ("QD'(_')")
|
||||||
|
|
||||||
translations
|
translations
|
||||||
"SI('a)" == "CONST dim_ty_sem TYPE('a)"
|
"QD('a)" == "CONST dim_ty_sem TYPE('a)"
|
||||||
|
|
||||||
text \<open> The sub-set of basic SI type expressions can be characterized by the following
|
text \<open> The sub-set of basic SI type expressions can be characterized by the following
|
||||||
operation: \<close>
|
operation: \<close>
|
||||||
|
|
||||||
class si_basedim = dim_type +
|
class si_basedim = dim_type +
|
||||||
assumes is_BaseDim: "is_BaseDim SI('a)"
|
assumes is_BaseDim: "is_BaseDim QD('a)"
|
||||||
|
|
||||||
subsubsection \<open> SI base type constructors \<close>
|
subsubsection \<open> SI base type constructors \<close>
|
||||||
|
|
||||||
|
@ -192,49 +211,49 @@ text\<open>We embed the basic SI types into the SI type expressions: \<close>
|
||||||
instantiation Length :: si_basedim
|
instantiation Length :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Length :: "Length itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Length :: "Length itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Length x = 1\<lparr>Length := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Length x = \<^bold>L"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Mass :: si_basedim
|
instantiation Mass :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Mass :: "Mass itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Mass :: "Mass itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Mass x = 1\<lparr>Mass := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Mass x = \<^bold>M"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Time :: si_basedim
|
instantiation Time :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Time :: "Time itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Time :: "Time itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Time x = 1\<lparr>Time := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Time x = \<^bold>T"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Current :: si_basedim
|
instantiation Current :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Current :: "Current itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Current :: "Current itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Current x = 1\<lparr>Current := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Current x = \<^bold>I"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Temperature :: si_basedim
|
instantiation Temperature :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Temperature :: "Temperature itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Temperature :: "Temperature itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Temperature x = 1\<lparr>Temperature := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Temperature x = \<^bold>\<Theta>"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Amount :: si_basedim
|
instantiation Amount :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Amount :: "Amount itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Amount :: "Amount itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Amount x = 1\<lparr>Amount := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Amount x = \<^bold>N"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Intensity :: si_basedim
|
instantiation Intensity :: si_basedim
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_Intensity :: "Intensity itself \<Rightarrow> Dimension"
|
definition dim_ty_sem_Intensity :: "Intensity itself \<Rightarrow> Dimension"
|
||||||
where [si_def]: "dim_ty_sem_Intensity x = 1\<lparr>Intensity := 1\<rparr>"
|
where [si_def]: "dim_ty_sem_Intensity x = \<^bold>J"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -245,10 +264,10 @@ definition dim_ty_sem_NoDimension :: "NoDimension itself \<Rightarrow> Dimension
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
lemma base_units [simp]:
|
lemma base_dimension_types [simp]:
|
||||||
"is_BaseDim SI(Length)" "is_BaseDim SI(Mass)" "is_BaseDim SI(Time)"
|
"is_BaseDim QD(Length)" "is_BaseDim QD(Mass)" "is_BaseDim QD(Time)"
|
||||||
"is_BaseDim SI(Current)" "is_BaseDim SI(Temperature)" "is_BaseDim SI(Amount)"
|
"is_BaseDim QD(Current)" "is_BaseDim QD(Temperature)" "is_BaseDim QD(Amount)"
|
||||||
"is_BaseDim SI(Intensity)" by (simp_all add: is_BaseDim)
|
"is_BaseDim QD(Intensity)" by (simp_all add: is_BaseDim)
|
||||||
|
|
||||||
subsubsection \<open> Higher SI Type Constructors: Inner Product and Inverse \<close>
|
subsubsection \<open> Higher SI Type Constructors: Inner Product and Inverse \<close>
|
||||||
text\<open>On the class of SI-types (in which we have already inserted the base SI types),
|
text\<open>On the class of SI-types (in which we have already inserted the base SI types),
|
||||||
|
@ -262,7 +281,7 @@ text \<open> We can prove that multiplication of two dimension types yields a di
|
||||||
instantiation DimTimes :: (dim_type, dim_type) dim_type
|
instantiation DimTimes :: (dim_type, dim_type) dim_type
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_DimTimes :: "('a \<cdot> 'b) itself \<Rightarrow> Dimension" where
|
definition dim_ty_sem_DimTimes :: "('a \<cdot> 'b) itself \<Rightarrow> Dimension" where
|
||||||
[si_eq]: "dim_ty_sem_DimTimes x = SI('a) * SI('b)"
|
[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)+)
|
instance by (intro_classes, simp_all add: dim_ty_sem_DimTimes_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -274,7 +293,7 @@ setup_lifting type_definition_DimInv
|
||||||
instantiation DimInv :: (dim_type) dim_type
|
instantiation DimInv :: (dim_type) dim_type
|
||||||
begin
|
begin
|
||||||
definition dim_ty_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \<Rightarrow> Dimension" where
|
definition dim_ty_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \<Rightarrow> Dimension" where
|
||||||
[si_eq]: "dim_ty_sem_DimInv x = inverse SI('a)"
|
[si_eq]: "dim_ty_sem_DimInv x = inverse QD('a)"
|
||||||
instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
|
instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
@ -314,7 +333,7 @@ print_translation \<open>
|
||||||
_ => raise Match)]
|
_ => raise Match)]
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection \<open> Derived Dimensions \<close>
|
subsection \<open> Derived Dimension Types \<close>
|
||||||
|
|
||||||
type_synonym Area = "L\<^sup>2"
|
type_synonym Area = "L\<^sup>2"
|
||||||
type_synonym Volume = "L\<^sup>3"
|
type_synonym Volume = "L\<^sup>3"
|
|
@ -0,0 +1,265 @@
|
||||||
|
section \<open> Quantities \<close>
|
||||||
|
|
||||||
|
theory ISQ_Quantities
|
||||||
|
imports ISQ_Dimensions
|
||||||
|
begin
|
||||||
|
|
||||||
|
section \<open> The Semantic SI-Unit-Type and its Operations \<close>
|
||||||
|
|
||||||
|
record 'a Quantity =
|
||||||
|
mag :: 'a \<comment> \<open> Magnitude of the unit \<close>
|
||||||
|
dim :: Dimension \<comment> \<open> Dimension of the unit \<close>
|
||||||
|
|
||||||
|
lemma Quantity_eq_intro:
|
||||||
|
assumes "mag x = mag y" "dim x = dim y" "more x = more y"
|
||||||
|
shows "x = y"
|
||||||
|
by (simp add: assms)
|
||||||
|
|
||||||
|
instantiation Quantity_ext :: (times, times) times
|
||||||
|
begin
|
||||||
|
definition [si_def]:
|
||||||
|
"times_Quantity_ext x y = \<lparr> mag = mag x \<cdot> mag y, dim = dim x \<cdot> dim y, \<dots> = more x \<cdot> more y \<rparr>"
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
lemma mag_times [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y" by (simp add: times_Quantity_ext_def)
|
||||||
|
lemma dim_times [simp]: "dim (x \<cdot> y) = dim x \<cdot> dim y" by (simp add: times_Quantity_ext_def)
|
||||||
|
lemma more_times [simp]: "more (x \<cdot> y) = more x \<cdot> more y" by (simp add: times_Quantity_ext_def)
|
||||||
|
|
||||||
|
instantiation Quantity_ext :: (zero, zero) zero
|
||||||
|
begin
|
||||||
|
definition "zero_Quantity_ext = \<lparr> mag = 0, dim = 1, \<dots> = 0 \<rparr>"
|
||||||
|
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, one) one
|
||||||
|
begin
|
||||||
|
definition [si_def]: "one_Quantity_ext = \<lparr> mag = 1, dim = 1, \<dots> = 1 \<rparr>"
|
||||||
|
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)
|
||||||
|
|
||||||
|
instantiation Quantity_ext :: (inverse, inverse) inverse
|
||||||
|
begin
|
||||||
|
definition [si_def]:
|
||||||
|
"inverse_Quantity_ext x = \<lparr> mag = inverse (mag x), dim = inverse (dim x), \<dots> = inverse (more x) \<rparr>"
|
||||||
|
definition [si_def]:
|
||||||
|
"divide_Quantity_ext x y = \<lparr> mag = mag x / mag y, dim = dim x / dim y, \<dots> = more x / more y \<rparr>"
|
||||||
|
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)
|
||||||
|
|
||||||
|
instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
|
||||||
|
by (intro_classes, simp_all add: one_Quantity_ext_def
|
||||||
|
times_Quantity_ext_def mult.assoc, simp add: mult.commute)
|
||||||
|
|
||||||
|
instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
|
||||||
|
by (intro_classes, rule Quantity_eq_intro, simp_all)
|
||||||
|
|
||||||
|
instantiation Quantity_ext :: (ord, ord) ord
|
||||||
|
begin
|
||||||
|
definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
|
||||||
|
where "less_eq_Quantity_ext x y = (mag x \<le> mag y \<and> dim x = dim y \<and> more x \<le> more y)"
|
||||||
|
definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
|
||||||
|
where "less_Quantity_ext x y = (x \<le> y \<and> \<not> y \<le> x)"
|
||||||
|
|
||||||
|
instance ..
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
instance Quantity_ext :: (order, order) order
|
||||||
|
by (intro_classes, auto simp add: less_Quantity_ext_def less_eq_Quantity_ext_def)
|
||||||
|
|
||||||
|
section \<open> The Abstract SI-\<^theory_text>\<open>Quantity\<close>-Type and its Operations \<close>
|
||||||
|
|
||||||
|
text\<open>We 'lift' SI type expressions to SI unit type expressions as follows:\<close>
|
||||||
|
|
||||||
|
typedef (overloaded) ('n, 'u::dim_type) QuantT ("_[_]" [999,0] 999)
|
||||||
|
= "{x :: 'n Quantity. dim x = QD('u)}"
|
||||||
|
morphisms fromQ toQ by (rule_tac x="\<lparr> mag = undefined, dim = QD('u) \<rparr>" in exI, simp)
|
||||||
|
|
||||||
|
setup_lifting type_definition_QuantT
|
||||||
|
|
||||||
|
text \<open> Coerce values when their dimensions are equivalent \<close>
|
||||||
|
|
||||||
|
definition coerceQuantT :: "'u\<^sub>2 itself \<Rightarrow> 'a['u\<^sub>1::dim_type] \<Rightarrow> 'a['u\<^sub>2::dim_type]" where
|
||||||
|
"QD('u\<^sub>1) = QD('u\<^sub>2) \<Longrightarrow> coerceQuantT t x = (toQ (fromQ x))"
|
||||||
|
|
||||||
|
subsection\<open>Predicates on Abstract SI-\<^theory_text>\<open>Unit\<close>-types\<close>
|
||||||
|
|
||||||
|
text \<open> Two SI Unit types are orderable if their magnitude type is of class @{class "order"},
|
||||||
|
and have the same dimensions (not necessarily dimension types).\<close>
|
||||||
|
|
||||||
|
lift_definition qless_eq ::
|
||||||
|
"'n::order['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50) is "(\<le>)" .
|
||||||
|
|
||||||
|
|
||||||
|
text\<open> Two SI Unit types are equivalent if they have the same dimensions
|
||||||
|
(not necessarily dimension types). This equivalence the a vital point
|
||||||
|
of the overall construction of SI Units. \<close>
|
||||||
|
|
||||||
|
lift_definition qequiv ::
|
||||||
|
"'n['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50) is "(=)" .
|
||||||
|
|
||||||
|
subsection\<open>The Equivalence on Abstract SI-\<^theory_text>\<open>Unit\<close>-Types\<close>
|
||||||
|
text\<open>The latter predicate gives us an equivalence, but, unfortunately, not a congruence.\<close>
|
||||||
|
|
||||||
|
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
|
||||||
|
by (simp add: qequiv_def)
|
||||||
|
|
||||||
|
lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
|
||||||
|
by (simp add: qequiv_def)
|
||||||
|
|
||||||
|
lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
|
||||||
|
by (simp add: qequiv_def)
|
||||||
|
|
||||||
|
theorem qeq_iff_same_dim:
|
||||||
|
fixes x y :: "'a['u::dim_type]"
|
||||||
|
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
|
||||||
|
by (transfer, simp)
|
||||||
|
|
||||||
|
(* the following series of equivalent statements ... *)
|
||||||
|
|
||||||
|
lemma coerceQuant_eq_iff:
|
||||||
|
fixes x :: "'a['u\<^sub>1::dim_type]"
|
||||||
|
assumes "QD('u\<^sub>1) = QD('u\<^sub>2::dim_type)"
|
||||||
|
shows "(coerceQuantT TYPE('u\<^sub>2) x) \<cong>\<^sub>Q x"
|
||||||
|
by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)
|
||||||
|
|
||||||
|
(* or equivalently *)
|
||||||
|
|
||||||
|
lemma coerceQuant_eq_iff2:
|
||||||
|
fixes x :: "'a['u\<^sub>1::dim_type]"
|
||||||
|
assumes "QD('u\<^sub>1) = QD('u\<^sub>2::dim_type)" and "y = (coerceQuantT TYPE('u\<^sub>2) x)"
|
||||||
|
shows "x \<cong>\<^sub>Q y"
|
||||||
|
using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
|
||||||
|
|
||||||
|
lemma updown_eq_iff:
|
||||||
|
fixes x :: "'a['u\<^sub>1::dim_type]" fixes y :: "'a['u\<^sub>2::dim_type]"
|
||||||
|
assumes "QD('u\<^sub>1) = QD('u\<^sub>2::dim_type)" and "y = (toQ (fromQ x))"
|
||||||
|
shows "x \<cong>\<^sub>Q y"
|
||||||
|
by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceQuantT_def)
|
||||||
|
|
||||||
|
text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^sub>Q y\<close>, since x and y may have different type.\<close>
|
||||||
|
|
||||||
|
lemma qeq:
|
||||||
|
fixes x :: "'a['u\<^sub>1::dim_type]" fixes y :: "'a['u\<^sub>2::dim_type]"
|
||||||
|
assumes "x \<cong>\<^sub>Q y"
|
||||||
|
shows "QD('u\<^sub>1) = QD('u\<^sub>2::dim_type)"
|
||||||
|
by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)
|
||||||
|
|
||||||
|
subsection\<open>Operations on Abstract SI-Unit-Types\<close>
|
||||||
|
|
||||||
|
lift_definition
|
||||||
|
qtimes :: "('n::comm_ring_1)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
|
||||||
|
by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def)
|
||||||
|
|
||||||
|
lift_definition
|
||||||
|
qinverse :: "('n::field)['a::dim_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
|
||||||
|
by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def)
|
||||||
|
|
||||||
|
abbreviation
|
||||||
|
qdivide :: "('n::field)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
|
||||||
|
"qdivide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
|
||||||
|
|
||||||
|
abbreviation qsq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
|
||||||
|
abbreviation qcube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||||
|
abbreviation qquart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||||
|
|
||||||
|
abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
|
||||||
|
abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||||
|
abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||||
|
|
||||||
|
instantiation QuantT :: (zero,dim_type) zero
|
||||||
|
begin
|
||||||
|
lift_definition zero_QuantT :: "('a, 'b) QuantT" is "\<lparr> mag = 0, dim = QD('b) \<rparr>"
|
||||||
|
by simp
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
instantiation QuantT :: (one,dim_type) one
|
||||||
|
begin
|
||||||
|
lift_definition one_QuantT :: "('a, 'b) QuantT" is "\<lparr> mag = 1, dim = QD('b) \<rparr>"
|
||||||
|
by simp
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
instantiation QuantT :: (plus,dim_type) plus
|
||||||
|
begin
|
||||||
|
lift_definition plus_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||||
|
is "\<lambda> x y. \<lparr> mag = mag x + mag y, dim = QD('b) \<rparr>"
|
||||||
|
by (simp)
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
instance QuantT :: (semigroup_add,dim_type) semigroup_add
|
||||||
|
by (intro_classes, transfer, simp add: add.assoc)
|
||||||
|
|
||||||
|
instance QuantT :: (ab_semigroup_add,dim_type) ab_semigroup_add
|
||||||
|
by (intro_classes, transfer, simp add: add.commute)
|
||||||
|
|
||||||
|
instance QuantT :: (monoid_add,dim_type) monoid_add
|
||||||
|
by (intro_classes; (transfer, simp))
|
||||||
|
|
||||||
|
instance QuantT :: (comm_monoid_add,dim_type) comm_monoid_add
|
||||||
|
by (intro_classes; transfer, simp)
|
||||||
|
|
||||||
|
instantiation QuantT :: (uminus,dim_type) uminus
|
||||||
|
begin
|
||||||
|
lift_definition uminus_QuantT :: "'a['b] \<Rightarrow> 'a['b]"
|
||||||
|
is "\<lambda> x. \<lparr> mag = - mag x, dim = dim x \<rparr>" by (simp)
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
instantiation QuantT :: (minus,dim_type) minus
|
||||||
|
begin
|
||||||
|
lift_definition minus_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||||
|
is "\<lambda> x y. \<lparr> mag = mag x - mag y, dim = dim x \<rparr>" by (simp)
|
||||||
|
|
||||||
|
instance ..
|
||||||
|
end
|
||||||
|
|
||||||
|
instance QuantT :: (numeral,dim_type) numeral ..
|
||||||
|
|
||||||
|
instance QuantT :: (ab_group_add,dim_type) ab_group_add
|
||||||
|
by (intro_classes, (transfer, simp)+)
|
||||||
|
|
||||||
|
instantiation QuantT :: (order,dim_type) order
|
||||||
|
begin
|
||||||
|
lift_definition less_eq_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x \<le> mag y" .
|
||||||
|
lift_definition less_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x < mag y" .
|
||||||
|
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
|
||||||
|
end
|
||||||
|
|
||||||
|
text\<open>The scaling operator permits to multiply the magnitude of a unit; this scalar product
|
||||||
|
produces what is called "prefixes" in the terminology of the SI system.\<close>
|
||||||
|
lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['u::dim_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
|
||||||
|
is "\<lambda> r x. \<lparr> mag = r * mag x, dim = QD('u) \<rparr>" by simp
|
||||||
|
|
||||||
|
notation scaleQ (infixr "\<odot>" 63)
|
||||||
|
|
||||||
|
end
|
|
@ -15,7 +15,7 @@ lemma unit_eq_iff_mag_eq [si_transfer]:
|
||||||
|
|
||||||
lemma unit_equiv_iff [si_transfer]:
|
lemma unit_equiv_iff [si_transfer]:
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]"
|
fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]"
|
||||||
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> SI('u\<^sub>1) = SI('u\<^sub>2)"
|
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> QD('u\<^sub>1) = QD('u\<^sub>2)"
|
||||||
proof -
|
proof -
|
||||||
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
|
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
|
||||||
by (simp add: magQuant_def unit_eq_iff_mag_eq)
|
by (simp add: magQuant_def unit_eq_iff_mag_eq)
|
||||||
|
@ -61,7 +61,7 @@ lemma magQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n
|
||||||
apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3))
|
apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3))
|
||||||
done
|
done
|
||||||
|
|
||||||
lemma magQuant_mk [si_eq]: "\<lbrakk>UNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
|
lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
|
||||||
by (simp add: magQuant_def, transfer, simp)
|
by (simp add: magQuant_def, transfer, simp)
|
||||||
|
|
||||||
text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
|
text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
|
||||||
|
@ -89,7 +89,7 @@ lemmas [si_def] = si_sem_Length_def si_sem_Mass_def si_sem_Time_def
|
||||||
times_Unit_ext_def one_Unit_ext_def
|
times_Unit_ext_def one_Unit_ext_def
|
||||||
*)
|
*)
|
||||||
|
|
||||||
lemma "SI(N \<cdot> \<Theta> \<cdot> N) = SI(\<Theta> \<cdot> N\<^sup>2)" by (simp add: si_eq si_def)
|
lemma "QD(N \<cdot> \<Theta> \<cdot> N) = QD(\<Theta> \<cdot> N\<^sup>2)" by (simp add: si_eq si_def)
|
||||||
|
|
||||||
lemma "(meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q meter"
|
lemma "(meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q meter"
|
||||||
by (si_calc)
|
by (si_calc)
|
||||||
|
|
|
@ -1,286 +1,27 @@
|
||||||
section \<open> SI Units \<close>
|
section \<open> SI Units \<close>
|
||||||
|
|
||||||
theory SI_Units
|
theory SI_Units
|
||||||
imports SI_Dimensions
|
imports ISQ_Quantities
|
||||||
begin
|
begin
|
||||||
|
|
||||||
section \<open> The Semantic SI-Unit-Type and its Operations \<close>
|
lift_definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]"
|
||||||
|
is "\<lambda> u. \<lparr> mag = 1, dim = QD('u) \<rparr>" by simp
|
||||||
|
|
||||||
record 'a Unit =
|
syntax "_mk_base_unit" :: "type \<Rightarrow> logic" ("BUNIT'(_')")
|
||||||
mag :: 'a \<comment> \<open> Magnitude of the unit \<close>
|
translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)"
|
||||||
dim :: Dimension \<comment> \<open> Dimension of the unit \<close>
|
|
||||||
|
|
||||||
lemma Unit_eq_intro:
|
subsection \<open>Polymorphic Operations for SI Base Units \<close>
|
||||||
assumes "mag x = mag y" "dim x = dim y" "more x = more y"
|
|
||||||
shows "x = y"
|
|
||||||
by (simp add: assms)
|
|
||||||
|
|
||||||
instantiation Unit_ext :: (times, times) times
|
definition [si_eq]: "meter = BUNIT(L)"
|
||||||
begin
|
definition [si_eq]: "second = BUNIT(T)"
|
||||||
definition [si_def]:
|
definition [si_eq]: "kilogram = BUNIT(M)"
|
||||||
"times_Unit_ext x y = \<lparr> mag = mag x \<cdot> mag y, dim = dim x \<cdot> dim y, \<dots> = more x \<cdot> more y \<rparr>"
|
definition [si_eq]: "ampere = BUNIT(I)"
|
||||||
instance ..
|
definition [si_eq]: "kelvin = BUNIT(\<Theta>)"
|
||||||
end
|
definition [si_eq]: "mole = BUNIT(N)"
|
||||||
|
definition [si_eq]: "candela = BUNIT(J)"
|
||||||
lemma mag_times [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y" by (simp add: times_Unit_ext_def)
|
|
||||||
lemma dim_times [simp]: "dim (x \<cdot> y) = dim x \<cdot> dim y" by (simp add: times_Unit_ext_def)
|
|
||||||
lemma more_times [simp]: "more (x \<cdot> y) = more x \<cdot> more y" by (simp add: times_Unit_ext_def)
|
|
||||||
|
|
||||||
instantiation Unit_ext :: (zero, zero) zero
|
|
||||||
begin
|
|
||||||
definition "zero_Unit_ext = \<lparr> mag = 0, dim = 1, \<dots> = 0 \<rparr>"
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
lemma mag_zero [simp]: "mag 0 = 0" by (simp add: zero_Unit_ext_def)
|
|
||||||
lemma dim_zero [simp]: "dim 0 = 1" by (simp add: zero_Unit_ext_def)
|
|
||||||
lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Unit_ext_def)
|
|
||||||
|
|
||||||
instantiation Unit_ext :: (one, one) one
|
|
||||||
begin
|
|
||||||
definition [si_def]: "one_Unit_ext = \<lparr> mag = 1, dim = 1, \<dots> = 1 \<rparr>"
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
lemma mag_one [simp]: "mag 1 = 1" by (simp add: one_Unit_ext_def)
|
|
||||||
lemma dim_one [simp]: "dim 1 = 1" by (simp add: one_Unit_ext_def)
|
|
||||||
lemma more_one [simp]: "more 1 = 1" by (simp add: one_Unit_ext_def)
|
|
||||||
|
|
||||||
instantiation Unit_ext :: (inverse, inverse) inverse
|
|
||||||
begin
|
|
||||||
definition [si_def]:
|
|
||||||
"inverse_Unit_ext x = \<lparr> mag = inverse (mag x), dim = inverse (dim x), \<dots> = inverse (more x) \<rparr>"
|
|
||||||
definition [si_def]:
|
|
||||||
"divide_Unit_ext x y = \<lparr> mag = mag x / mag y, dim = dim x / dim y, \<dots> = more x / more y \<rparr>"
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)"
|
|
||||||
by (simp add: inverse_Unit_ext_def)
|
|
||||||
|
|
||||||
lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)"
|
|
||||||
by (simp add: inverse_Unit_ext_def)
|
|
||||||
|
|
||||||
lemma more_inverse [simp]: "more (inverse x) = inverse (more x)"
|
|
||||||
by (simp add: inverse_Unit_ext_def)
|
|
||||||
|
|
||||||
lemma mag_divide [simp]: "mag (x / y) = mag x / mag y"
|
|
||||||
by (simp add: divide_Unit_ext_def)
|
|
||||||
|
|
||||||
lemma dim_divide [simp]: "dim (x / y) = dim x / dim y"
|
|
||||||
by (simp add: divide_Unit_ext_def)
|
|
||||||
|
|
||||||
lemma more_divide [simp]: "more (x / y) = more x / more y"
|
|
||||||
by (simp add: divide_Unit_ext_def)
|
|
||||||
|
|
||||||
instance Unit_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
|
|
||||||
by (intro_classes, simp_all add: one_Unit_ext_def
|
|
||||||
times_Unit_ext_def mult.assoc, simp add: mult.commute)
|
|
||||||
|
|
||||||
instance Unit_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
|
|
||||||
by (intro_classes, rule Unit_eq_intro, simp_all)
|
|
||||||
|
|
||||||
instantiation Unit_ext :: (ord, ord) ord
|
|
||||||
begin
|
|
||||||
definition less_eq_Unit_ext :: "('a, 'b) Unit_scheme \<Rightarrow> ('a, 'b) Unit_scheme \<Rightarrow> bool"
|
|
||||||
where "less_eq_Unit_ext x y = (mag x \<le> mag y \<and> dim x = dim y \<and> more x \<le> more y)"
|
|
||||||
definition less_Unit_ext :: "('a, 'b) Unit_scheme \<Rightarrow> ('a, 'b) Unit_scheme \<Rightarrow> bool"
|
|
||||||
where "less_Unit_ext x y = (x \<le> y \<and> \<not> y \<le> x)"
|
|
||||||
|
|
||||||
instance ..
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
instance Unit_ext :: (order, order) order
|
|
||||||
by (intro_classes, auto simp add: less_Unit_ext_def less_eq_Unit_ext_def)
|
|
||||||
|
|
||||||
section \<open> The Abstract SI-\<^theory_text>\<open>Unit\<close>-Type and its Operations \<close>
|
|
||||||
|
|
||||||
text\<open>We 'lift' SI type expressions to SI unit type expressions as follows:\<close>
|
|
||||||
|
|
||||||
typedef (overloaded) ('n, 'u::dim_type) UnitT ("_[_]" [999,0] 999)
|
|
||||||
= "{x :: 'n Unit. dim x = SI('u)}"
|
|
||||||
morphisms fromQ toQ by (rule_tac x="\<lparr> mag = undefined, dim = SI('u) \<rparr>" in exI, simp)
|
|
||||||
|
|
||||||
setup_lifting type_definition_UnitT
|
|
||||||
|
|
||||||
text \<open> Coerce values when their dimensions are equivalent \<close>
|
|
||||||
|
|
||||||
definition coerceUnit :: "'u\<^sub>2 itself \<Rightarrow> 'a['u\<^sub>1::dim_type] \<Rightarrow> 'a['u\<^sub>2::dim_type]" where
|
|
||||||
"SI('u\<^sub>1) = SI('u\<^sub>2) \<Longrightarrow> coerceUnit t x = (toQ (fromQ x))"
|
|
||||||
|
|
||||||
subsection\<open>Predicates on Abstract SI-\<^theory_text>\<open>Unit\<close>-types\<close>
|
|
||||||
|
|
||||||
text \<open> Two SI Unit types are orderable if their magnitude type is of class @{class "order"},
|
|
||||||
and have the same dimensions (not necessarily dimension types).\<close>
|
|
||||||
|
|
||||||
lift_definition qless_eq ::
|
|
||||||
"'n::order['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50) is "(\<le>)" .
|
|
||||||
|
|
||||||
|
|
||||||
text\<open> Two SI Unit types are equivalent if they have the same dimensions
|
|
||||||
(not necessarily dimension types). This equivalence the a vital point
|
|
||||||
of the overall construction of SI Units. \<close>
|
|
||||||
|
|
||||||
lift_definition qequiv ::
|
|
||||||
"'n['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50) is "(=)" .
|
|
||||||
|
|
||||||
subsection\<open>The Equivalence on Abstract SI-\<^theory_text>\<open>Unit\<close>-Types\<close>
|
|
||||||
text\<open>The latter predicate gives us an equivalence, but, unfortunately, not a congruence.\<close>
|
|
||||||
|
|
||||||
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
|
|
||||||
by (simp add: qequiv_def)
|
|
||||||
|
|
||||||
lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
|
|
||||||
by (simp add: qequiv_def)
|
|
||||||
|
|
||||||
lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
|
|
||||||
by (simp add: qequiv_def)
|
|
||||||
|
|
||||||
theorem qeq_iff_same_dim:
|
|
||||||
fixes x y :: "'a['u::dim_type]"
|
|
||||||
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
|
|
||||||
by (transfer, simp)
|
|
||||||
|
|
||||||
(* the following series of equivalent statements ... *)
|
|
||||||
|
|
||||||
lemma coerceQuant_eq_iff:
|
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]"
|
|
||||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)"
|
|
||||||
shows "(coerceUnit TYPE('u\<^sub>2) x) \<cong>\<^sub>Q x"
|
|
||||||
by (metis qequiv.rep_eq assms coerceUnit_def toQ_cases toQ_inverse)
|
|
||||||
|
|
||||||
(* or equivalently *)
|
|
||||||
|
|
||||||
lemma coerceQuant_eq_iff2:
|
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]"
|
|
||||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)" and "y = (coerceUnit TYPE('u\<^sub>2) x)"
|
|
||||||
shows "x \<cong>\<^sub>Q y"
|
|
||||||
using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
|
|
||||||
|
|
||||||
lemma updown_eq_iff:
|
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]" fixes y :: "'a['u\<^sub>2::dim_type]"
|
|
||||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)" and "y = (toQ (fromQ x))"
|
|
||||||
shows "x \<cong>\<^sub>Q y"
|
|
||||||
by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceUnit_def)
|
|
||||||
|
|
||||||
text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^sub>Q y\<close>, since x and y may have different type.\<close>
|
|
||||||
|
|
||||||
lemma qeq:
|
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]" fixes y :: "'a['u\<^sub>2::dim_type]"
|
|
||||||
assumes "x \<cong>\<^sub>Q y"
|
|
||||||
shows "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)"
|
|
||||||
by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)
|
|
||||||
|
|
||||||
subsection\<open>Operations on Abstract SI-Unit-Types\<close>
|
|
||||||
|
|
||||||
lift_definition
|
|
||||||
qtimes :: "('n::comm_ring_1)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
|
|
||||||
by (simp add: dim_ty_sem_DimTimes_def times_Unit_ext_def)
|
|
||||||
|
|
||||||
lift_definition
|
|
||||||
qinverse :: "('n::field)['a::dim_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
|
|
||||||
by (simp add: inverse_Unit_ext_def dim_ty_sem_DimInv_def)
|
|
||||||
|
|
||||||
abbreviation
|
|
||||||
qdivide :: "('n::field)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
|
|
||||||
"qdivide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
|
|
||||||
|
|
||||||
abbreviation qsq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
|
|
||||||
abbreviation qcube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
|
||||||
abbreviation qquart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
|
||||||
|
|
||||||
abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
|
|
||||||
abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
|
||||||
abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
|
||||||
|
|
||||||
instantiation UnitT :: (zero,dim_type) zero
|
|
||||||
begin
|
|
||||||
lift_definition zero_UnitT :: "('a, 'b) UnitT" is "\<lparr> mag = 0, dim = SI('b) \<rparr>"
|
|
||||||
by simp
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instantiation UnitT :: (one,dim_type) one
|
|
||||||
begin
|
|
||||||
lift_definition one_UnitT :: "('a, 'b) UnitT" is "\<lparr> mag = 1, dim = SI('b) \<rparr>"
|
|
||||||
by simp
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instantiation UnitT :: (plus,dim_type) plus
|
|
||||||
begin
|
|
||||||
lift_definition plus_UnitT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
|
||||||
is "\<lambda> x y. \<lparr> mag = mag x + mag y, dim = SI('b) \<rparr>"
|
|
||||||
by (simp)
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instance UnitT :: (semigroup_add,dim_type) semigroup_add
|
|
||||||
by (intro_classes, transfer, simp add: add.assoc)
|
|
||||||
|
|
||||||
instance UnitT :: (ab_semigroup_add,dim_type) ab_semigroup_add
|
|
||||||
by (intro_classes, transfer, simp add: add.commute)
|
|
||||||
|
|
||||||
instance UnitT :: (monoid_add,dim_type) monoid_add
|
|
||||||
by (intro_classes; (transfer, simp))
|
|
||||||
|
|
||||||
instance UnitT :: (comm_monoid_add,dim_type) comm_monoid_add
|
|
||||||
by (intro_classes; transfer, simp)
|
|
||||||
|
|
||||||
instantiation UnitT :: (uminus,dim_type) uminus
|
|
||||||
begin
|
|
||||||
lift_definition uminus_UnitT :: "'a['b] \<Rightarrow> 'a['b]"
|
|
||||||
is "\<lambda> x. \<lparr> mag = - mag x, dim = dim x \<rparr>" by (simp)
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instantiation UnitT :: (minus,dim_type) minus
|
|
||||||
begin
|
|
||||||
lift_definition minus_UnitT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
|
||||||
is "\<lambda> x y. \<lparr> mag = mag x - mag y, dim = dim x \<rparr>" by (simp)
|
|
||||||
|
|
||||||
instance ..
|
|
||||||
end
|
|
||||||
|
|
||||||
instance UnitT :: (numeral,dim_type) numeral ..
|
|
||||||
|
|
||||||
instance UnitT :: (ab_group_add,dim_type) ab_group_add
|
|
||||||
by (intro_classes, (transfer, simp)+)
|
|
||||||
|
|
||||||
instantiation UnitT :: (order,dim_type) order
|
|
||||||
begin
|
|
||||||
lift_definition less_eq_UnitT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x \<le> mag y" .
|
|
||||||
lift_definition less_UnitT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x < mag y" .
|
|
||||||
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
|
|
||||||
end
|
|
||||||
|
|
||||||
|
|
||||||
text\<open>The scaling operator permits to multiply the magnitude of a unit; this scalar product
|
|
||||||
produces what is called "prefixes" in the terminology of the SI system.\<close>
|
|
||||||
lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['u::dim_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
|
|
||||||
is "\<lambda> r x. \<lparr> mag = r * mag x, dim = SI('u) \<rparr>" by simp
|
|
||||||
|
|
||||||
notation scaleQ (infixr "\<odot>" 63)
|
|
||||||
|
|
||||||
lift_definition mk_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]"
|
|
||||||
is "\<lambda> u. \<lparr> mag = 1, dim = SI('u) \<rparr>" by simp
|
|
||||||
|
|
||||||
syntax "_mk_unit" :: "type \<Rightarrow> logic" ("UNIT'(_')")
|
|
||||||
translations "UNIT('a)" == "CONST mk_unit TYPE('a)"
|
|
||||||
|
|
||||||
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
|
|
||||||
|
|
||||||
definition [si_eq]: "meter = UNIT(L)"
|
|
||||||
definition [si_eq]: "second = UNIT(T)"
|
|
||||||
definition [si_eq]: "kilogram = UNIT(M)"
|
|
||||||
definition [si_eq]: "ampere = UNIT(I)"
|
|
||||||
definition [si_eq]: "kelvin = UNIT(\<Theta>)"
|
|
||||||
definition [si_eq]: "mole = UNIT(N)"
|
|
||||||
definition [si_eq]: "candela = UNIT(J)"
|
|
||||||
|
|
||||||
definition dimless ("\<one>")
|
definition dimless ("\<one>")
|
||||||
where [si_eq]: "dimless = UNIT(NoDimension)"
|
where [si_eq]: "dimless = BUNIT(NoDimension)"
|
||||||
|
|
||||||
text\<open>Note that as a consequence of our construction, the term @{term meter} is a SI Unit constant of
|
text\<open>Note that as a consequence of our construction, the term @{term meter} is a SI Unit constant of
|
||||||
SI-type @{typ "'a[L]"}, so a unit of dimension @{typ "Length"} with the magnitude of type @{typ"'a"}.
|
SI-type @{typ "'a[L]"}, so a unit of dimension @{typ "Length"} with the magnitude of type @{typ"'a"}.
|
||||||
|
@ -289,4 +30,10 @@ type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer
|
||||||
not to its components.
|
not to its components.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool"
|
||||||
|
is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
|
||||||
|
|
||||||
|
lemma meter_is_BaseUnit: "is_BaseUnit meter"
|
||||||
|
by (simp add: si_eq, transfer, simp)
|
||||||
|
|
||||||
end
|
end
|
Loading…
Reference in New Issue