Revision of the narrative in Dimensions and Quantities
This commit is contained in:
parent
1ee0a1610f
commit
da74d4ecc4
|
|
@ -116,7 +116,7 @@ qed
|
|||
|
||||
|
||||
text \<open> A base dimension is a dimension where precisely one component has power 1: it is the
|
||||
dimension of a base quantity. \<close>
|
||||
dimension of a base quantity. Here we define the seven base dimensions. \<close>
|
||||
|
||||
definition LengthBD ("\<^bold>L") where [si_def]: "\<^bold>L = (1::Dimension)\<lparr>Length := 1\<rparr>"
|
||||
definition MassBD ("\<^bold>M") where [si_def]: "\<^bold>M = (1::Dimension)\<lparr>Mass := 1\<rparr>"
|
||||
|
|
@ -136,17 +136,50 @@ lemma seven_BaseDimensions: "card BaseDimensions = 7"
|
|||
definition is_BaseDim :: "Dimension \<Rightarrow> bool" where [si_def]: "is_BaseDim x \<equiv> x \<in> BaseDimensions"
|
||||
|
||||
text \<open> We can use the base dimensions and algebra to form dimension expressions. Some examples
|
||||
are shown below \<close>
|
||||
are shown below. \<close>
|
||||
|
||||
term "\<^bold>L\<cdot>\<^bold>M\<cdot>\<^bold>T\<^sup>-\<^sup>2"
|
||||
term "\<^bold>M\<cdot>\<^bold>L\<^sup>-\<^sup>3"
|
||||
|
||||
subsection \<open> Dimensions as Types \<close>
|
||||
subsection \<open> Dimensions Type Expressions \<close>
|
||||
|
||||
text \<open> We provide a syntax for type expressions, which allows representation of dimensions as
|
||||
types in Isabelle. The definition of the basic type constructors is straightforward via a
|
||||
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>
|
||||
subsubsection \<open> Classification \<close>
|
||||
|
||||
text \<open> 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 \<^emph>\<open>type classes\<close>. The following type class is used to link particular Isabelle types
|
||||
to an instance of the type \<^typ>\<open>Dimension\<close>. It requires that any such type has the cardinality
|
||||
\<^term>\<open>1\<close>, since a dimension type is used only to mark a quantity.
|
||||
\<close>
|
||||
|
||||
class dim_type = finite +
|
||||
fixes dim_ty_sem :: "'a itself \<Rightarrow> Dimension"
|
||||
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
||||
|
||||
syntax
|
||||
"_QD" :: "type \<Rightarrow> logic" ("QD'(_')")
|
||||
|
||||
translations
|
||||
"QD('a)" == "CONST dim_ty_sem TYPE('a)"
|
||||
|
||||
text \<open> The notation \<^term>\<open>QD('a::dim_type)\<close> allows to obtain the dimension of a dimension type
|
||||
\<^typ>\<open>'a\<close>.
|
||||
|
||||
The subset of basic dimension types can be characterized by the following type class: \<close>
|
||||
|
||||
class si_basedim = dim_type +
|
||||
assumes is_BaseDim: "is_BaseDim QD('a)"
|
||||
|
||||
subsubsection \<open> Base Dimension Type Expressions \<close>
|
||||
|
||||
text \<open> The definition of the basic dimension type constructors is straightforward via a
|
||||
one-elementary set, \<^typ>\<open>unit set\<close>. 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. We define types for
|
||||
each of the seven base dimensions, and also for dimensionless quantities. \<close>
|
||||
|
||||
typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length
|
||||
typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass
|
||||
|
|
@ -175,108 +208,78 @@ translations
|
|||
(type) "N" <= (type) "Amount"
|
||||
(type) "J" <= (type) "Intensity"
|
||||
|
||||
subsection \<open>Dimension Type Expressions and their Interpretation \<close>
|
||||
|
||||
text \<open> The case for the construction of the multiplicative and inverse operators requires ---
|
||||
thus, the unary and binary operators on our SI type language --- require that their arguments
|
||||
are restricted to the set of SI-type expressions.
|
||||
|
||||
The mechanism in Isabelle to characterize a certain sub-class of Isabelle-type expressions
|
||||
are \<^emph>\<open>type classes\<close>. We therefore need such a sub-class; for reasons of convenience,
|
||||
we combine its construction also with the "semantics" of SI types in terms of
|
||||
@{typ Dimension}. \<close>
|
||||
|
||||
subsubsection \<open> SI-type expression definition as type-class \<close>
|
||||
|
||||
class dim_type = finite +
|
||||
fixes dim_ty_sem :: "'a itself \<Rightarrow> Dimension"
|
||||
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
||||
|
||||
syntax
|
||||
"_QD" :: "type \<Rightarrow> logic" ("QD'(_')")
|
||||
|
||||
translations
|
||||
"QD('a)" == "CONST dim_ty_sem TYPE('a)"
|
||||
|
||||
text \<open> The sub-set of basic SI type expressions can be characterized by the following
|
||||
operation: \<close>
|
||||
|
||||
class si_basedim = dim_type +
|
||||
assumes is_BaseDim: "is_BaseDim QD('a)"
|
||||
|
||||
subsubsection \<open> SI base type constructors \<close>
|
||||
|
||||
text\<open>We embed the basic SI types into the SI type expressions: \<close>
|
||||
text\<open> Next, we embed the base dimensions into the dimension type expressions by instantiating the
|
||||
class \<^class>\<open>si_basedim\<close> with each of the base dimension types. \<close>
|
||||
|
||||
instantiation Length :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Length :: "Length itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Length x = \<^bold>L"
|
||||
definition [si_def]: "dim_ty_sem_Length (_::Length itself) = \<^bold>L"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Mass :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Mass :: "Mass itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Mass x = \<^bold>M"
|
||||
definition [si_def]: "dim_ty_sem_Mass (_::Mass itself) = \<^bold>M"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Time :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Time :: "Time itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Time x = \<^bold>T"
|
||||
definition [si_def]: "dim_ty_sem_Time (_::Time itself) = \<^bold>T"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Current :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Current :: "Current itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Current x = \<^bold>I"
|
||||
definition [si_def]: "dim_ty_sem_Current (_::Current itself) = \<^bold>I"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Temperature :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Temperature :: "Temperature itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Temperature x = \<^bold>\<Theta>"
|
||||
definition [si_def]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\<Theta>"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Amount :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Amount :: "Amount itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Amount x = \<^bold>N"
|
||||
definition [si_def]: "dim_ty_sem_Amount (_::Amount itself) = \<^bold>N"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Intensity :: si_basedim
|
||||
begin
|
||||
definition dim_ty_sem_Intensity :: "Intensity itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_Intensity x = \<^bold>J"
|
||||
definition [si_def]: "dim_ty_sem_Intensity (_::Intensity itself) = \<^bold>J"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation NoDimension :: dim_type
|
||||
begin
|
||||
definition dim_ty_sem_NoDimension :: "NoDimension itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "dim_ty_sem_NoDimension x = 1"
|
||||
definition [si_def]: "dim_ty_sem_NoDimension (_::NoDimension itself) = (1::Dimension)"
|
||||
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
lemma base_dimension_types [simp]:
|
||||
"is_BaseDim QD(Length)" "is_BaseDim QD(Mass)" "is_BaseDim QD(Time)"
|
||||
"is_BaseDim QD(Current)" "is_BaseDim QD(Temperature)" "is_BaseDim QD(Amount)"
|
||||
"is_BaseDim QD(Intensity)" by (simp_all add: is_BaseDim)
|
||||
"is_BaseDim QD(Length)" "is_BaseDim QD(Mass)" "is_BaseDim QD(Time)" "is_BaseDim QD(Current)"
|
||||
"is_BaseDim QD(Temperature)" "is_BaseDim QD(Amount)" "is_BaseDim QD(Intensity)"
|
||||
by (simp_all add: is_BaseDim)
|
||||
|
||||
subsubsection \<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),
|
||||
the definitions of the type constructors for inner product and inverse is straight forward.\<close>
|
||||
subsubsection \<open> Dimension Type Constructors: Inner Product and Inverse \<close>
|
||||
|
||||
text\<open> 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. \<close>
|
||||
|
||||
typedef ('a::dim_type, 'b::dim_type) DimTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_DimTimes
|
||||
|
||||
text \<open> We can prove that multiplication of two dimension types yields a dimension type. \<close>
|
||||
text \<open> The type \<^typ>\<open>('a,'b) DimTimes\<close> is parameterised by two types, \<^typ>\<open>'a\<close> and \<^typ>\<open>'b\<close> that must
|
||||
both be elements of the \<^class>\<open>dim_type\<close> class. As with the base dimensions, it is a unitary type
|
||||
as its purpose is to represent dimension type expressions. We instantiate \<^class>\<open>dim_type\<close> 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. \<close>
|
||||
|
||||
instantiation DimTimes :: (dim_type, dim_type) dim_type
|
||||
begin
|
||||
|
|
@ -297,13 +300,13 @@ begin
|
|||
instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
subsection \<open> Syntactic Support for dim-type expressions. \<close>
|
||||
subsubsection \<open> Dimension Type Syntax \<close>
|
||||
|
||||
text \<open> A division is expressed, as usual, by multiplication with an inverted dimension. \<close>
|
||||
|
||||
type_synonym ('a, 'b) DimDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
|
||||
|
||||
text \<open> A number of further type-synonyms allow for more compact notation: \<close>
|
||||
text \<open> A number of further type synonyms allow for more compact notation: \<close>
|
||||
|
||||
type_synonym 'a DimSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
|
||||
type_synonym 'a DimCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
|
||||
|
|
@ -333,7 +336,7 @@ print_translation \<open>
|
|||
_ => raise Match)]
|
||||
\<close>
|
||||
|
||||
subsection \<open> Derived Dimension Types \<close>
|
||||
subsubsection \<open> Derived Dimension Types \<close>
|
||||
|
||||
type_synonym Area = "L\<^sup>2"
|
||||
type_synonym Volume = "L\<^sup>3"
|
||||
|
|
|
|||
|
|
@ -4,17 +4,28 @@ theory ISQ_Quantities
|
|||
imports ISQ_Dimensions
|
||||
begin
|
||||
|
||||
section \<open> The Semantic SI-Unit-Type and its Operations \<close>
|
||||
section \<open> Quantity Semantic Domain \<close>
|
||||
|
||||
text \<open> 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. \<close>
|
||||
|
||||
record 'a Quantity =
|
||||
mag :: 'a \<comment> \<open> Magnitude of the unit \<close>
|
||||
dim :: Dimension \<comment> \<open> Dimension of the unit \<close>
|
||||
mag :: 'a \<comment> \<open> Magnitude of the quantity. \<close>
|
||||
dim :: Dimension \<comment> \<open> Dimension of the quantity -- denote the kind of quantity. \<close>
|
||||
|
||||
text \<open> The quantity type is parametric as we permit the magnitude to be represented using any kind
|
||||
of numeric type, such as \<^typ>\<open>int\<close>, \<^typ>\<open>rat\<close>, or \<^typ>\<open>real\<close>, though we usually minimally expect
|
||||
a field. \<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)
|
||||
|
||||
text \<open> We can define several arithmetic operators on quantities. Multiplication takes multiplies
|
||||
both the magnitudes and the dimensions. \<close>
|
||||
|
||||
instantiation Quantity_ext :: (times, times) times
|
||||
begin
|
||||
definition [si_def]:
|
||||
|
|
@ -26,6 +37,9 @@ lemma mag_times [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y" by (simp add:
|
|||
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)
|
||||
|
||||
text \<open> The zero and one quantities are both dimensionless quantities with magnitude of \<^term>\<open>0\<close> and
|
||||
\<^term>\<open>1\<close>, respectively. \<close>
|
||||
|
||||
instantiation Quantity_ext :: (zero, zero) zero
|
||||
begin
|
||||
definition "zero_Quantity_ext = \<lparr> mag = 0, dim = 1, \<dots> = 0 \<rparr>"
|
||||
|
|
@ -46,6 +60,9 @@ 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 \<open> Quantity inversion inverts both the magnitude and the dimension. Similarly, division of
|
||||
one quantity by another, divides both the magnitudes and the dimensions. \<close>
|
||||
|
||||
instantiation Quantity_ext :: (inverse, inverse) inverse
|
||||
begin
|
||||
definition [si_def]:
|
||||
|
|
@ -73,6 +90,8 @@ lemma dim_divide [simp]: "dim (x / y) = dim x / dim y"
|
|||
lemma more_divide [simp]: "more (x / y) = more x / more y"
|
||||
by (simp add: divide_Quantity_ext_def)
|
||||
|
||||
text \<open> As for dimensions, quantities form a commutative monoid and an abelian group. \<close>
|
||||
|
||||
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)
|
||||
|
|
@ -80,6 +99,8 @@ instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
|
|||
instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
|
||||
by (intro_classes, rule Quantity_eq_intro, simp_all)
|
||||
|
||||
text \<open> We can also define a partial order on quantities. \<close>
|
||||
|
||||
instantiation Quantity_ext :: (ord, ord) ord
|
||||
begin
|
||||
definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
|
||||
|
|
@ -94,39 +115,68 @@ 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 can define plus and minus as well, but these are partial operators as they are defined
|
||||
only when the quantities have the same dimension. \<close>
|
||||
|
||||
text\<open>We 'lift' SI type expressions to SI unit type expressions as follows:\<close>
|
||||
instantiation Quantity_ext :: (plus, plus) plus
|
||||
begin
|
||||
definition [si_def]:
|
||||
"dim x = dim y \<Longrightarrow>
|
||||
plus_Quantity_ext x y = \<lparr> mag = mag x + mag y, dim = dim x, \<dots> = more x + more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
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)
|
||||
instantiation Quantity_ext :: (uminus, uminus) uminus
|
||||
begin
|
||||
definition [si_def]:
|
||||
"uminus_Quantity_ext x = \<lparr> mag = - mag x , dim = dim x, \<dots> = - more x \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Quantity_ext :: (minus, minus) minus
|
||||
begin
|
||||
definition [si_def]:
|
||||
"dim x = dim y \<Longrightarrow>
|
||||
minus_Quantity_ext x y = \<lparr> mag = mag x - mag y, dim = dim x, \<dots> = more x - more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
section \<open> Dimension Typed Quantities \<close>
|
||||
|
||||
text \<open> We can now define the type of quantities with parametrised dimension types. \<close>
|
||||
|
||||
typedef (overloaded) ('n, 'd::dim_type) QuantT ("_[_]" [999,0] 999)
|
||||
= "{x :: 'n Quantity. dim x = QD('d)}"
|
||||
morphisms fromQ toQ by (rule_tac x="\<lparr> mag = undefined, dim = QD('d) \<rparr>" in exI, simp)
|
||||
|
||||
setup_lifting type_definition_QuantT
|
||||
|
||||
text \<open> Coerce values when their dimensions are equivalent \<close>
|
||||
text \<open> A dimension typed quantity is parameterised by two types: \<^typ>\<open>'a\<close>, the numeric type for the
|
||||
magntitude, and \<^typ>\<open>'d\<close> for the dimension expression, which is an element of \<^class>\<open>dim_type\<close>.
|
||||
The type \<^typ>\<open>('n, 'd) QuantT\<close> is to \<^typ>\<open>'n Quantity\<close> as dimension types are to \<^typ>\<open>Dimension\<close>.
|
||||
Specifically, an element of \<^typ>\<open>('n', 'd) QuantT\<close> is a quantity whose dimension is \<^typ>\<open>'d\<close>. \<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))"
|
||||
text \<open> 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. \<close>
|
||||
|
||||
subsection\<open>Predicates on Abstract SI-\<^theory_text>\<open>Unit\<close>-types\<close>
|
||||
definition coerceQuantT :: "'d\<^sub>2 itself \<Rightarrow> 'a['d\<^sub>1::dim_type] \<Rightarrow> 'a['d\<^sub>2::dim_type]" where
|
||||
"QD('d\<^sub>1) = QD('d\<^sub>2) \<Longrightarrow> coerceQuantT t x = (toQ (fromQ x))"
|
||||
|
||||
subsection \<open> Predicates on Typed Quantities \<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>)" .
|
||||
|
||||
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>
|
||||
lift_definition qequiv :: "'n['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50)
|
||||
is "(=)" .
|
||||
|
||||
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
|
||||
by (simp add: qequiv_def)
|
||||
|
|
@ -138,49 +188,49 @@ lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk
|
|||
by (simp add: qequiv_def)
|
||||
|
||||
theorem qeq_iff_same_dim:
|
||||
fixes x y :: "'a['u::dim_type]"
|
||||
fixes x y :: "'a['d::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"
|
||||
fixes x :: "'a['d\<^sub>1::dim_type]"
|
||||
assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)"
|
||||
shows "(coerceQuantT TYPE('d\<^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)"
|
||||
fixes x :: "'a['d\<^sub>1::dim_type]"
|
||||
assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (coerceQuantT TYPE('d\<^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))"
|
||||
fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]"
|
||||
assumes "QD('d\<^sub>1) = QD('d\<^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]"
|
||||
fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]"
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "QD('u\<^sub>1) = QD('u\<^sub>2::dim_type)"
|
||||
shows "QD('d\<^sub>1) = QD('d\<^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)
|
||||
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)
|
||||
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
|
||||
|
|
@ -257,8 +307,8 @@ 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
|
||||
lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['d::dim_type] \<Rightarrow> 'a['d]" (infixr "*\<^sub>Q" 63)
|
||||
is "\<lambda> r x. \<lparr> mag = r * mag x, dim = QD('d) \<rparr>" by simp
|
||||
|
||||
notation scaleQ (infixr "\<odot>" 63)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue