Cleaning up the proof procedure, and additional algebraic laws
This commit is contained in:
parent
b8e347b4c8
commit
583637859a
|
|
@ -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
|
||||
|
|
@ -23,42 +23,50 @@ text \<open> The most general types we support must form a field into which the
|
|||
|
||||
default_sort field_char_0
|
||||
|
||||
abbreviation (input) caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\<Delta>v\<^sub>C\<^sub>s") where
|
||||
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"
|
||||
|
||||
abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" where
|
||||
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>)"
|
||||
|
||||
abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" where
|
||||
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)"
|
||||
|
||||
abbreviation elementary_charge :: "'a[I \<cdot> T]" where
|
||||
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]" where
|
||||
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]" where
|
||||
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]" 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)"
|
||||
|
||||
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>)"
|
||||
|
||||
thm si_def
|
||||
|
||||
theorem Quant_eq_iff_same_dim:
|
||||
"x \<approx>\<^sub>Q y \<longleftrightarrow> x = y"
|
||||
by (transfer, simp)
|
||||
|
||||
theorem second_definition: "1 \<odot> second \<approx>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
|
||||
by (simp add: unit_equiv_iff, simp add: Quant_equiv_def unit_eq_iff_magn_eq si_def)
|
||||
|
||||
default_sort type
|
||||
|
||||
end
|
||||
|
|
@ -4,22 +4,24 @@ theory SI_Derived
|
|||
imports SI_Prefix
|
||||
begin
|
||||
|
||||
definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where
|
||||
subsection \<open> Definitions \<close>
|
||||
|
||||
definition degree :: "'a::real_field[L/L]" where
|
||||
[si_def]: "degree = (2\<cdot>(of_real pi) / 180) \<odot> radian"
|
||||
|
||||
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odot> degree"
|
||||
|
||||
definition degrees_celcius :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
|
||||
definition degrees_celcius :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
|
||||
where [si_def]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
|
||||
|
||||
definition degrees_farenheit :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
|
||||
definition degrees_farenheit :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
|
||||
where [si_def]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
|
||||
|
||||
definition [si_def]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
|
||||
|
||||
definition [si_def]: "pint = 0.56826125 \<odot> litre"
|
||||
|
||||
definition [si_def]: "hour = 3600 \<odot> second"
|
||||
definition [si_def, si_eq]: "hour = 3600 \<odot> second"
|
||||
|
||||
definition [si_def]: "gram = milli \<odot> kilogram"
|
||||
|
||||
|
|
@ -39,4 +41,9 @@ 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 \<Rightarrow> real\<^sup>3)[L \<cdot> T\<^sup>-\<^sup>2]"
|
||||
|
||||
subsection \<open> Examples \<close>
|
||||
|
||||
lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"
|
||||
by (si_calc)
|
||||
|
||||
end
|
||||
|
|
@ -1,8 +1,69 @@
|
|||
section \<open> Tactic Support for SI type expressions. \<close>
|
||||
|
||||
theory SI_Proof
|
||||
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 (fromUnit 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 (fromUnit ta) \<noteq> magn (fromUnit 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
|
||||
|
|
@ -23,139 +84,4 @@ 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>Meters = 0, Kilograms = 0, Seconds = 1, 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>Meters = 1, Kilograms = 0, Seconds = 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>Meters = 0, Kilograms = 1, Seconds = 0, 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>Meters = 0, Kilograms = 0, Seconds = 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>Meters = 0, Kilograms = 0, Seconds = 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>Meters = 0, Kilograms = 0, Seconds = 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>Meters = 0, Kilograms = 0, Seconds = 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
|
||||
|
|
@ -79,6 +79,20 @@ 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>
|
||||
|
||||
|
|
@ -99,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 toUnit_cases toUnit_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"
|
||||
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 _))"
|
||||
|
||||
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 fromUnit 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
|
||||
|
|
@ -228,7 +250,7 @@ begin
|
|||
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
|
||||
end
|
||||
|
||||
lift_definition scaleQ :: "'a \<Rightarrow> 'a::times['u::si_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
|
||||
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)
|
||||
|
|
@ -241,70 +263,15 @@ translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)"
|
|||
|
||||
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
|
||||
|
||||
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)"
|
||||
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 dimless ("\<one>")
|
||||
where [si_def]: "dimless = UNIT(1, NoDimension)"
|
||||
|
||||
subsubsection \<open>The Projection: Stripping the SI-Tags \<close>
|
||||
|
||||
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
|
||||
"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_equiv_iff:
|
||||
fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]"
|
||||
shows "x \<approx>\<^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 (fromUnit ta) \<noteq> magn (fromUnit t)"
|
||||
by (simp add: magnQuant_def unit_eq_iff_magn_eq)
|
||||
then show ?thesis
|
||||
by (metis (full_types) Quant_equiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def)
|
||||
qed
|
||||
|
||||
lemma unit_le_iff_magn_le:
|
||||
"x \<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_scaleQ [si_def]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_qinv [si_def]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
|
||||
by (simp add: magnQuant_def, transfer, simp)
|
||||
|
||||
lemma magnQuant_qdiv [si_def]: "\<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_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)
|
||||
where [si_def, si_eq]: "dimless = UNIT(1, NoDimension)"
|
||||
|
||||
end
|
||||
|
|
@ -6,7 +6,7 @@ theory SI_Units
|
|||
"HOL-Eisbach.Eisbach"
|
||||
begin
|
||||
|
||||
named_theorems si_def
|
||||
named_theorems si_def and si_eq
|
||||
|
||||
text\<open>
|
||||
The International System of Units (SI, abbreviated from the French
|
||||
|
|
|
|||
Loading…
Reference in New Issue