diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy new file mode 100644 index 0000000..bb91b64 --- /dev/null +++ b/src/SI/SI_Accepted.thy @@ -0,0 +1,29 @@ +section \ Non-SI Units Accepted for SI use \ + +theory SI_Accepted + imports SI_Derived +begin + +definition [si_def, si_eq]: "minute = 60 \ second" + +definition [si_def, si_eq]: "hour = 60 \ minute" + +definition [si_def, si_eq]: "day = 24 \ hour" + +definition [si_def, si_eq]: "astronomical_unit = 149597870700 \ meter" + +definition degree :: "'a::real_field[L/L]" where +[si_def, si_eq]: "degree = (2\(of_real pi) / 180) \ radian" + +abbreviation degrees ("_\" [999] 999) where "n\ \ n \ degree" + +definition [si_def, si_eq]: "litre = 1/1000 \ meter\<^sup>\" + +abbreviation "tonne \ 10^3 \ kilogram" + +subsection \ Examples \ + +lemma "watt \<^bold>\ hour \\<^sub>Q 3600 \ joule" + by (si_calc) + +end \ No newline at end of file diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index b651630..c725955 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -4,6 +4,8 @@ theory SI_Constants imports SI_Proof begin +subsection \ Core Derived Units \ + abbreviation "hertz \ second\<^sup>-\<^sup>\" abbreviation "radian \ meter \<^bold>\ meter\<^sup>-\<^sup>\" @@ -18,6 +20,8 @@ abbreviation "coulomb \ ampere \<^bold>\ second" abbreviation "lumen \ candela \<^bold>\ steradian" +subsection \ Constants \ + text \ The most general types we support must form a field into which the natural numbers can be injected. \ diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index 0b27cbd..15a1067 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -6,44 +6,34 @@ begin subsection \ Definitions \ -definition degree :: "'a::real_field[L/L]" where -[si_def]: "degree = (2\(of_real pi) / 180) \ radian" +abbreviation "newton \ kilogram \<^bold>\ meter \<^bold>\ second\<^sup>-\<^sup>\" -abbreviation degrees ("_\" [999] 999) where "n\ \ n \ degree" - -definition degrees_celcius :: "'a::field \ 'a[\]" ("_\C" [999] 999) - where [si_def]: "degrees_celcius x = x + 273.151 \ kelvin" - -definition degrees_farenheit :: "'a::field \ 'a[\]" ("_\F" [999] 999) - where [si_def]: "degrees_farenheit x = (x + 459.67)\5/9 \ kelvin" - -definition [si_def]: "litre = 1/1000 \ meter\<^sup>\" - -definition [si_def]: "pint = 0.56826125 \ litre" - -definition [si_def, si_eq]: "hour = 3600 \ second" - -definition [si_def]: "gram = milli \ kilogram" - -abbreviation "tonne \ kilo \ kilogram" - -abbreviation "newton \ (kilogram \<^bold>\ meter) \<^bold>/ second\<^sup>\" +abbreviation "pascal \ kilogram \<^bold>\ meter\<^sup>-\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\" abbreviation "volt \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" -definition "inch = 25.5 \ milli \ meter" +abbreviation "farad \ kilogram\<^sup>-\<^sup>\ \<^bold>\ meter\<^sup>-\<^sup>\ \<^bold>\ second\<^sup>\ \<^bold>\ ampere\<^sup>\" -definition "foot = 0.3048 \ meter" +abbreviation "ohm \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" -definition "yard = 0.9144 \ meter" +abbreviation "siemens \ kilogram\<^sup>-\<^sup>\ \<^bold>\ meter\<^sup>-\<^sup>\ \<^bold>\ second\<^sup>\ \<^bold>\ ampere\<^sup>\" + +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 "henry \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" + +definition degrees_celcius :: "'a::field \ 'a[\]" ("_\C" [999] 999) + where [si_def, si_eq]: "degrees_celcius x = x + 273.151 \ kelvin" + +definition degrees_farenheit :: "'a::field \ 'a[\]" ("_\F" [999] 999) + where [si_def, si_eq]: "degrees_farenheit x = (x + 459.67)\5/9 \ kelvin" + +definition [si_def, si_eq]: "gram = milli \ kilogram" 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)[L \ T\<^sup>-\<^sup>2]" -subsection \ Examples \ - -lemma "watt \<^bold>\ hour \\<^sub>Q 3600 \ joule" - by (si_calc) - end \ No newline at end of file diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy new file mode 100644 index 0000000..bd20fcf --- /dev/null +++ b/src/SI/SI_Imperial.thy @@ -0,0 +1,15 @@ +section \ Imperial Units via SI \ + +theory SI_Imperial + imports SI_Accepted +begin + +definition [si_def, si_eq]: "pint = 0.56826125 \ litre" + +definition [si_def, si_eq]: "inch = 25.5 \ milli \ meter" + +definition [si_def, si_eq]: "foot = 0.3048 \ meter" + +definition [si_def, si_eq]: "yard = 0.9144 \ meter" + +end \ No newline at end of file diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy index c1c4360..dcc424f 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/SI_Proof.thy @@ -5,7 +5,7 @@ theory SI_Proof begin definition magnQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where -[si_def]: "magnQuant x = magn (fromUnit x)" +[si_def]: "magnQuant x = magn (fromQ x)" lemma unit_eq_iff_magn_eq: "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" @@ -15,7 +15,7 @@ lemma unit_equiv_iff: 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 (fromUnit ta) \ magn (fromUnit t)" + 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) then show ?thesis by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def) diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index bf1c9a3..0677f49 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -98,14 +98,14 @@ text\We 'lift' SI type expressions to SI tagged type expressions as follow 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) + morphisms fromQ toQ 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))" +"SI('u\<^sub>1) = SI('u\<^sub>2) \ coerceUnit t x = (toQ (fromQ x))" section\Operations SI-tagged types via their Semantic Domains\ @@ -141,7 +141,7 @@ 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 qequiv.rep_eq assms coerceUnit_def toUnit_cases toUnit_inverse) + by (metis qequiv.rep_eq assms coerceUnit_def toQ_cases toQ_inverse) (* or equivalently *) @@ -153,19 +153,19 @@ lemma coerceQuant_eq_iff2: 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))" + assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (toQ (fromQ 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 _))" +find_theorems "(toQ (fromQ _))" 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) qequiv.rep_eq assms fromUnit mem_Collect_eq) + by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq) subsection\Operations on SI-tagged types\ diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index 710f1e2..5882ef1 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -312,7 +312,7 @@ type_synonym ('a, 'b) UnitDiv = "'a \ ('b\<^sup>-\<^sup>1)" (infixl "'/" 6 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" ("(_)\<^sup>4" [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) @@ -321,6 +321,8 @@ 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 *) + print_translation \ [(@{type_syntax UnitTimes}, fn ctx => fn [a, b] => @@ -330,11 +332,11 @@ print_translation \ 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 | + else case a1 of + Const (@{type_syntax UnitTimes}, _) $ a11 $ a12 => + if (a11 = a12 andalso a12 = a2 andalso a2 = b) + then Const (@{type_syntax UnitQuart}, dummyT) $ a11 + else raise Match | _ => raise Match)] \