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

Added definition of a base unit

This commit is contained in:
Simon Foster 2020-03-12 09:25:40 +00:00
parent 3fa136ec72
commit 75e62c7356
1 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/SI/SI_Units.thy
View File

@ -269,7 +269,7 @@ lift_definition mk_unit :: "'u itself \<Rightarrow> ('a::one)['u::dim_type]"
syntax "_mk_unit" :: "type \<Rightarrow> logic" ("UNIT'(_')")
translations "UNIT('a)" == "CONST mk_unit TYPE('a)"
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
subsection \<open>Polymorphic Operations for SI Base Units \<close>
definition [si_eq]: "meter = UNIT(L)"
definition [si_eq]: "second = UNIT(T)"
@ -289,4 +289,10 @@ type @{typ "real\<^sup>3"}. Note than when considering vectors, dimensions refer
not to its components.
\<close>
lift_definition is_BaseUnit :: "'a::one['d::dim_type] \<Rightarrow> bool"
is "\<lambda> x. mag x = 1 \<and> is_BaseDim (dim x)" .
lemma meter_is_BaseUnit: "is_BaseUnit meter"
by (simp add: si_eq, transfer, simp)
end