Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

removed SI --- went to AFP

This commit is contained in:
Burkhart Wolff 2020-11-02 14:32:41 +01:00
parent 4e26aa6204
commit e59ac46299
20 changed files with 0 additions and 12993 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/DOF/Isa_DOF.thy
View File

@ -27,7 +27,6 @@ text\<open> Offering
text\<open> In this section, we develop on the basis of a management of references Isar-markups
that provide direct support in the PIDE framework. \<close>
theory Isa_DOF (* Isabelle Document Ontology Framework *)
imports Main

42
src/SI/Groups_mult.thy
View File

@ -1,42 +0,0 @@
chapter \<open> Multiplicative Groups \<close>
theory Groups_mult
imports Main
begin
notation times (infixl "\<cdot>" 70)
class group_mult = inverse + monoid_mult +
assumes left_inverse: "inverse a \<cdot> a = 1"
assumes multi_inverse_conv_div [simp]: "a \<cdot> (inverse b) = a / b"
begin
lemma div_conv_mult_inverse: "a / b = a \<cdot> (inverse b)"
by simp
sublocale mult: group times 1 inverse
by standard (simp_all add: left_inverse)
lemma diff_self [simp]: "a / a = 1"
using mult.right_inverse by auto
lemma mult_distrib_inverse [simp]: "(a * b) / b = a"
by (metis local.mult_1_right local.multi_inverse_conv_div mult.right_inverse mult_assoc)
end
class ab_group_mult = comm_monoid_mult + group_mult
begin
lemma mult_distrib_inverse' [simp]: "(a * b) / a = b"
using local.mult_distrib_inverse mult_commute by fastforce
lemma inverse_distrib: "inverse (a * b) = (inverse a) * (inverse b)"
by (simp add: local.mult.inverse_distrib_swap mult_commute)
end
abbreviation npower :: "'a::{power,inverse} \<Rightarrow> nat \<Rightarrow> 'a" ("(_\<^sup>-\<^sup>_)" [1000,999] 999)
where "npower x n \<equiv> inverse (x ^ n)"
end

5
src/SI/ISQ.thy
View File

@ -1,5 +0,0 @@
section \<open> Meta-Theory for ISQ \<close>
theory ISQ
imports ISQ_Dimensions ISQ_Quantities ISQ_Proof ISQ_Algebra
begin end

88
src/SI/ISQ_Algebra.thy
View File

@ -1,88 +0,0 @@
section \<open> Algebraic Laws \<close>
theory ISQ_Algebra
imports ISQ_Proof
begin
subsection \<open> Quantity Scale \<close>
lemma scaleQ_add_right: "a \<odot> x + y = (a \<odot> x) + (a \<odot> y)"
by (si_simp add: distrib_left)
lemma scaleQ_add_left: "a + b \<odot> x = (a \<odot> x) + (b \<odot> x)"
by (si_simp add: distrib_right)
lemma scaleQ_scaleQ: "a \<odot> b \<odot> x = a \<cdot> b \<odot> x"
by si_simp
lemma scaleQ_one [simp]: "1 \<odot> x = x"
by si_simp
lemma scaleQ_zero [simp]: "0 \<odot> x = 0"
by si_simp
lemma scaleQ_inv: "-a \<odot> x = a \<odot> -x"
by si_calc
lemma scaleQ_as_qprod: "a \<odot> x \<cong>\<^sub>Q (a \<odot> \<one>) \<^bold>\<cdot> x"
by (si_simp)
lemma mult_scaleQ_left [simp]: "(a \<odot> x) \<^bold>\<cdot> y = a \<odot> x \<^bold>\<cdot> y"
by (si_simp add: mult.assoc)
lemma mult_scaleQ_right [simp]: "x \<^bold>\<cdot> (a \<odot> y) = a \<odot> x \<^bold>\<cdot> y"
by si_simp
subsection \<open> Field Laws \<close>
lemma qtimes_commute: "x \<^bold>\<cdot> y \<cong>\<^sub>Q y \<^bold>\<cdot> x"
by si_calc
lemma qtimes_assoc: "(x \<^bold>\<cdot> y) \<^bold>\<cdot> z \<cong>\<^sub>Q x \<^bold>\<cdot> (y \<^bold>\<cdot> z)"
by (si_calc)
lemma qtimes_left_unit: "\<one> \<^bold>\<cdot> x \<cong>\<^sub>Q x"
by (si_calc)
lemma qtimes_right_unit: "x \<^bold>\<cdot> \<one> \<cong>\<^sub>Q x"
by (si_calc)
text\<open>The following weak congruences will allow for replacing equivalences in contexts
built from product and inverse. \<close>
lemma qtimes_weak_cong_left:
assumes "x \<cong>\<^sub>Q y"
shows "x\<^bold>\<cdot>z \<cong>\<^sub>Q y\<^bold>\<cdot>z"
using assms by si_simp
lemma qtimes_weak_cong_right:
assumes "x \<cong>\<^sub>Q y"
shows "z\<^bold>\<cdot>x \<cong>\<^sub>Q z\<^bold>\<cdot>y"
using assms by si_calc
lemma qinverse_weak_cong:
assumes "x \<cong>\<^sub>Q y"
shows "x\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y\<^sup>-\<^sup>\<one>"
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"
by si_calc
lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\<one> = 0 \<longleftrightarrow> x = 0"
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>"
by si_calc
lemma qinverse_qdivide: "(x \<^bold>/ y)\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y \<^bold>/ x"
by si_calc
lemma qtimes_cancel: "x \<noteq> 0 \<Longrightarrow> x \<^bold>/ x \<cong>\<^sub>Q \<one>"
by si_calc
end

354
src/SI/ISQ_Dimensions.thy
View File

@ -1,354 +0,0 @@
chapter \<open> International System of Quantities \<close>
section \<open> Quantity Dimensions \<close>
theory ISQ_Dimensions
imports Groups_mult
HOL.Transcendental
"HOL-Eisbach.Eisbach"
begin
subsection \<open> Preliminaries \<close>
named_theorems si_def and si_eq
instantiation unit :: comm_monoid_add
begin
definition "zero_unit = ()"
definition "plus_unit (x::unit) (y::unit) = ()"
instance proof qed (simp_all)
end
instantiation unit :: comm_monoid_mult
begin
definition "one_unit = ()"
definition "times_unit (x::unit) (y::unit) = ()"
instance proof qed (simp_all)
end
instantiation unit :: inverse
begin
definition "inverse_unit (x::unit) = ()"
definition "divide_unit (x::unit) (y::unit) = ()"
instance ..
end
instance unit :: ab_group_mult
by (intro_classes, simp_all)
subsection \<open> Dimensions Semantic Domain \<close>
text \<open> Quantity dimensions are used to distinguish quantities of different kinds. Only quantities
of the same kind can be compared and combined: it is a mistake to add a length to a mass, for
example. Dimensions are expressed in terms of seven base quantities, which can be combined to form
derived quantities. Consequently, a dimension associates with each of the seven base quantities an
integer that denotes the power to which it is raised. We use a record to represent this 7-tuple,
to enable code generation and thus efficient proof. \<close>
record Dimension =
Length :: int
Mass :: int
Time :: int
Current :: int
Temperature :: int
Amount :: int
Intensity :: int
text \<open> Next, we define dimension multiplication, and its unit, which corresponds to a dimensionless
quantity. These are then shown to form a commutative monoid. \<close>
instantiation Dimension_ext :: (one) one
begin
\<comment> \<open> Here, $1$ is the dimensionless unit \<close>
definition one_Dimension_ext :: "'a Dimension_ext"
where [code_unfold, si_def]: "1 = \<lparr> Length = 0, Mass = 0, Time = 0, Current = 0
, Temperature = 0, Amount = 0, Intensity = 0, \<dots> = 1 \<rparr>"
instance ..
end
instantiation Dimension_ext :: (times) times
begin
\<comment> \<open> Multiplication is defined by adding together the powers \<close>
definition times_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
where [code_unfold, si_def]:
"x * y = \<lparr> Length = Length x + Length y, Mass = Mass x + Mass y
, Time = Time x + Time y, Current = Current x + Current y
, Temperature = Temperature x + Temperature y, Amount = Amount x + Amount y
, Intensity = Intensity x + Intensity y, \<dots> = more x * more y \<rparr>"
instance ..
end
instance Dimension_ext :: (comm_monoid_mult) comm_monoid_mult
proof
fix a b c :: "'a Dimension_ext"
show "a * b * c = a * (b * c)"
by (simp add: times_Dimension_ext_def mult.assoc)
show "a * b = b * a"
by (simp add: times_Dimension_ext_def mult.commute)
show "1 * a = a"
by (simp add: times_Dimension_ext_def one_Dimension_ext_def)
qed
text \<open> We also define the inverse and division operations, and an abelian group, which will allow
us to perform dimensional analysis. \<close>
instantiation Dimension_ext :: ("{times,inverse}") inverse
begin
definition inverse_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
where [code_unfold, si_def]:
"inverse x = \<lparr> Length = - Length x, Mass = - Mass x
, Time = - Time x, Current = - Current x
, Temperature = - Temperature x, Amount = - Amount x
, Intensity = - Intensity x, \<dots> = inverse (more x) \<rparr>"
definition divide_Dimension_ext :: "'a Dimension_ext \<Rightarrow> 'a Dimension_ext \<Rightarrow> 'a Dimension_ext"
where [code_unfold, si_def]:
"divide_Dimension_ext x y = x * (inverse y)"
instance ..
end
instance Dimension_ext :: (ab_group_mult) ab_group_mult
proof
fix a b :: "'a Dimension_ext"
show "inverse a \<cdot> a = 1"
by (simp add: inverse_Dimension_ext_def times_Dimension_ext_def one_Dimension_ext_def)
show "a \<cdot> inverse b = a div b"
by (simp add: divide_Dimension_ext_def)
qed
text \<open> A base dimension is a dimension where precisely one component has power 1: it is the
dimension of a base quantity. Here we define the seven base dimensions. \<close>
definition LengthBD ("\<^bold>L") where [si_def]: "\<^bold>L = (1::Dimension)\<lparr>Length := 1\<rparr>"
definition MassBD ("\<^bold>M") where [si_def]: "\<^bold>M = (1::Dimension)\<lparr>Mass := 1\<rparr>"
definition TimeBD ("\<^bold>T") where [si_def]: "\<^bold>T = (1::Dimension)\<lparr>Time := 1\<rparr>"
definition CurrentBD ("\<^bold>I") where [si_def]: "\<^bold>I = (1::Dimension)\<lparr>Current := 1\<rparr>"
definition TemperatureBD ("\<^bold>\<Theta>") where [si_def]: "\<^bold>\<Theta> = (1::Dimension)\<lparr>Temperature := 1\<rparr>"
definition AmountBD ("\<^bold>N") where [si_def]: "\<^bold>N = (1::Dimension)\<lparr>Amount := 1\<rparr>"
definition IntensityBD ("\<^bold>J") where [si_def]: "\<^bold>J = (1::Dimension)\<lparr>Intensity := 1\<rparr>"
abbreviation "BaseDimensions \<equiv> {\<^bold>L, \<^bold>M, \<^bold>T, \<^bold>I, \<^bold>\<Theta>, \<^bold>N, \<^bold>J}"
text \<open> The following lemma confirms that there are indeed seven unique base dimensions. \<close>
lemma seven_BaseDimensions: "card BaseDimensions = 7"
by (simp add: si_def)
definition is_BaseDim :: "Dimension \<Rightarrow> bool" where [si_def]: "is_BaseDim x \<equiv> x \<in> BaseDimensions"
text \<open> We can use the base dimensions and algebra to form dimension expressions. Some examples
are shown below. \<close>
term "\<^bold>L\<cdot>\<^bold>M\<cdot>\<^bold>T\<^sup>-\<^sup>2"
term "\<^bold>M\<cdot>\<^bold>L\<^sup>-\<^sup>3"
subsection \<open> Dimensions Type Expressions \<close>
subsubsection \<open> Classification \<close>
text \<open> We provide a syntax for dimension type expressions, which allows representation of
dimensions as types in Isabelle. This will allow us to represent quantities that are parametrised
by a particular dimension type. We first must characterise the subclass of types that represent a
dimension.
The mechanism in Isabelle to characterize a certain subclass of Isabelle type expressions
are \<^emph>\<open>type classes\<close>. The following type class is used to link particular Isabelle types
to an instance of the type \<^typ>\<open>Dimension\<close>. It requires that any such type has the cardinality
\<^term>\<open>1\<close>, since a dimension type is used only to mark a quantity.
\<close>
class dim_type = finite +
fixes dim_ty_sem :: "'a itself \<Rightarrow> Dimension"
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
syntax
"_QD" :: "type \<Rightarrow> logic" ("QD'(_')")
translations
"QD('a)" == "CONST dim_ty_sem TYPE('a)"
text \<open> The notation \<^term>\<open>QD('a::dim_type)\<close> allows to obtain the dimension of a dimension type
\<^typ>\<open>'a\<close>.
The subset of basic dimension types can be characterized by the following type class: \<close>
class basedim_type = dim_type +
assumes is_BaseDim: "is_BaseDim QD('a)"
subsubsection \<open> Base Dimension Type Expressions \<close>
text \<open> The definition of the basic dimension type constructors is straightforward via a
one-elementary set, \<^typ>\<open>unit set\<close>. The latter is adequate since we need just an abstract syntax
for type expressions, so just one value for the \<^verbatim>\<open>dimension\<close>-type symbols. We define types for
each of the seven base dimensions, and also for dimensionless quantities. \<close>
typedef Length = "UNIV :: unit set" .. setup_lifting type_definition_Length
typedef Mass = "UNIV :: unit set" .. setup_lifting type_definition_Mass
typedef Time = "UNIV :: unit set" .. setup_lifting type_definition_Time
typedef Current = "UNIV :: unit set" .. setup_lifting type_definition_Current
typedef Temperature = "UNIV :: unit set" .. setup_lifting type_definition_Temperature
typedef Amount = "UNIV :: unit set" .. setup_lifting type_definition_Amount
typedef Intensity = "UNIV :: unit set" .. setup_lifting type_definition_Intensity
typedef NoDimension = "UNIV :: unit set" .. setup_lifting type_definition_NoDimension
type_synonym M = Mass
type_synonym L = Length
type_synonym T = Time
type_synonym I = Current
type_synonym \<Theta> = Temperature
type_synonym N = Amount
type_synonym J = Intensity
type_notation NoDimension ("\<one>")
translations
(type) "M" <= (type) "Mass"
(type) "L" <= (type) "Length"
(type) "T" <= (type) "Time"
(type) "I" <= (type) "Current"
(type) "\<Theta>" <= (type) "Temperature"
(type) "N" <= (type) "Amount"
(type) "J" <= (type) "Intensity"
text\<open> Next, we embed the base dimensions into the dimension type expressions by instantiating the
class \<^class>\<open>basedim_type\<close> with each of the base dimension types. \<close>
instantiation Length :: basedim_type
begin
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_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_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_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_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)+)
end
instantiation Amount :: basedim_type
begin
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_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_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
lemma base_dimension_types [simp]:
"is_BaseDim QD(Length)" "is_BaseDim QD(Mass)" "is_BaseDim QD(Time)" "is_BaseDim QD(Current)"
"is_BaseDim QD(Temperature)" "is_BaseDim QD(Amount)" "is_BaseDim QD(Intensity)"
by (simp_all add: is_BaseDim)
subsubsection \<open> Dimension Type Constructors: Inner Product and Inverse \<close>
text\<open> Dimension type expressions can be constructed by multiplication and division of the base
dimension types above. Consequently, we need to define multiplication and inverse operators
at the type level as well. On the class of dimension types (in which we have already inserted
the base dimension types), the definitions of the type constructors for inner product and inverse is
straightforward. \<close>
typedef ('a::dim_type, 'b::dim_type) DimTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
setup_lifting type_definition_DimTimes
text \<open> The type \<^typ>\<open>('a,'b) DimTimes\<close> is parameterised by two types, \<^typ>\<open>'a\<close> and \<^typ>\<open>'b\<close> that must
both be elements of the \<^class>\<open>dim_type\<close> class. As with the base dimensions, it is a unitary type
as its purpose is to represent dimension type expressions. We instantiate \<^class>\<open>dim_type\<close> with
this type, where the semantics of a product dimension expression is the product of the underlying
dimensions. This means that multiplication of two dimension types yields a dimension type. \<close>
instantiation DimTimes :: (dim_type, dim_type) dim_type
begin
definition dim_ty_sem_DimTimes :: "('a \<cdot> 'b) itself \<Rightarrow> Dimension" where
[si_eq]: "dim_ty_sem_DimTimes x = QD('a) * QD('b)"
instance by (intro_classes, simp_all add: dim_ty_sem_DimTimes_def, (transfer, simp)+)
end
text \<open> Similarly, we define inversion of dimension types and prove that dimension types are
closed under this. \<close>
typedef 'a DimInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" ..
setup_lifting type_definition_DimInv
instantiation DimInv :: (dim_type) dim_type
begin
definition dim_ty_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \<Rightarrow> Dimension" where
[si_eq]: "dim_ty_sem_DimInv x = inverse QD('a)"
instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
end
subsubsection \<open> Dimension Type Syntax \<close>
text \<open> A division is expressed, as usual, by multiplication with an inverted dimension. \<close>
type_synonym ('a, 'b) DimDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
text \<open> A number of further type synonyms allow for more compact notation: \<close>
type_synonym 'a DimSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
type_synonym 'a DimCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
type_synonym 'a DimQuart = "'a \<cdot> 'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>4" [999] 999)
type_synonym 'a DimInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999)
type_synonym 'a DimInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [999] 999)
type_synonym 'a DimInvQuart = "('a\<^sup>4)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>4" [999] 999)
translations (type) "'a\<^sup>-\<^sup>2" <= (type) "('a\<^sup>2)\<^sup>-\<^sup>1"
translations (type) "'a\<^sup>-\<^sup>3" <= (type) "('a\<^sup>3)\<^sup>-\<^sup>1"
translations (type) "'a\<^sup>-\<^sup>4" <= (type) "('a\<^sup>4)\<^sup>-\<^sup>1"
print_translation \<open>
[(@{type_syntax DimTimes},
fn ctx => fn [a, b] =>
if (a = b)
then Const (@{type_syntax DimSquare}, dummyT) $ a
else case a of
Const (@{type_syntax DimTimes}, _) $ a1 $ a2 =>
if (a1 = a2 andalso a2 = b)
then Const (@{type_syntax DimCube}, dummyT) $ a1
else case a1 of
Const (@{type_syntax DimTimes}, _) $ a11 $ a12 =>
if (a11 = a12 andalso a12 = a2 andalso a2 = b)
then Const (@{type_syntax DimQuart}, dummyT) $ a11
else raise Match |
_ => raise Match)]
\<close>
subsubsection \<open> Derived Dimension Types \<close>
type_synonym Area = "L\<^sup>2"
type_synonym Volume = "L\<^sup>3"
type_synonym Acceleration = "L\<cdot>T\<^sup>-\<^sup>1"
type_synonym Frequency = "T\<^sup>-\<^sup>1"
type_synonym Energy = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
type_synonym Power = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>3"
type_synonym Force = "L\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
type_synonym Pressure = "L\<^sup>-\<^sup>1\<cdot>M\<cdot>T\<^sup>-\<^sup>2"
type_synonym Charge = "I\<cdot>T"
type_synonym PotentialDifference = "L\<^sup>2\<cdot>M\<cdot>T\<^sup>-\<^sup>3\<cdot>I\<^sup>-\<^sup>1"
type_synonym Capacitance = "L\<^sup>-\<^sup>2\<cdot>M\<^sup>-\<^sup>1\<cdot>T\<^sup>4\<cdot>I\<^sup>2"
end

107
src/SI/ISQ_Proof.thy
View File

@ -1,107 +0,0 @@
section \<open> Proof Support for Quantities \<close>
theory ISQ_Proof
imports ISQ_Quantities
begin
named_theorems si_transfer
definition magQ :: "'a['u::dim_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
[si_def]: "magQ x = mag (fromQ x)"
definition dimQ :: "'a['u::dim_type] \<Rightarrow> Dimension" where
[si_def]: "dimQ x = dim (fromQ x)"
lemma quant_eq_iff_mag_eq [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_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]"
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 -
have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> mag (fromQ ta) \<noteq> mag (fromQ t)"
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 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"
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"
by (simp add: magQ_def, transfer, simp)
lemma magQ_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
by (simp add: magQ_def, transfer, simp)
lemma magQ_plus [si_eq]: "\<lbrakk>x + y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q + \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_minus [si_eq]: "\<lbrakk>x - y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q - \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_uminus [si_eq]: "\<lbrakk>- x\<rbrakk>\<^sub>Q = - \<lbrakk>x\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_scaleQ [si_eq]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_qtimes [si_eq]: "\<lbrakk>x \<^bold>\<cdot> y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q \<cdot> \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_qinverse [si_eq]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp)
lemma magQ_qdivivide [si_eq]: "\<lbrakk>(x::('a::field)[_]) \<^bold>/ y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q / \<lbrakk>y\<rbrakk>\<^sub>Q"
by (simp add: magQ_def, transfer, simp add: field_class.field_divide_inverse)
lemma magQ_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
apply (induct n, simp_all add: si_def)
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
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>
method si_simp uses add =
(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>
method si_calc uses add =
(si_simp add: add; simp add: si_def add)
lemma "QD(N \<cdot> \<Theta> \<cdot> N) = QD(\<Theta> \<cdot> N\<^sup>2)" by (simp add: si_eq si_def)
end

405
src/SI/ISQ_Quantities.thy
View File

@ -1,405 +0,0 @@
section \<open> Quantities \<close>
theory ISQ_Quantities
imports ISQ_Dimensions
begin
section \<open> Quantity Semantic Domain \<close>
text \<open> Here, we give a semantic domain for particular values of physical quantities. A quantity
is usually expressed as a number and a measurement unit, and the goal is to support this. First,
though, we give a more general semantic domain where a quantity has a magnitude and a dimension. \<close>
record 'a Quantity =
mag :: 'a \<comment> \<open> Magnitude of the quantity. \<close>
dim :: Dimension \<comment> \<open> Dimension of the quantity -- denote the kind of quantity. \<close>
text \<open> The quantity type is parametric as we permit the magnitude to be represented using any kind
of numeric type, such as \<^typ>\<open>int\<close>, \<^typ>\<open>rat\<close>, or \<^typ>\<open>real\<close>, though we usually minimally expect
a field. \<close>
lemma Quantity_eq_intro:
assumes "mag x = mag y" "dim x = dim y" "more x = more y"
shows "x = y"
by (simp add: assms)
text \<open> We can define several arithmetic operators on quantities. Multiplication takes multiplies
both the magnitudes and the dimensions. \<close>
instantiation Quantity_ext :: (times, times) times
begin
definition [si_def]:
"times_Quantity_ext x y = \<lparr> mag = mag x \<cdot> mag y, dim = dim x \<cdot> dim y, \<dots> = more x \<cdot> more y \<rparr>"
instance ..
end
lemma mag_times [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y" by (simp add: times_Quantity_ext_def)
lemma dim_times [simp]: "dim (x \<cdot> y) = dim x \<cdot> dim y" by (simp add: times_Quantity_ext_def)
lemma more_times [simp]: "more (x \<cdot> y) = more x \<cdot> more y" by (simp add: times_Quantity_ext_def)
text \<open> The zero and one quantities are both dimensionless quantities with magnitude of \<^term>\<open>0\<close> and
\<^term>\<open>1\<close>, respectively. \<close>
instantiation Quantity_ext :: (zero, zero) zero
begin
definition "zero_Quantity_ext = \<lparr> mag = 0, dim = 1, \<dots> = 0 \<rparr>"
instance ..
end
lemma mag_zero [simp]: "mag 0 = 0" by (simp add: zero_Quantity_ext_def)
lemma dim_zero [simp]: "dim 0 = 1" by (simp add: zero_Quantity_ext_def)
lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def)
instantiation Quantity_ext :: (one, one) one
begin
definition [si_def]: "one_Quantity_ext = \<lparr> mag = 1, dim = 1, \<dots> = 1 \<rparr>"
instance ..
end
lemma mag_one [simp]: "mag 1 = 1" by (simp add: one_Quantity_ext_def)
lemma dim_one [simp]: "dim 1 = 1" by (simp add: one_Quantity_ext_def)
lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def)
text \<open> Quantity inversion inverts both the magnitude and the dimension. Similarly, division of
one quantity by another, divides both the magnitudes and the dimensions. \<close>
instantiation Quantity_ext :: (inverse, inverse) inverse
begin
definition [si_def]:
"inverse_Quantity_ext x = \<lparr> mag = inverse (mag x), dim = inverse (dim x), \<dots> = inverse (more x) \<rparr>"
definition [si_def]:
"divide_Quantity_ext x y = \<lparr> mag = mag x / mag y, dim = dim x / dim y, \<dots> = more x / more y \<rparr>"
instance ..
end
lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)"
by (simp add: inverse_Quantity_ext_def)
lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)"
by (simp add: inverse_Quantity_ext_def)
lemma more_inverse [simp]: "more (inverse x) = inverse (more x)"
by (simp add: inverse_Quantity_ext_def)
lemma mag_divide [simp]: "mag (x / y) = mag x / mag y"
by (simp add: divide_Quantity_ext_def)
lemma dim_divide [simp]: "dim (x / y) = dim x / dim y"
by (simp add: divide_Quantity_ext_def)
lemma more_divide [simp]: "more (x / y) = more x / more y"
by (simp add: divide_Quantity_ext_def)
text \<open> As for dimensions, quantities form a commutative monoid and an abelian group. \<close>
instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
by (intro_classes, simp_all add: one_Quantity_ext_def
times_Quantity_ext_def mult.assoc, simp add: mult.commute)
instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
by (intro_classes, rule Quantity_eq_intro, simp_all)
text \<open> We can also define a partial order on quantities. \<close>
instantiation Quantity_ext :: (ord, ord) ord
begin
definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
where "less_eq_Quantity_ext x y = (mag x \<le> mag y \<and> dim x = dim y \<and> more x \<le> more y)"
definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
where "less_Quantity_ext x y = (x \<le> y \<and> \<not> y \<le> x)"
instance ..
end
instance Quantity_ext :: (order, order) order
by (intro_classes, auto simp add: less_Quantity_ext_def less_eq_Quantity_ext_def)
text \<open> We can define plus and minus as well, but these are partial operators as they are defined
only when the quantities have the same dimension. \<close>
instantiation Quantity_ext :: (plus, plus) plus
begin
definition [si_def]:
"dim x = dim y \<Longrightarrow>
plus_Quantity_ext x y = \<lparr> mag = mag x + mag y, dim = dim x, \<dots> = more x + more y \<rparr>"
instance ..
end
instantiation Quantity_ext :: (uminus, uminus) uminus
begin
definition [si_def]:
"uminus_Quantity_ext x = \<lparr> mag = - mag x , dim = dim x, \<dots> = - more x \<rparr>"
instance ..
end
instantiation Quantity_ext :: (minus, minus) minus
begin
definition [si_def]:
"dim x = dim y \<Longrightarrow>
minus_Quantity_ext x y = \<lparr> mag = mag x - mag y, dim = dim x, \<dots> = more x - more y \<rparr>"
instance ..
end
section \<open> Dimension Typed Quantities \<close>
text \<open> We can now define the type of quantities with parametrised dimension types. \<close>
typedef (overloaded) ('n, 'd::dim_type) QuantT ("_[_]" [999,0] 999)
= "{x :: 'n Quantity. dim x = QD('d)}"
morphisms fromQ toQ by (rule_tac x="\<lparr> mag = undefined, dim = QD('d) \<rparr>" in exI, simp)
setup_lifting type_definition_QuantT
text \<open> A dimension typed quantity is parameterised by two types: \<^typ>\<open>'a\<close>, the numeric type for the
magntitude, and \<^typ>\<open>'d\<close> for the dimension expression, which is an element of \<^class>\<open>dim_type\<close>.
The type \<^typ>\<open>('n, 'd) QuantT\<close> is to \<^typ>\<open>'n Quantity\<close> as dimension types are to \<^typ>\<open>Dimension\<close>.
Specifically, an element of \<^typ>\<open>('n', 'd) QuantT\<close> is a quantity whose dimension is \<^typ>\<open>'d\<close>.
Intuitively, the formula \<^term>\<open>x :: 'n['d]\<close> can be read as ``$x$ is a quantity of \<^typ>\<open>'d\<close>'',
for example it might be a quantity of length, or a quantity of mass. \<close>
text \<open> Since quantities can have dimension type expressions that are distinct, but denote the same
dimension, it is necessary to define the following function for coercion between two dimension
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
[si_def]: "QD('d\<^sub>1) = QD('d\<^sub>2) \<Longrightarrow> coerceQuantT t x = (toQ (fromQ x))"
syntax
"_QCOERCE" :: "type \<Rightarrow> logic \<Rightarrow> logic" ("QCOERCE[_]")
translations
"QCOERCE['t]" == "CONST coerceQuantT TYPE('t)"
subsection \<open> Predicates on Typed Quantities \<close>
text \<open> The standard HOL order \<^term>\<open>(\<le>)\<close> and equality \<^term>\<open>(=)\<close> have the homogeneous type
\<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> bool\<close> and so they cannot compare values of different types. Consequently,
we define a heterogeneous order and equivalence on typed quantities. \<close>
lift_definition qless_eq :: "'n::order['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50)
is "(\<le>)" .
lift_definition qequiv :: "'n['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50)
is "(=)" .
text \<open> These are both fundamentally the same as the usual order and equality relations, but they
permit potentially different dimension types, \<^typ>\<open>'a\<close> and \<^typ>\<open>'b\<close>. Two typed quantities are
comparable only when the two dimension types have the same semantic dimension.
\<close>
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
by (simp add: qequiv_def)
lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
by (simp add: qequiv_def)
lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
by (simp add: qequiv_def)
theorem qeq_iff_same_dim:
fixes x y :: "'a['d::dim_type]"
shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
by (transfer, simp)
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) \<cong>\<^sub>Q x"
by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)
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)"
shows "x \<cong>\<^sub>Q y"
using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
lemma updown_eq_iff:
fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]"
assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (toQ (fromQ x))"
shows "x \<cong>\<^sub>Q y"
by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceQuantT_def)
text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^sub>Q y\<close>, since x and y may have different type.\<close>
lemma qeq:
fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]"
assumes "x \<cong>\<^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\<open> Operators on Typed Quantities \<close>
text \<open> 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. \<close>
lift_definition
qtimes :: "('n::comm_ring_1)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69)
is "(*)" by (simp add: dim_ty_sem_DimTimes_def times_Quantity_ext_def)
lift_definition
qinverse :: "('n::field)['a::dim_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999)
is "inverse" by (simp add: inverse_Quantity_ext_def dim_ty_sem_DimInv_def)
abbreviation (input)
qdivide :: "('n::field)['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
"qdivide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
text \<open> We also provide some helpful notations for expressing heterogeneous powers. \<close>
abbreviation qsq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
abbreviation qcube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
abbreviation qquart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
text \<open> Analogous to the \<^const>\<open>scaleR\<close> 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. \<close>
lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['d::dim_type] \<Rightarrow> 'a['d]" (infixr "*\<^sub>Q" 63)
is "\<lambda> r x. \<lparr> mag = r * mag x, dim = QD('d) \<rparr>" by simp
notation scaleQ (infixr "\<odot>" 63)
text \<open> Finally, we instantiate the arithmetic types classes where possible. We do not instantiate
\<^class>\<open>times\<close> because this results in a nonsensical homogeneous product on quantities. \<close>
instantiation QuantT :: (zero,dim_type) zero
begin
lift_definition zero_QuantT :: "('a, 'b) QuantT" is "\<lparr> mag = 0, dim = QD('b) \<rparr>"
by simp
instance ..
end
instantiation QuantT :: (one,dim_type) one
begin
lift_definition one_QuantT :: "('a, 'b) QuantT" is "\<lparr> mag = 1, dim = QD('b) \<rparr>"
by simp
instance ..
end
text \<open> The following specialised one element has both magnitude and dimension 1: it is a
dimensionless quantity. \<close>
abbreviation qone :: "'n::one[\<one>]" ("\<one>") where "qone \<equiv> 1"
text \<open> 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. \<close>
instantiation QuantT :: (plus,dim_type) plus
begin
lift_definition plus_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
is "\<lambda> x y. \<lparr> mag = mag x + mag y, dim = QD('b) \<rparr>"
by (simp)
instance ..
end
text \<open> We can also show that typed quantities are commutative \<^emph>\<open>additive\<close> monoids. Indeed, addition
is a much easier operator to deal with in typed quantities, unlike product. \<close>
instance QuantT :: (semigroup_add,dim_type) semigroup_add
by (intro_classes, transfer, simp add: add.assoc)
instance QuantT :: (ab_semigroup_add,dim_type) ab_semigroup_add
by (intro_classes, transfer, simp add: add.commute)
instance QuantT :: (monoid_add,dim_type) monoid_add
by (intro_classes; (transfer, simp))
instance QuantT :: (comm_monoid_add,dim_type) comm_monoid_add
by (intro_classes; transfer, simp)
instantiation QuantT :: (uminus,dim_type) uminus
begin
lift_definition uminus_QuantT :: "'a['b] \<Rightarrow> 'a['b]"
is "\<lambda> x. \<lparr> mag = - mag x, dim = dim x \<rparr>" by (simp)
instance ..
end
instantiation QuantT :: (minus,dim_type) minus
begin
lift_definition minus_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
is "\<lambda> x y. \<lparr> mag = mag x - mag y, dim = dim x \<rparr>" by (simp)
instance ..
end
instance QuantT :: (numeral,dim_type) numeral ..
text \<open> Moreover, types quantities also form an additive group. \<close>
instance QuantT :: (ab_group_add,dim_type) ab_group_add
by (intro_classes, (transfer, simp)+)
text \<open> Typed quantities helpfully can be both partially and a linearly ordered. \<close>
instantiation QuantT :: (order,dim_type) order
begin
lift_definition less_eq_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x \<le> mag y" .
lift_definition less_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. mag x < mag y" .
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
end
instance QuantT :: (linorder,dim_type) linorder
by (intro_classes, transfer, auto)
instantiation QuantT :: (scaleR,dim_type) scaleR
begin
lift_definition scaleR_QuantT :: "real \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
is "\<lambda> n q. \<lparr> mag = n *\<^sub>R mag q, dim = dim q \<rparr>" by (simp)
instance ..
end
instance QuantT :: (real_vector,dim_type) real_vector
by (intro_classes, (transfer, simp add: scaleR_add_left scaleR_add_right)+)
instantiation QuantT :: (norm,dim_type) norm
begin
lift_definition norm_QuantT :: "'a['b] \<Rightarrow> real"
is "\<lambda> x. norm (mag x)" .
instance ..
end
instantiation QuantT :: (sgn_div_norm,dim_type) sgn_div_norm
begin
definition sgn_QuantT :: "'a['b] \<Rightarrow> 'a['b]" where
"sgn_QuantT x = x /\<^sub>R norm x"
instance by (intro_classes, simp add: sgn_QuantT_def)
end
instantiation QuantT :: (dist_norm,dim_type) dist_norm
begin
definition dist_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> real" where
"dist_QuantT x y = norm (x - y)"
instance
by (intro_classes, simp add: dist_QuantT_def)
end
instantiation QuantT :: ("{uniformity_dist,dist_norm}",dim_type) uniformity_dist
begin
definition uniformity_QuantT :: "('a['b] \<times> 'a['b]) filter" where
"uniformity_QuantT = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
instance
by (intro_classes, simp add: uniformity_QuantT_def)
end
instantiation QuantT :: ("{dist_norm,open_uniformity,uniformity_dist}",dim_type) open_uniformity
begin
definition open_QuantT :: "('a['b]) set \<Rightarrow> bool" where
"open_QuantT U = (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
instance by (intro_classes, simp add: open_QuantT_def)
end
text \<open> Quantities form a real normed vector space. \<close>
instance QuantT :: (real_normed_vector,dim_type) real_normed_vector
by (intro_classes; transfer, auto simp add: norm_triangle_ineq)
end

58
src/SI/ROOT
View File

@ -1,58 +0,0 @@
(*****************************************************************************
*
* Project : SI - Support for SI Units in Isabelle/HOL
* Version : 1.0
*
* Author : Simon Foster, Burkhart Wolff,
*
* This file : Configuration
*
* Copyright (c) 2020 University of York, GB, Université Paris-Saclay, France
*
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id:$ *)
session "SI" = Main +
description \<open> SI Unit Support \<close>
options [document = pdf, document_output = "document/output",
document_variants="document:outline=/proof,/ML"]
sessions
"HOL-Eisbach" "HOL-Decision_Procs"
theories
"ISQ"
"SI"
"SI_Astronomical"
document_files
"root.tex"
"adb-long.bib"
"root.bib"

5
src/SI/SI.thy
View File

@ -1,5 +0,0 @@
section \<open> Meta-Theory for SI Units \<close>
theory SI
imports SI_Units SI_Constants SI_Prefix SI_Derived SI_Accepted SI_Imperial
begin end

148
src/SI/SIOld.thy
View File

@ -1,148 +0,0 @@
theory SI
imports Main
begin
section\<open>SI's as Values.\<close>
record SI =
Second :: int
Meter :: int
Kilogram :: int
Ampere :: int
Kelvin :: int
Mole :: int
Candela :: int
definition ONE_SI::"SI" ("1\<^sub>S\<^sub>I")
where "1\<^sub>S\<^sub>I = (\<lparr> Second = 0::int, Meter = 0::int, Kilogram = 0::int,
Ampere = 0::int, Kelvin = 0::int, Mole = 0::int,
Candela = 0::int, \<dots> = () \<rparr>)"
text\<open>Example: Watt is \<open>kg\<cdot>m\<^sup>2\<cdot>s\<^sup>−\<^sup>3\<close>. Joule is \<open>kg\<cdot>m\<^sup>2\<cdot>s\<^sup>−\<^sup>2\<close>. \<close>
definition "Watt \<equiv> \<lparr> Second = -3, Meter = 2, Kilogram = 1,
Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \<rparr>"
definition "Joule\<equiv> \<lparr> Second = -2, Meter = 2, Kilogram = 1,
Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \<rparr>"
definition "Hertz\<equiv> 1\<^sub>S\<^sub>I\<lparr>Second := -1\<rparr>"
value " Watt = \<lparr> Second = -2, Meter = 1, Kilogram = 7,
Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0\<rparr>"
class unit\<^sub>C =
fixes id :: "'a \<Rightarrow> 'a" (* hack *)
assumes endo: "\<forall>x\<in>(UNIV::'a set). \<forall>y\<in>(UNIV::'a set). x = y"
instantiation unit :: unit\<^sub>C
begin
definition "id = (\<lambda>x::unit. x) "
instance proof(intro_classes)
show " \<forall>x\<in>(UNIV:: unit set). \<forall>y\<in>UNIV. x = y"
by auto
qed
end
instantiation SI_ext :: (unit\<^sub>C) one
begin
definition "(1::('a::unit\<^sub>C)SI_ext) =
\<lparr> Second = 0::int, Meter = 0::int, Kilogram = 0::int,
Ampere = 0::int, Kelvin = 0::int, Mole = 0::int,
Candela = 0::int,
\<dots> = undefined \<rparr>"
instance ..
end
lemma XXX [code_unfold] : "(1::SI) = 1\<^sub>S\<^sub>I "
by (simp add: one_SI_ext_def ONE_SI_def)
term "one ::('a::unit\<^sub>C)SI_ext "
term "1 ::('a::unit\<^sub>C)SI_ext "
term "(1::SI)\<lparr> more := () \<rparr> \<lparr>Second := -1\<rparr> "
value "1\<^sub>S\<^sub>I \<lparr>Second := -1\<rparr> "
instantiation SI_ext :: (unit\<^sub>C) times
begin
definition "(X::('a::unit\<^sub>C)SI_ext) * Y =
\<lparr> Second = Second X + Second Y,
Meter = Meter X + Meter Y,
Kilogram = Kilogram X + Kilogram Y,
Ampere = Ampere X + Ampere Y,
Kelvin = Kelvin X + Kelvin Y,
Mole = Mole X + Mole Y,
Candela = Candela X + Candela Y,
\<dots> = undefined \<rparr>"
instance ..
end
term "set"
lemma YYY [code_unfold] :
"(X::SI) * Y = \<lparr> Second = Second X + Second Y,
Meter = Meter X + Meter Y,
Kilogram = Kilogram X + Kilogram Y,
Ampere = Ampere X + Ampere Y,
Kelvin = Kelvin X + Kelvin Y,
Mole = Mole X + Mole Y,
Candela = Candela X + Candela Y,
\<dots> = () \<rparr> "
by (simp add: times_SI_ext_def)
instantiation SI_ext :: (unit\<^sub>C) comm_monoid_mult
begin
instance proof(intro_classes)
fix a b c show "(a:: ('a)SI_ext) * b * c = a * (b * c)"
unfolding times_SI_ext_def
by (auto simp: mult.assoc )
next
fix a b show "(a:: ('a)SI_ext) * b = b * a"
unfolding times_SI_ext_def
by (auto simp: mult.commute )
next
fix a::"('a::unit\<^sub>C)SI_ext" show "1 * a = a"
unfolding times_SI_ext_def one_SI_ext_def
apply (auto simp: mult.commute, rule sym)
apply(subst surjective)
by (metis UNIV_I endo)
qed
end
value "Hertz * 1\<^sub>S\<^sub>I "
value "Watt = Joule * Hertz"
section\<open>SI's as Types.\<close>
class si = one + ab_semigroup_mult +
fixes second :: "'a \<Rightarrow> int"
fixes meter :: "'a \<Rightarrow> int"
fixes kilogram :: "'a \<Rightarrow> int"
fixes ampere :: "'a \<Rightarrow> int"
fixes kelvin :: "'a \<Rightarrow> int"
fixes mole :: "'a \<Rightarrow> int"
fixes candela :: "'a \<Rightarrow> int"
definition si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e :: "'a::si \<Rightarrow> 'b::si \<Rightarrow> bool"
where "si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e X Y = (second X = second Y \<and> meter X = meter Y \<and>
kilogram X = kilogram Y \<and> ampere X = ampere Y \<and>
kelvin X = kelvin Y \<and> mole X = mole Y \<and> candela X = candela Y )"
text\<open>SI's as Value are perfectly compatible with this type interface.\<close>
instantiation SI_ext :: (unit\<^sub>C) si
begin
definition second where "second = Second"
definition meter where "meter = Meter"
definition kilogram where "kilogram = Kilogram"
definition ampere where "ampere = Ampere"
definition kelvin where "kelvin = Kelvin"
definition mole where "mole = Mole"
definition candela where "candela = Candela"
instance ..
end
end

36
src/SI/SI_Accepted.thy
View File

@ -1,36 +0,0 @@
section \<open> Non-SI Units Accepted for SI use \<close>
theory SI_Accepted
imports SI_Derived
begin
definition [si_def, si_eq]: "minute = 60 \<odot> second"
definition [si_def, si_eq]: "hour = 60 \<odot> minute"
definition [si_def, si_eq]: "day = 24 \<odot> hour"
definition [si_def, si_eq]: "astronomical_unit = 149597870700 \<odot> meter"
definition degree :: "'a::real_field[L/L]" where
[si_def, si_eq]: "degree = (2\<cdot>(of_real pi) / 180) \<odot> radian"
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odot> degree"
definition [si_def, si_eq]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
definition [si_def, si_eq]: "tonne = 10^3 \<odot> kilogram"
definition [si_def, si_eq]: "dalton = 1.66053906660 * (1 / 10^27) \<odot> kilogram"
subsection \<open> Example Unit Equations \<close>
lemma "1 \<odot> hour = 3600 \<odot> second"
by (si_simp)
lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule" by (si_calc)
lemma "25 \<odot> meter \<^bold>/ second = 90 \<odot> (kilo \<odot> meter) \<^bold>/ hour"
by (si_calc)
end

45
src/SI/SI_Astronomical.thy
View File

@ -1,45 +0,0 @@
section \<open> Astronomical Constants \<close>
theory SI_Astronomical
imports SI "HOL-Decision_Procs.Approximation"
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
[si_eq]: "julian_year = 365.25 \<odot> day"
definition light_year :: "'a::field_char_0[L]" where
"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

87
src/SI/SI_Constants.thy
View File

@ -1,87 +0,0 @@
section \<open> Physical Constants \<close>
theory SI_Constants
imports SI_Units
begin
subsection \<open> Core Derived Units \<close>
abbreviation (input) "hertz \<equiv> second\<^sup>-\<^sup>\<one>"
abbreviation "radian \<equiv> meter \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one>"
abbreviation "steradian \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two>"
abbreviation "joule \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
abbreviation "watt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three>"
abbreviation "coulomb \<equiv> ampere \<^bold>\<cdot> second"
abbreviation "lumen \<equiv> candela \<^bold>\<cdot> steradian"
subsection \<open> Constants \<close>
text \<open> The most general types we support must form a field into which the natural numbers can
be injected. \<close>
default_sort field_char_0
text \<open> Hyperfine transition frequency of frequency of Cs \<close>
abbreviation caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\<Delta>v\<^sub>C\<^sub>s") where
"caesium_frequency \<equiv> 9192631770 \<odot> hertz"
text \<open> Speed of light in vacuum \<close>
abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" ("\<^bold>c") where
"speed_of_light \<equiv> 299792458 \<odot> (meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
text \<open> Planck constant \<close>
abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" ("\<^bold>h") where
"Planck \<equiv> (6.62607015 \<cdot> 1/(10^34)) \<odot> (joule\<^bold>\<cdot>second)"
text \<open> Elementary charge \<close>
abbreviation elementary_charge :: "'a[I \<cdot> T]" ("\<^bold>e") where
"elementary_charge \<equiv> (1.602176634 \<cdot> 1/(10^19)) \<odot> coulomb"
text \<open> The Boltzmann constant \<close>
abbreviation Boltzmann :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> \<Theta>\<^sup>-\<^sup>1]" ("\<^bold>k") where
"Boltzmann \<equiv> (1.380649\<cdot>1/(10^23)) \<odot> (joule \<^bold>/ kelvin)"
text \<open> The Avogadro number \<close>
abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" ("N\<^sub>A") where
"Avogadro \<equiv> 6.02214076\<cdot>(10^23) \<odot> (mole\<^sup>-\<^sup>\<one>)"
abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where
"max_luminous_frequency \<equiv> (540\<cdot>10^12) \<odot> hertz"
text \<open> The luminous efficacy of monochromatic radiation of frequency \<^const>\<open>max_luminous_frequency\<close>. \<close>
abbreviation luminous_efficacy :: "'a[J \<cdot> (L\<^sup>2 \<cdot> L\<^sup>-\<^sup>2) \<cdot> (M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" ("K\<^sub>c\<^sub>d") where
"luminous_efficacy \<equiv> 683 \<odot> (lumen\<^bold>/watt)"
subsection \<open> Basis Theorems \<close>
theorem second_definition:
"1 \<odot> second \<cong>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
by si_calc
theorem meter_definition:
"1 \<odot> meter \<cong>\<^sub>Q (\<^bold>c \<^bold>/ (299792458 \<odot> \<one>))\<^bold>\<cdot>second"
"1 \<odot> meter \<cong>\<^sub>Q (9192631770 / 299792458) \<odot> (\<^bold>c \<^bold>/ \<Delta>v\<^sub>C\<^sub>s)"
by si_calc+
theorem kilogram_definition:
"1 \<odot> kilogram \<cong>\<^sub>Q (\<^bold>h \<^bold>/ (6.62607015 \<cdot> 1/(10^34) \<odot> \<one>))\<^bold>\<cdot>meter\<^sup>-\<^sup>\<two>\<^bold>\<cdot>second"
by si_calc
abbreviation "approx_ice_point \<equiv> 273.15 \<odot> kelvin"
default_sort type
end

88
src/SI/SI_Derived.thy
View File

@ -1,88 +0,0 @@
section \<open> Derived SI-Units\<close>
theory SI_Derived
imports SI_Prefix
begin
subsection \<open> Definitions \<close>
abbreviation "newton \<equiv> kilogram \<^bold>\<cdot> meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
abbreviation "pascal \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
abbreviation "volt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
abbreviation "farad \<equiv> kilogram\<^sup>-\<^sup>\<one> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two> \<^bold>\<cdot> second\<^sup>\<four> \<^bold>\<cdot> ampere\<^sup>\<two>"
abbreviation "ohm \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<two>"
abbreviation "siemens \<equiv> kilogram\<^sup>-\<^sup>\<one> \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two> \<^bold>\<cdot> second\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>\<two>"
abbreviation "weber \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
abbreviation "tesla \<equiv> kilogram \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
abbreviation "henry \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<two>"
abbreviation "lux \<equiv> candela \<^bold>\<cdot> steradian \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two>"
abbreviation (input) "becquerel \<equiv> second\<^sup>-\<^sup>\<one>"
abbreviation "gray \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
abbreviation "sievert \<equiv> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
abbreviation "katal \<equiv> mole \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>"
definition degrees_celcius :: "'a::field_char_0 \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
where [si_eq]: "degrees_celcius x = (x \<odot> kelvin) + approx_ice_point"
definition [si_eq]: "gram = milli \<odot> kilogram"
subsection \<open> Equivalences \<close>
lemma joule_alt_def: "joule \<cong>\<^sub>Q newton \<^bold>\<cdot> meter"
by si_calc
lemma watt_alt_def: "watt \<cong>\<^sub>Q joule \<^bold>/ second"
by si_calc
lemma volt_alt_def: "volt = watt \<^bold>/ ampere"
by simp
lemma farad_alt_def: "farad \<cong>\<^sub>Q coulomb \<^bold>/ volt"
by si_calc
lemma ohm_alt_def: "ohm \<cong>\<^sub>Q volt \<^bold>/ ampere"
by si_calc
lemma siemens_alt_def: "siemens \<cong>\<^sub>Q ampere \<^bold>/ volt"
by si_calc
lemma weber_alt_def: "weber \<cong>\<^sub>Q volt \<^bold>\<cdot> second"
by si_calc
lemma tesla_alt_def: "tesla \<cong>\<^sub>Q weber \<^bold>/ meter\<^sup>\<two>"
by si_calc
lemma henry_alt_def: "henry \<cong>\<^sub>Q weber \<^bold>/ ampere"
by si_calc
lemma lux_alt_def: "lux = lumen \<^bold>/ meter\<^sup>\<two>"
by simp
lemma gray_alt_def: "gray \<cong>\<^sub>Q joule \<^bold>/ kilogram"
by si_calc
lemma sievert_alt_def: "sievert \<cong>\<^sub>Q joule \<^bold>/ kilogram"
by si_calc
subsection \<open> Properties \<close>
lemma kilogram: "kilo \<odot> gram = kilogram"
by (si_simp)
lemma celcius_to_kelvin: "T\<degree>C = (T \<odot> kelvin) + (273.15 \<odot> kelvin)"
by (si_simp)
end

63
src/SI/SI_Imperial.thy
View File

@ -1,63 +0,0 @@
section \<open> Imperial Units via SI-Units\<close>
theory SI_Imperial
imports SI_Accepted
begin
subsection \<open> Definitions \<close>
default_sort field_char_0
definition inch :: "'a[L]" where
[si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
definition foot :: "'a[L]" where
[si_eq]: "foot = 0.3048 \<odot> meter"
definition yard :: "'a[L]" where
[si_eq]: "yard = 0.9144 \<odot> meter"
definition mile :: "'a[L]" where
[si_eq]: "mile = 1609.344 \<odot> meter"
definition nautical_mile :: "'a[L]" where
[si_eq]: "nautical_mile = 1852 \<odot> meter"
definition knot :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" where
[si_eq]: "knot = 1 \<odot> (nautical_mile \<^bold>/ hour)"
definition pint :: "'a[Volume]" where
[si_eq]: "pint = 0.56826125 \<odot> litre"
definition gallon :: "'a[Volume]" where
[si_eq]: "gallon = 8 \<odot> pint"
definition pound :: "'a[M]" where
[si_eq]: "pound = 0.45359237 \<odot> kilogram"
definition ounce :: "'a[M]" where
[si_eq]: "ounce = 1/16 \<odot> pound"
definition stone :: "'a[M]" where
[si_eq]: "stone = 14 \<odot> pound"
definition degrees_farenheit :: "'a \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_eq]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
default_sort type
subsection \<open> Unit Equations \<close>
lemma miles_to_yards: "mile = 1760 \<odot> yard"
by si_simp
lemma miles_to_feet: "mile = 5280 \<odot> foot"
by si_simp
lemma mph_to_kmh: "1 \<odot> (mile \<^bold>/ hour) = 1.609344 \<odot> ((kilo \<odot> meter) \<^bold>/ hour)"
by si_simp
lemma farenheit_to_celcius: "T\<degree>F = ((T - 32) \<cdot> 5/9)\<degree>C"
by si_simp
end

89
src/SI/SI_Prefix.thy
View File

@ -1,89 +0,0 @@
section \<open> SI Prefixes \<close>
theory SI_Prefix
imports SI_Constants
begin
subsection \<open> Definitions \<close>
text \<open> Prefixes are simply numbers that can be composed with units using the scalar
multiplication operator \<^const>\<open>scaleQ\<close>. \<close>
default_sort ring_char_0
definition deca :: "'a" where [si_eq]: "deca = 10^1"
definition hecto :: "'a" where [si_eq]: "hecto = 10^2"
definition kilo :: "'a" where [si_eq]: "kilo = 10^3"
definition mega :: "'a" where [si_eq]: "mega = 10^6"
definition giga :: "'a" where [si_eq]: "giga = 10^9"
definition tera :: "'a" where [si_eq]: "tera = 10^12"
definition peta :: "'a" where [si_eq]: "peta = 10^15"
definition exa :: "'a" where [si_eq]: "exa = 10^18"
definition zetta :: "'a" where [si_eq]: "zetta = 10^21"
definition yotta :: "'a" where [si_eq]: "yotta = 10^24"
default_sort field_char_0
definition deci :: "'a" where [si_eq]: "deci = 1/10^1"
definition centi :: "'a" where [si_eq]: "centi = 1/10^2"
definition milli :: "'a" where [si_eq]: "milli = 1/10^3"
definition micro :: "'a" where [si_eq]: "micro = 1/10^6"
definition nano :: "'a" where [si_eq]: "nano = 1/10^9"
definition pico :: "'a" where [si_eq]: "pico = 1/10^12"
definition femto :: "'a" where [si_eq]: "femto = 1/10^15"
definition atto :: "'a" where [si_eq]: "atto = 1/10^18"
definition zepto :: "'a" where [si_eq]: "zepto = 1/10^21"
definition yocto :: "'a" where [si_eq]: "yocto = 1/10^24"
subsection \<open> Examples \<close>
lemma "2.3 \<odot> (centi \<odot> meter)\<^sup>\<three> = 2.3 \<cdot> 1/10^6 \<odot> meter\<^sup>\<three>"
by (si_simp)
lemma "1 \<odot> (centi \<odot> meter)\<^sup>-\<^sup>\<one> = 100 \<odot> meter\<^sup>-\<^sup>\<one>"
by (si_simp)
subsection \<open> Binary Prefixes \<close>
text \<open> Although not in general applicable to physical quantities, we include these prefixes
for completeness. \<close>
default_sort ring_char_0
definition kibi :: "'a" where [si_eq]: "kibi = 2^10"
definition mebi :: "'a" where [si_eq]: "mebi = 2^20"
definition gibi :: "'a" where [si_eq]: "gibi = 2^30"
definition tebi :: "'a" where [si_eq]: "tebi = 2^40"
definition pebi :: "'a" where [si_eq]: "pebi = 2^50"
definition exbi :: "'a" where [si_eq]: "exbi = 2^60"
definition zebi :: "'a" where [si_eq]: "zebi = 2^70"
definition yobi :: "'a" where [si_eq]: "yobi = 2^80"
default_sort type
end

75
src/SI/SI_Units.thy
View File

@ -1,75 +0,0 @@
chapter \<open> International System of Units \<close>
section \<open> SI Units Semantics \<close>
theory SI_Units
imports ISQ
begin
text \<open> An SI unit is simply a particular kind of quantity. \<close>
type_synonym ('n, 'd) UnitT = "('n, 'd) QuantT"
text \<open> Parallel to the seven base quantities, there are seven base units. In the implementation of
the SI unit system, we fix these to be precisely those quantities that have a base dimension
and a magnitude of \<^term>\<open>1\<close>. Consequently, a base unit corresponds to a unit in the algebraic
sense. \<close>
lift_definition is_base_unit :: "'a::one['d::dim_type] \<Rightarrow> bool"
is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::basedim_type]"
where [si_eq]: "mk_base_unit t = 1"
syntax "_mk_base_unit" :: "type \<Rightarrow> logic" ("BUNIT'(_')")
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 magQ_mk [si_eq]: "\<lbrakk>BUNIT('u::basedim_type)\<rbrakk>\<^sub>Q = 1"
by (simp add: magQ_def si_eq, transfer, simp)
text \<open> We now define the seven base units. Effectively, these definitions axiomatise given names
for the \<^term>\<open>1\<close> elements of the base quantities. \<close>
definition [si_eq]: "meter = BUNIT(L)"
definition [si_eq]: "second = BUNIT(T)"
definition [si_eq]: "kilogram = BUNIT(M)"
definition [si_eq]: "ampere = BUNIT(I)"
definition [si_eq]: "kelvin = BUNIT(\<Theta>)"
definition [si_eq]: "mole = BUNIT(N)"
definition [si_eq]: "candela = BUNIT(J)"
text\<open>Note that as a consequence of our construction, the term \<^term>\<open>meter\<close> is a SI Unit constant of
SI-type \<^typ>\<open>'a[L]\<close>, so a unit of dimension \<^typ>\<open>Length\<close> with the magnitude of type \<^typ>\<open>'a\<close>.
A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of
type \<^typ>\<open>real\<^sup>3\<close>. Note than when considering vectors, dimensions refer to the \<^emph>\<open>norm\<close> of the vector,
not to its components. \<close>
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 \<open> 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. \<close>
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 \<open> We can therefore construct a quantity such as \<^term>\<open>5 :: rat[meter]\<close>, which unambiguously
identifies that the unit of $5$ is meters using the type system. This works because each base
unit it the one element. \<close>
subsection \<open> Example Unit Equations \<close>
lemma "(meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q meter"
by (si_calc)
end

80
src/SI/document/adb-long.bib
View File

@ -1,80 +0,0 @@
% $Id: adb-long.bib 6518 2010-01-24 14:18:10Z brucker $
@PREAMBLE{ {\providecommand{\ac}[1]{\textsc{#1}} }
# {\providecommand{\acs}[1]{\textsc{#1}} }
# {\providecommand{\acf}[1]{\textsc{#1}} }
# {\providecommand{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} }
# {\providecommand{\leanTAP}{\mbox{\sf lean\it\TAP}} }
# {\providecommand{\holz}{\textsc{hol-z}} }
# {\providecommand{\holocl}{\textsc{hol-ocl}} }
# {\providecommand{\isbn}{\textsc{isbn}} }
# {\providecommand{\Cpp}{C++} }
# {\providecommand{\Specsharp}{Spec\#} }
# {\providecommand{\doi}[1]{\href{http://dx.doi.org/#1}{doi:
{\urlstyle{rm}\nolinkurl{#1}}}}} }
@STRING{conf-tphols="\acs{tphols}" }
@STRING{iso = {International Organization for Standardization} }
@STRING{j-ar = "Journal of Automated Reasoning" }
@STRING{j-cacm = "Communications of the \acs{acm}" }
@STRING{j-acta-informatica = "Acta Informatica" }
@STRING{j-sosym = "Software and Systems Modeling" }
@STRING{j-sttt = "International Journal on Software Tools for Technology" }
@STRING{j-ist = "Information and Software Technology" }
@STRING{j-toplas= "\acs{acm} Transactions on Programming Languages and
Systems" }
@STRING{j-tosem = "\acs{acm} Transactions on Software Engineering and
Methodology" }
@STRING{j-eceasst="Electronic Communications of the \acs{easst}" }
@STRING{j-fac = "Formal Aspects of Computing" }
@STRING{j-ucs = "Journal of Universal Computer Science" }
@STRING{j-sl = "Journal of Symbolic Logic" }
@STRING{j-fp = "Journal of Functional Programming" }
@STRING{j-tkde = {\acs{ieee} Transaction on Knowledge and Data Engineering} }
@STRING{j-tse = {\acs{ieee} Transaction on Software Engineering} }
@STRING{j-entcs = {Electronic Notes in Theoretical Computer Science} }
@STRING{s-lnai = "Lecture Notes in Computer Science" }
@STRING{s-lncs = "Lecture Notes in Computer Science" }
@STRING{s-lnbip = "Lecture Notes in Business Information Processing" }
@String{j-computer = "Computer"}
@String{j-tissec = "\acs{acm} Transactions on Information and System Security"}
@STRING{omg = {Object Management Group} }
@STRING{j-ipl = {Information Processing Letters} }
@STRING{j-login = ";login: the USENIX Association newsletter" }
@STRING{PROC = "Proceedings of the " }
% Publisher:
% ==========
@STRING{pub-awl = {Addison-Wesley Longman, Inc.} }
@STRING{pub-awl:adr={Reading, MA, \acs{usa}} }
@STRING{pub-springer={Springer-Verlag} }
@STRING{pub-springer:adr={Heidelberg} }
@STRING{pub-cup = {Cambridge University Press} }
@STRING{pub-cup:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-mit = {\acs{mit} Press} }
@STRING{pub-mit:adr={Cambridge, Massachusetts} }
@STRING{pub-springer-ny={Springer-Verlag} }
,
@STRING{pub-springer-netherlands={Springer Netherlands} }
@STRING{pub-springer-netherlands:adr={} }
@STRING{pub-springer-ny:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-springer-london={Springer-Verlag} }
@STRING{pub-springer-london:adr={London} }
@STRING{pub-ieee= {\acs{ieee} Computer Society} }
@STRING{pub-ieee:adr={Los Alamitos, \acs{ca}, \acs{usa}} }
@STRING{pub-prentice={Prentice Hall, Inc.} }
@STRING{pub-prentice:adr={Upper Saddle River, \acs{nj}, \acs{usa}} }
@STRING{pub-acm = {\acs{acm} Press} }
@STRING{pub-acm:adr={New York, \acs{ny} \acs{usa}} }
@STRING{pub-oxford={Oxford University Press, Inc.} }
@STRING{pub-oxford:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-kluwer={Kluwer Academic Publishers} }
@STRING{pub-kluwer:adr={Dordrecht} }
@STRING{pub-elsevier={Elsevier Science Publishers} }
@STRING{pub-elsevier:adr={Amsterdam} }
@STRING{pub-north={North-Holland Publishing Co.} }
@STRING{pub-north:adr={Nijmegen, The Netherlands} }
@STRING{pub-ios = {\textsc{ios} Press} }
@STRING{pub-ios:adr={Amsterdam, The Netherlands} }
@STRING{pub-heise={Heise Zeitschriften Verlag} }
@STRING{pub-heise:adr={Hannover, Germany} }

11041
src/SI/document/root.bib
View File

File diff suppressed because it is too large Load Diff

176
src/SI/document/root.tex
View File

@ -1,176 +0,0 @@
\documentclass[11pt,a4paper]{book}
\usepackage{isabelle,isabellesym}
\usepackage{graphicx}
\graphicspath {{figures/}}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{latexsym}
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel}
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
%\usepackage[latin1]{inputenc}
%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
%\<threesuperior>, \<threequarters>, \<degree>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<cent>, \<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\newcommand{\HOL}[1]{\verb{HOL}}
\newcommand{\eg}[1]{e.g.}
\renewcommand{\isasymdegree}{XXX}
\begin{document}
\title{International Systems of Quantities and Units in Isabelle/HOL}
\author{Simon Foster \and Burkhart Wolff}
\maketitle
\textbf{ Abstract }
The International System of Units
(SI, abbreviated from the French Syst\`eme international (d’unit\'es)) is the modern form of
the metric system and is the most widely used system of measurement. It comprises a coherent
system of units of measurement built on seven base units, which are the second, metre, kilogram,
ampere, kelvin, mole, candela, and a set of twenty prefixes to the unit names and unit symbols
that may be used when specifying multiples and fractions of the units. The system also specifies
names for 22 derived units, such as lumen and watt, for other common physical quantities.
This theory represents a formal model of SI Units together with a deep integration in Isabelle's
type system: unitswere represented in a way that they have a \emph{unit type} comprising its
\emph{magnitude type} and its physical \emph{dimension}. Congruences on dimensions were supported.
Our construction is validated by a test-set of known equivalences between SI Units.
Moreover, the presented theory can be used for type-safe conversions between the SI system and
others, like the British Imperial System (BIS).
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
\chapter{SI Units in Isabelle \\ An Introduction}
The International System of Units (SI, abbreviated from the French
Système international (d'unités)) is the modern form of the metric
system and is the most widely used system of measurement. It comprises
a coherent system of units of measurement built on seven base units,
which are the second, metre, kilogram, ampere, kelvin, mole, candela,
and a set of twenty prefixes to the unit names and unit symbols that
may be used when specifying multiples and fractions of the units.
The system also specifies names for 22 derived units, such as lumen and
watt, for other common physical quantities.
(cited from \url{https://en.wikipedia.org/wiki/International_System_of_Units}).
In more detail, the SI provides the following fundamental concepts:
%
\begin{enumerate}%
\item \emph{quantities}, i.e. \emph{time}, \emph{length}, \emph{mass}, \emph{electric current},
\emph{temperature}, \emph{amount of substance},\emph{luminous intensity},
and other derived quantities such as \emph{volume};
\item \emph{dimensions}, i.e. a set of the symbols \isa{T}, \isa{L}, \isa{M}, \isa{I}, \isa{{\isasymTheta}}, \isa{N}, \isa{J} corresponding
to the above mentioned base quantities, indexed by an integer exponent
(dimensions were also called \emph{base unit names} or just \emph{base units});
\item \emph{magnitudes}, i.e. a factor or \emph{prefix}
(typically integers, reals, vectors on real or complex numbers);
\item \emph{units}, which are basically pairs of magnitudes and dimensions denoting quantities.
\end{enumerate}
Note that \emph{quantities} are understood as idealized \emph{physical concepts}, and are sharply
distinguished from \emph{units} representing \emph{a means to measure} them. The difference is
roughly similar between words (or: symbols) and notions. This distinction reflects the fact that
these concepts have been at times heavily questioned in the history of physics; the interested
reader is referred to the debate around the "relativistic mass" at in the twenties of the last century.
The purpose of the presented theory is to model SI units with polymorphic magnitudes inside the
Isabelle/HOL\cite{nipkow.ea:isabelle:2002} system. The objective of our construction is to
reflect the types of the magnitudes as well as their dimensions in order to allow type-safe
calculations on SI units.
As a result, it is possible to express "4500.0 kilogram times meter per second square" which can
have the type
\isa{{\isasymreal}\ {\isacharbrackleft}M\ \isactrlsup {\isachardot}\ L\ \isactrlsup
{\isachardot}\ T\isactrlsup {\isacharminus}\isactrlsup {\isadigit{3}}
\isactrlsup {\isachardot}\ T\isactrlsup {\isadigit{1}}{\isacharbrackright}}.
For units of this type we can infer that this corresponds to the derived unit "4.5 kN" (kilo-Newton)
of type \isa{{\isasymreal}\ {\isacharbrackleft}M\ \isactrlsup {\isachardot}\ L\ \isactrlsup
{\isachardot}\ T\isactrlsup {\isacharminus}\isactrlsup {\isadigit{2}}{\isacharbrackright}}.
This is an attempt to model the standard SI system and its derived entities (cf.
\url{https://www.quora.com/What-are-examples-of-SI-units}),
both from a type-checking as well as a proof-support perspective.
These design objectives are for the case of Isabelle system somewhat contradictory.
Since the Isabelle type system follows the Curry-style paradigm, which can be
characterized by: "be as implicit as possible, inference as automatic as possible", it is not
possible to do computations on type-terms (in contrast to, for example, Coq). We therefore
need a more involved construction using Isabelle's type-classes to establish a semantic
interpretation on certain classes of types. This paves the way to derive rules that
establish and exploit type isomorphisms implicitely. For example, the implicit
type isomorhisms for the dimensions $T^{-2} * T$ and $T^{-1}$ is dealt with appropriate
rules on terms and a special form of equivalence.
Our construction proceeds in three phases:
\begin{enumerate}%
\item We construct a type \isa{Dimension} which is basically a "semantic representation" or
"semantic domain" of all SI dimensions. Since SI-types have an interpretation in this domain,
it serves to give semantics to type-constructors by operations on this domain, too.
We construct a multiplicative group on it.
\item From \isa{Dimension} we build a language of type-constructors of \isa{dimS}-types,
captured in a type class \isa{dim-types} giving it a pseudo-inductive structure. Types of
this class are required to have an interpretation function into \isa{Dimension}'s, which
allows for establishing equivalences on \isa{dim-types}.
\item We construct a SI Unit-type as a pair of a polymorphic magnitude and a dimension type.
This type will be inhabited by all basic SI units and predicates expressing their relationship.
\end{enumerate}%
On this basis, an algebra of SI units can be derived; while types can not be "touched" inside
an Isabelle/HOL logic, it is possible to transform unit types by applying rules of this algebra.
Tactical support over this algebra is provided enabling the construction of normal forms on
both units and their type.
\subsubsection{Previous Attempts.} The work of \cite{HayesBrendan95} represents to our knowledge a
first attempt to formalize SI units in Z, thus a similar language of HOL. While our typing
representation is more rigourous due to the use of type-classes, this works lacks any attempt
to support formal and automated deduction on Si unit equivalences.
MORE TO COME.
\input{session}
% optional bibliography
\bibliographystyle{abbrv}
\bibliography{adb-long,root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: