From 2c63ef07e9934c02259f44ed472d4d50b1ba5830 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Tue, 18 Feb 2020 17:46:13 +0000 Subject: [PATCH] Added core physical constants of the 2019 SI standard, dimensionless units, and various proof facilities for support. --- src/SI/SI_Constants.thy | 60 ++++++++++++++++++++++++++++++-- src/SI/SI_Derived.thy | 23 +++++++++---- src/SI/SI_Prefix.thy | 2 +- src/SI/SI_Proof.thy | 22 ++++++------ src/SI/SI_Quantities.thy | 27 +++++++++++---- src/SI/SI_Units.thy | 74 ++++++++++++++++++++++++++++++---------- 6 files changed, 163 insertions(+), 45 deletions(-) diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index c892d17..e82fc31 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -1,13 +1,67 @@ section \ Physical Constants \ theory SI_Constants - imports SI_Quantities + imports SI_Proof begin -abbreviation speed_of_light :: "'a::division_ring[L \ T\<^sup>-\<^sup>1]" where +abbreviation "hertz \ second\<^sup>-\<^sup>\" + +abbreviation "radian \ meter \<^bold>\ meter\<^sup>-\<^sup>\" + +abbreviation "steradian \ meter\<^sup>\ \<^bold>\ meter\<^sup>-\<^sup>\" + +abbreviation "joule \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +abbreviation "watt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +abbreviation "coulomb \ ampere \<^bold>\ second" + +abbreviation "lumen \ candela \<^bold>\ steradian" + +text \ The most general types we support must form a field into which the natural numbers can + be injected. \ + +default_sort field_char_0 + +abbreviation (input) caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\v\<^sub>C\<^sub>s") where + "caesium_frequency \ 9192631770\hertz" + +abbreviation speed_of_light :: "'a[L \ T\<^sup>-\<^sup>1]" where "speed_of_light \ 299792458\(meter\<^bold>\second\<^sup>-\<^sup>\)" -abbreviation gravitational_constant where +abbreviation Planck :: "'a[M \ L\<^sup>2 \ T\<^sup>-\<^sup>2 \ T]" where + "Planck \ (6.62607015 \ 1/(10^34))\(joule\<^bold>\second)" + +abbreviation elementary_charge :: "'a[I \ T]" where + "elementary_charge \ (1.602176634 \ 1/(10^19))\coulomb" + +abbreviation Boltzmann :: "'a[M \ L\<^sup>2 \ T\<^sup>-\<^sup>2 \ \\<^sup>-\<^sup>1]" where + "Boltzmann \ (1.380649\1/(10^23))\(joule \<^bold>/ kelvin)" + +abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" 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" + +abbreviation luminous_efficacy :: "'a[J \ (L\<^sup>2 \ L\<^sup>-\<^sup>2) \ (M \ L\<^sup>2 \ T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" where +"luminous_efficacy \ 683\(lumen\<^bold>/watt)" + +abbreviation gravitational_constant :: "'a[L\<^sup>3 \ M\<^sup>-\<^sup>1 \ T\<^sup>-\<^sup>2]" where "gravitational_constant \ (6.6743015 \ 1/(10 ^ 11)) \ (meter\<^sup>\\<^bold>\kilogram\<^sup>-\<^sup>\\<^bold>\second\<^sup>-\<^sup>\)" +thm si_def + +theorem Quant_eq_iff_same_dim: + "x \\<^sub>Q y \ x = y" + by (transfer, simp) + +theorem hertz_definition: "1\hertz = \v\<^sub>C\<^sub>s / 9192631770" + by (simp add: unit_eq_iff_magn_eq si_def) + +theorem second_definition: "1\second \\<^sub>Q (9192631770::_[\]) \<^bold>/ \v\<^sub>C\<^sub>s" + by (simp add: unit_equiv_iff, simp add: Quant_equiv_def unit_eq_iff_magn_eq si_def) + +default_sort type + end \ No newline at end of file diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index 93e5383..eed8259 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -2,14 +2,18 @@ section \ Derived Units\ theory SI_Derived imports SI_Prefix -begin +begin -definition "radian = 1 \ (meter \<^bold>\ meter\<^sup>-\<^sup>\)" +definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where +[si_def]: "degree = (2\(UNIT(of_real pi,_)) / 180)\radian" -definition degree :: "real[L/L]" where -[si_def]: "degree = (2\(UNIT(pi,_)) / 180)\radian" +abbreviation degrees ("_\" [999] 999) where "n\ \ n\degree" -abbreviation degrees ("_\" [999] 999) where "n\ \ n\degree" +definition degrees_celcius :: "'a::division_ring[\] \ 'a[\]" ("_\C" [999] 999) + where [si_def]: "degrees_celcius x = (x + 273.151)\kelvin" + +definition degrees_farenheit :: "'a::division_ring[\] \ 'a[\]" ("_\F" [999] 999) + where [si_def]: "degrees_farenheit x = (x + 459.67)\5/9\kelvin" definition [si_def]: "litre = 1/1000 \ meter\<^sup>\" @@ -17,15 +21,20 @@ definition [si_def]: "pint = 0.56826125 \ litre" definition [si_def]: "hour = 3600 \ second" +definition [si_def]: "gram = milli\kilogram" + abbreviation "tonne \ kilo\kilogram" abbreviation "newton \ (kilogram \<^bold>\ meter) \<^bold>/ second\<^sup>\" abbreviation "volt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" -abbreviation "watt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" +definition "inch = 25.5\milli\meter" + +definition "foot = 0.3048\meter" + +definition "yard = 0.9144\meter" -abbreviation "joule \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" text\The full beauty of the approach is perhaps revealed here, with the type of a classical three-dimensional gravitation field:\ diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy index f104cae..9e6f42d 100644 --- a/src/SI/SI_Prefix.thy +++ b/src/SI/SI_Prefix.thy @@ -1,7 +1,7 @@ section \ SI Prefixes \ theory SI_Prefix - imports SI_Quantities + imports SI_Constants begin definition [si_def]: "giga = UNIT(1000000000, _)" diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy index f0641bb..570c437 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/SI_Proof.thy @@ -1,12 +1,12 @@ theory SI_Proof - imports SI_Derived + imports SI_Quantities begin section \ Tactic Support for SI type expressions. \ lemmas [si_def] = si_sem_Length_def si_sem_Mass_def si_sem_Time_def si_sem_Current_def si_sem_Temperature_def si_sem_Amount_def - si_sem_Intensity_def + si_sem_Intensity_def si_sem_NoDimension_def si_sem_UnitTimes_def si_sem_UnitInv_def times_Unit_ext_def one_Unit_ext_def @@ -19,48 +19,49 @@ lemma "SI(I) = 1\Amperes := 1\" by(simp add: si_def) lemma "SI(\) = 1\Kelvins := 1\ " by(simp add: si_def) lemma "SI(N) = 1\Moles := 1\" by(simp add: si_def) lemma "SI(J) = 1\Candelas := 1\" by(simp add: si_def) +lemma "SI(\) = 1" by(simp add: si_def) lemma "SI(N \ \ \ N) = SI(\ \ N\<^sup>2)" by(simp add: si_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Time) = \magn = x, - unit = \Seconds = 1, Meters = 0, Kilograms = 0, Amperes = 0, + unit = \Meters = 0, Kilograms = 0, Seconds = 1, Amperes = 0, Kelvins = 0, Moles = 0, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Time_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Length) = \magn = x, - unit = \Seconds = 0, Meters = 1, Kilograms = 0, Amperes = 0, + unit = \Meters = 1, Kilograms = 0, Seconds = 0, Amperes = 0, Kelvins = 0, Moles = 0, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Length_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Mass) = \magn = x, - unit = \Seconds = 0, Meters = 0, Kilograms = 1, Amperes = 0, + unit = \Meters = 0, Kilograms = 1, Seconds = 0, Amperes = 0, Kelvins = 0, Moles = 0, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Mass_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Current) = \magn = x, - unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 1, + unit = \Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 1, Kelvins = 0, Moles = 0, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Current_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Temperature) = \magn = x, - unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + unit = \Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, Kelvins = 1, Moles = 0, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Temperature_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Amount) = \magn = x, - unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + unit = \Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, Kelvins = 0, Moles = 1, Candelas = 0\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Amount_def) lemma [si_def]:"fromUnit UNIT(x::'a::one, Intensity) = \magn = x, - unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + unit = \Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, Kelvins = 0, Moles = 0, Candelas = 1\\" by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Intensity_def) @@ -109,6 +110,7 @@ lemma Unit_inverse_weak_cong: shows "(X)\<^sup>-\<^sup>\ \\<^sub>Q (Y)\<^sup>-\<^sup>\" using assms by (transfer, simp) +(* text\In order to compute a normal form, we would additionally need these three:\ (* field ? *) lemma Unit_inverse_distrib: @@ -154,6 +156,6 @@ lemma "watt \<^bold>\ hour \\<^sub>Q 3600 \<^bold>\ joule" lemma "watt \<^bold>\ hour \\<^sub>Q 3.6 \<^bold>\ kilo \<^bold>\ joule" oops - +*) end \ No newline at end of file diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index e04ba26..d0a365e 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -18,7 +18,8 @@ lemma Quantity_eq_intro: instantiation Quantity_ext :: (times, times) times begin - definition "times_Quantity_ext x y = \ magn = magn x \ magn y, unit = unit x \ unit y, \ = more x \ more y \" + definition [si_def]: + "times_Quantity_ext x y = \ magn = magn x \ magn y, unit = unit x \ unit y, \ = more x \ more y \" instance .. end @@ -38,7 +39,7 @@ lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def) instantiation Quantity_ext :: (one, one) one begin - definition "one_Quantity_ext = \ magn = 1, unit = 1, \ = 1 \" + definition [si_def]: "one_Quantity_ext = \ magn = 1, unit = 1, \ = 1 \" instance .. end @@ -48,8 +49,8 @@ lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def) instantiation Quantity_ext :: (inverse, inverse) inverse begin - definition "inverse_Quantity_ext x = \ magn = inverse (magn x), unit = inverse (unit x), \ = inverse (more x) \" - definition "divide_Quantity_ext x y = \ magn = magn x / magn y, unit = unit x / unit y, \ = more x / more y \" + definition [si_def]: "inverse_Quantity_ext x = \ magn = inverse (magn x), unit = inverse (unit x), \ = inverse (more x) \" + definition [si_def]: "divide_Quantity_ext x y = \ magn = magn x / magn y, unit = unit x / unit y, \ = more x / more y \" instance .. end @@ -300,8 +301,6 @@ translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)" subsection \Polymorphic Operations for Elementary SI Units \ -named_theorems si_def - definition [si_def]: "meter = UNIT(1, Length)" definition [si_def]: "second = UNIT(1, Time)" definition [si_def]: "kilogram = UNIT(1, Mass)" @@ -321,6 +320,16 @@ lemma unit_eq_iff_magn_eq: "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" by (auto simp add: magnQuant_def, transfer, simp) +lemma unit_equiv_iff: + fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]" + shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ SI('u\<^sub>1) = SI('u\<^sub>2)" +proof - + have "\t ta. (ta::'a['u\<^sub>2]) = t \ magn (fromUnit ta) \ magn (fromUnit t)" + by (simp add: magnQuant_def unit_eq_iff_magn_eq) + then show ?thesis + by (metis (full_types) Quant_equiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def) +qed + lemma unit_le_iff_magn_le: "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" by (auto simp add: magnQuant_def; (transfer, simp)) @@ -340,6 +349,12 @@ lemma magnQuant_times [si_def]: "\x * y\\<^sub>Q = \x\x / y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp) +lemma magnQuant_qinv [si_def]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_qdiv [si_def]: "\(x::('a::field)[_]) \<^bold>/ y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp add: field_class.field_divide_inverse) + lemma magnQuant_numeral [si_def]: "\numeral n\\<^sub>Q = numeral n" apply (induct n, simp_all add: si_def) apply (metis magnQuant_plus numeral_code(2)) diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index bce5905..e899f20 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -6,6 +6,8 @@ theory SI_Units "HOL-Eisbach.Eisbach" begin +named_theorems si_def + text\ The International System of Units (SI, abbreviated from the French Système international (d'unités)) is the modern form of the metric @@ -46,21 +48,28 @@ text \ An SI unit associates with each of the seven base unit an integer t to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \ record Unit = - Seconds :: int - Meters :: int - Kilograms :: int + Meters :: int + Kilograms :: int + Seconds :: int Amperes :: int Kelvins :: int Moles :: int Candelas :: int +text \ Units scaled by a power of 10 \ + +type_synonym SUnit = "int Unit_ext" + +abbreviation scale :: "SUnit \ int" where +"scale \ more" + text \ We define a commutative monoid for SI units. \ instantiation Unit_ext :: (one) one begin \ \ Here, $1$ is the dimensionless unit \ definition one_Unit_ext :: "'a Unit_ext" - where [code_unfold]: "1 = \ Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0 + where [code_unfold, si_def]: "1 = \ Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0 , Kelvins = 0, Moles = 0, Candelas = 0, \ = 1 \" instance .. end @@ -69,9 +78,9 @@ instantiation Unit_ext :: (times) times begin \ \ Multiplication is defined by adding together the powers \ definition times_Unit_ext :: "'a Unit_ext \ 'a Unit_ext \ 'a Unit_ext" - where [code_unfold]: - "x * y = \ Seconds = Seconds x + Seconds y, Meters = Meters x + Meters y - , Kilograms = Kilograms x + Kilograms y, Amperes = Amperes x + Amperes y + where [code_unfold, si_def]: + "x * y = \ Meters = Meters x + Meters y, Kilograms = Kilograms x + Kilograms y + , Seconds = Seconds x + Seconds y, Amperes = Amperes x + Amperes y , Kelvins = Kelvins x + Kelvins y, Moles = Moles x + Moles y , Candelas = Candelas x + Candelas y, \ = more x * more y \" instance .. @@ -93,9 +102,9 @@ text \ We also define the inverse and division operations, and an abelian instantiation Unit_ext :: ("{times,inverse}") inverse begin definition inverse_Unit_ext :: "'a Unit_ext \ 'a Unit_ext" - where [code_unfold]: - "inverse x = \ Seconds = - Seconds x , Meters = - Meters x - , Kilograms = - Kilograms x, Amperes = - Amperes x + where [code_unfold, si_def]: + "inverse x = \ Meters = - Meters x, Kilograms = - Kilograms x + , Seconds = - Seconds x, Amperes = - Amperes x , Kelvins = - Kelvins x, Moles = - Moles x , Candelas = - Candelas x, \ = inverse (more x) \" @@ -155,13 +164,32 @@ subsection \ Basic SI-types \ text \ We provide a syntax for type-expressions; The definition of the basic type constructors is straight-forward via a one-elementary set. \ -typedef Length ("L") = "UNIV :: unit set" .. setup_lifting type_definition_Length -typedef Mass ("M") = "UNIV :: unit set" .. setup_lifting type_definition_Mass -typedef Time ("T") = "UNIV :: unit set" .. setup_lifting type_definition_Time -typedef Current ("I") = "UNIV :: unit set" .. setup_lifting type_definition_Current -typedef Temperature ("\") = "UNIV :: unit set" .. setup_lifting type_definition_Temperature -typedef Amount ("N") = "UNIV :: unit set" .. setup_lifting type_definition_Amount -typedef Intensity ("J") = "UNIV :: unit set" .. setup_lifting type_definition_Intensity +typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length +typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass +typedef Time = "UNIV :: unit set" .. setup_lifting type_definition_Time +typedef Current = "UNIV :: unit set" .. setup_lifting type_definition_Current +typedef Temperature = "UNIV :: unit set" .. setup_lifting type_definition_Temperature +typedef Amount = "UNIV :: unit set" .. setup_lifting type_definition_Amount +typedef Intensity = "UNIV :: unit set" .. setup_lifting type_definition_Intensity +typedef NoDimension = "UNIV :: unit set" .. setup_lifting type_definition_NoDimension + +type_synonym M = Mass +type_synonym L = Length +type_synonym T = Time +type_synonym I = Current +type_synonym \ = Temperature +type_synonym N = Amount +type_synonym J = Intensity +type_notation NoDimension ("\") + +translations + (type) "M" <= (type) "Mass" + (type) "L" <= (type) "Length" + (type) "T" <= (type) "Time" + (type) "I" <= (type) "Current" + (type) "\" <= (type) "Temperature" + (type) "N" <= (type) "Amount" + (type) "J" <= (type) "Intensity" subsection \ SI-type expressions and SI-type interpretation \ @@ -238,6 +266,12 @@ begin instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseUnit_def, (transfer, simp)+) end +instantiation NoDimension :: si_type +begin + definition si_sem_NoDimension :: "NoDimension itself \ Unit" where "si_sem_NoDimension x = 1" + instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseUnit_def, (transfer, simp)+) +end + lemma base_units [simp]: "is_BaseUnit SI(Length)" "is_BaseUnit SI(Mass)" "is_BaseUnit SI(Time)" "is_BaseUnit SI(Current)" "is_BaseUnit SI(Temperature)" "is_BaseUnit SI(Amount)" @@ -313,5 +347,9 @@ type_synonym Frequency = "T\<^sup>-\<^sup>1" type_synonym Energy = "L\<^sup>2\M\T\<^sup>-\<^sup>2" type_synonym Power = "L\<^sup>2\M\T\<^sup>-\<^sup>3" type_synonym Force = "L\M\T\<^sup>-\<^sup>2" - +type_synonym Pressure = "L\<^sup>-\<^sup>1\M\T\<^sup>-\<^sup>2" +type_synonym Charge = "I\T" +type_synonym PotentialDifference = "L\<^sup>2\M\T\<^sup>-\<^sup>3\I\<^sup>-\<^sup>1" +type_synonym Capacitance = "L\<^sup>-\<^sup>2\M\<^sup>-\<^sup>1\T\<^sup>4\I\<^sup>2" + end \ No newline at end of file