From cf1004368019cd30206669ebfa851920e0a44865 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Fri, 13 Mar 2020 14:54:46 +0000 Subject: [PATCH] A few more revisions and explanations. --- src/SI/ISQ_Quantities.thy | 5 ++++- src/SI/SI_Accepted.thy | 9 +++++++-- src/SI/SI_Constants.thy | 6 ++++++ src/SI/SI_Units.thy | 19 +++++++++++++++---- 4 files changed, 32 insertions(+), 7 deletions(-) diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy index dffc665..b4b6144 100644 --- a/src/SI/ISQ_Quantities.thy +++ b/src/SI/ISQ_Quantities.thy @@ -154,7 +154,10 @@ setup_lifting type_definition_QuantT 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\. \ + Specifically, an element of \<^typ>\('n', 'd) QuantT\ is a quantity whose dimension is \<^typ>\'d\. + + Intuitively, the formula \<^term>\x :: 'n['d]\ can be read as ``$x$ is a quantity of \<^typ>\'d\'', + for example it might be a quantity of length, or a quantity of mass. \ 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 diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy index 4946f8f..b494106 100644 --- a/src/SI/SI_Accepted.thy +++ b/src/SI/SI_Accepted.thy @@ -19,9 +19,14 @@ abbreviation degrees ("_\" [999] 999) where "n\ \ n \ meter\<^sup>\" -abbreviation "tonne \ 10^3 \ kilogram" +definition [si_def, si_eq]: "tonne = 10^3 \ kilogram" -subsection \ Examples \ +definition [si_def, si_eq]: "dalton = 1.66053906660 * (1 / 10^27) \ kilogram" + +subsection \ Example Unit Equations \ + +lemma "1 \ hour = 3600 \ second" + by (si_simp) lemma "watt \<^bold>\ hour \\<^sub>Q 3600 \ joule" by (si_calc) diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index 5afe84b..06a44cb 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -47,15 +47,21 @@ text \ Elementary charge \ abbreviation elementary_charge :: "'a[I \ T]" ("\<^bold>e") where "elementary_charge \ (1.602176634 \ 1/(10^19)) \ coulomb" +text \ The Boltzmann constant \ + abbreviation Boltzmann :: "'a[M \ L\<^sup>2 \ T\<^sup>-\<^sup>2 \ \\<^sup>-\<^sup>1]" ("\<^bold>k") where "Boltzmann \ (1.380649\1/(10^23)) \ (joule \<^bold>/ kelvin)" +text \ The Avogadro number \ + abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" ("N\<^sub>A") where "Avogadro \ 6.02214076\(10^23) \ (mole\<^sup>-\<^sup>\)" abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where "max_luminous_frequency \ (540\10^12) \ hertz" +text \ The luminous efficacy of monochromatic radiation of frequency \<^const>\max_luminous_frequency\. \ + abbreviation luminous_efficacy :: "'a[J \ (L\<^sup>2 \ L\<^sup>-\<^sup>2) \ (M \ L\<^sup>2 \ T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" ("K\<^sub>c\<^sub>d") where "luminous_efficacy \ 683 \ (lumen\<^bold>/watt)" diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index 27db167..a925a89 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -4,6 +4,19 @@ theory SI_Units imports ISQ_Proof begin +text \ An SI unit is simply a particular kind of quantity. \ + +type_synonym ('n, 'd) UnitT = "('n, 'd) QuantT" + +text \ Parallel to the seven base quantities, there are seven base units. In the implementation of + the SI unit system, we fix these to be precisely those quantities that have a base dimension + and a magnitude of \<^term>\1\. Consequently, a base unit corresponds to a unit in the algebraic + sense. \ + +lift_definition is_BaseUnit :: "'a::one['d::dim_type] \ bool" + is "\ x. mag x = 1 \ is_BaseDim (dim x)" . + + lift_definition mk_base_unit :: "'u itself \ ('a::one)['u::dim_type]" is "\ u. \ mag = 1, dim = QD('u) \" by simp @@ -13,7 +26,8 @@ translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)" lemma magQuant_mk [si_eq]: "\BUNIT('u::dim_type)\\<^sub>Q = 1" by (simp add: magQuant_def, transfer, simp) -subsection \Polymorphic Operations for SI Base Units \ +text \ We now define the seven base units. Effectively, these definitions axiomatise give names + to the \<^term>\1\ elements of the base quantities. \ definition [si_eq]: "meter = BUNIT(L)" definition [si_eq]: "second = BUNIT(T)" @@ -30,9 +44,6 @@ type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer not to its components. \ -lift_definition is_BaseUnit :: "'a::one['d::dim_type] \ bool" - is "\ x. mag x = 1 \ is_BaseDim (dim x)" . - lemma meter_is_BaseUnit: "is_BaseUnit meter" by (simp add: si_eq, transfer, simp)