Renamed Unit to Dimension. Added several more definitions and results from the standard.
This commit is contained in:
parent
2599caed01
commit
e1d4079c0f
|
|
@ -59,6 +59,8 @@ abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where
|
|||
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)"
|
||||
|
||||
subsection \<open> Basis Theorems \<close>
|
||||
|
||||
theorem second_definition:
|
||||
"1 \<odot> second \<cong>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
|
||||
by si_calc
|
||||
|
|
@ -68,8 +70,11 @@ theorem meter_definition:
|
|||
"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>)"
|
||||
theorem kilogram_definition:
|
||||
"1 \<odot> kilogram \<cong>\<^sub>Q (\<^bold>h \<^bold>/ (6.62607015 \<cdot> 1/(10^34) \<odot> \<one>))\<^bold>\<cdot>meter\<^sup>-\<^sup>\<two>\<^bold>\<cdot>second"
|
||||
by si_calc
|
||||
|
||||
abbreviation "approx_ice_point \<equiv> 273.15 \<odot> kelvin"
|
||||
|
||||
default_sort type
|
||||
|
||||
|
|
|
|||
|
|
@ -20,12 +20,22 @@ abbreviation "siemens \<equiv> kilogram\<^sup>-\<^sup>\<one> \<^bold>\<cdot> met
|
|||
|
||||
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 "tesla \<equiv> kilogram \<^bold>\<cdot> second\<^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>"
|
||||
|
||||
abbreviation "lux \<equiv> candela \<^bold>\<cdot> steradian \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation (input) "becquerel \<equiv> second\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "gray \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "sievert \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
abbreviation "katal \<equiv> mole \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>"
|
||||
|
||||
definition degrees_celcius :: "'a::field_char_0 \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
|
||||
where [si_eq]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
|
||||
where [si_eq]: "degrees_celcius x = (x \<odot> kelvin) + approx_ice_point"
|
||||
|
||||
definition [si_eq]: "gram = milli \<odot> kilogram"
|
||||
|
||||
|
|
@ -33,9 +43,50 @@ text\<open>The full beauty of the approach is perhaps revealed here, with the
|
|||
type of a classical three-dimensional gravitation field:\<close>
|
||||
type_synonym gravitation_field = "real\<^sup>3[L] \<Rightarrow> (real\<^sup>3[L \<cdot> T\<^sup>-\<^sup>2])"
|
||||
|
||||
subsection \<open> Equivalences \<close>
|
||||
|
||||
lemma joule_alt_def: "joule \<cong>\<^sub>Q newton \<^bold>\<cdot> meter"
|
||||
by si_calc
|
||||
|
||||
lemma watt_alt_def: "watt \<cong>\<^sub>Q joule \<^bold>/ second"
|
||||
by si_calc
|
||||
|
||||
lemma volt_alt_def: "volt = watt \<^bold>/ ampere"
|
||||
by simp
|
||||
|
||||
lemma farad_alt_def: "farad \<cong>\<^sub>Q coulomb \<^bold>/ volt"
|
||||
by si_calc
|
||||
|
||||
lemma ohm_alt_def: "ohm \<cong>\<^sub>Q volt \<^bold>/ ampere"
|
||||
by si_calc
|
||||
|
||||
lemma siemens_alt_def: "siemens \<cong>\<^sub>Q ampere \<^bold>/ volt"
|
||||
by si_calc
|
||||
|
||||
lemma weber_alt_def: "weber \<cong>\<^sub>Q volt \<^bold>\<cdot> second"
|
||||
by si_calc
|
||||
|
||||
lemma tesla_alt_def: "tesla \<cong>\<^sub>Q weber \<^bold>/ meter\<^sup>\<two>"
|
||||
by si_calc
|
||||
|
||||
lemma henry_alt_def: "henry \<cong>\<^sub>Q weber \<^bold>/ ampere"
|
||||
by si_calc
|
||||
|
||||
lemma lux_alt_def: "lux = lumen \<^bold>/ meter\<^sup>\<two>"
|
||||
by simp
|
||||
|
||||
lemma gray_alt_def: "gray \<cong>\<^sub>Q joule \<^bold>/ kilogram"
|
||||
by si_calc
|
||||
|
||||
lemma sievert_alt_def: "sievert \<cong>\<^sub>Q joule \<^bold>/ kilogram"
|
||||
by si_calc
|
||||
|
||||
subsection \<open> Properties \<close>
|
||||
|
||||
lemma kilogram: "kilo \<odot> gram = kilogram"
|
||||
by (si_simp)
|
||||
|
||||
lemma celcius_to_kelvin: "T\<degree>C = (T \<odot> kelvin) + (273.15 \<odot> kelvin)"
|
||||
by (si_simp)
|
||||
|
||||
end
|
||||
|
|
@ -4,6 +4,8 @@ theory SI_Prefix
|
|||
imports SI_Constants
|
||||
begin
|
||||
|
||||
subsection \<open> Definitions \<close>
|
||||
|
||||
default_sort ring_char_0
|
||||
|
||||
definition deca :: "'a" where [si_eq]: "deca = 10^1"
|
||||
|
|
@ -20,6 +22,12 @@ definition tera :: "'a" where [si_eq]: "tera = 10^12"
|
|||
|
||||
definition peta :: "'a" where [si_eq]: "peta = 10^15"
|
||||
|
||||
definition exa :: "'a" where [si_eq]: "exa = 10^18"
|
||||
|
||||
definition zetta :: "'a" where [si_eq]: "zetta = 10^21"
|
||||
|
||||
definition yotta :: "'a" where [si_eq]: "yotta = 10^24"
|
||||
|
||||
default_sort field_char_0
|
||||
|
||||
definition deci :: "'a" where [si_eq]: "deci = 1/10^1"
|
||||
|
|
@ -32,6 +40,21 @@ definition micro :: "'a" where [si_eq]: "micro = 1/10^6"
|
|||
|
||||
definition nano :: "'a" where [si_eq]: "nano = 1/10^9"
|
||||
|
||||
definition pico :: "'a" where [si_eq]: "pico = 1/10^12"
|
||||
|
||||
definition femto :: "'a" where [si_eq]: "femto = 1/10^15"
|
||||
|
||||
definition atto :: "'a" where [si_eq]: "atto = 1/10^18"
|
||||
|
||||
definition zepto :: "'a" where [si_eq]: "zepto = 1/10^21"
|
||||
|
||||
definition yocto :: "'a" where [si_eq]: "yocto = 1/10^24"
|
||||
|
||||
default_sort type
|
||||
|
||||
subsection \<open> Examples \<close>
|
||||
|
||||
lemma "2.3 \<odot> (centi \<odot> meter)\<^sup>\<three> \<cong>\<^sub>Q 2.3 \<cdot> 1/10^6 \<odot> meter\<^sup>\<three>"
|
||||
by (si_simp)
|
||||
|
||||
end
|
||||
|
|
@ -6,63 +6,63 @@ begin
|
|||
|
||||
named_theorems si_transfer
|
||||
|
||||
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
|
||||
[si_def]: "magnQuant x = magn (fromQ x)"
|
||||
definition magQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
|
||||
[si_def]: "magQuant x = mag (fromQ x)"
|
||||
|
||||
lemma unit_eq_iff_magn_eq [si_transfer]:
|
||||
lemma unit_eq_iff_mag_eq [si_transfer]:
|
||||
"x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (auto simp add: magnQuant_def, transfer, simp)
|
||||
by (auto simp add: magQuant_def, transfer, simp)
|
||||
|
||||
lemma unit_equiv_iff [si_transfer]:
|
||||
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)
|
||||
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
|
||||
by (simp add: magQuant_def unit_eq_iff_mag_eq)
|
||||
then show ?thesis
|
||||
by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def)
|
||||
by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQuant_def)
|
||||
qed
|
||||
|
||||
lemma unit_le_iff_magn_le [si_transfer]:
|
||||
"x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (auto simp add: magnQuant_def; (transfer, simp))
|
||||
by (auto simp add: magQuant_def; (transfer, simp))
|
||||
|
||||
lemma magnQuant_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
lemma magQuant_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
||||
by (simp add: magQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
lemma magQuant_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magQuant_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 magQuant_plus [si_eq]: "\<lbrakk>x + y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q + \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_minus [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 magQuant_minus [si_eq]: "\<lbrakk>x - y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q - \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_uminus [si_eq]: "\<lbrakk>- x\<rbrakk>\<^sub>Q = - \<lbrakk>x\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
lemma magQuant_uminus [si_eq]: "\<lbrakk>- x\<rbrakk>\<^sub>Q = - \<lbrakk>x\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magQuant_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 magQuant_scaleQ [si_eq]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magQuant_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 magQuant_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: magQuant_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 magQuant_qinverse [si_eq]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magQuant_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 magQuant_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: magQuant_def, transfer, simp add: field_class.field_divide_inverse)
|
||||
|
||||
lemma magnQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
|
||||
lemma magQuant_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))
|
||||
apply (metis magQuant_def magQuant_one)
|
||||
apply (metis magQuant_def magQuant_plus numeral_code(2))
|
||||
apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3))
|
||||
done
|
||||
|
||||
lemma magnQuant_mk [si_eq]: "\<lbrakk>UNIT('u::si_type)\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
lemma magQuant_mk [si_eq]: "\<lbrakk>UNIT('u::si_type)\<rbrakk>\<^sub>Q = 1"
|
||||
by (simp add: magQuant_def, transfer, simp)
|
||||
|
||||
text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,72 +1,71 @@
|
|||
section \<open> SI Quantities \<close>
|
||||
|
||||
theory SI_Quantities
|
||||
imports SI_Units (* Optics.Lenses *)
|
||||
imports SI_Units
|
||||
begin
|
||||
|
||||
|
||||
subsection \<open> The \<^theory_text>\<open>Quantity\<close>-type and its operations \<close>
|
||||
|
||||
record 'a Quantity =
|
||||
magn :: 'a \<comment> \<open> Magnitude of the quantity \<close>
|
||||
unit :: Unit \<comment> \<open> Unit of the quantity \<close>
|
||||
mag :: 'a \<comment> \<open> Magnitude of the quantity \<close>
|
||||
dim :: Dimension \<comment> \<open> Dimension of the quantity \<close>
|
||||
|
||||
lemma Quantity_eq_intro:
|
||||
assumes "magn x = magn y" "unit x = unit y" "more x = more y"
|
||||
assumes "mag x = mag y" "dim x = dim y" "more x = more y"
|
||||
shows "x = y"
|
||||
by (simp add: assms)
|
||||
|
||||
instantiation Quantity_ext :: (times, times) times
|
||||
begin
|
||||
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>"
|
||||
"times_Quantity_ext x y = \<lparr> mag = mag x \<cdot> mag y, dim = dim x \<cdot> dim y, \<dots> = more x \<cdot> more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
lemma magn_times [simp]: "magn (x \<cdot> y) = magn x \<cdot> magn y" by (simp add: times_Quantity_ext_def)
|
||||
lemma unit_times [simp]: "unit (x \<cdot> y) = unit x \<cdot> unit y" by (simp add: times_Quantity_ext_def)
|
||||
lemma mag_times [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y" by (simp add: times_Quantity_ext_def)
|
||||
lemma dim_times [simp]: "dim (x \<cdot> y) = dim x \<cdot> dim y" by (simp add: times_Quantity_ext_def)
|
||||
lemma more_times [simp]: "more (x \<cdot> y) = more x \<cdot> more y" by (simp add: times_Quantity_ext_def)
|
||||
|
||||
instantiation Quantity_ext :: (zero, zero) zero
|
||||
begin
|
||||
definition "zero_Quantity_ext = \<lparr> magn = 0, unit = 1, \<dots> = 0 \<rparr>"
|
||||
definition "zero_Quantity_ext = \<lparr> mag = 0, dim = 1, \<dots> = 0 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
lemma magn_zero [simp]: "magn 0 = 0" by (simp add: zero_Quantity_ext_def)
|
||||
lemma unit_zero [simp]: "unit 0 = 1" by (simp add: zero_Quantity_ext_def)
|
||||
lemma mag_zero [simp]: "mag 0 = 0" by (simp add: zero_Quantity_ext_def)
|
||||
lemma dim_zero [simp]: "dim 0 = 1" by (simp add: zero_Quantity_ext_def)
|
||||
lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def)
|
||||
|
||||
instantiation Quantity_ext :: (one, one) one
|
||||
begin
|
||||
definition [si_def]: "one_Quantity_ext = \<lparr> magn = 1, unit = 1, \<dots> = 1 \<rparr>"
|
||||
definition [si_def]: "one_Quantity_ext = \<lparr> mag = 1, dim = 1, \<dots> = 1 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
lemma magn_one [simp]: "magn 1 = 1" by (simp add: one_Quantity_ext_def)
|
||||
lemma unit_one [simp]: "unit 1 = 1" by (simp add: one_Quantity_ext_def)
|
||||
lemma mag_one [simp]: "mag 1 = 1" by (simp add: one_Quantity_ext_def)
|
||||
lemma dim_one [simp]: "dim 1 = 1" by (simp add: one_Quantity_ext_def)
|
||||
lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def)
|
||||
|
||||
instantiation Quantity_ext :: (inverse, inverse) inverse
|
||||
begin
|
||||
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>"
|
||||
definition [si_def]: "inverse_Quantity_ext x = \<lparr> mag = inverse (mag x), dim = inverse (dim x), \<dots> = inverse (more x) \<rparr>"
|
||||
definition [si_def]: "divide_Quantity_ext x y = \<lparr> mag = mag x / mag y, dim = dim x / dim y, \<dots> = more x / more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
lemma magn_inverse [simp]: "magn (inverse x) = inverse (magn x)"
|
||||
lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)"
|
||||
by (simp add: inverse_Quantity_ext_def)
|
||||
|
||||
lemma unit_inverse [simp]: "unit (inverse x) = inverse (unit x)"
|
||||
lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)"
|
||||
by (simp add: inverse_Quantity_ext_def)
|
||||
|
||||
lemma more_inverse [simp]: "more (inverse x) = inverse (more x)"
|
||||
by (simp add: inverse_Quantity_ext_def)
|
||||
|
||||
lemma magn_divide [simp]: "magn (x / y) = magn x / magn y"
|
||||
lemma mag_divide [simp]: "mag (x / y) = mag x / mag y"
|
||||
by (simp add: divide_Quantity_ext_def)
|
||||
|
||||
lemma unit_divide [simp]: "unit (x / y) = unit x / unit y"
|
||||
lemma dim_divide [simp]: "dim (x / y) = dim x / dim y"
|
||||
by (simp add: divide_Quantity_ext_def)
|
||||
|
||||
lemma more_divide [simp]: "more (x / y) = more x / more y"
|
||||
|
|
@ -82,7 +81,7 @@ instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
|
|||
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)"
|
||||
where "less_eq_Quantity_ext x y = (mag x \<le> mag y \<and> dim x = dim 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)"
|
||||
|
||||
|
|
@ -97,12 +96,12 @@ 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 fromQ toQ by (rule_tac x="\<lparr> magn = undefined, unit = SI('u) \<rparr>" in exI, simp)
|
||||
= "{x :: 'n Quantity. dim x = SI('u)}"
|
||||
morphisms fromQ toQ by (rule_tac x="\<lparr> mag = undefined, dim = SI('u) \<rparr>" in exI, simp)
|
||||
|
||||
setup_lifting type_definition_tQuant
|
||||
|
||||
text \<open> Coerce values when their units are equivalent \<close>
|
||||
text \<open> Coerce values when their dimensions 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 = (toQ (fromQ x))"
|
||||
|
|
@ -111,7 +110,7 @@ section\<open>Operations SI-tagged types via their Semantic Domains\<close>
|
|||
|
||||
subsection\<open>Predicates on SI-tagged types\<close>
|
||||
|
||||
text \<open> Two SI types are equivalent if they have the same value-level units. \<close>
|
||||
text \<open> Two SI types are equivalent if they have the same value-level dimensions. \<close>
|
||||
|
||||
lift_definition qless_eq :: "'n::order['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50) is
|
||||
"(\<le>)" .
|
||||
|
|
@ -159,9 +158,7 @@ lemma updown_eq_iff:
|
|||
|
||||
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 "(toQ (fromQ _))"
|
||||
|
||||
lemma eq_ :
|
||||
lemma qeq:
|
||||
fixes x :: "'a['u\<^sub>1::si_type]" fixes y :: "'a['u\<^sub>2::si_type]"
|
||||
assumes "x \<cong>\<^sub>Q y"
|
||||
shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)"
|
||||
|
|
@ -171,11 +168,11 @@ subsection\<open>Operations on SI-tagged types\<close>
|
|||
|
||||
lift_definition
|
||||
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)
|
||||
by (simp add: si_sem_DimTimes_def times_Quantity_ext_def)
|
||||
|
||||
lift_definition
|
||||
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)
|
||||
by (simp add: inverse_Quantity_ext_def si_sem_DimInv_def)
|
||||
|
||||
abbreviation
|
||||
qdivide :: "('n::field)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
|
||||
|
|
@ -191,14 +188,14 @@ abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-
|
|||
|
||||
instantiation tQuant :: (zero,si_type) zero
|
||||
begin
|
||||
lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\<lparr> magn = 0, unit = SI('b) \<rparr>"
|
||||
lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\<lparr> mag = 0, dim = SI('b) \<rparr>"
|
||||
by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (one,si_type) one
|
||||
begin
|
||||
lift_definition one_tQuant :: "('a, 'b) tQuant" is "\<lparr> magn = 1, unit = SI('b) \<rparr>"
|
||||
lift_definition one_tQuant :: "('a, 'b) tQuant" is "\<lparr> mag = 1, dim = SI('b) \<rparr>"
|
||||
by simp
|
||||
instance ..
|
||||
end
|
||||
|
|
@ -206,7 +203,7 @@ end
|
|||
instantiation tQuant :: (plus,si_type) plus
|
||||
begin
|
||||
lift_definition plus_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x + magn y, unit = SI('b) \<rparr>"
|
||||
is "\<lambda> x y. \<lparr> mag = mag x + mag y, dim = SI('b) \<rparr>"
|
||||
by (simp)
|
||||
instance ..
|
||||
end
|
||||
|
|
@ -226,14 +223,14 @@ instance tQuant :: (comm_monoid_add,si_type) comm_monoid_add
|
|||
instantiation tQuant :: (uminus,si_type) uminus
|
||||
begin
|
||||
lift_definition uminus_tQuant :: "'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x. \<lparr> magn = - magn x, unit = unit x \<rparr>" by (simp)
|
||||
is "\<lambda> x. \<lparr> mag = - mag x, dim = dim x \<rparr>" by (simp)
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (minus,si_type) minus
|
||||
begin
|
||||
lift_definition minus_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x - magn y, unit = unit x \<rparr>" by (simp)
|
||||
is "\<lambda> x y. \<lparr> mag = mag x - mag y, dim = dim x \<rparr>" by (simp)
|
||||
|
||||
instance ..
|
||||
end
|
||||
|
|
@ -245,18 +242,18 @@ instance tQuant :: (ab_group_add,si_type) ab_group_add
|
|||
|
||||
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" .
|
||||
lift_definition less_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. magn x < magn y" .
|
||||
lift_definition less_eq_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x \<le> mag y" .
|
||||
lift_definition less_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x < mag y" .
|
||||
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
|
||||
is "\<lambda> r x. \<lparr> mag = r * mag x, dim = SI('u) \<rparr>" by simp
|
||||
|
||||
notation scaleQ (infixr "\<odot>" 63)
|
||||
|
||||
lift_definition mk_unit :: "'u itself \<Rightarrow> ('a::one)['u::si_type]"
|
||||
is "\<lambda> u. \<lparr> magn = 1, unit = SI('u) \<rparr>" by simp
|
||||
is "\<lambda> u. \<lparr> mag = 1, dim = SI('u) \<rparr>" by simp
|
||||
|
||||
syntax "_mk_unit" :: "type \<Rightarrow> logic" ("UNIT'(_')")
|
||||
translations "UNIT('a)" == "CONST mk_unit TYPE('a)"
|
||||
|
|
|
|||
|
|
@ -47,73 +47,73 @@ subsection \<open> The \<^theory_text>\<open>Unit\<close>-type and its operation
|
|||
text \<open> An SI unit associates with each of the seven base unit an integer that denotes the power
|
||||
to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \<close>
|
||||
|
||||
record Unit =
|
||||
Meters :: int
|
||||
Kilograms :: int
|
||||
Seconds :: int
|
||||
Amperes :: int
|
||||
Kelvins :: int
|
||||
Moles :: int
|
||||
Candelas :: int
|
||||
record Dimension =
|
||||
Length :: int
|
||||
Mass :: int
|
||||
Time :: int
|
||||
Current :: int
|
||||
Temperature :: int
|
||||
Amount :: int
|
||||
Intensity :: int
|
||||
|
||||
text \<open> We define a commutative monoid for SI units. \<close>
|
||||
|
||||
instantiation Unit_ext :: (one) one
|
||||
instantiation Dimension_ext :: (one) one
|
||||
begin
|
||||
\<comment> \<open> Here, $1$ is the dimensionless unit \<close>
|
||||
definition one_Unit_ext :: "'a Unit_ext"
|
||||
where [code_unfold, si_def]: "1 = \<lparr> Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0
|
||||
, Kelvins = 0, Moles = 0, Candelas = 0, \<dots> = 1 \<rparr>"
|
||||
definition one_Dimension_ext :: "'a Dimension_ext"
|
||||
where [code_unfold, si_def]: "1 = \<lparr> Length = 0, Mass = 0, Time = 0, Current = 0
|
||||
, Temperature = 0, Amount = 0, Intensity = 0, \<dots> = 1 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Unit_ext :: (times) times
|
||||
instantiation Dimension_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"
|
||||
definition times_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
|
||||
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>"
|
||||
"x * y = \<lparr> Length = Length x + Length y, Mass = Mass x + Mass y
|
||||
, Time = Time x + Time y, Current = Current x + Current y
|
||||
, Temperature = Temperature x + Temperature y, Amount = Amount x + Amount y
|
||||
, Intensity = Intensity x + Intensity y, \<dots> = more x * more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance Unit_ext :: (comm_monoid_mult) comm_monoid_mult
|
||||
instance Dimension_ext :: (comm_monoid_mult) comm_monoid_mult
|
||||
proof
|
||||
fix a b c :: "'a Unit_ext"
|
||||
fix a b c :: "'a Dimension_ext"
|
||||
show "a * b * c = a * (b * c)"
|
||||
by (simp add: times_Unit_ext_def mult.assoc)
|
||||
by (simp add: times_Dimension_ext_def mult.assoc)
|
||||
show "a * b = b * a"
|
||||
by (simp add: times_Unit_ext_def mult.commute)
|
||||
by (simp add: times_Dimension_ext_def mult.commute)
|
||||
show "1 * a = a"
|
||||
by (simp add: times_Unit_ext_def one_Unit_ext_def)
|
||||
by (simp add: times_Dimension_ext_def one_Dimension_ext_def)
|
||||
qed
|
||||
|
||||
text \<open> We also define the inverse and division operations, and an abelian group. \<close>
|
||||
|
||||
instantiation Unit_ext :: ("{times,inverse}") inverse
|
||||
instantiation Dimension_ext :: ("{times,inverse}") inverse
|
||||
begin
|
||||
definition inverse_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext"
|
||||
definition inverse_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
|
||||
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>"
|
||||
"inverse x = \<lparr> Length = - Length x, Mass = - Mass x
|
||||
, Time = - Time x, Current = - Current x
|
||||
, Temperature = - Temperature x, Amount = - Amount x
|
||||
, Intensity = - Intensity x, \<dots> = inverse (more x) \<rparr>"
|
||||
|
||||
definition divide_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext \<Rightarrow> 'a Unit_ext"
|
||||
definition divide_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
|
||||
where [code_unfold, si_def]:
|
||||
"divide_Unit_ext x y = x * (inverse y)"
|
||||
"divide_Dimension_ext x y = x * (inverse y)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance Unit_ext :: (ab_group_mult) ab_group_mult
|
||||
instance Dimension_ext :: (ab_group_mult) ab_group_mult
|
||||
proof
|
||||
fix a b :: "'a Unit_ext"
|
||||
fix a b :: "'a Dimension_ext"
|
||||
show "inverse a \<cdot> a = 1"
|
||||
by (simp add: inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def)
|
||||
by (simp add: inverse_Dimension_ext_def times_Dimension_ext_def one_Dimension_ext_def)
|
||||
show "a \<cdot> inverse b = a div b"
|
||||
by (simp add: divide_Unit_ext_def)
|
||||
by (simp add: divide_Dimension_ext_def)
|
||||
qed
|
||||
|
||||
text \<open> It makes no sense to define a plus operator for SI units because we can only add together
|
||||
|
|
@ -145,10 +145,10 @@ instance unit :: ab_group_mult
|
|||
|
||||
text \<open> A base unit is an SI_tagged_domain unit here precisely one unit has power 1. \<close>
|
||||
|
||||
definition is_BaseUnit :: "Unit \<Rightarrow> bool" where
|
||||
"is_BaseUnit u = (\<exists> n. u = 1\<lparr>Meters := n\<rparr> \<or> u = 1\<lparr>Kilograms := n\<rparr> \<or> u = 1\<lparr>Seconds := n\<rparr>
|
||||
\<or> u = 1\<lparr>Amperes := n\<rparr> \<or> u = 1\<lparr>Kelvins := n\<rparr> \<or> u = 1\<lparr>Moles := n\<rparr>
|
||||
\<or> u = 1\<lparr>Candelas := n\<rparr>)"
|
||||
definition is_BaseDim :: "Dimension \<Rightarrow> bool" where
|
||||
"is_BaseDim u = (\<exists> n. u = 1\<lparr>Length := n\<rparr> \<or> u = 1\<lparr>Mass := n\<rparr> \<or> u = 1\<lparr>Time := n\<rparr>
|
||||
\<or> u = 1\<lparr>Current := n\<rparr> \<or> u = 1\<lparr>Temperature := n\<rparr> \<or> u = 1\<lparr>Amount := n\<rparr>
|
||||
\<or> u = 1\<lparr>Intensity := n\<rparr>)"
|
||||
|
||||
section\<open>The Syntax and Semantics of SI types and SI-tagged types\<close>
|
||||
|
||||
|
|
@ -193,12 +193,12 @@ are restricted to the set of SI-type expressions.
|
|||
The mechanism in Isabelle to characterize a certain sub-class of Isabelle-type expressions
|
||||
are \<^emph>\<open>type classes\<close>. We therefore need such a sub-class; for reasons of convenience,
|
||||
we combine its construction also with the "semantics" of SI types in terms of
|
||||
@{typ Unit}. \<close>
|
||||
@{typ Dimension}. \<close>
|
||||
|
||||
subsubsection \<open> SI-type expression definition as type-class \<close>
|
||||
|
||||
class si_type = finite +
|
||||
fixes si_sem :: "'a itself \<Rightarrow> Unit"
|
||||
fixes si_sem :: "'a itself \<Rightarrow> Dimension"
|
||||
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
||||
|
||||
syntax
|
||||
|
|
@ -210,135 +210,133 @@ translations
|
|||
text \<open> The sub-set of basic SI type expressions can be characterized by the following
|
||||
operation: \<close>
|
||||
|
||||
class si_baseunit = si_type +
|
||||
assumes is_BaseUnit: "is_BaseUnit SI('a)"
|
||||
class si_basedim = si_type +
|
||||
assumes is_BaseDim: "is_BaseDim SI('a)"
|
||||
|
||||
subsubsection \<open> SI base type constructors \<close>
|
||||
|
||||
text\<open>We embed the basic SI types into the SI type expressions: \<close>
|
||||
|
||||
|
||||
instantiation Length :: si_baseunit
|
||||
instantiation Length :: si_basedim
|
||||
begin
|
||||
definition si_sem_Length :: "Length itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Length x = 1\<lparr>Meters := 1\<rparr>"
|
||||
instance
|
||||
by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Length :: "Length itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Length x = 1\<lparr>Length := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Mass :: si_baseunit
|
||||
instantiation Mass :: si_basedim
|
||||
begin
|
||||
definition si_sem_Mass :: "Mass itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Mass x = 1\<lparr>Kilograms := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Mass_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Mass :: "Mass itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Mass x = 1\<lparr>Mass := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Time :: si_baseunit
|
||||
instantiation Time :: si_basedim
|
||||
begin
|
||||
definition si_sem_Time :: "Time itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Time x = 1\<lparr>Seconds := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Time_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Time :: "Time itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Time x = 1\<lparr>Time := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Current :: si_baseunit
|
||||
instantiation Current :: si_basedim
|
||||
begin
|
||||
definition si_sem_Current :: "Current itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Current x = 1\<lparr>Amperes := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Current_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Current :: "Current itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Current x = 1\<lparr>Current := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Temperature :: si_baseunit
|
||||
instantiation Temperature :: si_basedim
|
||||
begin
|
||||
definition si_sem_Temperature :: "Temperature itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Temperature x = 1\<lparr>Kelvins := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Temperature_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Temperature :: "Temperature itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Temperature x = 1\<lparr>Temperature := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Amount :: si_baseunit
|
||||
instantiation Amount :: si_basedim
|
||||
begin
|
||||
definition si_sem_Amount :: "Amount itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Amount x = 1\<lparr>Moles := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Amount_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Amount :: "Amount itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Amount x = 1\<lparr>Amount := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation Intensity :: si_baseunit
|
||||
instantiation Intensity :: si_basedim
|
||||
begin
|
||||
definition si_sem_Intensity :: "Intensity itself \<Rightarrow> Unit"
|
||||
where [si_def]: "si_sem_Intensity x = 1\<lparr>Candelas := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseUnit_def, (transfer, simp)+)
|
||||
definition si_sem_Intensity :: "Intensity itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_Intensity x = 1\<lparr>Intensity := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation NoDimension :: si_type
|
||||
begin
|
||||
definition si_sem_NoDimension :: "NoDimension itself \<Rightarrow> Unit"
|
||||
definition si_sem_NoDimension :: "NoDimension itself \<Rightarrow> Dimension"
|
||||
where [si_def]: "si_sem_NoDimension x = 1"
|
||||
instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseUnit_def, (transfer, simp)+)
|
||||
instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseDim_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)"
|
||||
"is_BaseUnit SI(Intensity)" by (simp_all add: is_BaseUnit)
|
||||
"is_BaseDim SI(Length)" "is_BaseDim SI(Mass)" "is_BaseDim SI(Time)"
|
||||
"is_BaseDim SI(Current)" "is_BaseDim SI(Temperature)" "is_BaseDim SI(Amount)"
|
||||
"is_BaseDim SI(Intensity)" by (simp_all add: is_BaseDim)
|
||||
|
||||
subsubsection \<open> Higher SI Type Constructors: Inner Product and Inverse \<close>
|
||||
text\<open>On the class of SI-types (in which we have already inserted the base SI types),
|
||||
the definitions of the type constructors for inner product and inverse is straight) forward.\<close>
|
||||
|
||||
typedef ('a::si_type, 'b::si_type) UnitTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_UnitTimes
|
||||
typedef ('a::si_type, 'b::si_type) DimTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_DimTimes
|
||||
|
||||
text \<open> We can prove that multiplication of two SI types yields an SI type. \<close>
|
||||
|
||||
instantiation UnitTimes :: (si_type, si_type) si_type
|
||||
instantiation DimTimes :: (si_type, si_type) si_type
|
||||
begin
|
||||
definition si_sem_UnitTimes :: "('a \<cdot> 'b) itself \<Rightarrow> Unit" where
|
||||
[si_eq]: "si_sem_UnitTimes x = SI('a) * SI('b)"
|
||||
instance by (intro_classes, simp_all add: si_sem_UnitTimes_def, (transfer, simp)+)
|
||||
definition si_sem_DimTimes :: "('a \<cdot> 'b) itself \<Rightarrow> Dimension" where
|
||||
[si_eq]: "si_sem_DimTimes x = SI('a) * SI('b)"
|
||||
instance by (intro_classes, simp_all add: si_sem_DimTimes_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
text \<open> Similarly, we define division of two SI types and prove that SI types are closed under this. \<close>
|
||||
|
||||
typedef 'a UnitInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_UnitInv
|
||||
instantiation UnitInv :: (si_type) si_type
|
||||
typedef 'a DimInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_DimInv
|
||||
instantiation DimInv :: (si_type) si_type
|
||||
begin
|
||||
definition si_sem_UnitInv :: "('a\<^sup>-\<^sup>1) itself \<Rightarrow> Unit" where
|
||||
[si_eq]: "si_sem_UnitInv x = inverse SI('a)"
|
||||
instance by (intro_classes, simp_all add: si_sem_UnitInv_def, (transfer, simp)+)
|
||||
definition si_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \<Rightarrow> Dimension" where
|
||||
[si_eq]: "si_sem_DimInv x = inverse SI('a)"
|
||||
instance by (intro_classes, simp_all add: si_sem_DimInv_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
|
||||
subsubsection \<open> Syntactic Support for SI type expressions. \<close>
|
||||
|
||||
text\<open>A number of type-synonyms allow for more compact notation: \<close>
|
||||
type_synonym ('a, 'b) UnitDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
|
||||
type_synonym ('a, 'b) DimDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
|
||||
|
||||
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 \<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)
|
||||
type_synonym 'a DimSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
|
||||
type_synonym 'a DimCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
|
||||
type_synonym 'a DimQuart = "'a \<cdot> 'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>4" [999] 999)
|
||||
type_synonym 'a DimInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999)
|
||||
type_synonym 'a DimInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [999] 999)
|
||||
type_synonym 'a DimInvQuart = "('a\<^sup>4)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>4" [999] 999)
|
||||
|
||||
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 *)
|
||||
(* Need to add DimQuart to the print translation *)
|
||||
|
||||
print_translation \<open>
|
||||
[(@{type_syntax UnitTimes},
|
||||
[(@{type_syntax DimTimes},
|
||||
fn ctx => fn [a, b] =>
|
||||
if (a = b)
|
||||
then Const (@{type_syntax UnitSquare}, dummyT) $ a
|
||||
then Const (@{type_syntax DimSquare}, dummyT) $ a
|
||||
else case a of
|
||||
Const (@{type_syntax UnitTimes}, _) $ a1 $ a2 =>
|
||||
Const (@{type_syntax DimTimes}, _) $ a1 $ a2 =>
|
||||
if (a1 = a2 andalso a2 = b)
|
||||
then Const (@{type_syntax UnitCube}, dummyT) $ a1
|
||||
then Const (@{type_syntax DimCube}, dummyT) $ a1
|
||||
else case a1 of
|
||||
Const (@{type_syntax UnitTimes}, _) $ a11 $ a12 =>
|
||||
Const (@{type_syntax DimTimes}, _) $ a11 $ a12 =>
|
||||
if (a11 = a12 andalso a12 = a2 andalso a2 = b)
|
||||
then Const (@{type_syntax UnitQuart}, dummyT) $ a11
|
||||
then Const (@{type_syntax DimQuart}, dummyT) $ a11
|
||||
else raise Match |
|
||||
_ => raise Match)]
|
||||
\<close>
|
||||
|
|
|
|||
Loading…
Reference in New Issue