From 1ee0a1610f6c3d51741e3341f828fd6bd2436277 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Thu, 12 Mar 2020 11:11:30 +0000 Subject: [PATCH] Refactoring to better distinguish quantities and units, which are now distinct entities. --- src/SI/Groups_mult.thy | 3 + .../{SI_Dimensions.thy => ISQ_Dimensions.thy} | 139 +++++---- src/SI/ISQ_Quantities.thy | 265 ++++++++++++++++ src/SI/SI_Proof.thy | 6 +- src/SI/SI_Units.thy | 285 +----------------- 5 files changed, 363 insertions(+), 335 deletions(-) rename src/SI/{SI_Dimensions.thy => ISQ_Dimensions.thy} (73%) create mode 100644 src/SI/ISQ_Quantities.thy diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy index 54d8ad5..819393b 100644 --- a/src/SI/Groups_mult.thy +++ b/src/SI/Groups_mult.thy @@ -36,4 +36,7 @@ lemma inverse_distrib: "inverse (a * b) = (inverse a) * (inverse b)" end +abbreviation npower :: "'a::{power,inverse} \ nat \ 'a" ("(_\<^sup>-\<^sup>_)" [1000,999] 999) + where "npower x n \ inverse (x ^ n)" + end \ No newline at end of file diff --git a/src/SI/SI_Dimensions.thy b/src/SI/ISQ_Dimensions.thy similarity index 73% rename from src/SI/SI_Dimensions.thy rename to src/SI/ISQ_Dimensions.thy index 99cbd3b..89efea3 100644 --- a/src/SI/SI_Dimensions.thy +++ b/src/SI/ISQ_Dimensions.thy @@ -1,19 +1,47 @@ -section \ SI Dimensions \ +section \ Dimensions \ -theory SI_Dimensions +theory ISQ_Dimensions imports Groups_mult HOL.Transcendental "HOL-Eisbach.Eisbach" begin +subsection \ Preliminaries \ + named_theorems si_def and si_eq -section\The Semantic Domain of Dimensions\ +instantiation unit :: comm_monoid_add +begin + definition "zero_unit = ()" + definition "plus_unit (x::unit) (y::unit) = ()" + instance proof qed (simp_all) +end -subsection \ The Dimension-type and its operations \ +instantiation unit :: comm_monoid_mult +begin + definition "one_unit = ()" + definition "times_unit (x::unit) (y::unit) = ()" + instance proof qed (simp_all) +end -text \ An SI unit associates with each of the seven base unit an integer that denotes the power - to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \ +instantiation unit :: inverse +begin + definition "inverse_unit (x::unit) = ()" + definition "divide_unit (x::unit) (y::unit) = ()" + instance .. +end + +instance unit :: ab_group_mult + by (intro_classes, simp_all) + +subsection \ Dimensions Semantic Domain \ + +text \ Quantity dimensions are used to distinguish quantities of different kinds. Only quantities + of the same kind can be compared and combined: it is a mistake to add a length to a mass, for + example. Dimensions are 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. \ record Dimension = Length :: int @@ -24,7 +52,8 @@ record Dimension = Amount :: int Intensity :: int -text \ We define a commutative monoid for SI units. \ +text \ Next, we define dimension multiplication, and its unit, which corresponds to a dimensionless + quantity. These are then shown to form a commutative monoid. \ instantiation Dimension_ext :: (one) one begin @@ -58,7 +87,8 @@ proof by (simp add: times_Dimension_ext_def one_Dimension_ext_def) qed -text \ We also define the inverse and division operations, and an abelian group. \ +text \ We also define the inverse and division operations, and an abelian group, which will allow + us to perform dimensional analysis. \ instantiation Dimension_ext :: ("{times,inverse}") inverse begin @@ -84,49 +114,39 @@ proof by (simp add: divide_Dimension_ext_def) qed -text \ 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. \ -instantiation unit :: comm_monoid_add -begin - definition "zero_unit = ()" - definition "plus_unit (x::unit) (y::unit) = ()" - instance proof qed (simp_all) -end +text \ A base dimension is a dimension where precisely one component has power 1: it is the + dimension of a base quantity. \ -instantiation unit :: comm_monoid_mult -begin - definition "one_unit = ()" - definition "times_unit (x::unit) (y::unit) = ()" - instance proof qed (simp_all) -end +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\" +definition TimeBD ("\<^bold>T") where [si_def]: "\<^bold>T = (1::Dimension)\Time := 1\" +definition CurrentBD ("\<^bold>I") where [si_def]: "\<^bold>I = (1::Dimension)\Current := 1\" +definition TemperatureBD ("\<^bold>\") where [si_def]: "\<^bold>\ = (1::Dimension)\Temperature := 1\" +definition AmountBD ("\<^bold>N") where [si_def]: "\<^bold>N = (1::Dimension)\Amount := 1\" +definition IntensityBD ("\<^bold>J") where [si_def]: "\<^bold>J = (1::Dimension)\Intensity := 1\" -instantiation unit :: inverse -begin - definition "inverse_unit (x::unit) = ()" - definition "divide_unit (x::unit) (y::unit) = ()" - instance .. -end +abbreviation "BaseDimensions \ {\<^bold>L, \<^bold>M, \<^bold>T, \<^bold>I, \<^bold>\, \<^bold>N, \<^bold>J}" -instance unit :: ab_group_mult - by (intro_classes, simp_all) +text \ The following lemma confirms that there are indeed seven unique base dimensions. \ -text \ A base unit is an unit where precisely one component has power 1. \ +lemma seven_BaseDimensions: "card BaseDimensions = 7" + by (simp add: si_def) -definition is_BaseDim :: "Dimension \ bool" where -"is_BaseDim u = (\ n. u = 1\Length := n\ \ u = 1\Mass := n\ \ u = 1\Time := n\ - \ u = 1\Current := n\ \ u = 1\Temperature := n\ \ u = 1\Amount := n\ - \ u = 1\Intensity := n\)" +definition is_BaseDim :: "Dimension \ bool" where [si_def]: "is_BaseDim x \ x \ BaseDimensions" -section\The Syntax and Semantics of Dimension Types\ +text \ We can use the base dimensions and algebra to form dimension expressions. Some examples + are shown below \ -subsection \ Basic Dimensions as Types (Basic SI-types)\ +term "\<^bold>L\\<^bold>M\\<^bold>T\<^sup>-\<^sup>2" +term "\<^bold>M\\<^bold>L\<^sup>-\<^sup>3" -text \ We provide a syntax for type-expressions; The definition of -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, -so just one value for the \<^verbatim>\dimension\-type symbols. -\ +subsection \ Dimensions as Types \ + +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. \ typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass @@ -172,18 +192,17 @@ class dim_type = finite + fixes dim_ty_sem :: "'a itself \ Dimension" assumes unitary_unit_pres: "card (UNIV::'a set) = 1" - syntax - "_SI" :: "type \ logic" ("SI'(_')") + "_QD" :: "type \ logic" ("QD'(_')") translations - "SI('a)" == "CONST dim_ty_sem TYPE('a)" + "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 SI('a)" + assumes is_BaseDim: "is_BaseDim QD('a)" subsubsection \ SI base type constructors \ @@ -192,49 +211,49 @@ text\We embed the basic SI types into the SI type expressions: \ instantiation Length :: si_basedim begin definition dim_ty_sem_Length :: "Length itself \ Dimension" - where [si_def]: "dim_ty_sem_Length x = 1\Length := 1\" + 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)+) end instantiation Mass :: si_basedim begin definition dim_ty_sem_Mass :: "Mass itself \ Dimension" - where [si_def]: "dim_ty_sem_Mass x = 1\Mass := 1\" + 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)+) end instantiation Time :: si_basedim begin definition dim_ty_sem_Time :: "Time itself \ Dimension" - where [si_def]: "dim_ty_sem_Time x = 1\Time := 1\" + 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)+) end instantiation Current :: si_basedim begin definition dim_ty_sem_Current :: "Current itself \ Dimension" - where [si_def]: "dim_ty_sem_Current x = 1\Current := 1\" + 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)+) end instantiation Temperature :: si_basedim begin definition dim_ty_sem_Temperature :: "Temperature itself \ Dimension" - where [si_def]: "dim_ty_sem_Temperature x = 1\Temperature := 1\" + where [si_def]: "dim_ty_sem_Temperature x = \<^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 = 1\Amount := 1\" + 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)+) end instantiation Intensity :: si_basedim begin definition dim_ty_sem_Intensity :: "Intensity itself \ Dimension" - where [si_def]: "dim_ty_sem_Intensity x = 1\Intensity := 1\" + 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)+) end @@ -245,10 +264,10 @@ definition dim_ty_sem_NoDimension :: "NoDimension itself \ Dimension instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+) end -lemma base_units [simp]: - "is_BaseDim SI(Length)" "is_BaseDim SI(Mass)" "is_BaseDim SI(Time)" - "is_BaseDim SI(Current)" "is_BaseDim SI(Temperature)" "is_BaseDim SI(Amount)" - "is_BaseDim SI(Intensity)" by (simp_all add: is_BaseDim) +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) 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), @@ -262,7 +281,7 @@ text \ We can prove that multiplication of two dimension types yields a di instantiation DimTimes :: (dim_type, dim_type) dim_type begin definition dim_ty_sem_DimTimes :: "('a \ 'b) itself \ Dimension" where - [si_eq]: "dim_ty_sem_DimTimes x = 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)+) end @@ -274,7 +293,7 @@ setup_lifting type_definition_DimInv instantiation DimInv :: (dim_type) dim_type begin definition dim_ty_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \ 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)+) end @@ -314,7 +333,7 @@ print_translation \ _ => raise Match)] \ -subsection \ Derived Dimensions \ +subsection \ 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 new file mode 100644 index 0000000..91c6255 --- /dev/null +++ b/src/SI/ISQ_Quantities.thy @@ -0,0 +1,265 @@ +section \ Quantities \ + +theory ISQ_Quantities + imports ISQ_Dimensions +begin + +section \ The Semantic SI-Unit-Type and its Operations \ + +record 'a Quantity = + mag :: 'a \ \ Magnitude of the unit \ + dim :: Dimension \ \ Dimension of the unit \ + +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 = \ mag = mag x \ mag y, dim = dim x \ dim y, \ = more x \ more y \" +instance .. +end + +lemma mag_times [simp]: "mag (x \ y) = mag x \ mag y" by (simp add: times_Quantity_ext_def) +lemma dim_times [simp]: "dim (x \ y) = dim x \ dim y" by (simp add: times_Quantity_ext_def) +lemma more_times [simp]: "more (x \ y) = more x \ more y" by (simp add: times_Quantity_ext_def) + +instantiation Quantity_ext :: (zero, zero) zero +begin + definition "zero_Quantity_ext = \ mag = 0, dim = 1, \ = 0 \" +instance .. +end + +lemma mag_zero [simp]: "mag 0 = 0" by (simp add: zero_Quantity_ext_def) +lemma dim_zero [simp]: "dim 0 = 1" by (simp add: zero_Quantity_ext_def) +lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def) + +instantiation Quantity_ext :: (one, one) one +begin + definition [si_def]: "one_Quantity_ext = \ mag = 1, dim = 1, \ = 1 \" +instance .. +end + +lemma mag_one [simp]: "mag 1 = 1" by (simp add: one_Quantity_ext_def) +lemma dim_one [simp]: "dim 1 = 1" by (simp add: one_Quantity_ext_def) +lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def) + +instantiation Quantity_ext :: (inverse, inverse) inverse +begin +definition [si_def]: + "inverse_Quantity_ext x = \ mag = inverse (mag x), dim = inverse (dim x), \ = inverse (more x) \" +definition [si_def]: + "divide_Quantity_ext x y = \ mag = mag x / mag y, dim = dim x / dim y, \ = more x / more y \" +instance .. +end + +lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)" + by (simp add: inverse_Quantity_ext_def) + +lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)" + by (simp add: inverse_Quantity_ext_def) + +lemma more_inverse [simp]: "more (inverse x) = inverse (more x)" + by (simp add: inverse_Quantity_ext_def) + +lemma mag_divide [simp]: "mag (x / y) = mag x / mag y" + by (simp add: divide_Quantity_ext_def) + +lemma dim_divide [simp]: "dim (x / y) = dim x / dim y" + by (simp add: divide_Quantity_ext_def) + +lemma more_divide [simp]: "more (x / y) = more x / more y" + by (simp add: divide_Quantity_ext_def) + +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 \ ('a, 'b) Quantity_scheme \ bool" + where "less_eq_Quantity_ext x y = (mag x \ mag y \ dim x = dim y \ more x \ more y)" + definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \ ('a, 'b) Quantity_scheme \ bool" + where "less_Quantity_ext x y = (x \ y \ \ y \ 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 \ The Abstract SI-\<^theory_text>\Quantity\-Type and its Operations \ + +text\We 'lift' SI type expressions to SI unit type expressions as follows:\ + +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) + +setup_lifting type_definition_QuantT + +text \ Coerce values when their dimensions are equivalent \ + +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))" + +subsection\Predicates on Abstract SI-\<^theory_text>\Unit\-types\ + +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 "(\)" . + + +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.\ + +lemma qequiv_refl [simp]: "a \\<^sub>Q a" + by (simp add: qequiv_def) + +lemma qequiv_sym: "a \\<^sub>Q b \ b \\<^sub>Q a" + by (simp add: qequiv_def) + +lemma qequiv_trans: "\ a \\<^sub>Q b; b \\<^sub>Q c \ \ a \\<^sub>Q c" + by (simp add: qequiv_def) + +theorem qeq_iff_same_dim: + fixes x y :: "'a['u::dim_type]" + shows "x \\<^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" + 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 \\<^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 \\<^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]" + assumes "x \\<^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\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) + +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) + +abbreviation + qdivide :: "('n::field)['a::dim_type] \ 'n['b::dim_type] \ 'n['a/'b]" (infixl "\<^bold>'/" 70) where +"qdivide x y \ x \<^bold>\ y\<^sup>-\<^sup>\" + +abbreviation qsq ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u" +abbreviation qcube ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u" +abbreviation qquart ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u\<^bold>\u" + +abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" +abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" +abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" + +instantiation QuantT :: (zero,dim_type) zero +begin +lift_definition zero_QuantT :: "('a, 'b) QuantT" is "\ mag = 0, dim = QD('b) \" + by simp +instance .. +end + +instantiation QuantT :: (one,dim_type) one +begin +lift_definition one_QuantT :: "('a, 'b) QuantT" is "\ mag = 1, dim = QD('b) \" + by simp +instance .. +end + +instantiation QuantT :: (plus,dim_type) plus +begin +lift_definition plus_QuantT :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ mag = mag x + mag y, dim = QD('b) \" + 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] \ 'a['b]" + is "\ x. \ mag = - mag x, dim = dim x \" by (simp) +instance .. +end + +instantiation QuantT :: (minus,dim_type) minus +begin +lift_definition minus_QuantT :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ mag = mag x - mag y, dim = dim x \" 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] \ 'a['b] \ bool" is "\ x y. mag x \ mag y" . + lift_definition less_QuantT :: "'a['b] \ 'a['b] \ bool" is "\ x y. mag x < mag y" . + instance by (intro_classes, (transfer, simp add: less_le_not_le)+) +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 + +notation scaleQ (infixr "\" 63) + +end \ No newline at end of file diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy index 323ab26..2e95f45 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/SI_Proof.thy @@ -15,7 +15,7 @@ lemma unit_eq_iff_mag_eq [si_transfer]: lemma unit_equiv_iff [si_transfer]: fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]" - shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ SI('u\<^sub>1) = SI('u\<^sub>2)" + shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ QD('u\<^sub>1) = QD('u\<^sub>2)" proof - have "\t ta. (ta::'a['u\<^sub>2]) = t \ mag (fromQ ta) \ mag (fromQ t)" by (simp add: magQuant_def unit_eq_iff_mag_eq) @@ -61,7 +61,7 @@ lemma magQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3)) done -lemma magQuant_mk [si_eq]: "\UNIT('u::dim_type)\\<^sub>Q = 1" +lemma magQuant_mk [si_eq]: "\BUNIT('u::dim_type)\\<^sub>Q = 1" by (simp add: magQuant_def, transfer, simp) text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ @@ -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 *) -lemma "SI(N \ \ \ N) = SI(\ \ N\<^sup>2)" by (simp add: si_eq si_def) +lemma "QD(N \ \ \ N) = QD(\ \ N\<^sup>2)" by (simp add: si_eq si_def) lemma "(meter \<^bold>\ second\<^sup>-\<^sup>\) \<^bold>\ second \\<^sub>Q meter" by (si_calc) diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index e45d771..d4e2dfd 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -1,286 +1,27 @@ section \ SI Units \ theory SI_Units - imports SI_Dimensions + imports ISQ_Quantities begin -section \ The Semantic SI-Unit-Type and its Operations \ +lift_definition mk_base_unit :: "'u itself \ ('a::one)['u::dim_type]" + is "\ u. \ mag = 1, dim = QD('u) \" by simp -record 'a Unit = - mag :: 'a \ \ Magnitude of the unit \ - dim :: Dimension \ \ Dimension of the unit \ - -lemma Unit_eq_intro: - 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 -begin - definition [si_def]: - "times_Unit_ext x y = \ mag = mag x \ mag y, dim = dim x \ dim y, \ = more x \ more y \" -instance .. -end - -lemma mag_times [simp]: "mag (x \ y) = mag x \ mag y" by (simp add: times_Unit_ext_def) -lemma dim_times [simp]: "dim (x \ y) = dim x \ dim y" by (simp add: times_Unit_ext_def) -lemma more_times [simp]: "more (x \ y) = more x \ more y" by (simp add: times_Unit_ext_def) - -instantiation Unit_ext :: (zero, zero) zero -begin - definition "zero_Unit_ext = \ mag = 0, dim = 1, \ = 0 \" -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 = \ mag = 1, dim = 1, \ = 1 \" -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 = \ mag = inverse (mag x), dim = inverse (dim x), \ = inverse (more x) \" -definition [si_def]: - "divide_Unit_ext x y = \ mag = mag x / mag y, dim = dim x / dim y, \ = more x / more y \" -instance .. -end - -lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)" - by (simp add: inverse_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 \ ('a, 'b) Unit_scheme \ bool" - where "less_eq_Unit_ext x y = (mag x \ mag y \ dim x = dim y \ more x \ more y)" - definition less_Unit_ext :: "('a, 'b) Unit_scheme \ ('a, 'b) Unit_scheme \ bool" - where "less_Unit_ext x y = (x \ y \ \ y \ 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 \ The Abstract SI-\<^theory_text>\Unit\-Type and its Operations \ - -text\We 'lift' SI type expressions to SI unit type expressions as follows:\ - -typedef (overloaded) ('n, 'u::dim_type) UnitT ("_[_]" [999,0] 999) - = "{x :: 'n Unit. dim x = SI('u)}" - morphisms fromQ toQ by (rule_tac x="\ mag = undefined, dim = SI('u) \" in exI, simp) - -setup_lifting type_definition_UnitT - -text \ Coerce values when their dimensions are equivalent \ - -definition coerceUnit :: "'u\<^sub>2 itself \ 'a['u\<^sub>1::dim_type] \ 'a['u\<^sub>2::dim_type]" where -"SI('u\<^sub>1) = SI('u\<^sub>2) \ coerceUnit t x = (toQ (fromQ x))" - -subsection\Predicates on Abstract SI-\<^theory_text>\Unit\-types\ - -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 "(\)" . - - -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.\ - -lemma qequiv_refl [simp]: "a \\<^sub>Q a" - by (simp add: qequiv_def) - -lemma qequiv_sym: "a \\<^sub>Q b \ b \\<^sub>Q a" - by (simp add: qequiv_def) - -lemma qequiv_trans: "\ a \\<^sub>Q b; b \\<^sub>Q c \ \ a \\<^sub>Q c" - by (simp add: qequiv_def) - -theorem qeq_iff_same_dim: - fixes x y :: "'a['u::dim_type]" - shows "x \\<^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 "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)" - shows "(coerceUnit TYPE('u\<^sub>2) x) \\<^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 \\<^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 \\<^sub>Q y" - by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceUnit_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]" - assumes "x \\<^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\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_Unit_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_Unit_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 -"qdivide x y \ x \<^bold>\ y\<^sup>-\<^sup>\" - -abbreviation qsq ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u" -abbreviation qcube ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u" -abbreviation qquart ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u\<^bold>\u" - -abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" -abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" -abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" - -instantiation UnitT :: (zero,dim_type) zero -begin -lift_definition zero_UnitT :: "('a, 'b) UnitT" is "\ mag = 0, dim = SI('b) \" - by simp -instance .. -end - -instantiation UnitT :: (one,dim_type) one -begin -lift_definition one_UnitT :: "('a, 'b) UnitT" is "\ mag = 1, dim = SI('b) \" - by simp -instance .. -end - -instantiation UnitT :: (plus,dim_type) plus -begin -lift_definition plus_UnitT :: "'a['b] \ 'a['b] \ 'a['b]" - is "\ x y. \ mag = mag x + mag y, dim = SI('b) \" - 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] \ 'a['b]" - is "\ x. \ mag = - mag x, dim = dim x \" by (simp) -instance .. -end - -instantiation UnitT :: (minus,dim_type) minus -begin -lift_definition minus_UnitT :: "'a['b] \ 'a['b] \ 'a['b]" - is "\ x y. \ mag = mag x - mag y, dim = dim x \" 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] \ 'a['b] \ bool" is "\ x y. mag x \ mag y" . - lift_definition less_UnitT :: "'a['b] \ 'a['b] \ bool" is "\ x y. mag x < mag y" . - instance by (intro_classes, (transfer, simp add: less_le_not_le)+) -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 = SI('u) \" by simp - -notation scaleQ (infixr "\" 63) - -lift_definition mk_unit :: "'u itself \ ('a::one)['u::dim_type]" - is "\ u. \ mag = 1, dim = SI('u) \" by simp - -syntax "_mk_unit" :: "type \ logic" ("UNIT'(_')") -translations "UNIT('a)" == "CONST mk_unit TYPE('a)" +syntax "_mk_base_unit" :: "type \ logic" ("BUNIT'(_')") +translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)" subsection \Polymorphic Operations for SI Base Units \ -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(\)" -definition [si_eq]: "mole = UNIT(N)" -definition [si_eq]: "candela = UNIT(J)" +definition [si_eq]: "meter = BUNIT(L)" +definition [si_eq]: "second = BUNIT(T)" +definition [si_eq]: "kilogram = BUNIT(M)" +definition [si_eq]: "ampere = BUNIT(I)" +definition [si_eq]: "kelvin = BUNIT(\)" +definition [si_eq]: "mole = BUNIT(N)" +definition [si_eq]: "candela = BUNIT(J)" definition dimless ("\") - where [si_eq]: "dimless = UNIT(NoDimension)" + where [si_eq]: "dimless = BUNIT(NoDimension)" text\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"}.