From 9199bc310949f94724eb3cdd659b7ac512552672 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Mon, 10 Feb 2020 12:03:51 +0000 Subject: [PATCH] Split out SI units into several files, and began adapting proof automation --- src/SI/Groups_mult.thy | 5 +- src/SI/SI_Derived.thy | 35 +++++ src/SI/SI_Prefix.thy | 27 ++++ src/SI/SI_Proof.thy | 160 +++++++++++++++++++++ src/SI/SI_Quantities.thy | 297 ++++++++++++++++++++++++++++++++++++++ src/SI/SI_Units.thy | 299 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 822 insertions(+), 1 deletion(-) create mode 100644 src/SI/SI_Derived.thy create mode 100644 src/SI/SI_Prefix.thy create mode 100644 src/SI/SI_Proof.thy create mode 100644 src/SI/SI_Quantities.thy create mode 100644 src/SI/SI_Units.thy diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy index 2d967c9..54d8ad5 100644 --- a/src/SI/Groups_mult.thy +++ b/src/SI/Groups_mult.thy @@ -30,7 +30,10 @@ 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 end \ No newline at end of file diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy new file mode 100644 index 0000000..776cbc1 --- /dev/null +++ b/src/SI/SI_Derived.thy @@ -0,0 +1,35 @@ +section \ Derived Units\ + +theory SI_Derived + imports SI_Prefix +begin + +definition "radian = 1 \ (meter \<^bold>\ meter\<^sup>-\<^sup>\)" + +definition degree :: "real[meter / meter]" where +[si_def]: "degree = (2\(UNIT(pi,_)) / 180)\radian" + +abbreviation degrees ("_\" [999] 999) where "n\ \ n\degree" + +definition [si_def]: "litre = 1/1000 \ meter\<^sup>\" + +definition [si_def]: "pint = 0.56826125 \ litre" + +definition [si_def]: "hour = 3600 \ second" + +abbreviation "tonne \ kilo\kilogram" + +abbreviation "newton \ (kilogram \<^bold>\ meter) \<^bold>/ second\<^sup>\" + +abbreviation "volt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" + +abbreviation "watt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +abbreviation "joule \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +text\The full beauty of the approach is perhaps revealed here, with the + type of a classical three-dimensional gravitation field:\ +type_synonym gravitation_field = "(real\<^sup>3 \ real\<^sup>3)[meter \ (second)\<^sup>-\<^sup>2]" + + +end \ No newline at end of file diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy new file mode 100644 index 0000000..f104cae --- /dev/null +++ b/src/SI/SI_Prefix.thy @@ -0,0 +1,27 @@ +section \ SI Prefixes \ + +theory SI_Prefix + imports SI_Quantities +begin + +definition [si_def]: "giga = UNIT(1000000000, _)" + +definition [si_def]: "mega = UNIT(1000000, _)" + +definition [si_def]: "kilo = UNIT(1000, _)" + +definition [si_def]: "hecto = UNIT(100, _)" + +definition [si_def]: "deca = UNIT(10, _)" + +definition [si_def]: "deci = UNIT(0.1, _)" + +definition [si_def]: "centi = UNIT(0.01, _)" + +definition [si_def]: "milli = UNIT(0.001, _)" + +definition [si_def]: "micro = UNIT(0.000001, _)" + +definition [si_def]: "nano = UNIT(0.000000001, _)" + +end \ No newline at end of file diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy new file mode 100644 index 0000000..5b79273 --- /dev/null +++ b/src/SI/SI_Proof.thy @@ -0,0 +1,160 @@ +theory SI_Proof + imports SI_Derived +begin + +section \ Tactic Support for SI type expressions. \ + +lemmas [si_def] = si_sem_meter_def si_sem_kilogram_def si_sem_second_def + si_sem_ampere_def si_sem_kelvin_def si_sem_mole_def + si_sem_candela_def + + si_sem_UnitTimes_def si_sem_UnitInv_def + times_Unit_ext_def one_Unit_ext_def + +(* renaming and putting defs into the rewrite set (which is usually not a good idea) *) +lemma "SI(meter) = 1\Meters := 1\" by(simp add: si_def) +lemma "SI(kilogram)= 1\Kilograms := 1\" by(simp add: si_def) +lemma "SI(second) = 1\Seconds := 1\ " by(simp add: si_def) +lemma "SI(ampere) = 1\Amperes := 1\" by(simp add: si_def) +lemma "SI(kelvin) = 1\Kelvins := 1\ " by(simp add: si_def) +lemma "SI(mole) = 1\Moles := 1\" by(simp add: si_def) +lemma "SI(candela) = 1\Candelas := 1\" by(simp add: si_def) + +lemma "SI(mole \ kelvin \ mole) = SI(kelvin \ (mole)\<^sup>2)" by(simp add: si_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, second) = + \magn = x, + unit = \Seconds = 1, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_second_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, meter) = + \magn = x, + unit = \Seconds = 0, Meters = 1, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_meter_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, kilogram) = + \magn = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 1, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_kilogram_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, ampere) = + \magn = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 1, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_ampere_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, kelvin) = + \magn = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 1, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_kelvin_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, mole) = + \magn = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 1, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_mole_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, candela) = + \magn = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 1\\" + by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_candela_def) + +lemma Unit_times_commute: + fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"and Y::"'a['c::si_type]" + shows "X \<^bold>\ Y \\<^sub>Q Y \<^bold>\ X" + by (transfer, simp add: mult.commute times_Quantity_ext_def) + +text\Observe that this commutation law also commutes the types.\ + +(* just a check that instantiation works for special cases ... *) +lemma " (UNIT(x, candela) \<^bold>\ UNIT(y::'a::{one,ab_semigroup_mult}, mole)) + \\<^sub>Q (UNIT(y, mole) \<^bold>\ UNIT(x, candela)) " + by(simp add: Unit_times_commute) + + +lemma Unit_times_assoc: + fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]" + and Y::"'a['c::si_type]" + and Z::"'a['d::si_type]" + shows "(X \<^bold>\ Y) \<^bold>\ Z \\<^sub>Q X \<^bold>\ (Y \<^bold>\ Z)" + by (transfer, simp add: mult.commute mult.left_commute times_Quantity_ext_def) + +text\The following weak congruences will allow for replacing equivalences in contexts + built from product and inverse. \ +lemma Unit_times_weak_cong_left: + fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]" + and Y::"'a['c::si_type]" + and Z::"'a['d::si_type]" + assumes "X \\<^sub>Q Y" + shows "(X \<^bold>\ Z) \\<^sub>Q (Y \<^bold>\ Z)" + using assms by (transfer, simp) + +lemma Unit_times_weak_cong_right: + fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]" + and Y::"'a['c::si_type]" + and Z::"'a['d::si_type]" + assumes "X \\<^sub>Q Y" + shows "(Z \<^bold>\ X) \\<^sub>Q (Z \<^bold>\ Y)" + using assms by (transfer, simp) + +lemma Unit_inverse_weak_cong: + fixes X::"'a::{field}['b::si_type]" + and Y::"'a['c::si_type]" + assumes "X \\<^sub>Q Y" + shows "(X)\<^sup>-\<^sup>\ \\<^sub>Q (Y)\<^sup>-\<^sup>\" + using assms by (transfer, simp) + +text\In order to compute a normal form, we would additionally need these three:\ +(* field ? *) +lemma Unit_inverse_distrib: + fixes X::"'a::{field}['b::si_type]" + and Y::"'a['c::si_type]" + shows "(X \<^bold>\ Y)\<^sup>-\<^sup>\ \\<^sub>Q X\<^sup>-\<^sup>\ \<^bold>\ Y\<^sup>-\<^sup>\" + apply (transfer) + sorry + +(* field ? *) +lemma Unit_inverse_inverse: + fixes X::"'a::{field}['b::si_type]" + shows "((X)\<^sup>-\<^sup>\)\<^sup>-\<^sup>\ \\<^sub>Q X" + apply transfer + sorry + +(* field ? *) +lemma Unit_mult_cancel: + fixes X::"'a::{field}['b::si_type]" + shows "X \<^bold>/ X \\<^sub>Q 1" + apply transfer + sorry + + +lemma Unit_mult_mult_Left_cancel: + fixes X::"'a::{field}['b::si_type]" + shows "(1::'a['b/'b]) \<^bold>\ X \\<^sub>Q X" + apply transfer + sorry + + +lemma "watt \<^bold>\ hour \\<^sub>Q 3600 \<^bold>\ joule" + apply (transfer) + unfolding Unit_equiv_def hour_def + apply(simp add: Units.Unit_times.rep_eq si_def + zero_SI_tagged_domain_ext_def times_SI_tagged_domain_ext_def + inverse_SI_tagged_domain_ext_def + Unit_inverse_def Unit_times_def) + find_theorems fromUnit + oops + + thm Units.Unit.toUnit_inverse + + +lemma "watt \<^bold>\ hour \\<^sub>Q 3.6 \<^bold>\ kilo \<^bold>\ joule" + oops + + +end \ No newline at end of file diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy new file mode 100644 index 0000000..cfc92d0 --- /dev/null +++ b/src/SI/SI_Quantities.thy @@ -0,0 +1,297 @@ +section \ SI Quantities \ + +theory SI_Quantities + imports SI_Units +begin + +subsection \ The \<^theory_text>\Quantity\-type and its operations \ + +record 'a Quantity = + magn :: 'a \ \ Magnitude of the quantity \ + unit :: Unit \ \ Unit of the quantity \ + +lemma Quantity_eq_intro: + assumes "magn x = magn y" "unit x = unit y" "more x = more y" + shows "x = y" + by (simp add: assms) + +instantiation Quantity_ext :: (times, times) times +begin + definition "times_Quantity_ext x y = \ magn = magn x \ magn y, unit = unit x \ unit y, \ = more x \ more y \" +instance .. +end + +instantiation Quantity_ext :: (zero, zero) zero +begin + definition "zero_Quantity_ext = \ magn = 0, unit = 1, \ = 0 \" +instance .. +end + +instantiation Quantity_ext :: (one, one) one +begin + definition "one_Quantity_ext = \ magn = 1, unit = 1, \ = 1 \" +instance .. +end + +instantiation Quantity_ext :: (inverse, inverse) inverse +begin + definition "inverse_Quantity_ext x = \ magn = inverse (magn x), unit = inverse (unit x), \ = inverse (more x) \" + definition "divide_Quantity_ext x y = \ magn = magn x / magn y, unit = unit x / unit y, \ = more x / more y \" +instance .. +end + +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 + oops + +subsection \ SI Tagged Types \ +text\We 'lift' SI type expressions to SI tagged type expressions as follows:\ + +typedef (overloaded) ('n, 'u::si_type) tQuant ("_[_]" [999,0] 999) + = "{x :: 'n Quantity. unit x = SI('u)}" + morphisms fromUnit toUnit by (rule_tac x="\ magn = undefined, unit = SI('u) \" in exI, simp) + +setup_lifting type_definition_tQuant + +text \ Coerce values when their units are equivalent \ + +definition coerceUnit :: "'u\<^sub>2 itself \ 'a['u\<^sub>1::si_type] \ 'a['u\<^sub>2::si_type]" where +"SI('u\<^sub>1) = SI('u\<^sub>2) \ coerceUnit t x = (toUnit (fromUnit x))" + +section\Operations SI-tagged types via their Semantic Domains\ + +subsection\Predicates on SI-tagged types\ + +text \ Two SI types are equivalent if they have the same value-level units. \ + +lift_definition Quant_equiv :: "'n['a::si_type] \ 'n['b::si_type] \ bool" (infix "\\<^sub>Q" 50) is +"(=)" . + +text\This gives us an equivalence, but, unfortunately, not a congruence.\ + +lemma Quant_equiv_refl [simp]: "a \\<^sub>Q a" + by (simp add: Quant_equiv_def) + +lemma Quant_equiv_sym: "a \\<^sub>Q b \ b \\<^sub>Q a" + by (simp add: Quant_equiv_def) + +lemma Quant_equiv_trans: "\ a \\<^sub>Q b; b \\<^sub>Q c \ \ a \\<^sub>Q c" + by (simp add: Quant_equiv_def) + +(* the following series of equivalent statements ... *) + +lemma coerceQuant_eq_iff: + fixes x :: "'a['u\<^sub>1::si_type]" + assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" + shows "(coerceUnit TYPE('u\<^sub>2) x) \\<^sub>Q x" + by (metis Quant_equiv.rep_eq assms coerceUnit_def toUnit_cases toUnit_inverse) + +(* or equivalently *) + +lemma coerceQuant_eq_iff2: + fixes x :: "'a['u\<^sub>1::si_type]" + assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (coerceUnit TYPE('u\<^sub>2) x)" + shows "x \\<^sub>Q y" + using Quant_equiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast + +lemma updown_eq_iff: + fixes x :: "'a['u\<^sub>1::si_type]" fixes y :: "'a['u\<^sub>2::si_type]" + assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (toUnit (fromUnit x))" + shows "x \\<^sub>Q y" + by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceUnit_def) + +text\This is more general that \y = x \ x \\<^sub>Q y\, since x and y may have different type.\ + +find_theorems "(toUnit (fromUnit _))" + +lemma eq_ : + fixes x :: "'a['u\<^sub>1::si_type]" fixes y :: "'a['u\<^sub>2::si_type]" + assumes "x \\<^sub>Q y" + shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" + by (metis (full_types) Quant_equiv.rep_eq assms fromUnit mem_Collect_eq) + +subsection\Operations on SI-tagged types\ + +lift_definition + Quant_times :: "('n::times)['a::si_type] \ 'n['b::si_type] \ 'n['a \'b]" (infixl "\<^bold>\" 69) is "(*)" + by (simp add: si_sem_UnitTimes_def times_Quantity_ext_def) + +lift_definition + Quant_inverse :: "('n::inverse)['a::si_type] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) is "inverse" + by (simp add: inverse_Quantity_ext_def si_sem_UnitInv_def) + +abbreviation + Quant_divide :: "('n::{times,inverse})['a::si_type] \ 'n['b::si_type] \ 'n['a/'b]" (infixl "\<^bold>'/" 70) where +"Quant_divide x y \ x \<^bold>\ y\<^sup>-\<^sup>\" + +abbreviation Quant_sq ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u" +abbreviation Quant_cube ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u\<^bold>\u\<^bold>\u" + +abbreviation Quant_neq_sq ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" +abbreviation Quant_neq_cube ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" + +instantiation tQuant :: (zero,si_type) zero +begin +lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\ magn = 0, unit = SI('b) \" + by simp +instance .. +end + +instantiation tQuant :: (one,si_type) one +begin +lift_definition one_tQuant :: "('a, 'b) tQuant" is "\ magn = 1, unit = SI('b) \" + by simp +instance .. +end + +instantiation tQuant :: (plus,si_type) plus +begin +lift_definition plus_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ magn = magn x + magn y, unit = SI('b) \" + by (simp) +instance .. +end + +instance tQuant :: (semigroup_add,si_type) semigroup_add + by (intro_classes, transfer, simp add: add.assoc) + +instance tQuant :: (ab_semigroup_add,si_type) ab_semigroup_add + by (intro_classes, transfer, simp add: add.commute) + +instance tQuant :: (monoid_add,si_type) monoid_add + by (intro_classes; (transfer, simp)) + +instance tQuant :: (comm_monoid_add,si_type) comm_monoid_add + by (intro_classes; transfer, simp) + +instantiation tQuant :: (uminus,si_type) uminus +begin +lift_definition uminus_tQuant :: "'a['b] \ 'a['b]" + is "\ x. \ magn = - magn x, unit = unit x \" by (simp) +instance .. +end + +instantiation tQuant :: (minus,si_type) minus +begin +lift_definition minus_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ magn = magn x - magn y, unit = unit x \" by (simp) + +instance .. +end + +instance tQuant :: (numeral,si_type) numeral .. + +instantiation tQuant :: (times,si_type) times +begin +lift_definition times_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ magn = magn x * magn y, unit = SI('b) \" + by simp +instance .. +end + +instance tQuant :: (power,si_type) power .. + +instance tQuant :: (semigroup_mult,si_type) semigroup_mult + by (intro_classes, transfer, simp add: mult.assoc) + +instance tQuant :: (ab_semigroup_mult,si_type) ab_semigroup_mult + by (intro_classes, (transfer, simp add: mult.commute)) + +instance tQuant :: (comm_semiring,si_type) comm_semiring + by (intro_classes, transfer, simp add: linordered_field_class.sign_simps(18) mult.commute) + +instance tQuant :: (comm_semiring_0,si_type) comm_semiring_0 + by (intro_classes, (transfer, simp)+) + +instance tQuant :: (comm_monoid_mult,si_type) comm_monoid_mult + by (intro_classes, (transfer, simp add: mult.commute)+) + +instance tQuant :: (comm_semiring_1,si_type) comm_semiring_1 + by (intro_classes; (transfer, simp add: semiring_normalization_rules(1-8,24))) + +instantiation tQuant :: (divide,si_type) divide +begin +lift_definition divide_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" + is "\ x y. \ magn = magn x div magn y, unit = SI('b) \" by simp +instance .. +end + +instantiation tQuant :: (inverse,si_type) inverse +begin +lift_definition inverse_tQuant :: "'a['b] \ 'a['b]" + is "\ x. \ magn = inverse (magn x), unit = SI('b) \" by simp +instance .. +end + +instantiation tQuant :: (order,si_type) order +begin + lift_definition less_eq_tQuant :: "'a['b] \ 'a['b] \ bool" is "\ x y. magn x \ magn y" . + lift_definition less_tQuant :: "'a['b] \ 'a['b] \ bool" is "\ x y. magn x < magn y" . + instance by (intro_classes, (transfer, simp add: less_le_not_le)+) +end + +lift_definition mk_unit :: "'a \ 'u itself \ ('a::one)['u::si_type]" + is "\ n u. \ magn = n, unit = SI('u) \" by simp + +syntax "_mk_unit" :: "logic \ type \ logic" ("UNIT'(_, _')") +translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)" + +subsection \Polymorphic Operations for Elementary SI Units \ + +named_theorems si_def + +definition [si_def]: "meter = UNIT(1, meter)" +definition [si_def]: "second = UNIT(1, second)" +definition [si_def]: "kilogram = UNIT(1, kilogram)" +definition [si_def]: "ampere = UNIT(1, ampere)" +definition [si_def]: "kelvin = UNIT(1, kelvin)" +definition [si_def]: "mole = UNIT(1, mole)" +definition [si_def]: "candela = UNIT(1, candela)" + +subsubsection \The Projection: Stripping the SI-Tags \ + +definition magnQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where +"magnQuant x = magn (fromUnit x)" + +subsubsection \More Operations \ + +lemma unit_eq_iff_magn_eq: + "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" + by (auto simp add: magnQuant_def, transfer, simp) + +lemma unit_le_iff_magn_le: + "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" + by (auto simp add: magnQuant_def; (transfer, simp)) + +lemma magnQuant_zero [si_def]: "\0\\<^sub>Q = 0" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_one [si_def]: "\1\\<^sub>Q = 1" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_plus [si_def]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_times [si_def]: "\x * y\\<^sub>Q = \x\\<^sub>Q * \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_div [si_def]: "\x / y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_numeral [si_def]: "\numeral n\\<^sub>Q = numeral n" + apply (induct n, simp_all add: si_def) + apply (metis magnQuant_plus numeral_code(2)) + apply (metis magnQuant_one magnQuant_plus numeral_code(3)) + done + +lemma magnQuant_mk [si_def]: "\UNIT(n, 'u::si_type)\\<^sub>Q = n" + by (simp add: magnQuant_def, transfer, simp) + +method si_calc = + (simp add: unit_eq_iff_magn_eq unit_le_iff_magn_le si_def) + + +end \ No newline at end of file diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy new file mode 100644 index 0000000..756933c --- /dev/null +++ b/src/SI/SI_Units.thy @@ -0,0 +1,299 @@ +section \ SI Units \ + +theory SI_Units + imports Groups_mult + HOL.Transcendental + "HOL-Eisbach.Eisbach" +begin + +text\ +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\).\ + +text\ 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. +The design objective are twofold (and for the case of Isabelle somewhat +contradictory, see below) + +The construction proceeds in three phases: +\<^enum> We construct a generic type \<^theory_text>\Unit\ which is basically an "inner representation" or + "semantic domain" of all SI types. 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. +\<^enum> From \<^theory_text>\Unit\ we build a \<^theory_text>\'a SI_tagged_domain\ types, i.e. a polymorphic family of values + tagged with values from \<^theory_text>\Unit\. We construct multiplicative and additive + groups over it. +\<^enum> 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 + +\ + +section\The Domains of SI types and SI-tagged types\ + +subsection \ The \<^theory_text>\Unit\-type and its operations \ + +text \ 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. \ + +record Unit = + Seconds :: int + Meters :: int + Kilograms :: int + Amperes :: int + Kelvins :: int + Moles :: int + Candelas :: int + +text \ We define a commutative monoid for SI units. \ + +instantiation Unit_ext :: (one) one +begin + \ \ Here, $1$ is the dimensionless unit \ +definition one_Unit_ext :: "'a Unit_ext" + where [code_unfold]: "1 = \ Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0 + , Kelvins = 0, Moles = 0, Candelas = 0, \ = 1 \" + instance .. +end + +instantiation Unit_ext :: (times) times +begin + \ \ Multiplication is defined by adding together the powers \ +definition times_Unit_ext :: "'a Unit_ext \ 'a Unit_ext \ 'a Unit_ext" + where [code_unfold]: + "x * y = \ Seconds = Seconds x + Seconds y, Meters = Meters x + Meters y + , Kilograms = Kilograms x + Kilograms y, Amperes = Amperes x + Amperes y + , Kelvins = Kelvins x + Kelvins y, Moles = Moles x + Moles y + , Candelas = Candelas x + Candelas y, \ = more x * more y \" + instance .. +end + +instance Unit_ext :: (comm_monoid_mult) comm_monoid_mult +proof + fix a b c :: "'a Unit_ext" + show "a * b * c = a * (b * c)" + by (simp add: times_Unit_ext_def mult.assoc) + show "a * b = b * a" + by (simp add: times_Unit_ext_def mult.commute) + show "1 * a = a" + by (simp add: times_Unit_ext_def one_Unit_ext_def) +qed + +text \ We also define the inverse and division operations, and an abelian group. \ + +instantiation Unit_ext :: ("{times,inverse}") inverse +begin +definition inverse_Unit_ext :: "'a Unit_ext \ 'a Unit_ext" + where [code_unfold]: + "inverse x = \ Seconds = - Seconds x , Meters = - Meters x + , Kilograms = - Kilograms x, Amperes = - Amperes x + , Kelvins = - Kelvins x, Moles = - Moles x + , Candelas = - Candelas x, \ = inverse (more x) \" + +definition divide_Unit_ext :: "'a Unit_ext \ 'a Unit_ext \ 'a Unit_ext" + where [code_unfold]: + "divide_Unit_ext x y = x * (inverse y)" + instance .. +end + +instance Unit_ext :: (ab_group_mult) ab_group_mult +proof + fix a b :: "'a Unit_ext" + show "inverse a \ a = 1" + by (simp add: inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def) + show "a \ inverse b = a div b" + by (simp add: divide_Unit_ext_def) +qed + +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 + +text \ A base unit is an SI_tagged_domain unit here precisely one unit has power 1. \ + +definition is_BaseUnit :: "Unit \ bool" where +"is_BaseUnit u = (\ n. u = 1\Meters := n\ \ u = 1\Kilograms := n\ \ u = 1\Seconds := n\ + \ u = 1\Amperes := n\ \ u = 1\Kelvins := n\ \ u = 1\Moles := n\ + \ u = 1\Candelas := n\)" + +section\The Syntax and Semantics of SI types and SI-tagged types\ + +subsection \ Basic SI-types \ + +text \ We provide a syntax for type-expressions; The definition of +the basic type constructors is straight-forward via a one-elementary set. \ + +typedef meter = "UNIV :: unit set" .. setup_lifting type_definition_meter +typedef kilogram = "UNIV :: unit set" .. setup_lifting type_definition_kilogram +typedef second = "UNIV :: unit set" .. setup_lifting type_definition_second +typedef ampere = "UNIV :: unit set" .. setup_lifting type_definition_ampere +typedef kelvin = "UNIV :: unit set" .. setup_lifting type_definition_kelvin +typedef mole = "UNIV :: unit set" .. setup_lifting type_definition_mole +typedef candela = "UNIV :: unit set" .. setup_lifting type_definition_candela + +subsection \ SI-type expressions and SI-type interpretation \ + +text \ 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 +are restricted to the set of SI-type expressions. + +The mechanism in Isabelle to characterize a certain sub-class of Isabelle-type expressions +are \<^emph>\type classes\. We therefore need such a sub-class; for reasons of convenience, +we combine its construction also with the "semantics" of SI types in terms of +@{typ Unit}. \ + +subsubsection \ SI-type expression definition as type-class \ + +class si_type = finite + + fixes si_sem :: "'a itself \ Unit" + assumes unitary_unit_pres: "card (UNIV::'a set) = 1" + +syntax + "_SI" :: "type \ logic" ("SI'(_')") + +translations + "SI('a)" == "CONST si_sem TYPE('a)" + +text \ The sub-set of basic SI type expressions can be characterized by the following +operation: \ + +class si_baseunit = si_type + + assumes is_BaseUnit: "is_BaseUnit SI('a)" + +subsubsection \ SI base type constructors \ + +text\We embed the basic SI types into the SI type expressions: \ +declare [[show_sorts]] + +instantiation meter :: si_baseunit +begin + definition si_sem_meter :: "meter itself \ Unit" where "si_sem_meter x = 1\Meters := 1\" +instance by (intro_classes, auto simp add: si_sem_meter_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation kilogram :: si_baseunit +begin + definition si_sem_kilogram :: "kilogram itself \ Unit" where "si_sem_kilogram x = 1\Kilograms := 1\" +instance by (intro_classes, auto simp add: si_sem_kilogram_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation second :: si_baseunit +begin + definition si_sem_second :: "second itself \ Unit" where "si_sem_second x = 1\Seconds := 1\" +instance by (intro_classes, auto simp add: si_sem_second_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation ampere :: si_baseunit +begin + definition si_sem_ampere :: "ampere itself \ Unit" where "si_sem_ampere x = 1\Amperes := 1\" +instance by (intro_classes, auto simp add: si_sem_ampere_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation kelvin :: si_baseunit +begin + definition si_sem_kelvin :: "kelvin itself \ Unit" where "si_sem_kelvin x = 1\Kelvins := 1\" +instance by (intro_classes, auto simp add: si_sem_kelvin_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation mole :: si_baseunit +begin + definition si_sem_mole :: "mole itself \ Unit" where "si_sem_mole x = 1\Moles := 1\" +instance by (intro_classes, auto simp add: si_sem_mole_def is_BaseUnit_def, (transfer, simp)+) +end + +instantiation candela :: si_baseunit +begin + definition si_sem_candela :: "candela itself \ Unit" where "si_sem_candela x = 1\Candelas := 1\" +instance by (intro_classes, auto simp add: si_sem_candela_def is_BaseUnit_def, (transfer, simp)+) +end + +lemma base_units [simp]: + "is_BaseUnit SI(meter)" "is_BaseUnit SI(kilogram)" "is_BaseUnit SI(second)" + "is_BaseUnit SI(ampere)" "is_BaseUnit SI(kelvin)" "is_BaseUnit SI(mole)" + "is_BaseUnit SI(candela)" by (simp_all add: is_BaseUnit) + +subsubsection \ Higher SI Type Constructors: Inner Product and Inverse \ +text\On the class of SI-types (in which we have already inserted the base SI types), +the definitions of the type constructors for inner product and inverse is straight) forward.\ + +typedef ('a::si_type, 'b::si_type) UnitTimes (infixl "\" 69) = "UNIV :: unit set" .. +setup_lifting type_definition_UnitTimes + +text \ We can prove that multiplication of two SI types yields an SI type. \ + +instantiation UnitTimes :: (si_type, si_type) si_type +begin + definition si_sem_UnitTimes :: "('a \ 'b) itself \ Unit" where + "si_sem_UnitTimes x = SI('a) * SI('b)" + instance by (intro_classes, simp_all add: si_sem_UnitTimes_def, (transfer, simp)+) +end + +text \ Similarly, we define division of two SI types and prove that SI types are closed under this. \ + +typedef 'a UnitInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" .. +setup_lifting type_definition_UnitInv +instantiation UnitInv :: (si_type) si_type +begin + definition si_sem_UnitInv :: "('a\<^sup>-\<^sup>1) itself \ Unit" where + "si_sem_UnitInv x = inverse SI('a)" + instance by (intro_classes, simp_all add: si_sem_UnitInv_def, (transfer, simp)+) +end + + +subsubsection \ Syntactic Support for SI type expressions. \ + +text\A number of type-synonyms allow for more compact notation: \ +type_synonym ('a, 'b) UnitDiv = "'a \ ('b\<^sup>-\<^sup>1)" (infixl "'/" 69) + +type_synonym 'a UnitSquare = "'a \ 'a" ("(_)\<^sup>2" [999] 999) +type_synonym 'a UnitCube = "'a \ 'a \ 'a" ("(_)\<^sup>3" [999] 999) +type_synonym 'a UnitInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999) +type_synonym 'a UnitInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [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" + +print_translation \ + [(@{type_syntax UnitTimes}, + fn ctx => fn [a, b] => + if (a = b) + then Const (@{type_syntax UnitSquare}, dummyT) $ a + else case a of + Const (@{type_syntax UnitTimes}, _) $ a1 $ a2 => + if (a1 = a2 andalso a2 = b) + then Const (@{type_syntax UnitCube}, dummyT) $ a1 + else raise Match | + Const (@{type_syntax UnitSquare}, _) $ a' => + if (@{print} a' = b) + then Const (@{type_syntax UnitCube}, dummyT) $ a' + else raise Match | + _ => raise Match)] +\ + +end \ No newline at end of file