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

improved intro, improved global structure (TOC), normalized terminology.

This commit is contained in:
Burkhart Wolff 2020-02-24 18:36:07 +01:00
parent 17c64ea60b
commit 493a6c5559
8 changed files with 78 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/SI/SI.thy
View File

@ -2,24 +2,6 @@ theory SI
imports Main
begin
text\<open>
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>\<open>https://en.wikipedia.org/wiki/International_System_of_Units\<close>).\<close>
text\<open> This is an attempt to model the system and its derived entities (cf.
\<^url>\<open>https://www.quora.com/What-are-examples-of-SI-units\<close>) in Isabelle/HOL.
The design objective are twofold (and for the case of Isabelle somewhat
contradictory, see below)
\<close>
section\<open>SI's as Values.\<close>

2
src/SI/SI_Derived.thy
View File

@ -1,4 +1,4 @@
section \<open> Derived Units\<close>
section \<open> Derived SI-Units\<close>
theory SI_Derived
imports SI_Prefix

10
src/SI/SI_Dimensions.thy
View File

@ -1,4 +1,4 @@
section \<open> SI Units \<close>
section \<open> SI Dimensions \<close>
theory SI_Dimensions
imports Groups_mult
@ -10,7 +10,7 @@ named_theorems si_def and si_eq
section\<open>The Semantic Domain of Dimensions\<close>
subsection \<open> The DimS-type and its operations \<close>
subsection \<open> The Dimension-type and its operations \<close>
text \<open> An SI unit associates with each of the seven base unit an integer that denotes the power
to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \<close>
@ -120,7 +120,7 @@ definition is_BaseDim :: "Dimension \<Rightarrow> bool" where
section\<open>The Syntax and Semantics of Dimension Types\<close>
subsection \<open> Dimensions as Types (Basic SI-types)\<close>
subsection \<open> Basic Dimensions as Types (Basic SI-types)\<close>
text \<open> We provide a syntax for type-expressions; The definition of
the basic type constructors is straight-forward via a one-elementary set.
@ -155,7 +155,7 @@ translations
(type) "N" <= (type) "Amount"
(type) "J" <= (type) "Intensity"
subsection \<open> SI-type expressions and SI-type interpretation \<close>
subsection \<open>Dimension Type Expressions and their Interpretation \<close>
text \<open> The case for the construction of the multiplicative and inverse operators requires ---
thus, the unary and binary operators on our SI type language --- require that their arguments
@ -277,7 +277,7 @@ begin
end
subsubsection \<open> Syntactic Support for SI type expressions. \<close>
subsection \<open> Syntactic Support for dim-type expressions. \<close>
text\<open>A number of type-synonyms allow for more compact notation: \<close>
type_synonym ('a, 'b) DimDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)

2
src/SI/SI_Imperial.thy
View File

@ -1,4 +1,4 @@
section \<open> Imperial Units via SI \<close>
section \<open> Imperial Units via SI-Units\<close>
theory SI_Imperial
imports SI_Accepted

2
src/SI/SI_Proof.thy
View File

@ -1,4 +1,4 @@
section \<open> Tactic Support for SI type expressions. \<close>
section \<open>Basic Proof Support for SI Units \<close>
theory SI_Proof
imports SI_Units

12
src/SI/SI_Units.thy
View File

@ -4,7 +4,7 @@ theory SI_Units
imports SI_Dimensions
begin
subsection \<open> The \<^theory_text>\<open>Unit\<close>-type and its Operations \<close>
section \<open> The semantic SI-\<^theory_text>\<open>Unit\<close>-Type and its Operations \<close>
record 'a Unit =
mag :: 'a \<comment> \<open> Magnitude of the unit \<close>
@ -94,7 +94,8 @@ end
instance Unit_ext :: (order, order) order
by (intro_classes, auto simp add: less_Unit_ext_def less_eq_Unit_ext_def)
subsection \<open> SI Unit Types \<close>
section \<open> The abstract SI-\<^theory_text>\<open>Unit\<close>-type and its Operations \<close>
text\<open>We 'lift' SI type expressions to SI unit type expressions as follows:\<close>
typedef (overloaded) ('n, 'u::dim_type) UnitT ("_[_]" [999,0] 999)
@ -108,9 +109,7 @@ text \<open> Coerce values when their dimensions are equivalent \<close>
definition coerceUnit :: "'u\<^sub>2 itself \<Rightarrow> 'a['u\<^sub>1::dim_type] \<Rightarrow> 'a['u\<^sub>2::dim_type]" where
"SI('u\<^sub>1) = SI('u\<^sub>2) \<Longrightarrow> coerceUnit t x = (toQ (fromQ x))"
section\<open>Operations Unit types via their Semantic Domains\<close>
subsection\<open>Predicates on SI-tagged types\<close>
subsection\<open>Predicates on Abstract SI-\<^theory_text>\<open>Unit\<close>-types\<close>
text \<open> Two SI Unit types are equivalent if they have the same dimensions
(not necessarily dimension types). This is the whole point of the construction. \<close>
@ -121,6 +120,7 @@ lift_definition qless_eq ::
lift_definition qequiv ::
"'n['a::dim_type] \<Rightarrow> 'n['b::dim_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50) is "(=)" .
subsection\<open>The Equivalence on Abstract SI-\<^theory_text>\<open>Unit\<close>-types\<close>
text\<open>This gives us an equivalence, but, unfortunately, not a congruence.\<close>
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
@ -167,7 +167,7 @@ lemma qeq:
shows "SI('u\<^sub>1) = SI('u\<^sub>2::dim_type)"
by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)
subsection\<open>Operations on Unit types\<close>
subsection\<open>Operations on Abstract Unit types\<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 "(*)"

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

@ -11018,3 +11018,24 @@ isbn="978-3-540-45297-3"
public = yes,
url = {https://www.lri.fr/~wolff/papers/journals/2015-cirta-case-study.pdf}
}
@article{HayesBrendan95,
Abstract = {In the physical sciences and engineering, units of measurement provide a valuable aid to both the exposition and comprehension of physical systems. In addition, they provide an error checking facility comparable to static type checking commonly found with programming languages. It is argued that units of measurement can provide similar benefits in the specification and design of software and computer systems.},
Author = {Hayes, Ian J. and Mahony, Brendan P.},
Da = {1995/05/01},
Date-Added = {2020-02-24 17:35:41 +0100},
Date-Modified = {2020-02-24 17:35:41 +0100},
Doi = {10.1007/BF01211077},
Id = {Hayes1995},
Isbn = {1433-299X},
Journal = {Formal Aspects of Computing},
Number = {3},
Pages = {329--347},
Title = {Using units of measurement in formal specifications},
Ty = {JOUR},
Url = {https://doi.org/10.1007/BF01211077},
Volume = {7},
Year = {1995},
Bdsk-Url-1 = {https://doi.org/10.1007/BF01211077}}

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

@ -69,7 +69,7 @@ others, like the British Imperial System (BIS).
\parindent 0pt\parskip 0.5ex
\chapter{}
\chapter{Introduction to SI Units in Isabelle}
The International System of Units (SI, abbreviated from the French
Système international (d'unités)) is the modern form of the metric
@ -101,47 +101,66 @@ to the above mentioned base quantities, indexed by an integer exponent
\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 this theory is to model SI units with polymorphic magnitudes in terms of the
Isabelle/HOL\cite{nipkow.ea:isabelle:2002} type system. The objective of this construction is
reflecting the types of the magnitudes as well as their dimensions in order to allow type-safe
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 will
have the type \isa{{\isasymreal}\ {\isacharbrackleft}M\ \isactrlsup {\isachardot}\ L\ \isactrlsup
{\isachardot}\ T\isactrlsup {\isacharminus}\isactrlsup {\isadigit{2}}}, which can be used to infer
that this corresponds to the derived unit "4.5 kN" (kilo-Newton). %
%
This is an attempt to model the system and its derived entities (cf.
\url{https://www.quora.com/What-are-examples-of-SI-units}) in Isabelle/HOL,
both on a type-checking as well as a proof-support perspective.
Our design objective are for the case of Isabelle somewhat contradictory.
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: "as implicit as possible, inference as automatic as possible", it is not
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 a certain class of types, which paves the way to derive rules that
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 equality.
rules on terms and a special form of equivalence.
The construction proceeds in three phases:
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{Unit} we build a \isa{{\isacharprime}a\ SI{\isacharunderscore}tagged{\isacharunderscore}domain} types, i.e. a polymorphic family of values
tagged with values from \isa{Unit}. We construct multiplicative and additive
groups over it.
\item We construct a type-class characterizing SI - type expressions
and types tagged with SI - type expressions; this construction paves the
way to overloaded interpretation functions from SI type-expressions to
\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.
% generated text of all theories
\chapter{Appendix: The Theories}