From da74d4ecc428fa1b8cd19e24fc32e85c462b5e71 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Thu, 12 Mar 2020 17:23:47 +0000 Subject: [PATCH] Revision of the narrative in Dimensions and Quantities --- src/SI/ISQ_Dimensions.thy | 133 +++++++++++++++++++------------------- src/SI/ISQ_Quantities.thy | 122 +++++++++++++++++++++++----------- 2 files changed, 154 insertions(+), 101 deletions(-) diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy index 89efea3..b13561b 100644 --- a/src/SI/ISQ_Dimensions.thy +++ b/src/SI/ISQ_Dimensions.thy @@ -116,7 +116,7 @@ qed text \ A base dimension is a dimension where precisely one component has power 1: it is the - dimension of a base quantity. \ + dimension of a base quantity. Here we define the seven base dimensions. \ definition LengthBD ("\<^bold>L") where [si_def]: "\<^bold>L = (1::Dimension)\Length := 1\" definition MassBD ("\<^bold>M") where [si_def]: "\<^bold>M = (1::Dimension)\Mass := 1\" @@ -136,17 +136,50 @@ lemma seven_BaseDimensions: "card BaseDimensions = 7" definition is_BaseDim :: "Dimension \ bool" where [si_def]: "is_BaseDim x \ x \ BaseDimensions" text \ We can use the base dimensions and algebra to form dimension expressions. Some examples - are shown below \ + are shown below. \ term "\<^bold>L\\<^bold>M\\<^bold>T\<^sup>-\<^sup>2" term "\<^bold>M\\<^bold>L\<^sup>-\<^sup>3" -subsection \ Dimensions as Types \ +subsection \ Dimensions Type Expressions \ -text \ 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>\dimension\-type symbols. \ +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 \<^emph>\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 = finite + + fixes dim_ty_sem :: "'a itself \ Dimension" + assumes unitary_unit_pres: "card (UNIV::'a set) = 1" + +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 si_basedim = 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 \<^verbatim>\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 @@ -175,108 +208,78 @@ translations (type) "N" <= (type) "Amount" (type) "J" <= (type) "Intensity" -subsection \Dimension Type Expressions and their Interpretation \ - -text \ 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>\type classes\. 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}. \ - -subsubsection \ SI-type expression definition as type-class \ - -class dim_type = finite + - fixes dim_ty_sem :: "'a itself \ Dimension" - assumes unitary_unit_pres: "card (UNIV::'a set) = 1" - -syntax - "_QD" :: "type \ logic" ("QD'(_')") - -translations - "QD('a)" == "CONST dim_ty_sem TYPE('a)" - -text \ The sub-set of basic SI type expressions can be characterized by the following -operation: \ - -class si_basedim = dim_type + - assumes is_BaseDim: "is_BaseDim QD('a)" - -subsubsection \ SI base type constructors \ - -text\We embed the basic SI types into the SI type expressions: \ +text\ Next, we embed the base dimensions into the dimension type expressions by instantiating the + class \<^class>\si_basedim\ with each of the base dimension types. \ instantiation Length :: si_basedim begin -definition dim_ty_sem_Length :: "Length itself \ 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 \ 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 \ 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 \ 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 \ Dimension" - where [si_def]: "dim_ty_sem_Temperature x = \<^bold>\" +definition [si_def]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\" 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 \ 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 \ 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 \ 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 \ Higher SI Type Constructors: Inner Product and Inverse \ -text\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.\ +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 \ We can prove that multiplication of two dimension types yields a dimension type. \ +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 @@ -297,13 +300,13 @@ begin instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+) end -subsection \ Syntactic Support for dim-type expressions. \ +subsubsection \ Dimension Type Syntax \ text \ A division is expressed, as usual, by multiplication with an inverted dimension. \ type_synonym ('a, 'b) DimDiv = "'a \ ('b\<^sup>-\<^sup>1)" (infixl "'/" 69) -text \ A number of further type-synonyms allow for more compact notation: \ +text \ A number of further type synonyms allow for more compact notation: \ type_synonym 'a DimSquare = "'a \ 'a" ("(_)\<^sup>2" [999] 999) type_synonym 'a DimCube = "'a \ 'a \ 'a" ("(_)\<^sup>3" [999] 999) @@ -333,7 +336,7 @@ print_translation \ _ => raise Match)] \ -subsection \ Derived Dimension Types \ +subsubsection \ Derived Dimension Types \ type_synonym Area = "L\<^sup>2" type_synonym Volume = "L\<^sup>3" diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy index 91c6255..3021314 100644 --- a/src/SI/ISQ_Quantities.thy +++ b/src/SI/ISQ_Quantities.thy @@ -4,17 +4,28 @@ theory ISQ_Quantities imports ISQ_Dimensions begin -section \ The Semantic SI-Unit-Type and its Operations \ +section \ 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 Quantity = - mag :: 'a \ \ Magnitude of the unit \ - dim :: Dimension \ \ Dimension of the unit \ + mag :: 'a \ \ Magnitude of the quantity. \ + dim :: Dimension \ \ Dimension of the quantity -- denote 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) +text \ We can define several arithmetic operators on quantities. Multiplication takes multiplies + both the magnitudes and the dimensions. \ + instantiation Quantity_ext :: (times, times) times begin definition [si_def]: @@ -26,6 +37,9 @@ lemma mag_times [simp]: "mag (x \ y) = mag x \ mag y" by (simp add: 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, zero) zero begin definition "zero_Quantity_ext = \ mag = 0, dim = 1, \ = 0 \" @@ -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 \ 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, 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 \ As for dimensions, quantities form a commutative monoid and an abelian group. \ + 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 \ We can also define a partial order on quantities. \ + instantiation Quantity_ext :: (ord, ord) ord begin definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \ ('a, 'b) Quantity_scheme \ 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 \ The Abstract SI-\<^theory_text>\Quantity\-Type and its Operations \ +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. \ -text\We 'lift' SI type expressions to SI unit type expressions as follows:\ +instantiation Quantity_ext :: (plus, plus) plus +begin + definition [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 -typedef (overloaded) ('n, 'u::dim_type) QuantT ("_[_]" [999,0] 999) - = "{x :: 'n Quantity. dim x = QD('u)}" - morphisms fromQ toQ by (rule_tac x="\ mag = undefined, dim = QD('u) \" in exI, simp) +instantiation Quantity_ext :: (uminus, uminus) uminus +begin + definition [si_def]: + "uminus_Quantity_ext x = \ mag = - mag x , dim = dim x, \ = - more x \" +instance .. +end + +instantiation Quantity_ext :: (minus, minus) minus +begin + definition [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 + +section \ Dimension Typed Quantities \ + +text \ We can now define the type of quantities with parametrised dimension types. \ + +typedef (overloaded) ('n, 'd::dim_type) QuantT ("_[_]" [999,0] 999) + = "{x :: 'n Quantity. dim x = QD('d)}" + morphisms fromQ toQ by (rule_tac x="\ mag = undefined, dim = QD('d) \" in exI, simp) setup_lifting type_definition_QuantT -text \ Coerce values when their dimensions are equivalent \ +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) QuantT\ is to \<^typ>\'n Quantity\ as dimension types are to \<^typ>\Dimension\. + Specifically, an element of \<^typ>\('n', 'd) QuantT\ is a quantity whose dimension is \<^typ>\'d\. \ -definition coerceQuantT :: "'u\<^sub>2 itself \ 'a['u\<^sub>1::dim_type] \ 'a['u\<^sub>2::dim_type]" where -"QD('u\<^sub>1) = QD('u\<^sub>2) \ coerceQuantT t x = (toQ (fromQ x))" +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. \ -subsection\Predicates on Abstract SI-\<^theory_text>\Unit\-types\ +definition coerceQuantT :: "'d\<^sub>2 itself \ 'a['d\<^sub>1::dim_type] \ 'a['d\<^sub>2::dim_type]" where +"QD('d\<^sub>1) = QD('d\<^sub>2) \ coerceQuantT t x = (toQ (fromQ x))" + +subsection \ Predicates on Typed Quantities \ text \ Two SI Unit types are orderable if their magnitude type is of class @{class "order"}, and have the same dimensions (not necessarily dimension types).\ -lift_definition qless_eq :: - "'n::order['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) is "(\)" . - +lift_definition qless_eq :: "'n::order['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) + is "(\)" . text\ 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. \ -lift_definition qequiv :: - "'n['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) is "(=)" . - -subsection\The Equivalence on Abstract SI-\<^theory_text>\Unit\-Types\ -text\The latter predicate gives us an equivalence, but, unfortunately, not a congruence.\ +lift_definition qequiv :: "'n['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) + is "(=)" . lemma qequiv_refl [simp]: "a \\<^sub>Q a" by (simp add: qequiv_def) @@ -138,49 +188,49 @@ lemma qequiv_trans: "\ a \\<^sub>Q b; b \\<^sub>Q c \\<^sub>Q y \ 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) \\<^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) \\<^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 \\<^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 \\<^sub>Q y" by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceQuantT_def) text\This is more general that \y = x \ x \\<^sub>Q y\, since x and y may have different type.\ 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 \\<^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\Operations on Abstract SI-Unit-Types\ lift_definition - qtimes :: "('n::comm_ring_1)['a::dim_type] \ 'n['b::dim_type] \ 'n['a \'b]" (infixl "\<^bold>\" 69) is "(*)" - by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def) + qtimes :: "('n::comm_ring_1)['a::dim_type] \ 'n['b::dim_type] \ 'n['a \'b]" (infixl "\<^bold>\" 69) + is "(*)" by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def) lift_definition - qinverse :: "('n::field)['a::dim_type] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) is "inverse" - by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def) + qinverse :: "('n::field)['a::dim_type] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) + is "inverse" by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def) abbreviation qdivide :: "('n::field)['a::dim_type] \ 'n['b::dim_type] \ 'n['a/'b]" (infixl "\<^bold>'/" 70) where @@ -257,8 +307,8 @@ end text\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.\ -lift_definition scaleQ :: "'a \ 'a::comm_ring_1['u::dim_type] \ 'a['u]" (infixr "*\<^sub>Q" 63) - is "\ r x. \ mag = r * mag x, dim = QD('u) \" by simp +lift_definition scaleQ :: "'a \ 'a::comm_ring_1['d::dim_type] \ 'a['d]" (infixr "*\<^sub>Q" 63) + is "\ r x. \ mag = r * mag x, dim = QD('d) \" by simp notation scaleQ (infixr "\" 63)