Masses and mass units

Konrad Hinsen

Context mass
uses builtins/real-numbers

1 Masses

The sum of two masses is a mass:

mass + mass : mass

The product of a positive number with a mass is a mass:

ℝp × mass : mass

A mass divided by a positive number is a mass:

mass ÷ ℝp : mass

The quotient of two masses is a positive number:

mass ÷ mass : ℝp

1.1 Simplification rules

In the following, we use the variables M:mass, M1:mass, M2:mass and F:ℝp, F1:ℝp, F2:ℝp.

Combine multiples of the same mass:

(F1 × M) + (F2 × M) ⇒ (F1 + F2) × M

Replace multiple prefactors and divisions by simple prefactors:

F1 × (F2 × M) ⇒ F1 × F2 × M
M ÷ F ⇒ (1 ÷ F) × M

Reduce quotients of two masses to a number if possible:

M1 ÷ (F × M2) ⇒ M1 ÷ F ÷ M2
(F × M1) ÷ M2 ⇒ F × (M1 ÷ M2)
M ÷ M ⇒ 1

Context mass-units
extends mass
uses boolean/boolean

2 Mass units

A mass-unit ⊆ mass is a mass used as a reference in specifying other masses.

Some common mass units are:

kg : mass-unit
g : mass-unit
mg : mass-unit

A mass converted to another unit is a mass as well:

mass in mass-unit : mass

Mass conversion is done in two steps. First all masses are expressed in terms of a pivot unit, which is the kg. Next, the result is expressed in terms of the desired unit. Due to this two-step process, conversion factors must only be specified between each unit and the pivot unit:

g ÷ kg ⇒ 1/1000
mg ÷ kg ⇒ 1/1000000

2.1 Simplification rules

Additional variables: MU:mass-unit, MU1:mass-unit, MU2:mass-unit.

The following rule achieves unit conversion in concertation with the mass simplification rules, which reduce the quotient to a number with the help of the conversion factors:

M in MU ⇒ (M ÷ MU) × MU

Moreover, the quotient of two mass units is reduced to the quotient of their conversion factors with respect to the pivot unit:

MU1 ÷ MU2 ⇒ MU1 ÷ kg ÷ (MU2 ÷ kg) if ¬(MU2 == kg)

2.2 Tests

2 × (3 × kg) ⇒ 6 × kg ✓
2 × (kg ÷ 3) ⇒ 2/3 × kg ✓
(2 × kg) ÷ 3 ⇒ 2/3 × kg ✓
(2 × kg) ÷ (3 × kg) ⇒ 2/3 ✓
(2 × g) ÷ (3 × kg) ⇒ 1/1500 ✓
(2 × g) ÷ (3 × mg) ⇒ 2000/3 ✓
(2 × g) in mg ⇒ 2000 × mg ✓