From 4b605faa2d918b1ecb60a61b521a4b955aa6af14 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Fri, 20 Mar 2020 10:29:49 +0000 Subject: [PATCH] Improved proof support. Added some proofs of the astronomical constants. --- src/SI/ISQ_Algebra.thy | 11 ++++++++--- src/SI/ISQ_Dimensions.thy | 16 ++++++++-------- src/SI/ISQ_Proof.thy | 38 +++++++++++++++++++++++++++++++++----- src/SI/ISQ_Quantities.thy | 2 +- src/SI/ROOT | 3 ++- src/SI/SI_Astronomical.thy | 36 ++++++++++++++++++++++++++++++++++-- src/SI/SI_Derived.thy | 4 ---- src/SI/document/root.tex | 4 ++-- 8 files changed, 88 insertions(+), 26 deletions(-) diff --git a/src/SI/ISQ_Algebra.thy b/src/SI/ISQ_Algebra.thy index 2ab5e1c..7be69ae 100644 --- a/src/SI/ISQ_Algebra.thy +++ b/src/SI/ISQ_Algebra.thy @@ -25,7 +25,7 @@ lemma scaleQ_inv: "-a \ x = a \ -x" by si_calc lemma scaleQ_as_qprod: "a \ x \\<^sub>Q (a \ \) \<^bold>\ x" - by si_calc + by (si_simp) lemma mult_scaleQ_left [simp]: "(a \ x) \<^bold>\ y = a \ x \<^bold>\ y" by (si_simp add: mult.assoc) @@ -53,7 +53,7 @@ text\The following weak congruences will allow for replacing equivalences lemma qtimes_weak_cong_left: assumes "x \\<^sub>Q y" shows "x\<^bold>\z \\<^sub>Q y\<^bold>\z" - using assms by si_calc + using assms by si_simp lemma qtimes_weak_cong_right: assumes "x \\<^sub>Q y" @@ -65,11 +65,16 @@ lemma qinverse_weak_cong: shows "x\<^sup>-\<^sup>\ \\<^sub>Q y\<^sup>-\<^sup>\" using assms by si_calc +lemma scaleQ_cong: + assumes "y \\<^sub>Q z" + shows "x \ y \\<^sub>Q x \ z" + using assms by si_calc + lemma qinverse_qinverse: "x\<^sup>-\<^sup>\\<^sup>-\<^sup>\ \\<^sub>Q x" by si_calc lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\ = 0 \ x = 0" - by si_calc + by (auto, si_calc+) lemma qinverse_qtimes: "(x \<^bold>\ y)\<^sup>-\<^sup>\ \\<^sub>Q x\<^sup>-\<^sup>\ \<^bold>\ y\<^sup>-\<^sup>\" by si_calc diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy index 8439e77..3385ef9 100644 --- a/src/SI/ISQ_Dimensions.thy +++ b/src/SI/ISQ_Dimensions.thy @@ -215,49 +215,49 @@ text\ Next, we embed the base dimensions into the dimension type expressio instantiation Length :: basedim_type 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)+) end instantiation Mass :: basedim_type 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)+) end instantiation Time :: basedim_type 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)+) end instantiation Current :: basedim_type 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)+) end instantiation Temperature :: basedim_type begin -definition [si_def]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\" +definition [si_eq]: "dim_ty_sem_Temperature (_::Temperature itself) = \<^bold>\" instance by (intro_classes, auto simp add: dim_ty_sem_Temperature_def is_BaseDim_def, (transfer, simp)+) end instantiation Amount :: basedim_type 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)+) end instantiation Intensity :: basedim_type 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)+) end instantiation NoDimension :: dim_type 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)+) end diff --git a/src/SI/ISQ_Proof.thy b/src/SI/ISQ_Proof.thy index 1bfd840..3833fd9 100644 --- a/src/SI/ISQ_Proof.thy +++ b/src/SI/ISQ_Proof.thy @@ -12,24 +12,46 @@ definition magQ :: "'a['u::dim_type] \ 'a" ("\_\\<^s definition dimQ :: "'a['u::dim_type] \ Dimension" where [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 \ \x\\<^sub>Q = \y\\<^sub>Q" by (auto simp add: magQ_def, transfer, simp) -lemma unit_equiv_iff [si_transfer]: +lemma quant_eqI [si_transfer]: + "\x\\<^sub>Q = \y\\<^sub>Q \ 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]" shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ QD('u\<^sub>1) = QD('u\<^sub>2)" proof - have "\t ta. (ta::'a['u\<^sub>2]) = t \ mag (fromQ ta) \ 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 by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def) 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) \ \x\\<^sub>Q = \y\\<^sub>Q" + shows "x \\<^sub>Q y" + using assms quant_equiv_iff by blast + +lemma quant_le_iff_magn_le [si_eq]: "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" by (auto simp add: magQ_def; (transfer, simp)) +lemma quant_leI [si_transfer]: + "\x\\<^sub>Q \ \y\\<^sub>Q \ x \ y" + by (simp add: quant_le_iff_magn_le) + +lemma quant_less_iff_magn_less [si_eq]: + "x < y \ \x\\<^sub>Q < \y\\<^sub>Q" + by (auto simp add: magQ_def; (transfer, simp)) + +lemma quant_lessI [si_transfer]: + "\x\\<^sub>Q < \y\\<^sub>Q \ x < y" + by (simp add: quant_less_iff_magn_less) + lemma magQ_zero [si_eq]: "\0\\<^sub>Q = 0" by (simp add: magQ_def, transfer, simp) @@ -64,10 +86,16 @@ lemma magQ_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n" apply (metis magQ_def magQ_one magQ_plus numeral_code(3)) 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 "\coerceQuantT t q\\<^sub>Q = \q\\<^sub>Q" + by (simp add: coerceQuantT_def magQ_def assms, metis assms qequiv.rep_eq updown_eq_iff) + text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ 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 \ The next tactic additionally compiles the semantics of the underlying units \ diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy index fbb6b79..9f139cf 100644 --- a/src/SI/ISQ_Quantities.thy +++ b/src/SI/ISQ_Quantities.thy @@ -164,7 +164,7 @@ text \ Since quantities can have dimension type expressions that are disti expressions. This requires that the underlying dimensions are the same. \ definition coerceQuantT :: "'d\<^sub>2 itself \ 'a['d\<^sub>1::dim_type] \ 'a['d\<^sub>2::dim_type]" where -"QD('d\<^sub>1) = QD('d\<^sub>2) \ coerceQuantT t x = (toQ (fromQ x))" +[si_def]: "QD('d\<^sub>1) = QD('d\<^sub>2) \ coerceQuantT t x = (toQ (fromQ x))" syntax "_QCOERCE" :: "type \ logic \ logic" ("QCOERCE[_]") diff --git a/src/SI/ROOT b/src/SI/ROOT index 714c21a..89241f2 100644 --- a/src/SI/ROOT +++ b/src/SI/ROOT @@ -47,10 +47,11 @@ session "SI" = Main + options [document = pdf, document_output = "document/output", document_variants="document:outline=/proof,/ML"] sessions - "HOL-Eisbach" + "HOL-Eisbach" "HOL-Decision_Procs" theories "ISQ" "SI" + "SI_Astronomical" document_files "root.tex" "adb-long.bib" diff --git a/src/SI/SI_Astronomical.thy b/src/SI/SI_Astronomical.thy index aa09935..f9820b5 100644 --- a/src/SI/SI_Astronomical.thy +++ b/src/SI/SI_Astronomical.thy @@ -1,13 +1,45 @@ section \ Astronomical Constants \ theory SI_Astronomical - imports SI_Accepted + imports SI "HOL-Decision_Procs.Approximation" begin +text \ 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. \ + definition julian_year :: "'a::field[T]" where -"julian_year = 365.25 \ day" +[si_eq]: "julian_year = 365.25 \ day" definition light_year :: "'a::field_char_0[L]" where "light_year = QCOERCE[L] (\<^bold>c \<^bold>\ julian_year)" +text \ We need to apply a coercion in the definition of light year to convert the dimension type + from \<^typ>\L \ T\<^sup>-\<^sup>1 \ T\ to \<^typ>\L\. The correctness of this coercion is confirmed by the following + equivalence theorem. \ + +lemma light_year: "light_year \\<^sub>Q \<^bold>c \<^bold>\ julian_year" + unfolding light_year_def by (si_calc) + +lemma light_year_eq [si_eq]: "\light_year\\<^sub>Q = \\<^bold>c \<^bold>\ julian_year\\<^sub>Q" + using light_year quant_equiv_iff by blast + +text \ HOL can characterise \<^const>\pi\ exactly and so we also give an exact value for the parsec. \ + +definition parsec :: "real[L]" where +[si_eq]: "parsec = 648000 / pi \ astronomical_unit" + +text \ We calculate some conservative bounds on the parsec: it is somewhere between 3.26 and 3.27 + light-years. \ + +lemma parsec_lb: "3.26 \ light_year < parsec" + by (si_simp, approximation 12) + +lemma parsec_ub: "parsec < 3.27 \ light_year" + by (si_simp, approximation 12) + +text\ The full beauty of the approach is perhaps revealed here, with the + type of a classical three-dimensional gravitation field:\ + +type_synonym gravitation_field = "real\<^sup>3[L] \ (real\<^sup>3[L \ T\<^sup>-\<^sup>2])" + end \ No newline at end of file diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index e231ea6..51c5fa5 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -39,10 +39,6 @@ definition degrees_celcius :: "'a::field_char_0 \ 'a[\]" ("_\ definition [si_eq]: "gram = milli \ kilogram" -text\The full beauty of the approach is perhaps revealed here, with the - type of a classical three-dimensional gravitation field:\ -type_synonym gravitation_field = "real\<^sup>3[L] \ (real\<^sup>3[L \ T\<^sup>-\<^sup>2])" - subsection \ Equivalences \ lemma joule_alt_def: "joule \\<^sub>Q newton \<^bold>\ meter" diff --git a/src/SI/document/root.tex b/src/SI/document/root.tex index 078bfb2..f0c9a9a 100644 --- a/src/SI/document/root.tex +++ b/src/SI/document/root.tex @@ -43,8 +43,8 @@ \begin{document} -\title{Type and Proof Support for SI Units} -\author{ Simon Foster \and Burkhart Wolff} +\title{International Systems of Quantities and Units in Isabelle/HOL} +\author{Simon Foster \and Burkhart Wolff} \maketitle \textbf{ Abstract }