Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Added the the scaleQ function that should allow removal of the scalar product operator

This commit is contained in:
Simon Foster 2020-02-18 20:25:45 +00:00
parent 2c63ef07e9
commit c104f1e2b2
4 changed files with 47 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/SI/SI_Constants.thy
View File

@ -24,31 +24,31 @@ text \<open> 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]" ("\<Delta>v\<^sub>C\<^sub>s") where
"caesium_frequency \<equiv> 9192631770\<cdot>hertz"
"caesium_frequency \<equiv> 9192631770 \<odot> hertz"
abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" where
"speed_of_light \<equiv> 299792458\<cdot>(meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
"speed_of_light \<equiv> 299792458 \<odot> (meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" where
"Planck \<equiv> (6.62607015 \<cdot> 1/(10^34))\<cdot>(joule\<^bold>\<cdot>second)"
"Planck \<equiv> (6.62607015 \<cdot> 1/(10^34)) \<odot> (joule\<^bold>\<cdot>second)"
abbreviation elementary_charge :: "'a[I \<cdot> T]" where
"elementary_charge \<equiv> (1.602176634 \<cdot> 1/(10^19))\<cdot>coulomb"
"elementary_charge \<equiv> (1.602176634 \<cdot> 1/(10^19)) \<odot> coulomb"
abbreviation Boltzmann :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> \<Theta>\<^sup>-\<^sup>1]" where
"Boltzmann \<equiv> (1.380649\<cdot>1/(10^23))\<cdot>(joule \<^bold>/ kelvin)"
"Boltzmann \<equiv> (1.380649\<cdot>1/(10^23)) \<odot> (joule \<^bold>/ kelvin)"
abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" where
"Avogadro \<equiv> 6.02214076\<cdot>(10^23)\<cdot>(mole\<^sup>-\<^sup>\<one>)"
"Avogadro \<equiv> 6.02214076\<cdot>(10^23) \<odot> (mole\<^sup>-\<^sup>\<one>)"
abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where
"max_luminous_frequency \<equiv> (540\<cdot>10^12)\<cdot>hertz"
"max_luminous_frequency \<equiv> (540\<cdot>10^12) \<odot> hertz"
abbreviation luminous_efficacy :: "'a[J \<cdot> (L\<^sup>2 \<cdot> L\<^sup>-\<^sup>2) \<cdot> (M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" where
"luminous_efficacy \<equiv> 683\<cdot>(lumen\<^bold>/watt)"
"luminous_efficacy \<equiv> 683 \<odot> (lumen\<^bold>/watt)"
abbreviation gravitational_constant :: "'a[L\<^sup>3 \<cdot> M\<^sup>-\<^sup>1 \<cdot> T\<^sup>-\<^sup>2]" where
"gravitational_constant \<equiv> (6.6743015 \<cdot> 1/(10 ^ 11)) \<cdot> (meter\<^sup>\<three>\<^bold>\<cdot>kilogram\<^sup>-\<^sup>\<one>\<^bold>\<cdot>second\<^sup>-\<^sup>\<two>)"
"gravitational_constant \<equiv> (6.6743015 \<cdot> 1/(10 ^ 11)) \<odot> (meter\<^sup>\<three>\<^bold>\<cdot>kilogram\<^sup>-\<^sup>\<one>\<^bold>\<cdot>second\<^sup>-\<^sup>\<two>)"
thm si_def
@ -59,7 +59,7 @@ theorem Quant_eq_iff_same_dim:
theorem hertz_definition: "1\<cdot>hertz = \<Delta>v\<^sub>C\<^sub>s / 9192631770"
by (simp add: unit_eq_iff_magn_eq si_def)
theorem second_definition: "1\<cdot>second \<approx>\<^sub>Q (9192631770::_[\<one>]) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
theorem second_definition: "1\<cdot>second \<approx>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>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

26
src/SI/SI_Derived.thy
View File

@ -7,33 +7,33 @@ begin
definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where
[si_def]: "degree = (2\<cdot>(UNIT(of_real pi,_)) / 180)\<cdot>radian"
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n\<cdot>degree"
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odot> degree"
definition degrees_celcius :: "'a::division_ring[\<Theta>] \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
where [si_def]: "degrees_celcius x = (x + 273.151)\<cdot>kelvin"
definition degrees_celcius :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
where [si_def]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
definition degrees_farenheit :: "'a::division_ring[\<Theta>] \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_def]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9\<cdot>kelvin"
definition degrees_farenheit :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_def]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
definition [si_def]: "litre = 1/1000 \<cdot> meter\<^sup>\<three>"
definition [si_def]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
definition [si_def]: "pint = 0.56826125 \<cdot> litre"
definition [si_def]: "pint = 0.56826125 \<odot> litre"
definition [si_def]: "hour = 3600 \<cdot> second"
definition [si_def]: "hour = 3600 \<odot> second"
definition [si_def]: "gram = milli\<cdot>kilogram"
definition [si_def]: "gram = milli \<odot> kilogram"
abbreviation "tonne \<equiv> kilo\<cdot>kilogram"
abbreviation "tonne \<equiv> kilo \<odot> kilogram"
abbreviation "newton \<equiv> (kilogram \<^bold>\<cdot> meter) \<^bold>/ second\<^sup>\<two>"
abbreviation "volt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
definition "inch = 25.5\<cdot>milli\<cdot>meter"
definition "inch = 25.5 \<odot> milli \<odot> meter"
definition "foot = 0.3048\<cdot>meter"
definition "foot = 0.3048 \<odot> meter"
definition "yard = 0.9144\<cdot>meter"
definition "yard = 0.9144 \<odot> meter"
text\<open>The full beauty of the approach is perhaps revealed here, with the

24
src/SI/SI_Prefix.thy
View File

@ -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

10
src/SI/SI_Quantities.thy
View File

@ -292,6 +292,10 @@ begin
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
end
lift_definition scaleQ :: "'a \<Rightarrow> 'a::times['u::si_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
is "\<lambda> r x. \<lparr> magn = r * magn x, unit = SI('u) \<rparr>" by simp
notation scaleQ (infixr "\<odot>" 63)
lift_definition mk_unit :: "'a \<Rightarrow> 'u itself \<Rightarrow> ('a::one)['u::si_type]"
is "\<lambda> n u. \<lparr> magn = n, unit = SI('u) \<rparr>" 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 ("\<one>")
where [si_def]: "dimless = UNIT(1, NoDimension)"
subsubsection \<open>The Projection: Stripping the SI-Tags \<close>
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
@ -346,6 +353,9 @@ lemma magnQuant_plus [si_def]: "\<lbrakk>x + y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rb
lemma magnQuant_times [si_def]: "\<lbrakk>x * y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q * \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magnQuant_def, transfer, simp)
lemma magnQuant_scaleQ [si_def]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magnQuant_def, transfer, simp)
lemma magnQuant_div [si_def]: "\<lbrakk>x / y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q / \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magnQuant_def, transfer, simp)