diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index c725955..4aafe7a 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -59,6 +59,8 @@ abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where abbreviation luminous_efficacy :: "'a[J \ (L\<^sup>2 \ L\<^sup>-\<^sup>2) \ (M \ L\<^sup>2 \ T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" ("K\<^sub>c\<^sub>d") where "luminous_efficacy \ 683 \ (lumen\<^bold>/watt)" +subsection \ Basis Theorems \ + theorem second_definition: "1 \ second \\<^sub>Q (9192631770 \ \) \<^bold>/ \v\<^sub>C\<^sub>s" by si_calc @@ -68,8 +70,11 @@ theorem meter_definition: "1 \ meter \\<^sub>Q (9192631770 / 299792458) \ (\<^bold>c \<^bold>/ \v\<^sub>C\<^sub>s)" by si_calc+ -abbreviation gravitational_constant :: "'a[L\<^sup>3 \ M\<^sup>-\<^sup>1 \ T\<^sup>-\<^sup>2]" where - "gravitational_constant \ (6.6743015 \ 1/(10 ^ 11)) \ (meter\<^sup>\\<^bold>\kilogram\<^sup>-\<^sup>\\<^bold>\second\<^sup>-\<^sup>\)" +theorem kilogram_definition: + "1 \ kilogram \\<^sub>Q (\<^bold>h \<^bold>/ (6.62607015 \ 1/(10^34) \ \))\<^bold>\meter\<^sup>-\<^sup>\\<^bold>\second" + by si_calc + +abbreviation "approx_ice_point \ 273.15 \ kelvin" default_sort type diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index a45183e..4203faa 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -20,12 +20,22 @@ abbreviation "siemens \ kilogram\<^sup>-\<^sup>\ \<^bold>\ met abbreviation "weber \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" -abbreviation "tesla \ kilogram \<^bold>\ meter\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" +abbreviation "tesla \ kilogram \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" abbreviation "henry \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" +abbreviation "lux \ candela \<^bold>\ steradian \<^bold>\ meter\<^sup>-\<^sup>\" + +abbreviation (input) "becquerel \ second\<^sup>-\<^sup>\" + +abbreviation "gray \ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +abbreviation "sievert \ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" + +abbreviation "katal \ mole \<^bold>\ second\<^sup>-\<^sup>\" + definition degrees_celcius :: "'a::field_char_0 \ 'a[\]" ("_\C" [999] 999) - where [si_eq]: "degrees_celcius x = x + 273.151 \ kelvin" + where [si_eq]: "degrees_celcius x = (x \ kelvin) + approx_ice_point" definition [si_eq]: "gram = milli \ kilogram" @@ -33,9 +43,50 @@ 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[L] \ (real\<^sup>3[L \ T\<^sup>-\<^sup>2])" +subsection \ Equivalences \ + +lemma joule_alt_def: "joule \\<^sub>Q newton \<^bold>\ meter" + by si_calc + +lemma watt_alt_def: "watt \\<^sub>Q joule \<^bold>/ second" + by si_calc + +lemma volt_alt_def: "volt = watt \<^bold>/ ampere" + by simp + +lemma farad_alt_def: "farad \\<^sub>Q coulomb \<^bold>/ volt" + by si_calc + +lemma ohm_alt_def: "ohm \\<^sub>Q volt \<^bold>/ ampere" + by si_calc + +lemma siemens_alt_def: "siemens \\<^sub>Q ampere \<^bold>/ volt" + by si_calc + +lemma weber_alt_def: "weber \\<^sub>Q volt \<^bold>\ second" + by si_calc + +lemma tesla_alt_def: "tesla \\<^sub>Q weber \<^bold>/ meter\<^sup>\" + by si_calc + +lemma henry_alt_def: "henry \\<^sub>Q weber \<^bold>/ ampere" + by si_calc + +lemma lux_alt_def: "lux = lumen \<^bold>/ meter\<^sup>\" + by simp + +lemma gray_alt_def: "gray \\<^sub>Q joule \<^bold>/ kilogram" + by si_calc + +lemma sievert_alt_def: "sievert \\<^sub>Q joule \<^bold>/ kilogram" + by si_calc + subsection \ Properties \ lemma kilogram: "kilo \ gram = kilogram" by (si_simp) +lemma celcius_to_kelvin: "T\C = (T \ kelvin) + (273.15 \ kelvin)" + by (si_simp) + end \ No newline at end of file diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy index a53ce1e..5a1976b 100644 --- a/src/SI/SI_Prefix.thy +++ b/src/SI/SI_Prefix.thy @@ -4,6 +4,8 @@ theory SI_Prefix imports SI_Constants begin +subsection \ Definitions \ + default_sort ring_char_0 definition deca :: "'a" where [si_eq]: "deca = 10^1" @@ -20,6 +22,12 @@ definition tera :: "'a" where [si_eq]: "tera = 10^12" definition peta :: "'a" where [si_eq]: "peta = 10^15" +definition exa :: "'a" where [si_eq]: "exa = 10^18" + +definition zetta :: "'a" where [si_eq]: "zetta = 10^21" + +definition yotta :: "'a" where [si_eq]: "yotta = 10^24" + default_sort field_char_0 definition deci :: "'a" where [si_eq]: "deci = 1/10^1" @@ -32,6 +40,21 @@ definition micro :: "'a" where [si_eq]: "micro = 1/10^6" definition nano :: "'a" where [si_eq]: "nano = 1/10^9" +definition pico :: "'a" where [si_eq]: "pico = 1/10^12" + +definition femto :: "'a" where [si_eq]: "femto = 1/10^15" + +definition atto :: "'a" where [si_eq]: "atto = 1/10^18" + +definition zepto :: "'a" where [si_eq]: "zepto = 1/10^21" + +definition yocto :: "'a" where [si_eq]: "yocto = 1/10^24" + default_sort type +subsection \ Examples \ + +lemma "2.3 \ (centi \ meter)\<^sup>\ \\<^sub>Q 2.3 \ 1/10^6 \ meter\<^sup>\" + by (si_simp) + end \ No newline at end of file diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy index c558fca..b26ef50 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/SI_Proof.thy @@ -6,63 +6,63 @@ begin named_theorems si_transfer -definition magnQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where -[si_def]: "magnQuant x = magn (fromQ x)" +definition magQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where +[si_def]: "magQuant x = mag (fromQ x)" -lemma unit_eq_iff_magn_eq [si_transfer]: +lemma unit_eq_iff_mag_eq [si_transfer]: "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" - by (auto simp add: magnQuant_def, transfer, simp) + by (auto simp add: magQuant_def, transfer, simp) lemma unit_equiv_iff [si_transfer]: fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]" shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ SI('u\<^sub>1) = SI('u\<^sub>2)" proof - - have "\t ta. (ta::'a['u\<^sub>2]) = t \ magn (fromQ ta) \ magn (fromQ t)" - by (simp add: magnQuant_def unit_eq_iff_magn_eq) + have "\t ta. (ta::'a['u\<^sub>2]) = t \ mag (fromQ ta) \ mag (fromQ t)" + by (simp add: magQuant_def unit_eq_iff_mag_eq) then show ?thesis - by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def) + by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 qeq magQuant_def) qed lemma unit_le_iff_magn_le [si_transfer]: "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" - by (auto simp add: magnQuant_def; (transfer, simp)) + by (auto simp add: magQuant_def; (transfer, simp)) -lemma magnQuant_zero [si_eq]: "\0\\<^sub>Q = 0" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_zero [si_eq]: "\0\\<^sub>Q = 0" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_one [si_eq]: "\1\\<^sub>Q = 1" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_one [si_eq]: "\1\\<^sub>Q = 1" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_plus [si_eq]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_plus [si_eq]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_minus [si_eq]: "\x - y\\<^sub>Q = \x\\<^sub>Q - \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_minus [si_eq]: "\x - y\\<^sub>Q = \x\\<^sub>Q - \y\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_uminus [si_eq]: "\- x\\<^sub>Q = - \x\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_uminus [si_eq]: "\- x\\<^sub>Q = - \x\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_scaleQ [si_eq]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_scaleQ [si_eq]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_qtimes [si_eq]: "\x \<^bold>\ y\\<^sub>Q = \x\\<^sub>Q \ \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_qtimes [si_eq]: "\x \<^bold>\ y\\<^sub>Q = \x\\<^sub>Q \ \y\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_qinverse [si_eq]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_qinverse [si_eq]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp) -lemma magnQuant_qdivivide [si_eq]: "\(x::('a::field)[_]) \<^bold>/ y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp add: field_class.field_divide_inverse) +lemma magQuant_qdivivide [si_eq]: "\(x::('a::field)[_]) \<^bold>/ y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" + by (simp add: magQuant_def, transfer, simp add: field_class.field_divide_inverse) -lemma magnQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n" +lemma magQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral n" apply (induct n, simp_all add: si_def) - apply (metis magnQuant_def magnQuant_one) - apply (metis magnQuant_def magnQuant_plus numeral_code(2)) - apply (metis magnQuant_def magnQuant_one magnQuant_plus numeral_code(3)) + apply (metis magQuant_def magQuant_one) + apply (metis magQuant_def magQuant_plus numeral_code(2)) + apply (metis magQuant_def magQuant_one magQuant_plus numeral_code(3)) done -lemma magnQuant_mk [si_eq]: "\UNIT('u::si_type)\\<^sub>Q = 1" - by (simp add: magnQuant_def, transfer, simp) +lemma magQuant_mk [si_eq]: "\UNIT('u::si_type)\\<^sub>Q = 1" + by (simp add: magQuant_def, transfer, simp) text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index 8e57cc3..a0ef202 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -1,72 +1,71 @@ section \ SI Quantities \ theory SI_Quantities - imports SI_Units (* Optics.Lenses *) + 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 \ + mag :: 'a \ \ Magnitude of the quantity \ + dim :: Dimension \ \ Dimension of the quantity \ lemma Quantity_eq_intro: - assumes "magn x = magn y" "unit x = unit y" "more x = more y" + assumes "mag x = mag y" "dim x = dim y" "more x = more y" shows "x = y" by (simp add: assms) instantiation Quantity_ext :: (times, times) times begin definition [si_def]: - "times_Quantity_ext x y = \ magn = magn x \ magn y, unit = unit x \ unit y, \ = more x \ more y \" + "times_Quantity_ext x y = \ mag = mag x \ mag y, dim = dim x \ dim y, \ = more x \ more y \" instance .. end -lemma magn_times [simp]: "magn (x \ y) = magn x \ magn y" by (simp add: times_Quantity_ext_def) -lemma unit_times [simp]: "unit (x \ y) = unit x \ unit y" by (simp add: times_Quantity_ext_def) +lemma mag_times [simp]: "mag (x \ y) = mag x \ mag y" by (simp add: times_Quantity_ext_def) +lemma dim_times [simp]: "dim (x \ y) = dim x \ dim y" by (simp add: times_Quantity_ext_def) lemma more_times [simp]: "more (x \ y) = more x \ more y" by (simp add: times_Quantity_ext_def) instantiation Quantity_ext :: (zero, zero) zero begin - definition "zero_Quantity_ext = \ magn = 0, unit = 1, \ = 0 \" + definition "zero_Quantity_ext = \ mag = 0, dim = 1, \ = 0 \" instance .. end -lemma magn_zero [simp]: "magn 0 = 0" by (simp add: zero_Quantity_ext_def) -lemma unit_zero [simp]: "unit 0 = 1" by (simp add: zero_Quantity_ext_def) +lemma mag_zero [simp]: "mag 0 = 0" by (simp add: zero_Quantity_ext_def) +lemma dim_zero [simp]: "dim 0 = 1" by (simp add: zero_Quantity_ext_def) lemma more_zero [simp]: "more 0 = 0" by (simp add: zero_Quantity_ext_def) instantiation Quantity_ext :: (one, one) one begin - definition [si_def]: "one_Quantity_ext = \ magn = 1, unit = 1, \ = 1 \" + definition [si_def]: "one_Quantity_ext = \ mag = 1, dim = 1, \ = 1 \" instance .. end -lemma magn_one [simp]: "magn 1 = 1" by (simp add: one_Quantity_ext_def) -lemma unit_one [simp]: "unit 1 = 1" by (simp add: one_Quantity_ext_def) +lemma mag_one [simp]: "mag 1 = 1" by (simp add: one_Quantity_ext_def) +lemma dim_one [simp]: "dim 1 = 1" by (simp add: one_Quantity_ext_def) lemma more_one [simp]: "more 1 = 1" by (simp add: one_Quantity_ext_def) instantiation Quantity_ext :: (inverse, inverse) inverse begin - definition [si_def]: "inverse_Quantity_ext x = \ magn = inverse (magn x), unit = inverse (unit x), \ = inverse (more x) \" - definition [si_def]: "divide_Quantity_ext x y = \ magn = magn x / magn y, unit = unit x / unit y, \ = more x / more y \" + definition [si_def]: "inverse_Quantity_ext x = \ mag = inverse (mag x), dim = inverse (dim x), \ = inverse (more x) \" + definition [si_def]: "divide_Quantity_ext x y = \ mag = mag x / mag y, dim = dim x / dim y, \ = more x / more y \" instance .. end -lemma magn_inverse [simp]: "magn (inverse x) = inverse (magn x)" +lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)" by (simp add: inverse_Quantity_ext_def) -lemma unit_inverse [simp]: "unit (inverse x) = inverse (unit x)" +lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)" by (simp add: inverse_Quantity_ext_def) lemma more_inverse [simp]: "more (inverse x) = inverse (more x)" by (simp add: inverse_Quantity_ext_def) -lemma magn_divide [simp]: "magn (x / y) = magn x / magn y" +lemma mag_divide [simp]: "mag (x / y) = mag x / mag y" by (simp add: divide_Quantity_ext_def) -lemma unit_divide [simp]: "unit (x / y) = unit x / unit y" +lemma dim_divide [simp]: "dim (x / y) = dim x / dim y" by (simp add: divide_Quantity_ext_def) lemma more_divide [simp]: "more (x / y) = more x / more y" @@ -82,7 +81,7 @@ instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult instantiation Quantity_ext :: (ord, ord) ord begin definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \ ('a, 'b) Quantity_scheme \ bool" - where "less_eq_Quantity_ext x y = (magn x \ magn y \ unit x = unit y \ more x \ more y)" + where "less_eq_Quantity_ext x y = (mag x \ mag y \ dim x = dim y \ more x \ more y)" definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \ ('a, 'b) Quantity_scheme \ bool" where "less_Quantity_ext x y = (x \ y \ \ y \ x)" @@ -97,12 +96,12 @@ 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 fromQ toQ by (rule_tac x="\ magn = undefined, unit = SI('u) \" in exI, simp) + = "{x :: 'n Quantity. dim x = SI('u)}" + morphisms fromQ toQ by (rule_tac x="\ mag = undefined, dim = SI('u) \" in exI, simp) setup_lifting type_definition_tQuant -text \ Coerce values when their units are equivalent \ +text \ Coerce values when their dimensions 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 = (toQ (fromQ x))" @@ -111,7 +110,7 @@ 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. \ +text \ Two SI types are equivalent if they have the same value-level dimensions. \ lift_definition qless_eq :: "'n::order['a::si_type] \ 'n['b::si_type] \ bool" (infix "\\<^sub>Q" 50) is "(\)" . @@ -159,9 +158,7 @@ lemma updown_eq_iff: text\This is more general that \y = x \ x \\<^sub>Q y\, since x and y may have different type.\ -find_theorems "(toQ (fromQ _))" - -lemma eq_ : +lemma qeq: 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)" @@ -171,11 +168,11 @@ subsection\Operations on SI-tagged types\ lift_definition qtimes :: "('n::comm_ring_1)['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) + by (simp add: si_sem_DimTimes_def times_Quantity_ext_def) lift_definition qinverse :: "('n::field)['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) + by (simp add: inverse_Quantity_ext_def si_sem_DimInv_def) abbreviation qdivide :: "('n::field)['a::si_type] \ 'n['b::si_type] \ 'n['a/'b]" (infixl "\<^bold>'/" 70) where @@ -191,14 +188,14 @@ abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\" [999] 999) where "u\<^sup>- instantiation tQuant :: (zero,si_type) zero begin -lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\ magn = 0, unit = SI('b) \" +lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\ mag = 0, dim = 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) \" +lift_definition one_tQuant :: "('a, 'b) tQuant" is "\ mag = 1, dim = SI('b) \" by simp instance .. end @@ -206,7 +203,7 @@ 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) \" + is "\ x y. \ mag = mag x + mag y, dim = SI('b) \" by (simp) instance .. end @@ -226,14 +223,14 @@ instance tQuant :: (comm_monoid_add,si_type) comm_monoid_add 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) + is "\ x. \ mag = - mag x, dim = dim 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) + is "\ x y. \ mag = mag x - mag y, dim = dim x \" by (simp) instance .. end @@ -245,18 +242,18 @@ instance tQuant :: (ab_group_add,si_type) ab_group_add 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" . + lift_definition less_eq_tQuant :: "'a['b] \ 'a['b] \ bool" is "\ x y. mag x \ mag y" . + lift_definition less_tQuant :: "'a['b] \ 'a['b] \ bool" is "\ x y. mag x < mag y" . instance by (intro_classes, (transfer, simp add: less_le_not_le)+) end lift_definition scaleQ :: "'a \ 'a::comm_ring_1['u::si_type] \ 'a['u]" (infixr "*\<^sub>Q" 63) - is "\ r x. \ magn = r * magn x, unit = SI('u) \" by simp + is "\ r x. \ mag = r * mag x, dim = SI('u) \" by simp notation scaleQ (infixr "\" 63) lift_definition mk_unit :: "'u itself \ ('a::one)['u::si_type]" - is "\ u. \ magn = 1, unit = SI('u) \" by simp + is "\ u. \ mag = 1, dim = SI('u) \" by simp syntax "_mk_unit" :: "type \ logic" ("UNIT'(_')") translations "UNIT('a)" == "CONST mk_unit TYPE('a)" diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index 47c5880..a296c24 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -47,73 +47,73 @@ subsection \ The \<^theory_text>\Unit\-type and its operation 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 = - Meters :: int - Kilograms :: int - Seconds :: int - Amperes :: int - Kelvins :: int - Moles :: int - Candelas :: int +record Dimension = + Length :: int + Mass :: int + Time :: int + Current :: int + Temperature :: int + Amount :: int + Intensity :: int text \ We define a commutative monoid for SI units. \ -instantiation Unit_ext :: (one) one +instantiation Dimension_ext :: (one) one begin \ \ Here, $1$ is the dimensionless unit \ -definition one_Unit_ext :: "'a Unit_ext" - where [code_unfold, si_def]: "1 = \ Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0 - , Kelvins = 0, Moles = 0, Candelas = 0, \ = 1 \" +definition one_Dimension_ext :: "'a Dimension_ext" + where [code_unfold, si_def]: "1 = \ Length = 0, Mass = 0, Time = 0, Current = 0 + , Temperature = 0, Amount = 0, Intensity = 0, \ = 1 \" instance .. end -instantiation Unit_ext :: (times) times +instantiation Dimension_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" +definition times_Dimension_ext :: "'a Dimension_ext \ 'a Dimension_ext \ 'a Dimension_ext" where [code_unfold, si_def]: - "x * y = \ Meters = Meters x + Meters y, Kilograms = Kilograms x + Kilograms y - , Seconds = Seconds x + Seconds 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 \" + "x * y = \ Length = Length x + Length y, Mass = Mass x + Mass y + , Time = Time x + Time y, Current = Current x + Current y + , Temperature = Temperature x + Temperature y, Amount = Amount x + Amount y + , Intensity = Intensity x + Intensity y, \ = more x * more y \" instance .. end -instance Unit_ext :: (comm_monoid_mult) comm_monoid_mult +instance Dimension_ext :: (comm_monoid_mult) comm_monoid_mult proof - fix a b c :: "'a Unit_ext" + fix a b c :: "'a Dimension_ext" show "a * b * c = a * (b * c)" - by (simp add: times_Unit_ext_def mult.assoc) + by (simp add: times_Dimension_ext_def mult.assoc) show "a * b = b * a" - by (simp add: times_Unit_ext_def mult.commute) + by (simp add: times_Dimension_ext_def mult.commute) show "1 * a = a" - by (simp add: times_Unit_ext_def one_Unit_ext_def) + by (simp add: times_Dimension_ext_def one_Dimension_ext_def) qed text \ We also define the inverse and division operations, and an abelian group. \ -instantiation Unit_ext :: ("{times,inverse}") inverse +instantiation Dimension_ext :: ("{times,inverse}") inverse begin -definition inverse_Unit_ext :: "'a Unit_ext \ 'a Unit_ext" +definition inverse_Dimension_ext :: "'a Dimension_ext \ 'a Dimension_ext" where [code_unfold, si_def]: - "inverse x = \ Meters = - Meters x, Kilograms = - Kilograms x - , Seconds = - Seconds x, Amperes = - Amperes x - , Kelvins = - Kelvins x, Moles = - Moles x - , Candelas = - Candelas x, \ = inverse (more x) \" + "inverse x = \ Length = - Length x, Mass = - Mass x + , Time = - Time x, Current = - Current x + , Temperature = - Temperature x, Amount = - Amount x + , Intensity = - Intensity x, \ = inverse (more x) \" -definition divide_Unit_ext :: "'a Unit_ext \ 'a Unit_ext \ 'a Unit_ext" +definition divide_Dimension_ext :: "'a Dimension_ext \ 'a Dimension_ext \ 'a Dimension_ext" where [code_unfold, si_def]: - "divide_Unit_ext x y = x * (inverse y)" + "divide_Dimension_ext x y = x * (inverse y)" instance .. end -instance Unit_ext :: (ab_group_mult) ab_group_mult +instance Dimension_ext :: (ab_group_mult) ab_group_mult proof - fix a b :: "'a Unit_ext" + fix a b :: "'a Dimension_ext" show "inverse a \ a = 1" - by (simp add: inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def) + by (simp add: inverse_Dimension_ext_def times_Dimension_ext_def one_Dimension_ext_def) show "a \ inverse b = a div b" - by (simp add: divide_Unit_ext_def) + by (simp add: divide_Dimension_ext_def) qed text \ It makes no sense to define a plus operator for SI units because we can only add together @@ -145,10 +145,10 @@ instance unit :: ab_group_mult 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\)" +definition is_BaseDim :: "Dimension \ bool" where +"is_BaseDim u = (\ n. u = 1\Length := n\ \ u = 1\Mass := n\ \ u = 1\Time := n\ + \ u = 1\Current := n\ \ u = 1\Temperature := n\ \ u = 1\Amount := n\ + \ u = 1\Intensity := n\)" section\The Syntax and Semantics of SI types and SI-tagged types\ @@ -193,12 +193,12 @@ 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}. \ +@{typ Dimension}. \ subsubsection \ SI-type expression definition as type-class \ class si_type = finite + - fixes si_sem :: "'a itself \ Unit" + fixes si_sem :: "'a itself \ Dimension" assumes unitary_unit_pres: "card (UNIV::'a set) = 1" syntax @@ -210,135 +210,133 @@ translations 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)" +class si_basedim = si_type + + assumes is_BaseDim: "is_BaseDim SI('a)" subsubsection \ SI base type constructors \ text\We embed the basic SI types into the SI type expressions: \ - -instantiation Length :: si_baseunit +instantiation Length :: si_basedim begin -definition si_sem_Length :: "Length itself \ Unit" - where [si_def]: "si_sem_Length x = 1\Meters := 1\" -instance - by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Length :: "Length itself \ Dimension" + where [si_def]: "si_sem_Length x = 1\Length := 1\" +instance by (intro_classes, auto simp add: si_sem_Length_def is_BaseDim_def, (transfer, simp)+) end -instantiation Mass :: si_baseunit +instantiation Mass :: si_basedim begin -definition si_sem_Mass :: "Mass itself \ Unit" - where [si_def]: "si_sem_Mass x = 1\Kilograms := 1\" -instance by (intro_classes, auto simp add: si_sem_Mass_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Mass :: "Mass itself \ Dimension" + where [si_def]: "si_sem_Mass x = 1\Mass := 1\" +instance by (intro_classes, auto simp add: si_sem_Mass_def is_BaseDim_def, (transfer, simp)+) end -instantiation Time :: si_baseunit +instantiation Time :: si_basedim begin -definition si_sem_Time :: "Time itself \ Unit" - where [si_def]: "si_sem_Time x = 1\Seconds := 1\" -instance by (intro_classes, auto simp add: si_sem_Time_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Time :: "Time itself \ Dimension" + where [si_def]: "si_sem_Time x = 1\Time := 1\" +instance by (intro_classes, auto simp add: si_sem_Time_def is_BaseDim_def, (transfer, simp)+) end -instantiation Current :: si_baseunit +instantiation Current :: si_basedim begin -definition si_sem_Current :: "Current itself \ Unit" - where [si_def]: "si_sem_Current x = 1\Amperes := 1\" -instance by (intro_classes, auto simp add: si_sem_Current_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Current :: "Current itself \ Dimension" + where [si_def]: "si_sem_Current x = 1\Current := 1\" +instance by (intro_classes, auto simp add: si_sem_Current_def is_BaseDim_def, (transfer, simp)+) end -instantiation Temperature :: si_baseunit +instantiation Temperature :: si_basedim begin -definition si_sem_Temperature :: "Temperature itself \ Unit" - where [si_def]: "si_sem_Temperature x = 1\Kelvins := 1\" -instance by (intro_classes, auto simp add: si_sem_Temperature_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Temperature :: "Temperature itself \ Dimension" + where [si_def]: "si_sem_Temperature x = 1\Temperature := 1\" +instance by (intro_classes, auto simp add: si_sem_Temperature_def is_BaseDim_def, (transfer, simp)+) end -instantiation Amount :: si_baseunit +instantiation Amount :: si_basedim begin -definition si_sem_Amount :: "Amount itself \ Unit" - where [si_def]: "si_sem_Amount x = 1\Moles := 1\" -instance by (intro_classes, auto simp add: si_sem_Amount_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Amount :: "Amount itself \ Dimension" + where [si_def]: "si_sem_Amount x = 1\Amount := 1\" +instance by (intro_classes, auto simp add: si_sem_Amount_def is_BaseDim_def, (transfer, simp)+) end -instantiation Intensity :: si_baseunit +instantiation Intensity :: si_basedim begin -definition si_sem_Intensity :: "Intensity itself \ Unit" - where [si_def]: "si_sem_Intensity x = 1\Candelas := 1\" -instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_Intensity :: "Intensity itself \ Dimension" + where [si_def]: "si_sem_Intensity x = 1\Intensity := 1\" +instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseDim_def, (transfer, simp)+) end instantiation NoDimension :: si_type begin -definition si_sem_NoDimension :: "NoDimension itself \ Unit" +definition si_sem_NoDimension :: "NoDimension itself \ Dimension" where [si_def]: "si_sem_NoDimension x = 1" -instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseUnit_def, (transfer, simp)+) +instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseDim_def, (transfer, simp)+) end lemma base_units [simp]: - "is_BaseUnit SI(Length)" "is_BaseUnit SI(Mass)" "is_BaseUnit SI(Time)" - "is_BaseUnit SI(Current)" "is_BaseUnit SI(Temperature)" "is_BaseUnit SI(Amount)" - "is_BaseUnit SI(Intensity)" by (simp_all add: is_BaseUnit) + "is_BaseDim SI(Length)" "is_BaseDim SI(Mass)" "is_BaseDim SI(Time)" + "is_BaseDim SI(Current)" "is_BaseDim SI(Temperature)" "is_BaseDim SI(Amount)" + "is_BaseDim SI(Intensity)" by (simp_all add: is_BaseDim) 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 +typedef ('a::si_type, 'b::si_type) DimTimes (infixl "\" 69) = "UNIV :: unit set" .. +setup_lifting type_definition_DimTimes text \ We can prove that multiplication of two SI types yields an SI type. \ -instantiation UnitTimes :: (si_type, si_type) si_type +instantiation DimTimes :: (si_type, si_type) si_type begin - definition si_sem_UnitTimes :: "('a \ 'b) itself \ Unit" where - [si_eq]: "si_sem_UnitTimes x = SI('a) * SI('b)" - instance by (intro_classes, simp_all add: si_sem_UnitTimes_def, (transfer, simp)+) + definition si_sem_DimTimes :: "('a \ 'b) itself \ Dimension" where + [si_eq]: "si_sem_DimTimes x = SI('a) * SI('b)" + instance by (intro_classes, simp_all add: si_sem_DimTimes_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 +typedef 'a DimInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" .. +setup_lifting type_definition_DimInv +instantiation DimInv :: (si_type) si_type begin - definition si_sem_UnitInv :: "('a\<^sup>-\<^sup>1) itself \ Unit" where - [si_eq]: "si_sem_UnitInv x = inverse SI('a)" - instance by (intro_classes, simp_all add: si_sem_UnitInv_def, (transfer, simp)+) + definition si_sem_DimInv :: "('a\<^sup>-\<^sup>1) itself \ Dimension" where + [si_eq]: "si_sem_DimInv x = inverse SI('a)" + instance by (intro_classes, simp_all add: si_sem_DimInv_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, 'b) DimDiv = "'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 UnitQuart = "'a \ 'a \ 'a \ 'a" ("(_)\<^sup>4" [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) -type_synonym 'a UnitInvQuart = "('a\<^sup>4)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>4" [999] 999) +type_synonym 'a DimSquare = "'a \ 'a" ("(_)\<^sup>2" [999] 999) +type_synonym 'a DimCube = "'a \ 'a \ 'a" ("(_)\<^sup>3" [999] 999) +type_synonym 'a DimQuart = "'a \ 'a \ 'a \ 'a" ("(_)\<^sup>4" [999] 999) +type_synonym 'a DimInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999) +type_synonym 'a DimInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [999] 999) +type_synonym 'a DimInvQuart = "('a\<^sup>4)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>4" [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" translations (type) "'a\<^sup>-\<^sup>4" <= (type) "('a\<^sup>4)\<^sup>-\<^sup>1" -(* Need to add UnitQuart to the print translation *) +(* Need to add DimQuart to the print translation *) print_translation \ - [(@{type_syntax UnitTimes}, + [(@{type_syntax DimTimes}, fn ctx => fn [a, b] => if (a = b) - then Const (@{type_syntax UnitSquare}, dummyT) $ a + then Const (@{type_syntax DimSquare}, dummyT) $ a else case a of - Const (@{type_syntax UnitTimes}, _) $ a1 $ a2 => + Const (@{type_syntax DimTimes}, _) $ a1 $ a2 => if (a1 = a2 andalso a2 = b) - then Const (@{type_syntax UnitCube}, dummyT) $ a1 + then Const (@{type_syntax DimCube}, dummyT) $ a1 else case a1 of - Const (@{type_syntax UnitTimes}, _) $ a11 $ a12 => + Const (@{type_syntax DimTimes}, _) $ a11 $ a12 => if (a11 = a12 andalso a12 = a2 andalso a2 = b) - then Const (@{type_syntax UnitQuart}, dummyT) $ a11 + then Const (@{type_syntax DimQuart}, dummyT) $ a11 else raise Match | _ => raise Match)] \