Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Added some additional non-SI units

This commit is contained in:
Simon Foster 2020-03-20 16:50:01 +00:00
parent 4b605faa2d
commit 4cba4bbdc8
2 changed files with 29 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/SI/SI_Constants.thy
View File

@ -6,7 +6,7 @@ begin
subsection \<open> Core Derived Units \<close>
abbreviation "hertz \<equiv> second\<^sup>-\<^sup>\<one>"
abbreviation (input) "hertz \<equiv> second\<^sup>-\<^sup>\<one>"
abbreviation "radian \<equiv> meter \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one>"

38
src/SI/SI_Imperial.thy
View File

@ -8,23 +8,41 @@ subsection \<open> Definitions \<close>
default_sort field_char_0
definition degrees_farenheit :: "'a \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_eq]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
definition pint :: "'a[Volume]" where
[si_def, si_eq]: "pint = 0.56826125 \<odot> litre"
definition inch :: "'a[L]" where
[si_def, si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
[si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
definition foot :: "'a[L]" where
[si_def, si_eq]: "foot = 0.3048 \<odot> meter"
[si_eq]: "foot = 0.3048 \<odot> meter"
definition yard :: "'a[L]" where
[si_def, si_eq]: "yard = 0.9144 \<odot> meter"
[si_eq]: "yard = 0.9144 \<odot> meter"
definition mile :: "'a[L]" where
[si_def, si_eq]: "mile = 1609.344 \<odot> meter"
[si_eq]: "mile = 1609.344 \<odot> meter"
definition nautical_mile :: "'a[L]" where
[si_eq]: "nautical_mile = 1852 \<odot> meter"
definition knot :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" where
[si_eq]: "knot = 1 \<odot> (nautical_mile \<^bold>/ hour)"
definition pint :: "'a[Volume]" where
[si_eq]: "pint = 0.56826125 \<odot> litre"
definition gallon :: "'a[Volume]" where
[si_eq]: "gallon = 8 \<odot> pint"
definition pound :: "'a[M]" where
[si_eq]: "pound = 0.45359237 \<odot> kilogram"
definition ounce :: "'a[M]" where
[si_eq]: "ounce = 1/16 \<odot> pound"
definition stone :: "'a[M]" where
[si_eq]: "stone = 14 \<odot> pound"
definition degrees_farenheit :: "'a \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_eq]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
default_sort type