Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
1de90a23b2
|
|
@ -0,0 +1,29 @@
|
|||
section \<open> Non-SI Units Accepted for SI use \<close>
|
||||
|
||||
theory SI_Accepted
|
||||
imports SI_Derived
|
||||
begin
|
||||
|
||||
definition [si_def, si_eq]: "minute = 60 \<odot> second"
|
||||
|
||||
definition [si_def, si_eq]: "hour = 60 \<odot> minute"
|
||||
|
||||
definition [si_def, si_eq]: "day = 24 \<odot> hour"
|
||||
|
||||
definition [si_def, si_eq]: "astronomical_unit = 149597870700 \<odot> meter"
|
||||
|
||||
definition degree :: "'a::real_field[L/L]" where
|
||||
[si_def, si_eq]: "degree = (2\<cdot>(of_real pi) / 180) \<odot> radian"
|
||||
|
||||
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odot> degree"
|
||||
|
||||
definition [si_def, si_eq]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
|
||||
|
||||
abbreviation "tonne \<equiv> 10^3 \<odot> kilogram"
|
||||
|
||||
subsection \<open> Examples \<close>
|
||||
|
||||
lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"
|
||||
by (si_calc)
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,91 @@
|
|||
section \<open> Algebraic Laws \<close>
|
||||
|
||||
theory SI_Algebra
|
||||
imports SI_Proof
|
||||
begin
|
||||
|
||||
subsection \<open> Quantity Scale \<close>
|
||||
|
||||
lemma scaleQ_add_right: "a \<odot> x + y = (a \<odot> x) + (a \<odot> y)"
|
||||
by (transfer, simp add: distrib_left)
|
||||
|
||||
lemma scaleQ_add_left: "a + b \<odot> x = (a \<odot> x) + (b \<odot> x)"
|
||||
by (transfer, simp add: distrib_right)
|
||||
|
||||
lemma scaleQ_scaleQ: "a \<odot> b \<odot> x = a \<cdot> b \<odot> x"
|
||||
by (transfer, simp add: mult.assoc)
|
||||
|
||||
lemma scaleQ_one [simp]: "1 \<odot> x = x"
|
||||
by (transfer, simp)
|
||||
|
||||
lemma scaleQ_zero [simp]: "0 \<odot> x = 0"
|
||||
by (transfer, simp)
|
||||
|
||||
lemma scaleQ_inv: "-a \<odot> x = a \<odot> -x"
|
||||
by (transfer, simp)
|
||||
|
||||
lemma scaleQ_as_qprod: "a \<odot> x \<cong>\<^sub>Q (a \<odot> \<one>) \<^bold>\<cdot> x"
|
||||
unfolding si_def
|
||||
by (transfer, simp add: si_sem_NoDimension_def)
|
||||
|
||||
lemma mult_scaleQ_left [simp]: "(a \<odot> x) \<^bold>\<cdot> y = a \<odot> x \<^bold>\<cdot> y"
|
||||
by (transfer, simp add: si_sem_UnitTimes_def mult.assoc)
|
||||
|
||||
lemma mult_scaleQ_right [simp]: "x \<^bold>\<cdot> (a \<odot> y) = a \<odot> x \<^bold>\<cdot> y"
|
||||
by (transfer, simp add: si_sem_UnitTimes_def times_Quantity_ext_def mult.assoc)
|
||||
|
||||
subsection \<open> Field Laws \<close>
|
||||
|
||||
lemma qtimes_commute: "x \<^bold>\<cdot> y \<cong>\<^sub>Q y \<^bold>\<cdot> x"
|
||||
by si_calc
|
||||
|
||||
text\<open>Observe that this commutation law also commutes the types.\<close>
|
||||
|
||||
(* just a check that instantiation works for special cases ... *)
|
||||
lemma " (UNIT(x, J) \<^bold>\<cdot> UNIT(y::'a::comm_ring_1, N))
|
||||
\<cong>\<^sub>Q (UNIT(y, N) \<^bold>\<cdot> UNIT(x, J)) "
|
||||
by(simp add: qtimes_commute)
|
||||
|
||||
lemma qtimes_assoc: "(x \<^bold>\<cdot> y) \<^bold>\<cdot> z \<cong>\<^sub>Q x \<^bold>\<cdot> (y \<^bold>\<cdot> z)"
|
||||
by (si_calc)
|
||||
|
||||
lemma qtimes_left_unit: "\<one> \<^bold>\<cdot> x \<cong>\<^sub>Q x"
|
||||
by (si_calc)
|
||||
|
||||
lemma qtimes_right_unit: "x \<^bold>\<cdot> \<one> \<cong>\<^sub>Q x"
|
||||
by (si_calc)
|
||||
|
||||
text\<open>The following weak congruences will allow for replacing equivalences in contexts
|
||||
built from product and inverse. \<close>
|
||||
|
||||
lemma qtimes_weak_cong_left:
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "x\<^bold>\<cdot>z \<cong>\<^sub>Q y\<^bold>\<cdot>z"
|
||||
using assms by si_calc
|
||||
|
||||
lemma qtimes_weak_cong_right:
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "z\<^bold>\<cdot>x \<cong>\<^sub>Q z\<^bold>\<cdot>y"
|
||||
using assms by si_calc
|
||||
|
||||
lemma qinverse_weak_cong:
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "x\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y\<^sup>-\<^sup>\<one>"
|
||||
using assms by si_calc
|
||||
|
||||
lemma qinverse_qinverse: "x\<^sup>-\<^sup>\<one>\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x"
|
||||
by si_calc
|
||||
|
||||
lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\<one> = 0 \<longleftrightarrow> x = 0"
|
||||
by si_calc
|
||||
|
||||
lemma qinverse_qtimes: "(x \<^bold>\<cdot> y)\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x\<^sup>-\<^sup>\<one> \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
|
||||
by si_calc
|
||||
|
||||
lemma qinverse_qdivide: "(x \<^bold>/ y)\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y \<^bold>/ x"
|
||||
by si_calc
|
||||
|
||||
lemma qtimes_cancel: "x \<noteq> 0 \<Longrightarrow> x \<^bold>/ x \<cong>\<^sub>Q \<one>"
|
||||
by si_calc
|
||||
|
||||
end
|
||||
|
|
@ -1,13 +1,76 @@
|
|||
section \<open> Physical Constants \<close>
|
||||
|
||||
theory SI_Constants
|
||||
imports SI_Quantities
|
||||
imports SI_Proof
|
||||
begin
|
||||
|
||||
abbreviation speed_of_light :: "'a::division_ring[L \<cdot> T\<^sup>-\<^sup>1]" where
|
||||
"speed_of_light \<equiv> 299792458\<cdot>(meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
|
||||
subsection \<open> Core Derived Units \<close>
|
||||
|
||||
abbreviation gravitational_constant 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>)"
|
||||
abbreviation "hertz \<equiv> second\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "radian \<equiv> meter \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "steradian \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "joule \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "watt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three>"
|
||||
|
||||
abbreviation "coulomb \<equiv> ampere \<^bold>\<cdot> second"
|
||||
|
||||
abbreviation "lumen \<equiv> candela \<^bold>\<cdot> steradian"
|
||||
|
||||
subsection \<open> Constants \<close>
|
||||
|
||||
text \<open> The most general types we support must form a field into which the natural numbers can
|
||||
be injected. \<close>
|
||||
|
||||
default_sort field_char_0
|
||||
|
||||
text \<open> Hyperfine transition frequency of frequency of Cs \<close>
|
||||
|
||||
abbreviation caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\<Delta>v\<^sub>C\<^sub>s") where
|
||||
"caesium_frequency \<equiv> 9192631770 \<odot> hertz"
|
||||
|
||||
text \<open> Speed of light in vacuum \<close>
|
||||
|
||||
abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" ("\<^bold>c") where
|
||||
"speed_of_light \<equiv> 299792458 \<odot> (meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
|
||||
|
||||
text \<open> Planck constant \<close>
|
||||
|
||||
abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" ("\<^bold>h") where
|
||||
"Planck \<equiv> (6.62607015 \<cdot> 1/(10^34)) \<odot> (joule\<^bold>\<cdot>second)"
|
||||
|
||||
text \<open> Elementary charge \<close>
|
||||
|
||||
abbreviation elementary_charge :: "'a[I \<cdot> T]" ("\<^bold>e") where
|
||||
"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]" ("\<^bold>k") where
|
||||
"Boltzmann \<equiv> (1.380649\<cdot>1/(10^23)) \<odot> (joule \<^bold>/ kelvin)"
|
||||
|
||||
abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" ("N\<^sub>A") where
|
||||
"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) \<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]" ("K\<^sub>c\<^sub>d") where
|
||||
"luminous_efficacy \<equiv> 683 \<odot> (lumen\<^bold>/watt)"
|
||||
|
||||
theorem second_definition:
|
||||
"1 \<odot> second \<cong>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
|
||||
by si_calc
|
||||
|
||||
theorem meter_definition:
|
||||
"1 \<odot> meter \<cong>\<^sub>Q (\<^bold>c \<^bold>/ (299792458 \<odot> \<one>))\<^bold>\<cdot>second"
|
||||
"1 \<odot> meter \<cong>\<^sub>Q (9192631770 / 299792458) \<odot> (\<^bold>c \<^bold>/ \<Delta>v\<^sub>C\<^sub>s)"
|
||||
by si_calc+
|
||||
|
||||
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)) \<odot> (meter\<^sup>\<three>\<^bold>\<cdot>kilogram\<^sup>-\<^sup>\<one>\<^bold>\<cdot>second\<^sup>-\<^sup>\<two>)"
|
||||
|
||||
default_sort type
|
||||
|
||||
end
|
||||
|
|
@ -2,30 +2,35 @@ section \<open> Derived Units\<close>
|
|||
|
||||
theory SI_Derived
|
||||
imports SI_Prefix
|
||||
begin
|
||||
begin
|
||||
|
||||
definition "radian = 1 \<cdot> (meter \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one>)"
|
||||
subsection \<open> Definitions \<close>
|
||||
|
||||
definition degree :: "real[L/L]" where
|
||||
[si_def]: "degree = (2\<cdot>(UNIT(pi,_)) / 180)\<cdot>radian"
|
||||
abbreviation "newton \<equiv> kilogram \<^bold>\<cdot> meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n\<cdot>degree"
|
||||
|
||||
definition [si_def]: "litre = 1/1000 \<cdot> meter\<^sup>\<three>"
|
||||
|
||||
definition [si_def]: "pint = 0.56826125 \<cdot> litre"
|
||||
|
||||
definition [si_def]: "hour = 3600 \<cdot> second"
|
||||
|
||||
abbreviation "tonne \<equiv> kilo\<cdot>kilogram"
|
||||
|
||||
abbreviation "newton \<equiv> (kilogram \<^bold>\<cdot> meter) \<^bold>/ second\<^sup>\<two>"
|
||||
abbreviation "pascal \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "volt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "watt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three>"
|
||||
abbreviation "farad \<equiv> kilogram\<^sup>-\<^sup>\<one> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two> \<^bold>\<cdot> second\<^sup>\<four> \<^bold>\<cdot> ampere\<^sup>\<two>"
|
||||
|
||||
abbreviation "joule \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
abbreviation "ohm \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "siemens \<equiv> kilogram\<^sup>-\<^sup>\<one> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two> \<^bold>\<cdot> second\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>\<two>"
|
||||
|
||||
abbreviation "weber \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "tesla \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "henry \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<two>"
|
||||
|
||||
definition degrees_celcius :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
|
||||
where [si_def, si_eq]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
|
||||
|
||||
definition degrees_farenheit :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
|
||||
where [si_def, si_eq]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
|
||||
|
||||
definition [si_def, si_eq]: "gram = milli \<odot> kilogram"
|
||||
|
||||
text\<open>The full beauty of the approach is perhaps revealed here, with the
|
||||
type of a classical three-dimensional gravitation field:\<close>
|
||||
|
|
|
|||
|
|
@ -0,0 +1,15 @@
|
|||
section \<open> Imperial Units via SI \<close>
|
||||
|
||||
theory SI_Imperial
|
||||
imports SI_Accepted
|
||||
begin
|
||||
|
||||
definition [si_def, si_eq]: "pint = 0.56826125 \<odot> litre"
|
||||
|
||||
definition [si_def, si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
|
||||
|
||||
definition [si_def, si_eq]: "foot = 0.3048 \<odot> meter"
|
||||
|
||||
definition [si_def, si_eq]: "yard = 0.9144 \<odot> meter"
|
||||
|
||||
end
|
||||
|
|
@ -1,27 +1,31 @@
|
|||
section \<open> SI Prefixes \<close>
|
||||
|
||||
theory SI_Prefix
|
||||
imports SI_Quantities
|
||||
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
|
||||
|
|
@ -1,12 +1,73 @@
|
|||
section \<open> Tactic Support for SI type expressions. \<close>
|
||||
|
||||
theory SI_Proof
|
||||
imports SI_Derived
|
||||
imports SI_Quantities
|
||||
begin
|
||||
|
||||
section \<open> Tactic Support for SI type expressions. \<close>
|
||||
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
|
||||
[si_def]: "magnQuant x = magn (fromQ x)"
|
||||
|
||||
lemma unit_eq_iff_magn_eq:
|
||||
"x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^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 \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> SI('u\<^sub>1) = SI('u\<^sub>2)"
|
||||
proof -
|
||||
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> magn (fromQ ta) \<noteq> magn (fromQ t)"
|
||||
by (simp add: magnQuant_def unit_eq_iff_magn_eq)
|
||||
then show ?thesis
|
||||
by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def)
|
||||
qed
|
||||
|
||||
lemma unit_le_iff_magn_le:
|
||||
"x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (auto simp add: magnQuant_def; (transfer, simp))
|
||||
|
||||
lemma magnQuant_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_plus [si_eq]: "\<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_eq]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_qtimes [si_eq]: "\<lbrakk>x \<^bold>\<cdot> y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q \<cdot> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_qinverse [si_eq]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_qdivivide [si_eq]: "\<lbrakk>(x::('a::field)[_]) \<^bold>/ y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q / \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp add: field_class.field_divide_inverse)
|
||||
|
||||
lemma magnQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
|
||||
apply (induct n, simp_all add: si_def)
|
||||
apply (metis magnQuant_def magnQuant_one)
|
||||
apply (metis magnQuant_def magnQuant_plus numeral_code(2))
|
||||
apply (metis magnQuant_def magnQuant_one magnQuant_plus numeral_code(3))
|
||||
done
|
||||
|
||||
lemma magnQuant_mk [si_eq]: "\<lbrakk>UNIT(n, 'u::si_type)\<rbrakk>\<^sub>Q = n"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
method si_calc uses simps =
|
||||
(simp add: unit_equiv_iff unit_eq_iff_magn_eq unit_le_iff_magn_le si_eq simps)
|
||||
|
||||
lemmas [si_eq] = 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_NoDimension_def
|
||||
si_sem_UnitTimes_def si_sem_UnitInv_def
|
||||
inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def
|
||||
|
||||
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,141 +80,8 @@ lemma "SI(I) = 1\<lparr>Amperes := 1\<rparr>" by(simp add: si_def)
|
|||
lemma "SI(\<Theta>) = 1\<lparr>Kelvins := 1\<rparr> " by(simp add: si_def)
|
||||
lemma "SI(N) = 1\<lparr>Moles := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(J) = 1\<lparr>Candelas := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(\<one>) = 1" by(simp add: si_def)
|
||||
|
||||
lemma "SI(N \<cdot> \<Theta> \<cdot> N) = SI(\<Theta> \<cdot> N\<^sup>2)" by(simp add: si_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Time) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 1, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Time_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Length) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 1, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Length_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Mass) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 1, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Mass_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Current) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 1,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Current_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Temperature) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 1, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Temperature_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Amount) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 1, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Amount_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, Intensity) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 1\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Intensity_def)
|
||||
|
||||
lemma Unit_times_commute:
|
||||
fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"and Y::"'a['c::si_type]"
|
||||
shows "X \<^bold>\<cdot> Y \<approx>\<^sub>Q Y \<^bold>\<cdot> X"
|
||||
by (transfer, simp add: mult.commute times_Quantity_ext_def)
|
||||
|
||||
text\<open>Observe that this commutation law also commutes the types.\<close>
|
||||
|
||||
(* just a check that instantiation works for special cases ... *)
|
||||
lemma " (UNIT(x, J) \<^bold>\<cdot> UNIT(y::'a::{one,ab_semigroup_mult}, N))
|
||||
\<approx>\<^sub>Q (UNIT(y, N) \<^bold>\<cdot> UNIT(x, J)) "
|
||||
by(simp add: Unit_times_commute)
|
||||
|
||||
|
||||
lemma Unit_times_assoc:
|
||||
fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
|
||||
and Y::"'a['c::si_type]"
|
||||
and Z::"'a['d::si_type]"
|
||||
shows "(X \<^bold>\<cdot> Y) \<^bold>\<cdot> Z \<approx>\<^sub>Q X \<^bold>\<cdot> (Y \<^bold>\<cdot> Z)"
|
||||
by (transfer, simp add: mult.commute mult.left_commute times_Quantity_ext_def)
|
||||
|
||||
text\<open>The following weak congruences will allow for replacing equivalences in contexts
|
||||
built from product and inverse. \<close>
|
||||
lemma Unit_times_weak_cong_left:
|
||||
fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
|
||||
and Y::"'a['c::si_type]"
|
||||
and Z::"'a['d::si_type]"
|
||||
assumes "X \<approx>\<^sub>Q Y"
|
||||
shows "(X \<^bold>\<cdot> Z) \<approx>\<^sub>Q (Y \<^bold>\<cdot> Z)"
|
||||
using assms by (transfer, simp)
|
||||
|
||||
lemma Unit_times_weak_cong_right:
|
||||
fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
|
||||
and Y::"'a['c::si_type]"
|
||||
and Z::"'a['d::si_type]"
|
||||
assumes "X \<approx>\<^sub>Q Y"
|
||||
shows "(Z \<^bold>\<cdot> X) \<approx>\<^sub>Q (Z \<^bold>\<cdot> Y)"
|
||||
using assms by (transfer, simp)
|
||||
|
||||
lemma Unit_inverse_weak_cong:
|
||||
fixes X::"'a::{field}['b::si_type]"
|
||||
and Y::"'a['c::si_type]"
|
||||
assumes "X \<approx>\<^sub>Q Y"
|
||||
shows "(X)\<^sup>-\<^sup>\<one> \<approx>\<^sub>Q (Y)\<^sup>-\<^sup>\<one>"
|
||||
using assms by (transfer, simp)
|
||||
|
||||
text\<open>In order to compute a normal form, we would additionally need these three:\<close>
|
||||
(* field ? *)
|
||||
lemma Unit_inverse_distrib:
|
||||
fixes X::"'a::{field}['b::si_type]"
|
||||
and Y::"'a['c::si_type]"
|
||||
shows "(X \<^bold>\<cdot> Y)\<^sup>-\<^sup>\<one> \<approx>\<^sub>Q X\<^sup>-\<^sup>\<one> \<^bold>\<cdot> Y\<^sup>-\<^sup>\<one>"
|
||||
apply (transfer)
|
||||
sorry
|
||||
|
||||
(* field ? *)
|
||||
lemma Unit_inverse_inverse:
|
||||
fixes X::"'a::{field}['b::si_type]"
|
||||
shows "((X)\<^sup>-\<^sup>\<one>)\<^sup>-\<^sup>\<one> \<approx>\<^sub>Q X"
|
||||
apply transfer
|
||||
sorry
|
||||
|
||||
(* field ? *)
|
||||
lemma Unit_mult_cancel:
|
||||
fixes X::"'a::{field}['b::si_type]"
|
||||
shows "X \<^bold>/ X \<approx>\<^sub>Q 1"
|
||||
apply transfer
|
||||
sorry
|
||||
|
||||
|
||||
lemma Unit_mult_mult_Left_cancel:
|
||||
fixes X::"'a::{field}['b::si_type]"
|
||||
shows "(1::'a['b/'b]) \<^bold>\<cdot> X \<approx>\<^sub>Q X"
|
||||
apply transfer
|
||||
sorry
|
||||
|
||||
|
||||
lemma "watt \<^bold>\<cdot> hour \<approx>\<^sub>Q 3600 \<^bold>\<cdot> joule"
|
||||
unfolding Unit_equiv_def hour_def
|
||||
apply(simp add: Units.Unit_times.rep_eq si_def
|
||||
zero_SI_tagged_domain_ext_def times_SI_tagged_domain_ext_def
|
||||
inverse_SI_tagged_domain_ext_def
|
||||
Unit_inverse_def Unit_times_def)
|
||||
find_theorems fromUnit
|
||||
oops
|
||||
|
||||
thm Units.Unit.toUnit_inverse
|
||||
|
||||
|
||||
lemma "watt \<^bold>\<cdot> hour \<approx>\<^sub>Q 3.6 \<^bold>\<cdot> kilo \<^bold>\<cdot> joule"
|
||||
oops
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -18,7 +18,8 @@ lemma Quantity_eq_intro:
|
|||
|
||||
instantiation Quantity_ext :: (times, times) times
|
||||
begin
|
||||
definition "times_Quantity_ext x y = \<lparr> magn = magn x \<cdot> magn y, unit = unit x \<cdot> unit y, \<dots> = more x \<cdot> more y \<rparr>"
|
||||
definition [si_def]:
|
||||
"times_Quantity_ext x y = \<lparr> magn = magn x \<cdot> magn y, unit = unit x \<cdot> unit y, \<dots> = more x \<cdot> more y \<rparr>"
|
||||
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 = \<lparr> magn = 1, unit = 1, \<dots> = 1 \<rparr>"
|
||||
definition [si_def]: "one_Quantity_ext = \<lparr> magn = 1, unit = 1, \<dots> = 1 \<rparr>"
|
||||
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 = \<lparr> magn = inverse (magn x), unit = inverse (unit x), \<dots> = inverse (more x) \<rparr>"
|
||||
definition "divide_Quantity_ext x y = \<lparr> magn = magn x / magn y, unit = unit x / unit y, \<dots> = more x / more y \<rparr>"
|
||||
definition [si_def]: "inverse_Quantity_ext x = \<lparr> magn = inverse (magn x), unit = inverse (unit x), \<dots> = inverse (more x) \<rparr>"
|
||||
definition [si_def]: "divide_Quantity_ext x y = \<lparr> magn = magn x / magn y, unit = unit x / unit y, \<dots> = more x / more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
|
|
@ -78,19 +79,33 @@ instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
|
|||
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 \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
|
||||
where "less_eq_Quantity_ext x y = (magn x \<le> magn y \<and> unit x = unit y \<and> more x \<le> more y)"
|
||||
definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
|
||||
where "less_Quantity_ext x y = (x \<le> y \<and> \<not> y \<le> x)"
|
||||
|
||||
instance ..
|
||||
|
||||
end
|
||||
|
||||
instance Quantity_ext :: (order, order) order
|
||||
by (intro_classes, auto simp add: less_Quantity_ext_def less_eq_Quantity_ext_def)
|
||||
|
||||
subsection \<open> SI Tagged Types \<close>
|
||||
text\<open>We 'lift' SI type expressions to SI tagged type expressions as follows:\<close>
|
||||
|
||||
typedef (overloaded) ('n, 'u::si_type) tQuant ("_[_]" [999,0] 999)
|
||||
= "{x :: 'n Quantity. unit x = SI('u)}"
|
||||
morphisms fromUnit toUnit by (rule_tac x="\<lparr> magn = undefined, unit = SI('u) \<rparr>" in exI, simp)
|
||||
morphisms fromQ toQ by (rule_tac x="\<lparr> magn = undefined, unit = SI('u) \<rparr>" in exI, simp)
|
||||
|
||||
setup_lifting type_definition_tQuant
|
||||
|
||||
text \<open> Coerce values when their units are equivalent \<close>
|
||||
|
||||
definition coerceUnit :: "'u\<^sub>2 itself \<Rightarrow> 'a['u\<^sub>1::si_type] \<Rightarrow> 'a['u\<^sub>2::si_type]" where
|
||||
"SI('u\<^sub>1) = SI('u\<^sub>2) \<Longrightarrow> coerceUnit t x = (toUnit (fromUnit x))"
|
||||
"SI('u\<^sub>1) = SI('u\<^sub>2) \<Longrightarrow> coerceUnit t x = (toQ (fromQ x))"
|
||||
|
||||
section\<open>Operations SI-tagged types via their Semantic Domains\<close>
|
||||
|
||||
|
|
@ -98,73 +113,81 @@ subsection\<open>Predicates on SI-tagged types\<close>
|
|||
|
||||
text \<open> Two SI types are equivalent if they have the same value-level units. \<close>
|
||||
|
||||
lift_definition Quant_equiv :: "'n['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<approx>\<^sub>Q" 50) is
|
||||
lift_definition qless_eq :: "'n::order['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50) is
|
||||
"(\<le>)" .
|
||||
|
||||
lift_definition qequiv :: "'n['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50) is
|
||||
"(=)" .
|
||||
|
||||
text\<open>This gives us an equivalence, but, unfortunately, not a congruence.\<close>
|
||||
|
||||
lemma Quant_equiv_refl [simp]: "a \<approx>\<^sub>Q a"
|
||||
by (simp add: Quant_equiv_def)
|
||||
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
|
||||
by (simp add: qequiv_def)
|
||||
|
||||
lemma Quant_equiv_sym: "a \<approx>\<^sub>Q b \<Longrightarrow> b \<approx>\<^sub>Q a"
|
||||
by (simp add: Quant_equiv_def)
|
||||
lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
|
||||
by (simp add: qequiv_def)
|
||||
|
||||
lemma Quant_equiv_trans: "\<lbrakk> a \<approx>\<^sub>Q b; b \<approx>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<approx>\<^sub>Q c"
|
||||
by (simp add: Quant_equiv_def)
|
||||
lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
|
||||
by (simp add: qequiv_def)
|
||||
|
||||
theorem qeq_iff_same_dim:
|
||||
fixes x y :: "'a['u::si_type]"
|
||||
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
|
||||
by (transfer, simp)
|
||||
|
||||
(* the following series of equivalent statements ... *)
|
||||
|
||||
lemma coerceQuant_eq_iff:
|
||||
fixes x :: "'a['u\<^sub>1::si_type]"
|
||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)"
|
||||
shows "(coerceUnit TYPE('u\<^sub>2) x) \<approx>\<^sub>Q x"
|
||||
by (metis Quant_equiv.rep_eq assms coerceUnit_def toUnit_cases toUnit_inverse)
|
||||
shows "(coerceUnit TYPE('u\<^sub>2) x) \<cong>\<^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::si_type]"
|
||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (coerceUnit TYPE('u\<^sub>2) x)"
|
||||
shows "x \<approx>\<^sub>Q y"
|
||||
using Quant_equiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
|
||||
shows "x \<cong>\<^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::si_type]" fixes y :: "'a['u\<^sub>2::si_type]"
|
||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (toUnit (fromUnit x))"
|
||||
shows "x \<approx>\<^sub>Q y"
|
||||
assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (toQ (fromQ x))"
|
||||
shows "x \<cong>\<^sub>Q y"
|
||||
by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceUnit_def)
|
||||
|
||||
text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<approx>\<^sub>Q y\<close>, since x and y may have different type.\<close>
|
||||
text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^sub>Q y\<close>, since x and y may have different type.\<close>
|
||||
|
||||
find_theorems "(toUnit (fromUnit _))"
|
||||
find_theorems "(toQ (fromQ _))"
|
||||
|
||||
lemma eq_ :
|
||||
fixes x :: "'a['u\<^sub>1::si_type]" fixes y :: "'a['u\<^sub>2::si_type]"
|
||||
assumes "x \<approx>\<^sub>Q y"
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)"
|
||||
by (metis (full_types) Quant_equiv.rep_eq assms fromUnit mem_Collect_eq)
|
||||
by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)
|
||||
|
||||
subsection\<open>Operations on SI-tagged types\<close>
|
||||
|
||||
lift_definition
|
||||
Quant_times :: "('n::times)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
|
||||
qtimes :: "('n::comm_ring_1)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
|
||||
by (simp add: si_sem_UnitTimes_def times_Quantity_ext_def)
|
||||
|
||||
lift_definition
|
||||
Quant_inverse :: "('n::inverse)['a::si_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
|
||||
qinverse :: "('n::field)['a::si_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
|
||||
by (simp add: inverse_Quantity_ext_def si_sem_UnitInv_def)
|
||||
|
||||
abbreviation
|
||||
Quant_divide :: "('n::{times,inverse})['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
|
||||
"Quant_divide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
|
||||
qdivide :: "('n::field)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
|
||||
"qdivide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation Quant_sq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
|
||||
abbreviation Quant_cube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||
abbreviation Quant_quart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||
abbreviation qsq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
|
||||
abbreviation qcube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||
abbreviation qquart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
|
||||
|
||||
abbreviation Quant_neq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
|
||||
abbreviation Quant_neq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||
abbreviation Quant_neq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||
abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
|
||||
abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||
abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
|
||||
|
||||
instantiation tQuant :: (zero,si_type) zero
|
||||
begin
|
||||
|
|
@ -220,70 +243,6 @@ instance tQuant :: (numeral,si_type) numeral ..
|
|||
instance tQuant :: (ab_group_add,si_type) ab_group_add
|
||||
by (intro_classes, (transfer, simp)+)
|
||||
|
||||
instantiation tQuant :: (times,si_type) times
|
||||
begin
|
||||
lift_definition times_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x * magn y, unit = SI('b) \<rparr>"
|
||||
by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance tQuant :: (power,si_type) power ..
|
||||
|
||||
instance tQuant :: (semigroup_mult,si_type) semigroup_mult
|
||||
by (intro_classes, transfer, simp add: mult.assoc)
|
||||
|
||||
instance tQuant :: (ab_semigroup_mult,si_type) ab_semigroup_mult
|
||||
by (intro_classes, (transfer, simp add: mult.commute))
|
||||
|
||||
instance tQuant :: (semiring,si_type) semiring
|
||||
by (intro_classes, (transfer, simp add: distrib_left distrib_right)+)
|
||||
|
||||
instance tQuant :: (semiring_0,si_type) semiring_0
|
||||
by (intro_classes, (transfer, simp)+)
|
||||
|
||||
instance tQuant :: (comm_semiring,si_type) comm_semiring
|
||||
by (intro_classes, transfer, simp add: linordered_field_class.sign_simps(18) mult.commute)
|
||||
|
||||
instance tQuant :: (mult_zero,si_type) mult_zero
|
||||
by (intro_classes, (transfer, simp)+)
|
||||
|
||||
instance tQuant :: (comm_semiring_0,si_type) comm_semiring_0
|
||||
by (intro_classes, (transfer, simp)+)
|
||||
|
||||
instantiation tQuant :: (real_vector,si_type) real_vector
|
||||
begin
|
||||
|
||||
lift_definition scaleR_tQuant :: "real \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> r x. \<lparr> magn = r *\<^sub>R magn x, unit = unit x \<rparr>" by simp
|
||||
|
||||
instance
|
||||
by (intro_classes, (transfer, simp add: scaleR_add_left scaleR_add_right)+)
|
||||
end
|
||||
|
||||
instance tQuant :: (ring,si_type) ring
|
||||
by (intro_classes, (transfer, simp)+)
|
||||
|
||||
instance tQuant :: (comm_monoid_mult,si_type) comm_monoid_mult
|
||||
by (intro_classes, (transfer, simp add: mult.commute)+)
|
||||
|
||||
instance tQuant :: (comm_semiring_1,si_type) comm_semiring_1
|
||||
by (intro_classes; (transfer, simp add: semiring_normalization_rules(1-8,24)))
|
||||
|
||||
instantiation tQuant :: (divide,si_type) divide
|
||||
begin
|
||||
lift_definition divide_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x div magn y, unit = SI('b) \<rparr>" by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (inverse,si_type) inverse
|
||||
begin
|
||||
lift_definition inverse_tQuant :: "'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x. \<lparr> magn = inverse (magn x), unit = SI('b) \<rparr>" by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (order,si_type) order
|
||||
begin
|
||||
lift_definition less_eq_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. magn x \<le> magn y" .
|
||||
|
|
@ -291,6 +250,10 @@ begin
|
|||
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
|
||||
end
|
||||
|
||||
lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['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
|
||||
|
|
@ -300,56 +263,15 @@ translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)"
|
|||
|
||||
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
|
||||
|
||||
named_theorems si_def
|
||||
definition [si_def, si_eq]: "meter = UNIT(1, Length)"
|
||||
definition [si_def, si_eq]: "second = UNIT(1, Time)"
|
||||
definition [si_def, si_eq]: "kilogram = UNIT(1, Mass)"
|
||||
definition [si_def, si_eq]: "ampere = UNIT(1, Current)"
|
||||
definition [si_def, si_eq]: "kelvin = UNIT(1, Temperature)"
|
||||
definition [si_def, si_eq]: "mole = UNIT(1, Amount)"
|
||||
definition [si_def, si_eq]: "candela = UNIT(1, Intensity)"
|
||||
|
||||
definition [si_def]: "meter = UNIT(1, Length)"
|
||||
definition [si_def]: "second = UNIT(1, Time)"
|
||||
definition [si_def]: "kilogram = UNIT(1, Mass)"
|
||||
definition [si_def]: "ampere = UNIT(1, Current)"
|
||||
definition [si_def]: "kelvin = UNIT(1, Temperature)"
|
||||
definition [si_def]: "mole = UNIT(1, Amount)"
|
||||
definition [si_def]: "candela = UNIT(1, Intensity)"
|
||||
|
||||
subsubsection \<open>The Projection: Stripping the SI-Tags \<close>
|
||||
|
||||
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
|
||||
"magnQuant x = magn (fromUnit x)"
|
||||
|
||||
subsubsection \<open>More Operations \<close>
|
||||
|
||||
lemma unit_eq_iff_magn_eq:
|
||||
"x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (auto simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma unit_le_iff_magn_le:
|
||||
"x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (auto simp add: magnQuant_def; (transfer, simp))
|
||||
|
||||
lemma magnQuant_zero [si_def]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_one [si_def]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_plus [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_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_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)
|
||||
|
||||
lemma magnQuant_numeral [si_def]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
|
||||
apply (induct n, simp_all add: si_def)
|
||||
apply (metis magnQuant_plus numeral_code(2))
|
||||
apply (metis magnQuant_one magnQuant_plus numeral_code(3))
|
||||
done
|
||||
|
||||
lemma magnQuant_mk [si_def]: "\<lbrakk>UNIT(n, 'u::si_type)\<rbrakk>\<^sub>Q = n"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
method si_calc =
|
||||
(simp add: unit_eq_iff_magn_eq unit_le_iff_magn_le si_def)
|
||||
definition dimless ("\<one>")
|
||||
where [si_def, si_eq]: "dimless = UNIT(1, NoDimension)"
|
||||
|
||||
end
|
||||
|
|
@ -6,6 +6,8 @@ theory SI_Units
|
|||
"HOL-Eisbach.Eisbach"
|
||||
begin
|
||||
|
||||
named_theorems si_def and si_eq
|
||||
|
||||
text\<open>
|
||||
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 \<open> 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. \<close>
|
||||
|
||||
record Unit =
|
||||
Seconds :: int
|
||||
Meters :: int
|
||||
Kilograms :: int
|
||||
Meters :: int
|
||||
Kilograms :: int
|
||||
Seconds :: int
|
||||
Amperes :: int
|
||||
Kelvins :: int
|
||||
Moles :: int
|
||||
Candelas :: int
|
||||
|
||||
text \<open> Units scaled by a power of 10 \<close>
|
||||
|
||||
type_synonym SUnit = "int Unit_ext"
|
||||
|
||||
abbreviation scale :: "SUnit \<Rightarrow> int" where
|
||||
"scale \<equiv> more"
|
||||
|
||||
text \<open> We define a commutative monoid for SI units. \<close>
|
||||
|
||||
instantiation Unit_ext :: (one) one
|
||||
begin
|
||||
\<comment> \<open> Here, $1$ is the dimensionless unit \<close>
|
||||
definition one_Unit_ext :: "'a Unit_ext"
|
||||
where [code_unfold]: "1 = \<lparr> Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0
|
||||
where [code_unfold, si_def]: "1 = \<lparr> Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0
|
||||
, Kelvins = 0, Moles = 0, Candelas = 0, \<dots> = 1 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
|
@ -69,9 +78,9 @@ instantiation Unit_ext :: (times) times
|
|||
begin
|
||||
\<comment> \<open> Multiplication is defined by adding together the powers \<close>
|
||||
definition times_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext \<Rightarrow> 'a Unit_ext"
|
||||
where [code_unfold]:
|
||||
"x * y = \<lparr> 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 = \<lparr> 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, \<dots> = more x * more y \<rparr>"
|
||||
instance ..
|
||||
|
|
@ -93,9 +102,9 @@ text \<open> 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 \<Rightarrow> 'a Unit_ext"
|
||||
where [code_unfold]:
|
||||
"inverse x = \<lparr> Seconds = - Seconds x , Meters = - Meters x
|
||||
, Kilograms = - Kilograms x, Amperes = - Amperes x
|
||||
where [code_unfold, si_def]:
|
||||
"inverse x = \<lparr> Meters = - Meters x, Kilograms = - Kilograms x
|
||||
, Seconds = - Seconds x, Amperes = - Amperes x
|
||||
, Kelvins = - Kelvins x, Moles = - Moles x
|
||||
, Candelas = - Candelas x, \<dots> = inverse (more x) \<rparr>"
|
||||
|
||||
|
|
@ -155,13 +164,32 @@ subsection \<open> Basic SI-types \<close>
|
|||
text \<open> We provide a syntax for type-expressions; The definition of
|
||||
the basic type constructors is straight-forward via a one-elementary set. \<close>
|
||||
|
||||
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 ("\<Theta>") = "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 \<Theta> = Temperature
|
||||
type_synonym N = Amount
|
||||
type_synonym J = Intensity
|
||||
type_notation NoDimension ("\<one>")
|
||||
|
||||
translations
|
||||
(type) "M" <= (type) "Mass"
|
||||
(type) "L" <= (type) "Length"
|
||||
(type) "T" <= (type) "Time"
|
||||
(type) "I" <= (type) "Current"
|
||||
(type) "\<Theta>" <= (type) "Temperature"
|
||||
(type) "N" <= (type) "Amount"
|
||||
(type) "J" <= (type) "Intensity"
|
||||
|
||||
subsection \<open> SI-type expressions and SI-type interpretation \<close>
|
||||
|
||||
|
|
@ -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 \<Rightarrow> 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)"
|
||||
|
|
@ -278,7 +312,7 @@ type_synonym ('a, 'b) UnitDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 6
|
|||
|
||||
type_synonym 'a UnitSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
|
||||
type_synonym 'a UnitCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
|
||||
type_synonym 'a UnitQuart = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>4" [999] 999)
|
||||
type_synonym 'a UnitQuart = "'a \<cdot> 'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>4" [999] 999)
|
||||
type_synonym 'a UnitInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999)
|
||||
type_synonym 'a UnitInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [999] 999)
|
||||
type_synonym 'a UnitInvQuart = "('a\<^sup>4)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>4" [999] 999)
|
||||
|
|
@ -287,6 +321,8 @@ translations (type) "'a\<^sup>-\<^sup>2" <= (type) "('a\<^sup>2)\<^sup>-\<^sup>1
|
|||
translations (type) "'a\<^sup>-\<^sup>3" <= (type) "('a\<^sup>3)\<^sup>-\<^sup>1"
|
||||
translations (type) "'a\<^sup>-\<^sup>4" <= (type) "('a\<^sup>4)\<^sup>-\<^sup>1"
|
||||
|
||||
(* Need to add UnitQuart to the print translation *)
|
||||
|
||||
print_translation \<open>
|
||||
[(@{type_syntax UnitTimes},
|
||||
fn ctx => fn [a, b] =>
|
||||
|
|
@ -296,11 +332,11 @@ print_translation \<open>
|
|||
Const (@{type_syntax UnitTimes}, _) $ a1 $ a2 =>
|
||||
if (a1 = a2 andalso a2 = b)
|
||||
then Const (@{type_syntax UnitCube}, dummyT) $ a1
|
||||
else raise Match |
|
||||
Const (@{type_syntax UnitSquare}, _) $ a' =>
|
||||
if (@{print} a' = b)
|
||||
then Const (@{type_syntax UnitCube}, dummyT) $ a'
|
||||
else raise Match |
|
||||
else case a1 of
|
||||
Const (@{type_syntax UnitTimes}, _) $ a11 $ a12 =>
|
||||
if (a11 = a12 andalso a12 = a2 andalso a2 = b)
|
||||
then Const (@{type_syntax UnitQuart}, dummyT) $ a11
|
||||
else raise Match |
|
||||
_ => raise Match)]
|
||||
\<close>
|
||||
|
||||
|
|
@ -313,5 +349,9 @@ type_synonym Frequency = "T\<^sup>-\<^sup>1"
|
|||
type_synonym Energy = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
|
||||
type_synonym Power = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>3"
|
||||
type_synonym Force = "L\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
|
||||
|
||||
type_synonym Pressure = "L\<^sup>-\<^sup>1\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
|
||||
type_synonym Charge = "I\<cdot>T"
|
||||
type_synonym PotentialDifference = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>3\<cdot>I\<^sup>-\<^sup>1"
|
||||
type_synonym Capacitance = "L\<^sup>-\<^sup>2\<cdot>M\<^sup>-\<^sup>1\<cdot>T\<^sup>4\<cdot>I\<^sup>2"
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue