diff --git a/src/SI/SI_Algebra.thy b/src/SI/ISQ_Algebra.thy similarity index 98% rename from src/SI/SI_Algebra.thy rename to src/SI/ISQ_Algebra.thy index 82095fc..2ab5e1c 100644 --- a/src/SI/SI_Algebra.thy +++ b/src/SI/ISQ_Algebra.thy @@ -1,7 +1,7 @@ section \ Algebraic Laws \ -theory SI_Algebra - imports SI_Proof +theory ISQ_Algebra + imports ISQ_Proof begin subsection \ Quantity Scale \ diff --git a/src/SI/SI_Proof.thy b/src/SI/ISQ_Proof.thy similarity index 76% rename from src/SI/SI_Proof.thy rename to src/SI/ISQ_Proof.thy index 2e95f45..16209cf 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/ISQ_Proof.thy @@ -1,7 +1,7 @@ -section \Basic Proof Support for SI Units \ +section \ Proof Support for Quantities \ -theory SI_Proof - imports SI_Units +theory ISQ_Proof + imports ISQ_Quantities begin named_theorems si_transfer @@ -61,9 +61,6 @@ lemma magQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3)) done -lemma magQuant_mk [si_eq]: "\BUNIT('u::dim_type)\\<^sub>Q = 1" - by (simp add: magQuant_def, transfer, simp) - text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ method si_simp uses add = @@ -74,24 +71,6 @@ text \ The next tactic additionally compiles the semantics of the underlyi method si_calc uses add = (si_simp add: add; simp add: si_def add) -(* -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 - si_sem_Intensity_def si_sem_NoDimension_def - - si_sem_UnitTimes_def si_sem_UnitInv_def - times_Unit_ext_def one_Unit_ext_def -*) - lemma "QD(N \ \ \ N) = QD(\ \ N\<^sup>2)" by (simp add: si_eq si_def) -lemma "(meter \<^bold>\ second\<^sup>-\<^sup>\) \<^bold>\ second \\<^sub>Q meter" - by (si_calc) - end \ No newline at end of file diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy index 3021314..dffc665 100644 --- a/src/SI/ISQ_Quantities.thy +++ b/src/SI/ISQ_Quantities.thy @@ -165,19 +165,21 @@ definition coerceQuantT :: "'d\<^sub>2 itself \ 'a['d\<^sub>1::dim_t subsection \ Predicates on Typed Quantities \ -text \ Two SI Unit types are orderable if their magnitude type is of class @{class "order"}, - and have the same dimensions (not necessarily dimension types).\ +text \ The standard HOL order \<^term>\(\)\ and equality \<^term>\(=)\ have the homogeneous type + \<^typ>\'a \ 'a \ bool\ and so they cannot compare values of different types. Consequently, + we define a heterogeneous order and equivalence on typed quantities. \ lift_definition qless_eq :: "'n::order['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) is "(\)" . -text\ Two SI Unit types are equivalent if they have the same dimensions - (not necessarily dimension types). This equivalence the a vital point - of the overall construction of SI Units. \ - lift_definition qequiv :: "'n['a::dim_type] \ 'n['b::dim_type] \ bool" (infix "\\<^sub>Q" 50) is "(=)" . +text \ These are both fundamentally the same as the usual order and equality relations, but they + permit potentially different dimension types, \<^typ>\'a\ and \<^typ>\'b\. Two typed quantities are + comparable only when the two dimension types have the same semantic dimension. +\ + lemma qequiv_refl [simp]: "a \\<^sub>Q a" by (simp add: qequiv_def) @@ -192,16 +194,12 @@ theorem qeq_iff_same_dim: shows "x \\<^sub>Q y \ x = y" by (transfer, simp) -(* the following series of equivalent statements ... *) - lemma coerceQuant_eq_iff: fixes x :: "'a['d\<^sub>1::dim_type]" assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" shows "(coerceQuantT TYPE('d\<^sub>2) x) \\<^sub>Q x" by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse) -(* or equivalently *) - lemma coerceQuant_eq_iff2: fixes x :: "'a['d\<^sub>1::dim_type]" assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (coerceQuantT TYPE('d\<^sub>2) x)" @@ -218,16 +216,20 @@ text\This is more general that \y = x \ x \\<^ lemma qeq: fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]" - assumes "x \\<^sub>Q y" - shows "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" + assumes "x \\<^sub>Q y" + shows "QD('d\<^sub>1) = QD('d\<^sub>2)" by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq) -subsection\Operations on Abstract SI-Unit-Types\ +subsection\ Operators on Typed Quantities \ + +text \ We define several operators on typed quantities. These variously compose the dimension types + as well. Multiplication composes the two dimension types. Inverse constructs and inverted + dimension type. Division is defined in terms of multiplication and inverse. \ lift_definition qtimes :: "('n::comm_ring_1)['a::dim_type] \ 'n['b::dim_type] \ 'n['a \'b]" (infixl "\<^bold>\" 69) is "(*)" by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def) - + 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) @@ -236,6 +238,8 @@ abbreviation 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>\" +text \ We also provide some helpful notations for expressing heterogeneous powers. \ + abbreviation qsq ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u" abbreviation qcube ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u" abbreviation qquart ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u\<^bold>\u" @@ -244,6 +248,19 @@ abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>- abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" +text \ Analogous to the \<^const>\scaleR\ operator for vectors, we define the following scalar + multiplication that scales an existing quantity by a numeric value. This operator is + especially important for the representation of quantity values, which consist of a numeric + value and a unit. \ + +lift_definition scaleQ :: "'a \ 'a::comm_ring_1['d::dim_type] \ 'a['d]" (infixr "*\<^sub>Q" 63) + is "\ r x. \ mag = r * mag x, dim = QD('d) \" by simp + +notation scaleQ (infixr "\" 63) + +text \ Finally, we instantiate the arithmetic types classes where possible. We do not instantiate + \<^class>\times\ because this results in a nonsensical homogeneous product on quantities. \ + instantiation QuantT :: (zero,dim_type) zero begin lift_definition zero_QuantT :: "('a, 'b) QuantT" is "\ mag = 0, dim = QD('b) \" @@ -258,6 +275,14 @@ lift_definition one_QuantT :: "('a, 'b) QuantT" is "\ mag = 1, dim = QD(' instance .. end +text \ The following specialised one element has both magnitude and dimension 1: it is a + dimensionless quantity. \ + +abbreviation qone :: "'n::one[\]" ("\") where "qone \ 1" + +text \ Unlike for semantic quantities, the plus operator on typed quantities is total, since the + type system ensures that the dimensions (and the dimension types) must be the same. \ + instantiation QuantT :: (plus,dim_type) plus begin lift_definition plus_QuantT :: "'a['b] \ 'a['b] \ 'a['b]" @@ -266,6 +291,9 @@ lift_definition plus_QuantT :: "'a['b] \ 'a['b] \ 'a['b] instance .. end +text \ We can also show that typed quantities are commutative \<^emph>\additive\ monoids. Indeed, addition + is a much easier operator to deal with in typed quantities, unlike product. \ + instance QuantT :: (semigroup_add,dim_type) semigroup_add by (intro_classes, transfer, simp add: add.assoc) @@ -295,9 +323,13 @@ end instance QuantT :: (numeral,dim_type) numeral .. +text \ Moreover, types quantities also form an additive group. \ + instance QuantT :: (ab_group_add,dim_type) ab_group_add by (intro_classes, (transfer, simp)+) +text \ Typed quantities helpfully can be both partially and a linearly ordered. \ + instantiation QuantT :: (order,dim_type) order begin lift_definition less_eq_QuantT :: "'a['b] \ 'a['b] \ bool" is "\ x y. mag x \ mag y" . @@ -305,11 +337,7 @@ begin instance by (intro_classes, (transfer, simp add: less_le_not_le)+) end -text\The scaling operator permits to multiply the magnitude of a unit; this scalar product -produces what is called "prefixes" in the terminology of the SI system.\ -lift_definition scaleQ :: "'a \ 'a::comm_ring_1['d::dim_type] \ 'a['d]" (infixr "*\<^sub>Q" 63) - is "\ r x. \ mag = r * mag x, dim = QD('d) \" by simp - -notation scaleQ (infixr "\" 63) +instance QuantT :: (linorder,dim_type) linorder + by (intro_classes, transfer, auto) end \ No newline at end of file diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index 4aafe7a..5afe84b 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -1,7 +1,7 @@ section \ Physical Constants \ theory SI_Constants - imports SI_Proof + imports SI_Units begin subsection \ Core Derived Units \ diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index d4e2dfd..342c175 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -1,7 +1,7 @@ section \ SI Units \ theory SI_Units - imports ISQ_Quantities + imports SI_Proof begin lift_definition mk_base_unit :: "'u itself \ ('a::one)['u::dim_type]" @@ -10,6 +10,9 @@ lift_definition mk_base_unit :: "'u itself \ ('a::one)['u::dim_type] syntax "_mk_base_unit" :: "type \ logic" ("BUNIT'(_')") translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)" +lemma magQuant_mk [si_eq]: "\BUNIT('u::dim_type)\\<^sub>Q = 1" + by (simp add: magQuant_def, transfer, simp) + subsection \Polymorphic Operations for SI Base Units \ definition [si_eq]: "meter = BUNIT(L)" @@ -20,9 +23,6 @@ definition [si_eq]: "kelvin = BUNIT(\)" definition [si_eq]: "mole = BUNIT(N)" definition [si_eq]: "candela = BUNIT(J)" -definition dimless ("\") - where [si_eq]: "dimless = BUNIT(NoDimension)" - text\Note that as a consequence of our construction, the term @{term meter} is a SI Unit constant of SI-type @{typ "'a[L]"}, so a unit of dimension @{typ "Length"} with the magnitude of type @{typ"'a"}. A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of @@ -36,4 +36,9 @@ lift_definition is_BaseUnit :: "'a::one['d::dim_type] \ bool" lemma meter_is_BaseUnit: "is_BaseUnit meter" by (simp add: si_eq, transfer, simp) +subsection \ Example Unit Equations \ + +lemma "(meter \<^bold>\ second\<^sup>-\<^sup>\) \<^bold>\ second \\<^sub>Q meter" + by (si_calc) + end \ No newline at end of file