From 1172f0f30a4fa5335ed8ac97ebf3f388e4aec783 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 5 Feb 2020 14:00:59 +0100 Subject: [PATCH] Varous little changes, and attemps to improve example sections and proof support. --- src/SI/Units.thy | 520 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 364 insertions(+), 156 deletions(-) diff --git a/src/SI/Units.thy b/src/SI/Units.thy index 42823760..a577f269 100644 --- a/src/SI/Units.thy +++ b/src/SI/Units.thy @@ -21,14 +21,29 @@ 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>\SI_domain\ 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>\SI_domain\ we build a \<^theory_text>\'a SI_tagged_domain\ types, i.e. a polymorphic family of values + tagged with values from \<^theory_text>\SI_domain\. 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 + \ -subsection \ Data-level Units \ +section\The Domains of SI types and SI-tagged types\ + +subsection \ The \<^theory_text>\SI_domain\-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 SIUnit = +record SI_domain = Seconds :: int Meters :: int Kilograms :: int @@ -39,21 +54,20 @@ record SIUnit = text \ We define a commutative monoid for SI units. \ -instantiation SIUnit_ext :: (one) one +instantiation SI_domain_ext :: (one) one begin \ \ Here, $1$ is the dimensionless unit \ - definition one_SIUnit_ext :: "'a SIUnit_ext" where - [code_unfold]: - "1 = \ Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0 - , Kelvins = 0, Moles = 0, Candelas = 0, \ = 1 \" +definition one_SI_domain_ext :: "'a SI_domain_ext" + where [code_unfold]: "1 = \ Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0 + , Kelvins = 0, Moles = 0, Candelas = 0, \ = 1 \" instance .. end -instantiation SIUnit_ext :: (times) times +instantiation SI_domain_ext :: (times) times begin \ \ Multiplication is defined by adding together the powers \ - definition times_SIUnit_ext :: "'a SIUnit_ext \ 'a SIUnit_ext \ 'a SIUnit_ext" where - [code_unfold]: +definition times_SI_domain_ext :: "'a SI_domain_ext \ 'a SI_domain_ext \ 'a SI_domain_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 @@ -61,45 +75,49 @@ begin instance .. end -instance SIUnit_ext :: (comm_monoid_mult) comm_monoid_mult +instance SI_domain_ext :: (comm_monoid_mult) comm_monoid_mult proof - fix a b c :: "'a SIUnit_ext" + fix a b c :: "'a SI_domain_ext" show "a * b * c = a * (b * c)" - by (simp add: times_SIUnit_ext_def mult.assoc) + by (simp add: times_SI_domain_ext_def mult.assoc) show "a * b = b * a" - by (simp add: times_SIUnit_ext_def mult.commute) + by (simp add: times_SI_domain_ext_def mult.commute) show "1 * a = a" - by (simp add: times_SIUnit_ext_def one_SIUnit_ext_def) + by (simp add: times_SI_domain_ext_def one_SI_domain_ext_def) qed text \ We also define the inverse and division operations, and an abelian group. \ -instantiation SIUnit_ext :: ("{times,inverse}") inverse +instantiation SI_domain_ext :: ("{times,inverse}") inverse begin - definition inverse_SIUnit_ext :: "'a SIUnit_ext \ 'a SIUnit_ext" where - [code_unfold]: +definition inverse_SI_domain_ext :: "'a SI_domain_ext \ 'a SI_domain_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_SIUnit_ext :: "'a SIUnit_ext \ 'a SIUnit_ext \ 'a SIUnit_ext" where - [code_unfold]: "divide_SIUnit_ext x y = x * (inverse y)" +definition divide_SI_domain_ext :: "'a SI_domain_ext \ 'a SI_domain_ext \ 'a SI_domain_ext" + where [code_unfold]: + "divide_SI_domain_ext x y = x * (inverse y)" instance .. end -instance SIUnit_ext :: (ab_group_mult) ab_group_mult +instance SI_domain_ext :: (ab_group_mult) ab_group_mult proof - fix a b :: "'a SIUnit_ext" + fix a b :: "'a SI_domain_ext" show "inverse a \ a = 1" - by (simp add: inverse_SIUnit_ext_def times_SIUnit_ext_def one_SIUnit_ext_def) + by (simp add: inverse_SI_domain_ext_def times_SI_domain_ext_def one_SI_domain_ext_def) show "a \ inverse b = a div b" - by (simp add: divide_SIUnit_ext_def) + by (simp add: divide_SI_domain_ext_def) qed -record 'a SI = + +subsection \ The \<^theory_text>\SI_tagged_domain\-type and its operations \ + +record 'a SI_tagged_domain = factor :: 'a - unit :: SIUnit + unit :: SI_domain instantiation unit :: comm_monoid_add begin @@ -122,90 +140,175 @@ begin instance .. end -instantiation SI_ext :: (times, times) times +instantiation SI_tagged_domain_ext :: (times, times) times begin - definition "times_SI_ext x y = \ factor = factor x \ factor y, unit = unit x \ unit y, \ = more x \ more y \" + definition "times_SI_tagged_domain_ext x y = \ factor = factor x \ factor y, unit = unit x \ unit y, \ = more x \ more y \" instance .. end -instantiation SI_ext :: (zero, zero) zero +instantiation SI_tagged_domain_ext :: (zero, zero) zero begin - definition "zero_SI_ext = \ factor = 0, unit = 1, \ = 0 \" + definition "zero_SI_tagged_domain_ext = \ factor = 0, unit = 1, \ = 0 \" instance .. end -instantiation SI_ext :: (one, one) one +instantiation SI_tagged_domain_ext :: (one, one) one begin - definition "one_SI_ext = \ factor = 1, unit = 1, \ = 1 \" + definition "one_SI_tagged_domain_ext = \ factor = 1, unit = 1, \ = 1 \" instance .. end -instantiation SI_ext :: (inverse, inverse) inverse +instantiation SI_tagged_domain_ext :: (inverse, inverse) inverse begin - definition "inverse_SI_ext x = \ factor = inverse (factor x), unit = inverse (unit x), \ = inverse (more x) \" - definition "divide_SI_ext x y = \ factor = factor x / factor y, unit = unit x / unit y, \ = more x / more y \" + definition "inverse_SI_tagged_domain_ext x = \ factor = inverse (factor x), unit = inverse (unit x), \ = inverse (more x) \" + definition "divide_SI_tagged_domain_ext x y = \ factor = factor x / factor y, unit = unit x / unit y, \ = more x / more y \" instance .. end -instance SI_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult - by (intro_classes, simp_all add: one_SI_ext_def times_SI_ext_def mult.assoc, simp add: mult.commute) +instance SI_tagged_domain_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult + by (intro_classes, simp_all add: one_SI_tagged_domain_ext_def + times_SI_tagged_domain_ext_def mult.assoc, simp add: mult.commute) -text \ A base unit is an SI unit here precisely one unit has power 1. \ +text \ A base unit is an SI_tagged_domain unit here precisely one unit has power 1. \ -definition is_BaseUnit :: "SIUnit \ bool" where +definition is_BaseUnit :: "SI_domain \ 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\)" -subsection \ Type-level Units \ -subsubsection \ Classes \ +section\The Syntax and Semantics of SI types and SI-tagged types\ -text \ A type class for unit denoting types. A type-level unit is a singleton type that associates - with an value-level SI unit. \ +subsection \ Basic SI-types \ -class siunit = finite + - fixes siunit_of :: "'a itself \ SIUnit" +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 SI_domain}. \ + +subsubsection \ SI-type expression definition as type-class \ + +class si_type = finite + + fixes si_sem :: "'a itself \ SI_domain" assumes unitary_unit_pres: "card (UNIV::'a set) = 1" syntax "_SI" :: "type \ logic" ("SI'(_')") translations - "SI('a)" == "CONST siunit_of TYPE('a)" + "SI('a)" == "CONST si_sem TYPE('a)" -text \ An SI base unit type has a value-level base unit. \ +text \ The sub-set of basic SI type expressions can be characterized by the following +operation: \ -class sibaseunit = siunit + +class si_baseunit = si_type + assumes is_BaseUnit: "is_BaseUnit SI('a)" -subsubsection \ Arithmetic \ +subsubsection \ SI base type constructors \ -text \ We define multiplication at the SI type level \ +text\We embed the basic SI types into the SI type expressions: \ +declare [[show_sorts]] -typedef ('a::siunit, 'b::siunit) UnitTimes (infixl "\" 69) = "UNIV :: unit set" .. +instantiation meter :: si_baseunit +begin + definition si_sem_meter :: "meter itself \ SI_domain" 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 \ SI_domain" 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 \ SI_domain" 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 \ SI_domain" 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 \ SI_domain" 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 \ SI_domain" 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 \ SI_domain" 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 [simp] : "is_BaseUnit SI(meter)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(kilogram)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(second)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(ampere)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(kelvin)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(mole)" by(simp add: Units.si_baseunit_class.is_BaseUnit) +lemma [simp] : "is_BaseUnit SI(candela)" by(simp add: Units.si_baseunit_class.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 :: (siunit, siunit) siunit +instantiation UnitTimes :: (si_type, si_type) si_type begin - definition siunit_of_UnitTimes :: "('a \ 'b) itself \ SIUnit" where - "siunit_of_UnitTimes x = SI('a) * SI('b)" - instance by (intro_classes, simp_all add: siunit_of_UnitTimes_def, (transfer, simp)+) + definition si_sem_UnitTimes :: "('a \ 'b) itself \ SI_domain" 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 :: (siunit) siunit +instantiation UnitInv :: (si_type) si_type begin - definition siunit_of_UnitInv :: "('a\<^sup>-\<^sup>1) itself \ SIUnit" where - "siunit_of_UnitInv x = inverse SI('a)" - instance by (intro_classes, simp_all add: siunit_of_UnitInv_def, (transfer, simp)+) + definition si_sem_UnitInv :: "('a\<^sup>-\<^sup>1) itself \ SI_domain" 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) @@ -213,6 +316,8 @@ 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" @@ -233,74 +338,32 @@ print_translation \ _ => raise Match)] \ -subsubsection \ SI base type constructors \ -declare [[show_sorts]] -typedef meter = "UNIV :: unit set" .. setup_lifting type_definition_meter -instantiation meter :: sibaseunit -begin - definition siunit_of_meter :: "meter itself \ SIUnit" where "siunit_of_meter x = 1\Meters := 1\" -instance by (intro_classes, auto simp add: siunit_of_meter_def is_BaseUnit_def, (transfer, simp)+) -end +subsection \ SI Tagged Types \ +text\We 'lift' SI type expressions to SI tagged type expressions as follows:\ -typedef kilogram = "UNIV :: unit set" .. setup_lifting type_definition_kilogram -instantiation kilogram :: sibaseunit -begin - definition siunit_of_kilogram :: "kilogram itself \ SIUnit" where "siunit_of_kilogram x = 1\Kilograms := 1\" -instance by (intro_classes, auto simp add: siunit_of_kilogram_def is_BaseUnit_def, (transfer, simp)+) -end - -typedef second = "UNIV :: unit set" .. setup_lifting type_definition_second -instantiation second :: sibaseunit -begin - definition siunit_of_second :: "second itself \ SIUnit" where "siunit_of_second x = 1\Seconds := 1\" -instance by (intro_classes, auto simp add: siunit_of_second_def is_BaseUnit_def, (transfer, simp)+) -end - -typedef ampere = "UNIV :: unit set" .. setup_lifting type_definition_ampere -instantiation ampere :: sibaseunit -begin - definition siunit_of_ampere :: "ampere itself \ SIUnit" where "siunit_of_ampere x = 1\Amperes := 1\" -instance by (intro_classes, auto simp add: siunit_of_ampere_def is_BaseUnit_def, (transfer, simp)+) -end - -typedef kelvin = "UNIV :: unit set" .. setup_lifting type_definition_kelvin -instantiation kelvin :: sibaseunit -begin - definition siunit_of_kelvin :: "kelvin itself \ SIUnit" where "siunit_of_kelvin x = 1\Kelvins := 1\" -instance by (intro_classes, auto simp add: siunit_of_kelvin_def is_BaseUnit_def, (transfer, simp)+) -end - -typedef mole = "UNIV :: unit set" .. setup_lifting type_definition_mole -instantiation mole :: sibaseunit -begin - definition siunit_of_mole :: "mole itself \ SIUnit" where "siunit_of_mole x = 1\Moles := 1\" -instance by (intro_classes, auto simp add: siunit_of_mole_def is_BaseUnit_def, (transfer, simp)+) -end - -typedef candela = "UNIV :: unit set" .. setup_lifting type_definition_candela -instantiation candela :: sibaseunit -begin - definition siunit_of_candela :: "candela itself \ SIUnit" where "siunit_of_candela x = 1\Candelas := 1\" -instance by (intro_classes, auto simp add: siunit_of_candela_def is_BaseUnit_def, (transfer, simp)+) -end - -subsection \ SI tagged types \ - -typedef (overloaded) ('n, 'u::siunit) Unit ("_[_]" [999,0] 999) = "{x :: 'n SI. unit x = SI('u)}" +typedef (overloaded) ('n, 'u::si_type) Unit ("_[_]" [999,0] 999) + = "{x :: 'n SI_tagged_domain. unit x = SI('u)}" morphisms fromUnit toUnit by (rule_tac x="\ factor = undefined, unit = SI('u) \" in exI, simp) text \ Coerce values when their units are equivalent \ -definition coerceUnit :: "'u\<^sub>2 itself \ 'a['u\<^sub>1::siunit] \ 'a['u\<^sub>2::siunit]" where -"coerceUnit t x = (if SI('u\<^sub>1) = SI('u\<^sub>2) then toUnit (fromUnit x) else undefined)" +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. \ -definition Unit_equiv :: "'n['a::siunit] \ 'n['b::siunit] \ bool" (infix "\\<^sub>U" 50) where +definition Unit_equiv :: "'n['a::si_type] \ 'n['b::si_type] \ bool" (infix "\\<^sub>U" 50) where "a \\<^sub>U b \ fromUnit a = fromUnit b" +text\This gives us an equivalence, but, unfortunately, not a congruence.\ + lemma Unit_equiv_refl [simp]: "a \\<^sub>U a" by (simp add: Unit_equiv_def) @@ -310,24 +373,54 @@ lemma Unit_equiv_sym: "a \\<^sub>U b \ b \\<^sub lemma Unit_equiv_trans: "\ a \\<^sub>U b; b \\<^sub>U c \ \ a \\<^sub>U c" by (simp add: Unit_equiv_def) +(* the following series of equivalent statements ... *) + lemma coerceUnit_eq_iff: - fixes x :: "'a['u\<^sub>1::siunit]" - assumes "SI('u\<^sub>1) = SI('u\<^sub>2::siunit)" + 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>U x" by (metis Unit_equiv_def assms coerceUnit_def fromUnit toUnit_inverse) +(* or equivalently *) + +lemma coerceUnit_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>U y" + by (metis Unit_equiv_def assms coerceUnit_def fromUnit toUnit_inverse) + +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>U y" + by (metis Unit_equiv_def assms fromUnit toUnit_inverse) + +text\This is more general that \y = x \ x \\<^sub>U 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>U y" + shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" + by (metis (full_types) Unit_equiv_def assms fromUnit mem_Collect_eq) + + +subsection\Operations on SI-tagged types\ + setup_lifting type_definition_Unit lift_definition - Unit_times :: "('n::times)['a::siunit] \ 'n['b::siunit] \ 'n['a\'b]" (infixl "*\<^sub>U" 69) is "(*)" - by (simp add: siunit_of_UnitTimes_def times_SI_ext_def) + Unit_times :: "('n::times)['a::si_type] \ 'n['b::si_type] \ 'n['a \'b]" (infixl "*\<^sub>U" 69) is "(*)" + by (simp add: si_sem_UnitTimes_def times_SI_tagged_domain_ext_def) lift_definition - Unit_inverse :: "('n::inverse)['a::siunit] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) is "inverse" - by (simp add: inverse_SI_ext_def siunit_of_UnitInv_def) + Unit_inverse :: "('n::inverse)['a::si_type] \ 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\)" [999] 999) is "inverse" + by (simp add: inverse_SI_tagged_domain_ext_def si_sem_UnitInv_def) abbreviation - Unit_divide :: "('n::{times,inverse})['a::siunit] \ 'n['b::siunit] \ 'n['a/'b]" (infixl "'/\<^sub>U" 70) where + Unit_divide :: "('n::{times,inverse})['a::si_type] \ 'n['b::si_type] \ 'n['a/'b]" (infixl "'/\<^sub>U" 70) where "Unit_divide x y \ x *\<^sub>U y\<^sup>-\<^sup>\" abbreviation Unit_sq ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ \ u *\<^sub>U u" @@ -336,21 +429,21 @@ abbreviation Unit_cube ("(_)\<^sup>\" [999] 999) where "u\<^sup>\ abbreviation Unit_neq_sq ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" abbreviation Unit_neq_cube ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>-\<^sup>\ \ (u\<^sup>\)\<^sup>-\<^sup>\" -instantiation Unit :: (zero,siunit) zero +instantiation Unit :: (zero,si_type) zero begin lift_definition zero_Unit :: "('a, 'b) Unit" is "\ factor = 0, unit = SI('b) \" by simp instance .. end -instantiation Unit :: (one,siunit) one +instantiation Unit :: (one,si_type) one begin lift_definition one_Unit :: "('a, 'b) Unit" is "\ factor = 1, unit = SI('b) \" by simp instance .. end -instantiation Unit :: (plus,siunit) plus +instantiation Unit :: (plus,si_type) plus begin lift_definition plus_Unit :: "'a['b] \ 'a['b] \ 'a['b]" is "\ x y. \ factor = factor x + factor y, unit = SI('b) \" @@ -358,26 +451,26 @@ lift_definition plus_Unit :: "'a['b] \ 'a['b] \ 'a['b]" instance .. end -instance Unit :: (semigroup_add,siunit) semigroup_add +instance Unit :: (semigroup_add,si_type) semigroup_add by (intro_classes, transfer, simp add: add.assoc) -instance Unit :: (ab_semigroup_add,siunit) ab_semigroup_add +instance Unit :: (ab_semigroup_add,si_type) ab_semigroup_add by (intro_classes, transfer, simp add: add.commute) -instance Unit :: (monoid_add,siunit) monoid_add +instance Unit :: (monoid_add,si_type) monoid_add by (intro_classes; (transfer, simp)) -instance Unit :: (comm_monoid_add,siunit) comm_monoid_add +instance Unit :: (comm_monoid_add,si_type) comm_monoid_add by (intro_classes; transfer, simp) -instantiation Unit :: (uminus,siunit) uminus +instantiation Unit :: (uminus,si_type) uminus begin lift_definition uminus_Unit :: "'a['b] \ 'a['b]" is "\ x. \ factor = - factor x, unit = unit x \" by (simp) instance .. end -instantiation Unit :: (minus,siunit) minus +instantiation Unit :: (minus,si_type) minus begin lift_definition minus_Unit :: "'a['b] \ 'a['b] \ 'a['b]" is "\ x y. \ factor = factor x - factor y, unit = unit x \" by (simp) @@ -385,9 +478,9 @@ lift_definition minus_Unit :: "'a['b] \ 'a['b] \ 'a['b]" instance .. end -instance Unit :: (numeral,siunit) numeral .. +instance Unit :: (numeral,si_type) numeral .. -instantiation Unit :: (times,siunit) times +instantiation Unit :: (times,si_type) times begin lift_definition times_Unit :: "'a['b] \ 'a['b] \ 'a['b]" is "\ x y. \ factor = factor x * factor y, unit = SI('b) \" @@ -395,66 +488,73 @@ lift_definition times_Unit :: "'a['b] \ 'a['b] \ 'a['b]" instance .. end -instance Unit :: (power,siunit) power .. +instance Unit :: (power,si_type) power .. -instance Unit :: (semigroup_mult,siunit) semigroup_mult +instance Unit :: (semigroup_mult,si_type) semigroup_mult by (intro_classes, transfer, simp add: mult.assoc) -instance Unit :: (ab_semigroup_mult,siunit) ab_semigroup_mult +instance Unit :: (ab_semigroup_mult,si_type) ab_semigroup_mult by (intro_classes, (transfer, simp add: mult.commute)) -instance Unit :: (comm_semiring,siunit) comm_semiring +instance Unit :: (comm_semiring,si_type) comm_semiring by (intro_classes, transfer, simp add: linordered_field_class.sign_simps(18) mult.commute) -instance Unit :: (comm_semiring_0,siunit) comm_semiring_0 +instance Unit :: (comm_semiring_0,si_type) comm_semiring_0 by (intro_classes, (transfer, simp)+) -instance Unit :: (comm_monoid_mult,siunit) comm_monoid_mult +instance Unit :: (comm_monoid_mult,si_type) comm_monoid_mult by (intro_classes, (transfer, simp add: mult.commute)+) -instance Unit :: (comm_semiring_1,siunit) comm_semiring_1 +instance Unit :: (comm_semiring_1,si_type) comm_semiring_1 by (intro_classes; (transfer, simp add: semiring_normalization_rules(1-8,24))) -instantiation Unit :: (divide,siunit) divide +instantiation Unit :: (divide,si_type) divide begin lift_definition divide_Unit :: "'a['b] \ 'a['b] \ 'a['b]" is "\ x y. \ factor = factor x div factor y, unit = SI('b) \" by simp instance .. end -instantiation Unit :: (inverse,siunit) inverse +instantiation Unit :: (inverse,si_type) inverse begin lift_definition inverse_Unit :: "'a['b] \ 'a['b]" is "\ x. \ factor = inverse (factor x), unit = SI('b) \" by simp instance .. end -instantiation Unit :: (order,siunit) order +instantiation Unit :: (order,si_type) order begin lift_definition less_eq_Unit :: "'a['b] \ 'a['b] \ bool" is "\ x y. factor x \ factor y" . lift_definition less_Unit :: "'a['b] \ 'a['b] \ bool" is "\ x y. factor x < factor y" . instance by (intro_classes, (transfer, simp add: less_le_not_le)+) end -lift_definition mk_unit :: "'a \ 'u itself \ ('a::one)['u::siunit]" +lift_definition mk_unit :: "'a \ 'u itself \ ('a::one)['u::si_type]" is "\ n u. \ factor = 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]: "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)" +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)" -definition factorUnit :: "'a['u::siunit] \ 'a" ("\_\\<^sub>U") where +subsubsection \The Projection: Stripping the SI-Tags \ + +definition factorUnit :: "'a['u::si_type] \ 'a" ("\_\\<^sub>U") where "factorUnit x = factor (fromUnit x)" + +subsubsection \More Operations \ + lemma unit_eq_iff_factor_eq: "x = y \ \x\\<^sub>U = \y\\<^sub>U" by (auto simp add: factorUnit_def, transfer, simp) @@ -484,15 +584,15 @@ lemma factorUnit_numeral [si_def]: "\numeral n\\<^sub>U = numera apply (metis factorUnit_one factorUnit_plus numeral_code(3)) done -lemma factorUnit_mk [si_def]: "\UNIT(n, 'u::siunit)\\<^sub>U = n" +lemma factorUnit_mk [si_def]: "\UNIT(n, 'u::si_type)\\<^sub>U = n" by (simp add: factorUnit_def, transfer, simp) method si_calc = (simp add: unit_eq_iff_factor_eq unit_le_iff_factor_le si_def) -subsubsection \ Derived Units \ +section \ Some Derived Units \ -definition "radian = 1 \ (meter *\<^sub>U meter\<^sup>-\<^sup>\)" +definition "radian = 1 \ (meter *\<^sub>U meter\<^sup>-\<^sup>\)" definition degree :: "real[meter / meter]" where [si_def]: "degree = (2\(UNIT(pi,_)) / 180)\radian" @@ -505,14 +605,122 @@ definition [si_def]: "pint = 0.56826125 \ litre" definition [si_def]: "milli = UNIT(0.001, _)" -definition [si_def]: "centi = UNIT(0.01, _)" - definition [si_def]: "kilo = UNIT(1000, _)" +definition [si_def]: "hour = 3600 \ second" + abbreviation "tonne \ kilo\kilogram" abbreviation "newton \ (kilogram *\<^sub>U meter) /\<^sub>U second\<^sup>\" abbreviation "volt \ kilogram *\<^sub>U meter\<^sup>\ *\<^sub>U second\<^sup>-\<^sup>\ *\<^sub>U ampere\<^sup>-\<^sup>\" +abbreviation "watt \ kilogram *\<^sub>U meter\<^sup>\ *\<^sub>U second\<^sup>-\<^sup>\" + +abbreviation "joule \ kilogram *\<^sub>U meter\<^sup>\ *\<^sub>U second\<^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]" + +section \ Tactic Support for SI type expressions. \ + +lemmas [si_def] = Units.si_sem_meter_def Units.si_sem_kilogram_def Units.si_sem_second_def + Units.si_sem_ampere_def Units.si_sem_kelvin_def Units.si_sem_mole_def + Units.si_sem_candela_def + + si_sem_UnitTimes_def si_sem_UnitInv_def + times_SI_domain_ext_def one_SI_domain_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) = + \factor = x, + unit = \Seconds = 1, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_second_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, meter) = + \factor = x, + unit = \Seconds = 0, Meters = 1, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_meter_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, kilogram) = + \factor = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 1, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_kilogram_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, ampere) = + \factor = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 1, + Kelvins = 0, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_ampere_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, kelvin) = + \factor = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 1, Moles = 0, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_kelvin_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, mole) = + \factor = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 1, Candelas = 0\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_mole_def) + +lemma [si_def]:"fromUnit UNIT(x::'a::one, candela) = + \factor = x, + unit = \Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0, + Kelvins = 0, Moles = 0, Candelas = 1\\" + by (simp add: mk_unit.rep_eq one_SI_domain_ext_def si_sem_candela_def) + + + + +lemma Unit_times_commute: + "((X::'a::{one,ab_semigroup_mult}['b::si_type]) *\<^sub>U (Y::'a['c::si_type])) \\<^sub>U (Y *\<^sub>U X)" + unfolding Unit_equiv_def + by (simp add: Unit_times.rep_eq linordered_field_class.sign_simps(5) times_SI_tagged_domain_ext_def) + + +(* just a check that instantiation works for special cases ... *) +lemma " (UNIT(x, candela) *\<^sub>U UNIT(y::'a::{one,ab_semigroup_mult}, mole)) + \\<^sub>U (UNIT(y, mole) *\<^sub>U UNIT(x, candela)) " + by(simp add: Unit_times_commute) + + + + + + +lemma "watt *\<^sub>U hour \\<^sub>U 3600 *\<^sub>U joule" + unfolding Unit_equiv_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 "factor(fromUnit(toUnit\factor = X:: 'a :: {inverse,times,numeral}, + unit = SI('b::si_type) \)) = X" + apply(subst Units.Unit.toUnit_inverse,auto) + oops + +lemma "watt *\<^sub>U hour \\<^sub>U 3.6 *\<^sub>U kilo *\<^sub>U joule" + oops + end