diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy index b13561b..39b2185 100644 --- a/src/SI/ISQ_Dimensions.thy +++ b/src/SI/ISQ_Dimensions.thy @@ -171,7 +171,7 @@ text \ The notation \<^term>\QD('a::dim_type)\ allows to obta The subset of basic dimension types can be characterized by the following type class: \ -class si_basedim = dim_type + +class basedim_type = dim_type + assumes is_BaseDim: "is_BaseDim QD('a)" subsubsection \ Base Dimension Type Expressions \ @@ -209,45 +209,45 @@ translations (type) "J" <= (type) "Intensity" text\ Next, we embed the base dimensions into the dimension type expressions by instantiating the - class \<^class>\si_basedim\ with each of the base dimension types. \ + class \<^class>\basedim_type\ with each of the base dimension types. \ -instantiation Length :: si_basedim +instantiation Length :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Mass :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Time :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Current :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Temperature :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Amount :: basedim_type begin definition [si_def]: "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 :: si_basedim +instantiation Intensity :: basedim_type begin definition [si_def]: "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)+) diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy index 603c5d1..57b14e7 100644 --- a/src/SI/SI_Prefix.thy +++ b/src/SI/SI_Prefix.thy @@ -6,6 +6,9 @@ begin subsection \ Definitions \ +text \ Prefixes are simply numbers that can be composed with units using the scalar + multiplication operator \<^const>\scaleQ\. \ + default_sort ring_char_0 definition deca :: "'a" where [si_eq]: "deca = 10^1" @@ -60,6 +63,9 @@ lemma "1 \ (centi \ meter)\<^sup>-\<^sup>\ = 100 \ meter\ subsection \ Binary Prefixes \ +text \ Although not in general applicable to physical quantities, we include these prefixes + for completeness. \ + default_sort ring_char_0 definition kibi :: "'a" where [si_eq]: "kibi = 2^10" diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index a925a89..a996157 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -13,21 +13,23 @@ text \ Parallel to the seven base quantities, there are seven base units. and a magnitude of \<^term>\1\. Consequently, a base unit corresponds to a unit in the algebraic sense. \ -lift_definition is_BaseUnit :: "'a::one['d::dim_type] \ bool" - is "\ x. mag x = 1 \ is_BaseDim (dim x)" . +lift_definition is_base_unit :: "'a::one['d::dim_type] \ bool" + is "\ x. mag x = 1 \ is_BaseDim (dim x)" . - -lift_definition mk_base_unit :: "'u itself \ ('a::one)['u::dim_type]" - is "\ u. \ mag = 1, dim = QD('u) \" by simp +definition mk_base_unit :: "'u itself \ ('a::one)['u::basedim_type]" + where [si_eq]: "mk_base_unit t = 1" 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) +lemma mk_base_unit: "is_base_unit (mk_base_unit a)" + by (simp add: si_eq, transfer, simp add: is_BaseDim) -text \ We now define the seven base units. Effectively, these definitions axiomatise give names - to the \<^term>\1\ elements of the base quantities. \ +lemma magQuant_mk [si_eq]: "\BUNIT('u::basedim_type)\\<^sub>Q = 1" + by (simp add: magQuant_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. \ definition [si_eq]: "meter = BUNIT(L)" definition [si_eq]: "second = BUNIT(T)" @@ -37,15 +39,31 @@ definition [si_eq]: "kelvin = BUNIT(\)" definition [si_eq]: "mole = BUNIT(N)" definition [si_eq]: "candela = BUNIT(J)" -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"}. +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 -type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer to the \<^emph>\norm\ of the vector, -not to its components. -\ +type \<^typ>\real\<^sup>3\. Note than when considering vectors, dimensions refer to the \<^emph>\norm\ of the vector, +not to its components. \ -lemma meter_is_BaseUnit: "is_BaseUnit meter" - by (simp add: si_eq, transfer, simp) +lemma BaseUnits: + "is_base_unit meter" "is_base_unit second" "is_base_unit kilogram" "is_base_unit ampere" + "is_base_unit kelvin" "is_base_unit mole" "is_base_unit candela" + by (simp add: si_eq, transfer, simp)+ + +text \ The effect of the above encoding is that we can use the SI base units as synonyms for their + corresponding dimensions at the type level. \ + +type_synonym meter = Length +type_synonym second = Time +type_synonym kilogram = Mass +type_synonym ampere = Current +type_synonym kelvin = Temperature +type_synonym mole = Amount +type_synonym candela = Intensity + +text \ We can therefore construct a quantity such as \<^term>\5 :: rat[meter]\, which unambiguously + identifies that the unit of $5$ is meters using the type system. This works because each base + unit it the one element. \ subsection \ Example Unit Equations \