More refactoring. The mechanisation is now split conveniently into a quantity and unit part. Most of the technical foundations

can be found in the former.

src/SI/ISQ_Algebra.thy

@@ -1,7 +1,7 @@
 section \<open> Algebraic Laws \<close>
 
-theory SI_Algebra
+theory ISQ_Algebra
-  imports SI_Proof
+  imports ISQ_Proof
 begin
 
 subsection \<open> Quantity Scale \<close>

src/SI/ISQ_Proof.thy

@@ -1,7 +1,7 @@
-section \<open>Basic Proof Support for SI Units \<close>
+section \<open> Proof Support for Quantities \<close>
 
-theory SI_Proof
+theory ISQ_Proof
-  imports SI_Units
+  imports ISQ_Quantities
 begin
 
 named_theorems si_transfer
@@ -61,9 +61,6 @@ lemma magQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n
   apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3))
   done
 
-lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
-  by (simp add: magQuant_def, transfer, simp)
-
 text \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
 
 method si_simp uses add =
@@ -74,24 +71,6 @@ text \<open> The next tactic additionally compiles the semantics of the underlyi
 method si_calc uses add = 
   (si_simp add: add; simp add: si_def add)
 
-(*
-lemmas [si_eq] = si_sem_Length_def si_sem_Mass_def si_sem_Time_def 
-                   si_sem_Current_def si_sem_Temperature_def si_sem_Amount_def
-                   si_sem_Intensity_def si_sem_NoDimension_def
-                   si_sem_UnitTimes_def si_sem_UnitInv_def
-                   inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def
-
-lemmas [si_def] =  si_sem_Length_def si_sem_Mass_def si_sem_Time_def 
-                   si_sem_Current_def si_sem_Temperature_def si_sem_Amount_def
-                   si_sem_Intensity_def si_sem_NoDimension_def
-
-                   si_sem_UnitTimes_def si_sem_UnitInv_def
-                   times_Unit_ext_def one_Unit_ext_def
-*)
-
 lemma "QD(N \<cdot> \<Theta> \<cdot> N) = QD(\<Theta> \<cdot> N\<^sup>2)" by (simp add: si_eq si_def)
 
-lemma "(meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q meter"
-  by (si_calc)
-
 end

src/SI/ISQ_Quantities.thy

@@ -165,19 +165,21 @@ definition coerceQuantT :: "'d\<^sub>2 itself \<Rightarrow> 'a['d\<^sub>1::dim_t
 
 subsection \<open> Predicates on Typed Quantities \<close>
 
-text \<open> Two SI Unit types are orderable if their magnitude type is of class @{class "order"},
+text \<open> The standard HOL order \<^term>\<open>(\<le>)\<close> and equality \<^term>\<open>(=)\<close> have the homogeneous type
-       and have the same dimensions (not necessarily dimension types).\<close>
+  \<^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>)" .
 
-text\<open> Two SI Unit types are equivalent if they have the same dimensions
-      (not necessarily dimension types). This equivalence the a vital point 
-      of the overall construction of SI Units. \<close>
-
 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)
 
@@ -192,16 +194,12 @@ theorem qeq_iff_same_dim:
   shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
   by (transfer, simp)
 
-(* the following series of equivalent statements ... *)
-
 lemma coerceQuant_eq_iff:
   fixes x :: "'a['d\<^sub>1::dim_type]"
   assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)"
   shows "(coerceQuantT TYPE('d\<^sub>2) x) \<cong>\<^sub>Q x"
   by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)
 
-(* or equivalently *)
-
 lemma coerceQuant_eq_iff2:
   fixes x :: "'a['d\<^sub>1::dim_type]"
   assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (coerceQuantT TYPE('d\<^sub>2) x)"
@@ -218,16 +216,20 @@ text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^
 
 lemma qeq: 
   fixes x :: "'a['d\<^sub>1::dim_type]" fixes y :: "'a['d\<^sub>2::dim_type]"
-  assumes  "x \<cong>\<^sub>Q y"
+  assumes "x \<cong>\<^sub>Q y"
-  shows "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)"
+  shows "QD('d\<^sub>1) = QD('d\<^sub>2)"
   by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)
 
-subsection\<open>Operations on Abstract SI-Unit-Types\<close>
+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)
@@ -236,6 +238,8 @@ abbreviation
   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"
@@ -244,6 +248,19 @@ abbreviation qneq_sq     ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-
 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>" 
@@ -258,6 +275,14 @@ lift_definition one_QuantT :: "('a, 'b) QuantT" is "\<lparr> mag = 1, dim = QD('
 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]"
@@ -266,6 +291,9 @@ lift_definition plus_QuantT :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]
 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)
 
@@ -295,9 +323,13 @@ 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" .
@@ -305,11 +337,7 @@ begin
   instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
 end
 
-text\<open>The scaling operator permits to multiply the magnitude of a unit; this scalar product 
+instance QuantT :: (linorder,dim_type) linorder
-produces what is called "prefixes" in the terminology of the SI system.\<close>
+  by (intro_classes, transfer, auto)
-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)
 
 end

src/SI/SI_Constants.thy

@@ -1,7 +1,7 @@
 section \<open> Physical Constants \<close>
 
 theory SI_Constants
-  imports SI_Proof
+  imports SI_Units
 begin
 
 subsection \<open> Core Derived Units \<close>

src/SI/SI_Units.thy

@@ -1,7 +1,7 @@
 section \<open> SI Units \<close>
 
 theory SI_Units
-  imports ISQ_Quantities
+  imports SI_Proof
 begin
 
 lift_definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]" 
@@ -10,6 +10,9 @@ lift_definition mk_base_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]
 syntax "_mk_base_unit" :: "type \<Rightarrow> logic" ("BUNIT'(_')")
 translations "BUNIT('a)" == "CONST mk_base_unit TYPE('a)"
 
+lemma magQuant_mk [si_eq]: "\<lbrakk>BUNIT('u::dim_type)\<rbrakk>\<^sub>Q = 1"
+  by (simp add: magQuant_def, transfer, simp)
+
 subsection \<open>Polymorphic Operations for SI Base Units \<close>
 
 definition [si_eq]: "meter    = BUNIT(L)"
@@ -20,9 +23,6 @@ definition [si_eq]: "kelvin   = BUNIT(\<Theta>)"
 definition [si_eq]: "mole     = BUNIT(N)"
 definition [si_eq]: "candela  = BUNIT(J)"
 
-definition dimless ("\<one>") 
-  where    [si_eq]: "dimless  = BUNIT(NoDimension)"
-
 text\<open>Note that as a consequence of our construction, the term @{term meter} is a SI Unit constant of 
 SI-type @{typ "'a[L]"}, so a unit of dimension @{typ "Length"} with the magnitude of type @{typ"'a"}.
 A magnitude instantiation can be, e.g., an integer, a rational number, a real number, or a vector of 
@@ -36,4 +36,9 @@ lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool"
 lemma meter_is_BaseUnit: "is_BaseUnit meter"
   by (simp add: si_eq, transfer, simp)
 
+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