From 31c0dd56e86cb833a837618b96c4ffe1da753704 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Wed, 18 Mar 2020 16:02:09 +0000 Subject: [PATCH] Some renaming, cleaning, and addition of astronomical units --- src/SI/ISQ.thy | 2 ++ src/SI/ISQ_Proof.thy | 59 ++++++++++++++++++++------------------ src/SI/ISQ_Quantities.thy | 8 +++++- src/SI/SI.thy | 2 ++ src/SI/SI_Astronomical.thy | 13 +++++++++ src/SI/SI_Units.thy | 6 ++-- 6 files changed, 58 insertions(+), 32 deletions(-) create mode 100644 src/SI/SI_Astronomical.thy diff --git a/src/SI/ISQ.thy b/src/SI/ISQ.thy index 53f6142..61410c3 100644 --- a/src/SI/ISQ.thy +++ b/src/SI/ISQ.thy @@ -1,3 +1,5 @@ +section \ Meta-Theory for ISQ \ + theory ISQ imports ISQ_Dimensions ISQ_Quantities ISQ_Proof ISQ_Algebra begin end \ No newline at end of file diff --git a/src/SI/ISQ_Proof.thy b/src/SI/ISQ_Proof.thy index 9ce97b9..1bfd840 100644 --- a/src/SI/ISQ_Proof.thy +++ b/src/SI/ISQ_Proof.thy @@ -6,59 +6,62 @@ begin named_theorems si_transfer -definition magQuant :: "'a['u::dim_type] \ 'a" ("\_\\<^sub>Q") where -[si_def]: "magQuant x = mag (fromQ x)" +definition magQ :: "'a['u::dim_type] \ 'a" ("\_\\<^sub>Q") where +[si_def]: "magQ x = mag (fromQ x)" + +definition dimQ :: "'a['u::dim_type] \ Dimension" where +[si_def]: "dimQ x = dim (fromQ x)" lemma unit_eq_iff_mag_eq [si_transfer]: "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" - by (auto simp add: magQuant_def, transfer, simp) + by (auto simp add: magQ_def, transfer, simp) lemma unit_equiv_iff [si_transfer]: 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: magQuant_def unit_eq_iff_mag_eq) + by (simp add: magQ_def unit_eq_iff_mag_eq) then show ?thesis - by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQuant_def) + by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQ_def) qed lemma unit_le_iff_magn_le [si_transfer]: "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" - by (auto simp add: magQuant_def; (transfer, simp)) + by (auto simp add: magQ_def; (transfer, simp)) -lemma magQuant_zero [si_eq]: "\0\\<^sub>Q = 0" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_zero [si_eq]: "\0\\<^sub>Q = 0" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_one [si_eq]: "\1\\<^sub>Q = 1" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_one [si_eq]: "\1\\<^sub>Q = 1" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_plus [si_eq]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_plus [si_eq]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_minus [si_eq]: "\x - y\\<^sub>Q = \x\\<^sub>Q - \y\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_minus [si_eq]: "\x - y\\<^sub>Q = \x\\<^sub>Q - \y\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_uminus [si_eq]: "\- x\\<^sub>Q = - \x\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_uminus [si_eq]: "\- x\\<^sub>Q = - \x\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_scaleQ [si_eq]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_scaleQ [si_eq]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_qtimes [si_eq]: "\x \<^bold>\ y\\<^sub>Q = \x\\<^sub>Q \ \y\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_qtimes [si_eq]: "\x \<^bold>\ y\\<^sub>Q = \x\\<^sub>Q \ \y\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_qinverse [si_eq]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp) +lemma magQ_qinverse [si_eq]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" + by (simp add: magQ_def, transfer, simp) -lemma magQuant_qdivivide [si_eq]: "\(x::('a::field)[_]) \<^bold>/ y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" - by (simp add: magQuant_def, transfer, simp add: field_class.field_divide_inverse) +lemma magQ_qdivivide [si_eq]: "\(x::('a::field)[_]) \<^bold>/ y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" + by (simp add: magQ_def, transfer, simp add: field_class.field_divide_inverse) -lemma magQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n" +lemma magQ_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n" apply (induct n, simp_all add: si_def) - 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)) + apply (metis magQ_def magQ_one) + apply (metis magQ_def magQ_plus numeral_code(2)) + apply (metis magQ_def magQ_one magQ_plus numeral_code(3)) done text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy index b4b6144..fbb6b79 100644 --- a/src/SI/ISQ_Quantities.thy +++ b/src/SI/ISQ_Quantities.thy @@ -166,6 +166,12 @@ text \ Since quantities can have dimension type expressions that are disti 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))" +syntax + "_QCOERCE" :: "type \ logic \ logic" ("QCOERCE[_]") + +translations + "QCOERCE['t]" == "CONST coerceQuantT TYPE('t)" + subsection \ Predicates on Typed Quantities \ text \ The standard HOL order \<^term>\(\)\ and equality \<^term>\(=)\ have the homogeneous type @@ -237,7 +243,7 @@ lift_definition qinverse :: "('n::field)['a::dim_type] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) is "inverse" by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def) -abbreviation +abbreviation (input) qdivide :: "('n::field)['a::dim_type] \ 'n['b::dim_type] \ 'n['a/'b]" (infixl "\<^bold>'/" 70) where "qdivide x y \ x \<^bold>\ y\<^sup>-\<^sup>\" diff --git a/src/SI/SI.thy b/src/SI/SI.thy index c3d961b..299e6e9 100644 --- a/src/SI/SI.thy +++ b/src/SI/SI.thy @@ -1,3 +1,5 @@ +section \ Meta-Theory for SI Units \ + theory SI imports SI_Units SI_Constants SI_Prefix SI_Derived SI_Accepted SI_Imperial begin end \ No newline at end of file diff --git a/src/SI/SI_Astronomical.thy b/src/SI/SI_Astronomical.thy new file mode 100644 index 0000000..aa09935 --- /dev/null +++ b/src/SI/SI_Astronomical.thy @@ -0,0 +1,13 @@ +section \ Astronomical Constants \ + +theory SI_Astronomical + imports SI_Accepted +begin + +definition julian_year :: "'a::field[T]" where +"julian_year = 365.25 \ day" + +definition light_year :: "'a::field_char_0[L]" where +"light_year = QCOERCE[L] (\<^bold>c \<^bold>\ julian_year)" + +end \ No newline at end of file diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index c817560..e41eaaa 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -3,7 +3,7 @@ chapter \ International System of Units \ section \ SI Units Semantics \ theory SI_Units - imports ISQ_Proof + imports ISQ begin text \ An SI unit is simply a particular kind of quantity. \ @@ -27,8 +27,8 @@ translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)" lemma mk_base_unit: "is_base_unit (mk_base_unit a)" by (simp add: si_eq, transfer, simp add: is_BaseDim) -lemma magQuant_mk [si_eq]: "\BUNIT('u::basedim_type)\\<^sub>Q = 1" - by (simp add: magQuant_def si_eq, transfer, simp) +lemma magQ_mk [si_eq]: "\BUNIT('u::basedim_type)\\<^sub>Q = 1" + by (simp add: magQ_def si_eq, transfer, simp) text \ We now define the seven base units. Effectively, these definitions axiomatise given names for the \<^term>\1\ elements of the base quantities. \