Improved proof support. Added some proofs of the astronomical constants.
This commit is contained in:
parent
31c0dd56e8
commit
4b605faa2d
|
@ -25,7 +25,7 @@ lemma scaleQ_inv: "-a \<odot> x = a \<odot> -x"
|
||||||
by si_calc
|
by si_calc
|
||||||
|
|
||||||
lemma scaleQ_as_qprod: "a \<odot> x \<cong>\<^sub>Q (a \<odot> \<one>) \<^bold>\<cdot> x"
|
lemma scaleQ_as_qprod: "a \<odot> x \<cong>\<^sub>Q (a \<odot> \<one>) \<^bold>\<cdot> x"
|
||||||
by si_calc
|
by (si_simp)
|
||||||
|
|
||||||
lemma mult_scaleQ_left [simp]: "(a \<odot> x) \<^bold>\<cdot> y = a \<odot> x \<^bold>\<cdot> y"
|
lemma mult_scaleQ_left [simp]: "(a \<odot> x) \<^bold>\<cdot> y = a \<odot> x \<^bold>\<cdot> y"
|
||||||
by (si_simp add: mult.assoc)
|
by (si_simp add: mult.assoc)
|
||||||
|
@ -53,7 +53,7 @@ text\<open>The following weak congruences will allow for replacing equivalences
|
||||||
lemma qtimes_weak_cong_left:
|
lemma qtimes_weak_cong_left:
|
||||||
assumes "x \<cong>\<^sub>Q y"
|
assumes "x \<cong>\<^sub>Q y"
|
||||||
shows "x\<^bold>\<cdot>z \<cong>\<^sub>Q y\<^bold>\<cdot>z"
|
shows "x\<^bold>\<cdot>z \<cong>\<^sub>Q y\<^bold>\<cdot>z"
|
||||||
using assms by si_calc
|
using assms by si_simp
|
||||||
|
|
||||||
lemma qtimes_weak_cong_right:
|
lemma qtimes_weak_cong_right:
|
||||||
assumes "x \<cong>\<^sub>Q y"
|
assumes "x \<cong>\<^sub>Q y"
|
||||||
|
@ -65,11 +65,16 @@ lemma qinverse_weak_cong:
|
||||||
shows "x\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y\<^sup>-\<^sup>\<one>"
|
shows "x\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y\<^sup>-\<^sup>\<one>"
|
||||||
using assms by si_calc
|
using assms by si_calc
|
||||||
|
|
||||||
|
lemma scaleQ_cong:
|
||||||
|
assumes "y \<cong>\<^sub>Q z"
|
||||||
|
shows "x \<odot> y \<cong>\<^sub>Q x \<odot> z"
|
||||||
|
using assms by si_calc
|
||||||
|
|
||||||
lemma qinverse_qinverse: "x\<^sup>-\<^sup>\<one>\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x"
|
lemma qinverse_qinverse: "x\<^sup>-\<^sup>\<one>\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x"
|
||||||
by si_calc
|
by si_calc
|
||||||
|
|
||||||
lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\<one> = 0 \<longleftrightarrow> x = 0"
|
lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\<one> = 0 \<longleftrightarrow> x = 0"
|
||||||
by si_calc
|
by (auto, 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>"
|
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
|
by si_calc
|
||||||
|
|
|
@ -215,49 +215,49 @@ text\<open> Next, we embed the base dimensions into the dimension type expressio
|
||||||
|
|
||||||
instantiation Length :: basedim_type
|
instantiation Length :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Length (_::Length itself) = \<^bold>L"
|
definition [si_eq]: "dim_ty_sem_Length (_::Length itself) = \<^bold>L"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Length_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Mass :: basedim_type
|
instantiation Mass :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Mass (_::Mass itself) = \<^bold>M"
|
definition [si_eq]: "dim_ty_sem_Mass (_::Mass itself) = \<^bold>M"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Mass_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Time :: basedim_type
|
instantiation Time :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Time (_::Time itself) = \<^bold>T"
|
definition [si_eq]: "dim_ty_sem_Time (_::Time itself) = \<^bold>T"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Time_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Current :: basedim_type
|
instantiation Current :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Current (_::Current itself) = \<^bold>I"
|
definition [si_eq]: "dim_ty_sem_Current (_::Current itself) = \<^bold>I"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Current_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Temperature :: basedim_type
|
instantiation Temperature :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\<Theta>"
|
definition [si_eq]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\<Theta>"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Amount :: basedim_type
|
instantiation Amount :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Amount (_::Amount itself) = \<^bold>N"
|
definition [si_eq]: "dim_ty_sem_Amount (_::Amount itself) = \<^bold>N"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Amount_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation Intensity :: basedim_type
|
instantiation Intensity :: basedim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_Intensity (_::Intensity itself) = \<^bold>J"
|
definition [si_eq]: "dim_ty_sem_Intensity (_::Intensity itself) = \<^bold>J"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_Intensity_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
instantiation NoDimension :: dim_type
|
instantiation NoDimension :: dim_type
|
||||||
begin
|
begin
|
||||||
definition [si_def]: "dim_ty_sem_NoDimension (_::NoDimension itself) = (1::Dimension)"
|
definition [si_eq]: "dim_ty_sem_NoDimension (_::NoDimension itself) = (1::Dimension)"
|
||||||
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+)
|
instance by (intro_classes, auto simp add: dim_ty_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
|
@ -12,24 +12,46 @@ definition magQ :: "'a['u::dim_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^s
|
||||||
definition dimQ :: "'a['u::dim_type] \<Rightarrow> Dimension" where
|
definition dimQ :: "'a['u::dim_type] \<Rightarrow> Dimension" where
|
||||||
[si_def]: "dimQ x = dim (fromQ x)"
|
[si_def]: "dimQ x = dim (fromQ x)"
|
||||||
|
|
||||||
lemma unit_eq_iff_mag_eq [si_transfer]:
|
lemma quant_eq_iff_mag_eq [si_eq]:
|
||||||
"x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
|
"x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||||
by (auto simp add: magQ_def, transfer, simp)
|
by (auto simp add: magQ_def, transfer, simp)
|
||||||
|
|
||||||
lemma unit_equiv_iff [si_transfer]:
|
lemma quant_eqI [si_transfer]:
|
||||||
|
"\<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<Longrightarrow> x = y"
|
||||||
|
by (simp add: quant_eq_iff_mag_eq)
|
||||||
|
|
||||||
|
lemma quant_equiv_iff [si_eq]:
|
||||||
fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]"
|
fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]"
|
||||||
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> QD('u\<^sub>1) = QD('u\<^sub>2)"
|
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> QD('u\<^sub>1) = QD('u\<^sub>2)"
|
||||||
proof -
|
proof -
|
||||||
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
|
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
|
||||||
by (simp add: magQ_def unit_eq_iff_mag_eq)
|
by (simp add: magQ_def quant_eq_iff_mag_eq)
|
||||||
then show ?thesis
|
then show ?thesis
|
||||||
by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def)
|
by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
lemma unit_le_iff_magn_le [si_transfer]:
|
lemma quant_equivI [si_transfer]:
|
||||||
|
fixes x :: "'a['u\<^sub>1::dim_type]" and y :: "'a['u\<^sub>2::dim_type]"
|
||||||
|
assumes "QD('u\<^sub>1) = QD('u\<^sub>2)" "QD('u\<^sub>1) = QD('u\<^sub>2) \<Longrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||||
|
shows "x \<cong>\<^sub>Q y"
|
||||||
|
using assms quant_equiv_iff by blast
|
||||||
|
|
||||||
|
lemma quant_le_iff_magn_le [si_eq]:
|
||||||
"x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
"x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||||
by (auto simp add: magQ_def; (transfer, simp))
|
by (auto simp add: magQ_def; (transfer, simp))
|
||||||
|
|
||||||
|
lemma quant_leI [si_transfer]:
|
||||||
|
"\<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q \<Longrightarrow> x \<le> y"
|
||||||
|
by (simp add: quant_le_iff_magn_le)
|
||||||
|
|
||||||
|
lemma quant_less_iff_magn_less [si_eq]:
|
||||||
|
"x < y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q < \<lbrakk>y\<rbrakk>\<^sub>Q"
|
||||||
|
by (auto simp add: magQ_def; (transfer, simp))
|
||||||
|
|
||||||
|
lemma quant_lessI [si_transfer]:
|
||||||
|
"\<lbrakk>x\<rbrakk>\<^sub>Q < \<lbrakk>y\<rbrakk>\<^sub>Q \<Longrightarrow> x < y"
|
||||||
|
by (simp add: quant_less_iff_magn_less)
|
||||||
|
|
||||||
lemma magQ_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
lemma magQ_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
|
||||||
by (simp add: magQ_def, transfer, simp)
|
by (simp add: magQ_def, transfer, simp)
|
||||||
|
|
||||||
|
@ -64,10 +86,16 @@ lemma magQ_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
|
||||||
apply (metis magQ_def magQ_one magQ_plus numeral_code(3))
|
apply (metis magQ_def magQ_one magQ_plus numeral_code(3))
|
||||||
done
|
done
|
||||||
|
|
||||||
|
lemma magQ_coerce [si_eq]:
|
||||||
|
fixes q :: "'a['d\<^sub>1::dim_type]" and t :: "'d\<^sub>2::dim_type itself"
|
||||||
|
assumes "QD('d\<^sub>1) = QD('d\<^sub>2)"
|
||||||
|
shows "\<lbrakk>coerceQuantT t q\<rbrakk>\<^sub>Q = \<lbrakk>q\<rbrakk>\<^sub>Q"
|
||||||
|
by (simp add: coerceQuantT_def magQ_def assms, metis assms qequiv.rep_eq updown_eq_iff)
|
||||||
|
|
||||||
text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
|
text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
|
||||||
|
|
||||||
method si_simp uses add =
|
method si_simp uses add =
|
||||||
(simp add: add si_transfer si_eq field_simps)
|
(rule_tac si_transfer; simp add: add si_eq field_simps)
|
||||||
|
|
||||||
text \<open> The next tactic additionally compiles the semantics of the underlying units \<close>
|
text \<open> The next tactic additionally compiles the semantics of the underlying units \<close>
|
||||||
|
|
||||||
|
|
|
@ -164,7 +164,7 @@ text \<open> Since quantities can have dimension type expressions that are disti
|
||||||
expressions. This requires that the underlying dimensions are the same. \<close>
|
expressions. This requires that the underlying dimensions are the same. \<close>
|
||||||
|
|
||||||
definition coerceQuantT :: "'d\<^sub>2 itself \<Rightarrow> 'a['d\<^sub>1::dim_type] \<Rightarrow> 'a['d\<^sub>2::dim_type]" where
|
definition coerceQuantT :: "'d\<^sub>2 itself \<Rightarrow> 'a['d\<^sub>1::dim_type] \<Rightarrow> 'a['d\<^sub>2::dim_type]" where
|
||||||
"QD('d\<^sub>1) = QD('d\<^sub>2) \<Longrightarrow> coerceQuantT t x = (toQ (fromQ x))"
|
[si_def]: "QD('d\<^sub>1) = QD('d\<^sub>2) \<Longrightarrow> coerceQuantT t x = (toQ (fromQ x))"
|
||||||
|
|
||||||
syntax
|
syntax
|
||||||
"_QCOERCE" :: "type \<Rightarrow> logic \<Rightarrow> logic" ("QCOERCE[_]")
|
"_QCOERCE" :: "type \<Rightarrow> logic \<Rightarrow> logic" ("QCOERCE[_]")
|
||||||
|
|
|
@ -47,10 +47,11 @@ session "SI" = Main +
|
||||||
options [document = pdf, document_output = "document/output",
|
options [document = pdf, document_output = "document/output",
|
||||||
document_variants="document:outline=/proof,/ML"]
|
document_variants="document:outline=/proof,/ML"]
|
||||||
sessions
|
sessions
|
||||||
"HOL-Eisbach"
|
"HOL-Eisbach" "HOL-Decision_Procs"
|
||||||
theories
|
theories
|
||||||
"ISQ"
|
"ISQ"
|
||||||
"SI"
|
"SI"
|
||||||
|
"SI_Astronomical"
|
||||||
document_files
|
document_files
|
||||||
"root.tex"
|
"root.tex"
|
||||||
"adb-long.bib"
|
"adb-long.bib"
|
||||||
|
|
|
@ -1,13 +1,45 @@
|
||||||
section \<open> Astronomical Constants \<close>
|
section \<open> Astronomical Constants \<close>
|
||||||
|
|
||||||
theory SI_Astronomical
|
theory SI_Astronomical
|
||||||
imports SI_Accepted
|
imports SI "HOL-Decision_Procs.Approximation"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
text \<open> We create a number of astronomical constants and prove relationships between some of them.
|
||||||
|
For this, we use the approximation method that can compute bounds on transcendental functions. \<close>
|
||||||
|
|
||||||
definition julian_year :: "'a::field[T]" where
|
definition julian_year :: "'a::field[T]" where
|
||||||
"julian_year = 365.25 \<odot> day"
|
[si_eq]: "julian_year = 365.25 \<odot> day"
|
||||||
|
|
||||||
definition light_year :: "'a::field_char_0[L]" where
|
definition light_year :: "'a::field_char_0[L]" where
|
||||||
"light_year = QCOERCE[L] (\<^bold>c \<^bold>\<cdot> julian_year)"
|
"light_year = QCOERCE[L] (\<^bold>c \<^bold>\<cdot> julian_year)"
|
||||||
|
|
||||||
|
text \<open> We need to apply a coercion in the definition of light year to convert the dimension type
|
||||||
|
from \<^typ>\<open>L \<cdot> T\<^sup>-\<^sup>1 \<cdot> T\<close> to \<^typ>\<open>L\<close>. The correctness of this coercion is confirmed by the following
|
||||||
|
equivalence theorem. \<close>
|
||||||
|
|
||||||
|
lemma light_year: "light_year \<cong>\<^sub>Q \<^bold>c \<^bold>\<cdot> julian_year"
|
||||||
|
unfolding light_year_def by (si_calc)
|
||||||
|
|
||||||
|
lemma light_year_eq [si_eq]: "\<lbrakk>light_year\<rbrakk>\<^sub>Q = \<lbrakk>\<^bold>c \<^bold>\<cdot> julian_year\<rbrakk>\<^sub>Q"
|
||||||
|
using light_year quant_equiv_iff by blast
|
||||||
|
|
||||||
|
text \<open> HOL can characterise \<^const>\<open>pi\<close> exactly and so we also give an exact value for the parsec. \<close>
|
||||||
|
|
||||||
|
definition parsec :: "real[L]" where
|
||||||
|
[si_eq]: "parsec = 648000 / pi \<odot> astronomical_unit"
|
||||||
|
|
||||||
|
text \<open> We calculate some conservative bounds on the parsec: it is somewhere between 3.26 and 3.27
|
||||||
|
light-years. \<close>
|
||||||
|
|
||||||
|
lemma parsec_lb: "3.26 \<odot> light_year < parsec"
|
||||||
|
by (si_simp, approximation 12)
|
||||||
|
|
||||||
|
lemma parsec_ub: "parsec < 3.27 \<odot> light_year"
|
||||||
|
by (si_simp, approximation 12)
|
||||||
|
|
||||||
|
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])"
|
||||||
|
|
||||||
end
|
end
|
|
@ -39,10 +39,6 @@ definition degrees_celcius :: "'a::field_char_0 \<Rightarrow> 'a[\<Theta>]" ("_\
|
||||||
|
|
||||||
definition [si_eq]: "gram = milli \<odot> kilogram"
|
definition [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>
|
|
||||||
type_synonym gravitation_field = "real\<^sup>3[L] \<Rightarrow> (real\<^sup>3[L \<cdot> T\<^sup>-\<^sup>2])"
|
|
||||||
|
|
||||||
subsection \<open> Equivalences \<close>
|
subsection \<open> Equivalences \<close>
|
||||||
|
|
||||||
lemma joule_alt_def: "joule \<cong>\<^sub>Q newton \<^bold>\<cdot> meter"
|
lemma joule_alt_def: "joule \<cong>\<^sub>Q newton \<^bold>\<cdot> meter"
|
||||||
|
|
|
@ -43,8 +43,8 @@
|
||||||
|
|
||||||
\begin{document}
|
\begin{document}
|
||||||
|
|
||||||
\title{Type and Proof Support for SI Units}
|
\title{International Systems of Quantities and Units in Isabelle/HOL}
|
||||||
\author{ Simon Foster \and Burkhart Wolff}
|
\author{Simon Foster \and Burkhart Wolff}
|
||||||
\maketitle
|
\maketitle
|
||||||
|
|
||||||
\textbf{ Abstract }
|
\textbf{ Abstract }
|
||||||
|
|
Loading…
Reference in New Issue