From c104f1e2b2ed1f6c3e69f4fe7dee8fe6516e0d7f Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Tue, 18 Feb 2020 20:25:45 +0000 Subject: [PATCH] Added the the scaleQ function that should allow removal of the scalar product operator --- src/SI/SI_Constants.thy | 20 ++++++++++---------- src/SI/SI_Derived.thy | 26 +++++++++++++------------- src/SI/SI_Prefix.thy | 24 ++++++++++++++---------- src/SI/SI_Quantities.thy | 10 ++++++++++ 4 files changed, 47 insertions(+), 33 deletions(-) diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index e82fc31..71e66d6 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -24,31 +24,31 @@ text \ The most general types we support must form a field into which the default_sort field_char_0 abbreviation (input) caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\v\<^sub>C\<^sub>s") where - "caesium_frequency \ 9192631770\hertz" + "caesium_frequency \ 9192631770 \ hertz" abbreviation speed_of_light :: "'a[L \ T\<^sup>-\<^sup>1]" where - "speed_of_light \ 299792458\(meter\<^bold>\second\<^sup>-\<^sup>\)" + "speed_of_light \ 299792458 \ (meter\<^bold>\second\<^sup>-\<^sup>\)" abbreviation Planck :: "'a[M \ L\<^sup>2 \ T\<^sup>-\<^sup>2 \ T]" where - "Planck \ (6.62607015 \ 1/(10^34))\(joule\<^bold>\second)" + "Planck \ (6.62607015 \ 1/(10^34)) \ (joule\<^bold>\second)" abbreviation elementary_charge :: "'a[I \ T]" where - "elementary_charge \ (1.602176634 \ 1/(10^19))\coulomb" + "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)" + "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>\)" +"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" +"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)" +"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>\)" + "gravitational_constant \ (6.6743015 \ 1/(10 ^ 11)) \ (meter\<^sup>\\<^bold>\kilogram\<^sup>-\<^sup>\\<^bold>\second\<^sup>-\<^sup>\)" thm si_def @@ -59,7 +59,7 @@ theorem Quant_eq_iff_same_dim: 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" +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 diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index eed8259..7408191 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -7,33 +7,33 @@ begin definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where [si_def]: "degree = (2\(UNIT(of_real 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_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 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>\" +definition [si_def]: "litre = 1/1000 \ meter\<^sup>\" -definition [si_def]: "pint = 0.56826125 \ litre" +definition [si_def]: "pint = 0.56826125 \ litre" -definition [si_def]: "hour = 3600 \ second" +definition [si_def]: "hour = 3600 \ second" -definition [si_def]: "gram = milli\kilogram" +definition [si_def]: "gram = milli \ kilogram" -abbreviation "tonne \ kilo\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>\" -definition "inch = 25.5\milli\meter" +definition "inch = 25.5 \ milli \ meter" -definition "foot = 0.3048\meter" +definition "foot = 0.3048 \ meter" -definition "yard = 0.9144\meter" +definition "yard = 0.9144 \ meter" text\The full beauty of the approach is perhaps revealed here, with the diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy index 9e6f42d..0ed5bd9 100644 --- a/src/SI/SI_Prefix.thy +++ b/src/SI/SI_Prefix.thy @@ -4,24 +4,28 @@ theory SI_Prefix imports SI_Constants begin -definition [si_def]: "giga = UNIT(1000000000, _)" +definition [si_def]: "deca = 10^1" -definition [si_def]: "mega = UNIT(1000000, _)" +definition [si_def]: "hecto = 10^2" -definition [si_def]: "kilo = UNIT(1000, _)" +definition [si_def]: "kilo = 10^3" -definition [si_def]: "hecto = UNIT(100, _)" +definition [si_def]: "mega = 10^6" -definition [si_def]: "deca = UNIT(10, _)" +definition [si_def]: "giga = 10^9" -definition [si_def]: "deci = UNIT(0.1, _)" +definition [si_def]: "tera = 10^12" -definition [si_def]: "centi = UNIT(0.01, _)" +definition [si_def]: "peta = 10^15" -definition [si_def]: "milli = UNIT(0.001, _)" +definition [si_def]: "deci = 1/10^1" -definition [si_def]: "micro = UNIT(0.000001, _)" +definition [si_def]: "centi = 1/10^2" -definition [si_def]: "nano = UNIT(0.000000001, _)" +definition [si_def]: "milli = 1/10^3" + +definition [si_def]: "micro = 1/10^6" + +definition [si_def]: "nano = 1/10^9" end \ No newline at end of file diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index d0a365e..0da6757 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -292,6 +292,10 @@ begin instance by (intro_classes, (transfer, simp add: less_le_not_le)+) end +lift_definition scaleQ :: "'a \ 'a::times['u::si_type] \ 'a['u]" (infixr "*\<^sub>Q" 63) + is "\ r x. \ magn = r * magn x, unit = SI('u) \" by simp + +notation scaleQ (infixr "\" 63) lift_definition mk_unit :: "'a \ 'u itself \ ('a::one)['u::si_type]" is "\ n u. \ magn = n, unit = SI('u) \" by simp @@ -309,6 +313,9 @@ definition [si_def]: "kelvin = UNIT(1, Temperature)" definition [si_def]: "mole = UNIT(1, Amount)" definition [si_def]: "candela = UNIT(1, Intensity)" +definition dimless ("\") + where [si_def]: "dimless = UNIT(1, NoDimension)" + subsubsection \The Projection: Stripping the SI-Tags \ definition magnQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where @@ -346,6 +353,9 @@ lemma magnQuant_plus [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_scaleQ [si_def]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + lemma magnQuant_div [si_def]: "\x / y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp)