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

A few additional properties and proofs

This commit is contained in:
Simon Foster 2020-02-25 15:42:42 +00:00
parent 3c90e19d11
commit 3fa136ec72
3 changed files with 36 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/SI/SI_Accepted.thy
View File

@ -25,4 +25,7 @@ subsection \<open> Examples \<close>
lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule" by (si_calc)
lemma "25 \<odot> meter \<^bold>/ second = 90 \<odot> (kilo \<odot> meter) \<^bold>/ hour"
by (si_calc)
end

15
src/SI/SI_Dimensions.thy
View File

@ -252,12 +252,12 @@ lemma base_units [simp]:
subsubsection \<open> Higher SI Type Constructors: Inner Product and Inverse \<close>
text\<open>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.\<close>
the definitions of the type constructors for inner product and inverse is straight forward.\<close>
typedef ('a::dim_type, 'b::dim_type) DimTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
setup_lifting type_definition_DimTimes
text \<open> We can prove that multiplication of two SI types yields an SI type. \<close>
text \<open> We can prove that multiplication of two dimension types yields a dimension type. \<close>
instantiation DimTimes :: (dim_type, dim_type) dim_type
begin
@ -266,7 +266,8 @@ begin
instance by (intro_classes, simp_all add: dim_ty_sem_DimTimes_def, (transfer, simp)+)
end
text \<open> Similarly, we define division of two SI types and prove that SI types are closed under this. \<close>
text \<open> Similarly, we define inversion of dimension types and prove that dimension types are
closed under this. \<close>
typedef 'a DimInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" ..
setup_lifting type_definition_DimInv
@ -277,12 +278,14 @@ begin
instance by (intro_classes, simp_all add: dim_ty_sem_DimInv_def, (transfer, simp)+)
end
subsection \<open> Syntactic Support for dim-type expressions. \<close>
text\<open>A number of type-synonyms allow for more compact notation: \<close>
text \<open> A division is expressed, as usual, by multiplication with an inverted dimension. \<close>
type_synonym ('a, 'b) DimDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
text \<open> A number of further type-synonyms allow for more compact notation: \<close>
type_synonym 'a DimSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
type_synonym 'a DimCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
type_synonym 'a DimQuart = "'a \<cdot> 'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>4" [999] 999)
@ -294,8 +297,6 @@ 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 DimQuart to the print translation *)
print_translation \<open>
[(@{type_syntax DimTimes},
fn ctx => fn [a, b] =>

30
src/SI/SI_Imperial.thy
View File

@ -6,19 +6,39 @@ begin
subsection \<open> Definition \<close>
definition degrees_farenheit :: "'a::field_char_0 \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
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 [si_def, si_eq]: "pint = 0.56826125 \<odot> litre"
definition pint :: "'a[Volume]" where
[si_def, si_eq]: "pint = 0.56826125 \<odot> litre"
definition [si_def, si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
definition inch :: "'a[L]" where
[si_def, si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
definition [si_def, si_eq]: "foot = 0.3048 \<odot> meter"
definition foot :: "'a[L]" where
[si_def, si_eq]: "foot = 0.3048 \<odot> meter"
definition [si_def, si_eq]: "yard = 0.9144 \<odot> meter"
definition yard :: "'a[L]" where
[si_def, si_eq]: "yard = 0.9144 \<odot> meter"
definition mile :: "'a[L]" where
[si_def, si_eq]: "mile = 1609.344 \<odot> meter"
default_sort type
subsection \<open> Properties \<close>
lemma miles_to_yards: "mile = 1760 \<odot> yard"
by si_simp
lemma miles_to_feet: "mile = 5280 \<odot> foot"
by si_simp
lemma mph_to_kmh: "1 \<odot> (mile \<^bold>/ hour) = 1.609344 \<odot> ((kilo \<odot> meter) \<^bold>/ hour)"
by si_simp
lemma celcius_to_farenheit: "(T::rat)\<degree>C = ((T - 32) \<cdot> 5/9)\<degree>F"
oops