From 3fa136ec72e4d80775af64f60704c483b3263fd4 Mon Sep 17 00:00:00 2001
From: Simon Foster <simon.foster@york.ac.uk>
Date: Tue, 25 Feb 2020 15:42:42 +0000
Subject: [PATCH] A few additional properties and proofs

---
 src/SI/SI_Accepted.thy   |  3 +++
 src/SI/SI_Dimensions.thy | 15 ++++++++-------
 src/SI/SI_Imperial.thy   | 30 +++++++++++++++++++++++++-----
 3 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy
index 92c502e..4946f8f 100644
--- a/src/SI/SI_Accepted.thy
+++ b/src/SI/SI_Accepted.thy
@@ -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
\ No newline at end of file
diff --git a/src/SI/SI_Dimensions.thy b/src/SI/SI_Dimensions.thy
index c35c58c..99cbd3b 100644
--- a/src/SI/SI_Dimensions.thy
+++ b/src/SI/SI_Dimensions.thy
@@ -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] => 
diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy
index 3fe0ef9..fca8011 100644
--- a/src/SI/SI_Imperial.thy
+++ b/src/SI/SI_Imperial.thy
@@ -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