diff --git a/src/SI/SI_Algebra.thy b/src/SI/SI_Algebra.thy
new file mode 100644
index 0000000..69f7007
--- /dev/null
+++ b/src/SI/SI_Algebra.thy
@@ -0,0 +1,91 @@
+section \<open> Algebraic Laws \<close>
+
+theory SI_Algebra
+  imports SI_Proof
+begin
+
+subsection \<open> Quantity Scale \<close>
+
+lemma scaleQ_add_right: "a \<odot> x + y = (a \<odot> x) + (a \<odot> y)"
+  by (transfer, simp add: distrib_left)
+
+lemma scaleQ_add_left: "a + b \<odot> x = (a \<odot> x) + (b \<odot> x)"
+  by (transfer, simp add: distrib_right)
+
+lemma scaleQ_scaleQ: "a \<odot> b \<odot> x = a \<cdot> b \<odot> x"
+  by (transfer, simp add: mult.assoc)
+
+lemma scaleQ_one [simp]: "1 \<odot> x = x"
+  by (transfer, simp)
+
+lemma scaleQ_zero [simp]: "0 \<odot> x = 0"
+  by (transfer, simp)
+
+lemma scaleQ_inv: "-a \<odot> x = a \<odot> -x"
+  by (transfer, simp)
+
+lemma scaleQ_as_qprod: "a \<odot> x \<cong>\<^sub>Q (a \<odot> \<one>) \<^bold>\<cdot> x"
+  unfolding si_def
+  by (transfer, simp add: si_sem_NoDimension_def)
+
+lemma mult_scaleQ_left [simp]: "(a \<odot> x) \<^bold>\<cdot> y = a \<odot> x \<^bold>\<cdot> y"
+  by (transfer, simp add: si_sem_UnitTimes_def mult.assoc)
+
+lemma mult_scaleQ_right [simp]: "x \<^bold>\<cdot> (a \<odot> y) = a \<odot> x \<^bold>\<cdot> y"
+  by (transfer, simp add: si_sem_UnitTimes_def times_Quantity_ext_def mult.assoc)
+
+subsection \<open> Field Laws \<close>
+
+lemma qtimes_commute: "x \<^bold>\<cdot> y \<cong>\<^sub>Q y \<^bold>\<cdot> x"
+  by si_calc
+
+text\<open>Observe that this commutation law also commutes the types.\<close>
+ 
+(* just a check that instantiation works for special cases ... *)
+lemma "    (UNIT(x, J) \<^bold>\<cdot> UNIT(y::'a::comm_ring_1, N))
+        \<cong>\<^sub>Q (UNIT(y, N) \<^bold>\<cdot> UNIT(x, J)) "
+  by(simp add: qtimes_commute)
+
+lemma qtimes_assoc: "(x \<^bold>\<cdot> y) \<^bold>\<cdot> z  \<cong>\<^sub>Q  x \<^bold>\<cdot> (y \<^bold>\<cdot> z)"
+  by (si_calc)
+
+lemma qtimes_left_unit: "\<one> \<^bold>\<cdot> x \<cong>\<^sub>Q x"
+  by (si_calc)
+
+lemma qtimes_right_unit: "x \<^bold>\<cdot> \<one> \<cong>\<^sub>Q x"
+  by (si_calc)
+
+text\<open>The following weak congruences will allow for replacing equivalences in contexts
+     built from product and inverse. \<close>
+
+lemma qtimes_weak_cong_left:
+  assumes "x \<cong>\<^sub>Q y"
+  shows  "x\<^bold>\<cdot>z \<cong>\<^sub>Q y\<^bold>\<cdot>z"
+  using assms by si_calc
+
+lemma qtimes_weak_cong_right:
+  assumes "x \<cong>\<^sub>Q y"
+  shows  "z\<^bold>\<cdot>x \<cong>\<^sub>Q z\<^bold>\<cdot>y"
+  using assms by si_calc
+
+lemma qinverse_weak_cong:
+  assumes "x \<cong>\<^sub>Q y"
+  shows   "x\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y\<^sup>-\<^sup>\<one>"
+  using assms by si_calc
+
+lemma qinverse_qinverse: "x\<^sup>-\<^sup>\<one>\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x"
+  by si_calc
+
+lemma qinverse_nonzero_iff_nonzero: "x\<^sup>-\<^sup>\<one> = 0 \<longleftrightarrow> x = 0"
+  by si_calc
+
+lemma qinverse_qtimes: "(x \<^bold>\<cdot> y)\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q x\<^sup>-\<^sup>\<one> \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
+  by si_calc
+
+lemma qinverse_qdivide: "(x \<^bold>/ y)\<^sup>-\<^sup>\<one> \<cong>\<^sub>Q y \<^bold>/ x"
+  by si_calc
+
+lemma qtimes_cancel: "x \<noteq> 0 \<Longrightarrow> x \<^bold>/ x \<cong>\<^sub>Q \<one>"
+  by si_calc
+
+end
diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy
index 8080420..b651630 100644
--- a/src/SI/SI_Constants.thy
+++ b/src/SI/SI_Constants.thy
@@ -23,42 +23,50 @@ text \<open> The most general types we support must form a field into which the
 
 default_sort field_char_0
 
-abbreviation (input) caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\<Delta>v\<^sub>C\<^sub>s") where
+text \<open> Hyperfine transition frequency of frequency of Cs \<close>
+
+abbreviation caesium_frequency:: "'a[T\<^sup>-\<^sup>1]" ("\<Delta>v\<^sub>C\<^sub>s") where
   "caesium_frequency \<equiv> 9192631770 \<odot> hertz"
 
-abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" where
+text \<open> Speed of light in vacuum \<close>
+
+abbreviation speed_of_light :: "'a[L \<cdot> T\<^sup>-\<^sup>1]" ("\<^bold>c") where
   "speed_of_light \<equiv> 299792458 \<odot> (meter\<^bold>\<cdot>second\<^sup>-\<^sup>\<one>)"
 
-abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" where
+text \<open> Planck constant \<close>
+
+abbreviation Planck :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> T]" ("\<^bold>h") where
   "Planck \<equiv> (6.62607015 \<cdot> 1/(10^34)) \<odot> (joule\<^bold>\<cdot>second)"
 
-abbreviation elementary_charge :: "'a[I \<cdot> T]" where
+text \<open> Elementary charge \<close>
+
+abbreviation elementary_charge :: "'a[I \<cdot> T]" ("\<^bold>e") where
   "elementary_charge \<equiv> (1.602176634 \<cdot> 1/(10^19)) \<odot> coulomb"
 
-abbreviation Boltzmann :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> \<Theta>\<^sup>-\<^sup>1]" where
+abbreviation Boltzmann :: "'a[M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>2 \<cdot> \<Theta>\<^sup>-\<^sup>1]" ("\<^bold>k") where
   "Boltzmann \<equiv> (1.380649\<cdot>1/(10^23)) \<odot> (joule \<^bold>/ kelvin)"
 
-abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" where
+abbreviation Avogadro :: "'a[N\<^sup>-\<^sup>1]" ("N\<^sub>A") where
 "Avogadro \<equiv> 6.02214076\<cdot>(10^23) \<odot> (mole\<^sup>-\<^sup>\<one>)"
 
 abbreviation max_luminous_frequency :: "'a[T\<^sup>-\<^sup>1]" where
 "max_luminous_frequency \<equiv> (540\<cdot>10^12) \<odot> hertz"
 
-abbreviation luminous_efficacy :: "'a[J \<cdot> (L\<^sup>2 \<cdot> L\<^sup>-\<^sup>2) \<cdot> (M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" where
+abbreviation luminous_efficacy :: "'a[J \<cdot> (L\<^sup>2 \<cdot> L\<^sup>-\<^sup>2) \<cdot> (M \<cdot> L\<^sup>2 \<cdot> T\<^sup>-\<^sup>3)\<^sup>-\<^sup>1]" ("K\<^sub>c\<^sub>d") where
 "luminous_efficacy \<equiv> 683 \<odot> (lumen\<^bold>/watt)"
 
+theorem second_definition: 
+  "1 \<odot> second \<cong>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
+  by si_calc
+
+theorem meter_definition: 
+  "1 \<odot> meter \<cong>\<^sub>Q (\<^bold>c \<^bold>/ (299792458 \<odot> \<one>))\<^bold>\<cdot>second"
+  "1 \<odot> meter \<cong>\<^sub>Q (9192631770 / 299792458) \<odot> (\<^bold>c \<^bold>/ \<Delta>v\<^sub>C\<^sub>s)"
+  by si_calc+
+
 abbreviation gravitational_constant :: "'a[L\<^sup>3 \<cdot> M\<^sup>-\<^sup>1 \<cdot> T\<^sup>-\<^sup>2]" where
   "gravitational_constant \<equiv> (6.6743015 \<cdot> 1/(10 ^ 11)) \<odot> (meter\<^sup>\<three>\<^bold>\<cdot>kilogram\<^sup>-\<^sup>\<one>\<^bold>\<cdot>second\<^sup>-\<^sup>\<two>)"
 
-thm si_def
-
-theorem Quant_eq_iff_same_dim:
-  "x \<approx>\<^sub>Q y \<longleftrightarrow> x = y"
-  by (transfer, simp)
-
-theorem second_definition: "1 \<odot> second \<approx>\<^sub>Q (9192631770 \<odot> \<one>) \<^bold>/ \<Delta>v\<^sub>C\<^sub>s"
-  by (simp add: unit_equiv_iff, simp add: Quant_equiv_def unit_eq_iff_magn_eq si_def)
-
 default_sort type
 
 end
\ No newline at end of file
diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy
index b7664d5..0b27cbd 100644
--- a/src/SI/SI_Derived.thy
+++ b/src/SI/SI_Derived.thy
@@ -4,22 +4,24 @@ theory SI_Derived
   imports SI_Prefix
 begin                                  
 
-definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where
+subsection \<open> Definitions \<close>
+
+definition degree :: "'a::real_field[L/L]" where
 [si_def]: "degree = (2\<cdot>(of_real pi) / 180) \<odot> radian"
 
 abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n \<odot> degree"
 
-definition degrees_celcius :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999) 
+definition degrees_celcius :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999) 
   where [si_def]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
 
-definition degrees_farenheit :: "'a::division_ring \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
+definition degrees_farenheit :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
   where [si_def]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
 
 definition [si_def]: "litre = 1/1000 \<odot> meter\<^sup>\<three>"
 
 definition [si_def]: "pint = 0.56826125 \<odot> litre"
 
-definition [si_def]: "hour = 3600 \<odot> second"
+definition [si_def, si_eq]: "hour = 3600 \<odot> second"
 
 definition [si_def]: "gram = milli \<odot> kilogram"
 
@@ -39,4 +41,9 @@ text\<open>The full beauty of the approach is perhaps revealed here, with the
      type of a classical three-dimensional gravitation field:\<close>
 type_synonym gravitation_field = "(real\<^sup>3 \<Rightarrow> real\<^sup>3)[L \<cdot> T\<^sup>-\<^sup>2]"
 
+subsection \<open> Examples \<close>
+
+lemma "watt \<^bold>\<cdot> hour \<cong>\<^sub>Q 3600 \<odot> joule"
+  by (si_calc)
+
 end
\ No newline at end of file
diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy
index 570c437..c1c4360 100644
--- a/src/SI/SI_Proof.thy
+++ b/src/SI/SI_Proof.thy
@@ -1,8 +1,69 @@
+section \<open> Tactic Support for SI type expressions. \<close>
+
 theory SI_Proof
   imports SI_Quantities
 begin
 
-section \<open> Tactic Support for SI type expressions. \<close>
+definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
+[si_def]: "magnQuant x = magn (fromUnit x)"
+
+lemma unit_eq_iff_magn_eq:
+  "x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (auto simp add: magnQuant_def, transfer, simp)
+
+lemma unit_equiv_iff:
+  fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]"
+  shows "x \<cong>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> SI('u\<^sub>1) = SI('u\<^sub>2)"
+proof -
+  have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> magn (fromUnit ta) \<noteq> magn (fromUnit 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)
+qed
+
+lemma unit_le_iff_magn_le:
+  "x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (auto simp add: magnQuant_def; (transfer, simp))
+
+lemma magnQuant_zero [si_eq]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_plus [si_eq]: "\<lbrakk>x + y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q + \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_scaleQ [si_eq]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_qtimes [si_eq]: "\<lbrakk>x \<^bold>\<cdot> y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q \<cdot> \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_qinverse [si_eq]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
+  by (simp add: magnQuant_def, transfer, simp)
+
+lemma magnQuant_qdivivide [si_eq]: "\<lbrakk>(x::('a::field)[_]) \<^bold>/ y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q / \<lbrakk>y\<rbrakk>\<^sub>Q"
+  by (simp add: magnQuant_def, transfer, simp add: field_class.field_divide_inverse)
+
+lemma magnQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
+  apply (induct n, simp_all add: si_def)
+  apply (metis magnQuant_def magnQuant_one)
+  apply (metis magnQuant_def magnQuant_plus numeral_code(2))
+  apply (metis magnQuant_def magnQuant_one magnQuant_plus numeral_code(3))
+  done
+
+lemma magnQuant_mk [si_eq]: "\<lbrakk>UNIT(n, 'u::si_type)\<rbrakk>\<^sub>Q = n"
+  by (simp add: magnQuant_def, transfer, simp)
+
+method si_calc uses simps = 
+  (simp add: unit_equiv_iff unit_eq_iff_magn_eq unit_le_iff_magn_le si_eq simps)
+
+lemmas [si_eq] = si_sem_Length_def si_sem_Mass_def si_sem_Time_def 
+                   si_sem_Current_def si_sem_Temperature_def si_sem_Amount_def
+                   si_sem_Intensity_def si_sem_NoDimension_def
+                   si_sem_UnitTimes_def si_sem_UnitInv_def
+                   inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def
 
 lemmas [si_def] =  si_sem_Length_def si_sem_Mass_def si_sem_Time_def 
                    si_sem_Current_def si_sem_Temperature_def si_sem_Amount_def
@@ -23,139 +84,4 @@ lemma "SI(\<one>)  = 1"                 by(simp add: si_def)
 
 lemma "SI(N \<cdot> \<Theta> \<cdot> N) = SI(\<Theta> \<cdot> N\<^sup>2)" by(simp add: si_def)
 
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Time) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 0, Seconds = 1, Amperes = 0, 
-                           Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Time_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Length) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 1, Kilograms = 0, Seconds = 0, Amperes = 0, 
-                           Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Length_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Mass) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 1, Seconds = 0, Amperes = 0, 
-                           Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Mass_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Current) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 1, 
-                           Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Current_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Temperature) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, 
-                           Kelvins = 1, Moles = 0, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Temperature_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Amount) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, 
-                           Kelvins = 0, Moles = 1, Candelas = 0\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Amount_def)
-
-lemma [si_def]:"fromUnit UNIT(x::'a::one, Intensity) = 
-                  \<lparr>magn = x,
-                   unit = \<lparr>Meters = 0, Kilograms = 0, Seconds = 0, Amperes = 0, 
-                           Kelvins = 0, Moles = 0, Candelas = 1\<rparr>\<rparr>"
-  by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_Intensity_def)
-
-lemma Unit_times_commute:
-  fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"and Y::"'a['c::si_type]"
-  shows "X \<^bold>\<cdot> Y  \<approx>\<^sub>Q  Y \<^bold>\<cdot> X"
-  by (transfer, simp add: mult.commute times_Quantity_ext_def)
-
-text\<open>Observe that this commutation law also commutes the types.\<close>
- 
-(* just a check that instantiation works for special cases ... *)
-lemma "    (UNIT(x, J) \<^bold>\<cdot> UNIT(y::'a::{one,ab_semigroup_mult}, N))
-        \<approx>\<^sub>Q (UNIT(y, N) \<^bold>\<cdot> UNIT(x, J)) "
-  by(simp add: Unit_times_commute)
-
-
-lemma Unit_times_assoc:
-  fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
-    and Y::"'a['c::si_type]"
-    and Z::"'a['d::si_type]"
-  shows  "(X \<^bold>\<cdot> Y) \<^bold>\<cdot> Z  \<approx>\<^sub>Q  X \<^bold>\<cdot> (Y \<^bold>\<cdot> Z)"
-  by (transfer, simp add: mult.commute mult.left_commute times_Quantity_ext_def)
-
-text\<open>The following weak congruences will allow for replacing equivalences in contexts
-     built from product and inverse. \<close>
-lemma Unit_times_weak_cong_left:
-  fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
-    and Y::"'a['c::si_type]"
-    and Z::"'a['d::si_type]"
-  assumes "X \<approx>\<^sub>Q Y"
-  shows  "(X \<^bold>\<cdot> Z)  \<approx>\<^sub>Q  (Y \<^bold>\<cdot> Z)"
-  using assms by (transfer, simp)
-
-lemma Unit_times_weak_cong_right:
-  fixes X::"'a::{one,ab_semigroup_mult}['b::si_type]"
-    and Y::"'a['c::si_type]"
-    and Z::"'a['d::si_type]"
-  assumes "X \<approx>\<^sub>Q Y"
-  shows  "(Z \<^bold>\<cdot> X)  \<approx>\<^sub>Q  (Z \<^bold>\<cdot> Y)"
-  using assms by (transfer, simp)
-
-lemma Unit_inverse_weak_cong:
-  fixes   X::"'a::{field}['b::si_type]"
-    and   Y::"'a['c::si_type]"
-  assumes "X  \<approx>\<^sub>Q Y"
-  shows   "(X)\<^sup>-\<^sup>\<one>  \<approx>\<^sub>Q  (Y)\<^sup>-\<^sup>\<one>"
-  using assms by (transfer, simp)
-
-(*
-text\<open>In order to compute a normal form, we would additionally need these three:\<close>
-(* field ? *)
-lemma Unit_inverse_distrib:
-  fixes X::"'a::{field}['b::si_type]"
-    and Y::"'a['c::si_type]"
-  shows "(X \<^bold>\<cdot> Y)\<^sup>-\<^sup>\<one>  \<approx>\<^sub>Q  X\<^sup>-\<^sup>\<one> \<^bold>\<cdot> Y\<^sup>-\<^sup>\<one>"
-  apply (transfer)
-  sorry
-
-(* field ? *)
-lemma Unit_inverse_inverse:
-  fixes X::"'a::{field}['b::si_type]"
-  shows "((X)\<^sup>-\<^sup>\<one>)\<^sup>-\<^sup>\<one>  \<approx>\<^sub>Q  X"
-  apply transfer
-  sorry
-
-(* field ? *)
-lemma Unit_mult_cancel:
-  fixes  X::"'a::{field}['b::si_type]"
-  shows  "X \<^bold>/ X  \<approx>\<^sub>Q  1"
-  apply transfer
-  sorry
-
-
-lemma Unit_mult_mult_Left_cancel:
-  fixes  X::"'a::{field}['b::si_type]"
-  shows  "(1::'a['b/'b]) \<^bold>\<cdot> X  \<approx>\<^sub>Q  X"
-  apply transfer
-  sorry
-
-
-lemma "watt \<^bold>\<cdot> hour \<approx>\<^sub>Q 3600 \<^bold>\<cdot> joule"
-  unfolding Unit_equiv_def hour_def
-  apply(simp add: Units.Unit_times.rep_eq si_def 
-                 zero_SI_tagged_domain_ext_def times_SI_tagged_domain_ext_def 
-                 inverse_SI_tagged_domain_ext_def 
-                 Unit_inverse_def Unit_times_def)
-  find_theorems fromUnit
-  oops
-
-  thm Units.Unit.toUnit_inverse
-
-
-lemma "watt \<^bold>\<cdot> hour \<approx>\<^sub>Q 3.6 \<^bold>\<cdot> kilo \<^bold>\<cdot> joule"
-  oops
-*)
-
 end
\ No newline at end of file
diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy
index b8d8036..bf1c9a3 100644
--- a/src/SI/SI_Quantities.thy
+++ b/src/SI/SI_Quantities.thy
@@ -79,6 +79,20 @@ instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
 instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
   by (intro_classes, rule Quantity_eq_intro, simp_all)
 
+instantiation Quantity_ext :: (ord, ord) ord
+begin
+  definition less_eq_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
+    where "less_eq_Quantity_ext x y = (magn x \<le> magn y \<and> unit x = unit y \<and> more x \<le> more y)"
+  definition less_Quantity_ext :: "('a, 'b) Quantity_scheme \<Rightarrow> ('a, 'b) Quantity_scheme \<Rightarrow> bool"
+    where "less_Quantity_ext x y = (x \<le> y \<and> \<not> y \<le> x)"
+
+instance ..
+
+end
+
+instance Quantity_ext :: (order, order) order
+  by (intro_classes, auto simp add: less_Quantity_ext_def less_eq_Quantity_ext_def)
+
 subsection \<open> SI Tagged Types \<close>
 text\<open>We 'lift' SI type expressions to SI tagged type expressions as follows:\<close>
 
@@ -99,73 +113,81 @@ subsection\<open>Predicates on SI-tagged types\<close>
 
 text \<open> Two SI types are equivalent if they have the same value-level units. \<close>
 
-lift_definition Quant_equiv :: "'n['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<approx>\<^sub>Q" 50) is
+lift_definition qless_eq :: "'n::order['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<lesssim>\<^sub>Q" 50) is
+"(\<le>)" .
+
+lift_definition qequiv :: "'n['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> bool" (infix "\<cong>\<^sub>Q" 50) is
 "(=)" .
 
 text\<open>This gives us an equivalence, but, unfortunately, not a congruence.\<close>
 
-lemma Quant_equiv_refl [simp]: "a \<approx>\<^sub>Q a"
-  by (simp add: Quant_equiv_def)
+lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
+  by (simp add: qequiv_def)
 
-lemma Quant_equiv_sym: "a \<approx>\<^sub>Q b \<Longrightarrow> b \<approx>\<^sub>Q a"
-  by (simp add: Quant_equiv_def)
+lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
+  by (simp add: qequiv_def)
 
-lemma Quant_equiv_trans: "\<lbrakk> a \<approx>\<^sub>Q b; b \<approx>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<approx>\<^sub>Q c"
-  by (simp add: Quant_equiv_def)
+lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
+  by (simp add: qequiv_def)
+
+theorem qeq_iff_same_dim:
+  fixes x y :: "'a['u::si_type]"
+  shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
+  by (transfer, simp)
 
 (* the following series of equivalent statements ... *)
 
 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) \<approx>\<^sub>Q x"
-  by (metis Quant_equiv.rep_eq assms coerceUnit_def toUnit_cases toUnit_inverse)
+  shows "(coerceUnit TYPE('u\<^sub>2) x) \<cong>\<^sub>Q x"
+  by (metis qequiv.rep_eq assms coerceUnit_def toUnit_cases toUnit_inverse)
 
 (* or equivalently *)
 
 lemma coerceQuant_eq_iff2:
   fixes x :: "'a['u\<^sub>1::si_type]"
   assumes "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)" and "y = (coerceUnit TYPE('u\<^sub>2) x)"
-  shows "x \<approx>\<^sub>Q y"
-  using Quant_equiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
+  shows "x \<cong>\<^sub>Q y"
+  using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff by blast
 
 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))"
-  shows "x \<approx>\<^sub>Q y"
+  shows "x \<cong>\<^sub>Q y"
   by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceUnit_def)
 
-text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<approx>\<^sub>Q y\<close>, since x and y may have different type.\<close>
+text\<open>This is more general that \<open>y = x \<Longrightarrow> x \<cong>\<^sub>Q y\<close>, since x and y may have different type.\<close>
 
 find_theorems "(toUnit (fromUnit _))"
 
 lemma eq_ : 
   fixes x :: "'a['u\<^sub>1::si_type]" fixes y :: "'a['u\<^sub>2::si_type]"
-  assumes  "x \<approx>\<^sub>Q y"
+  assumes  "x \<cong>\<^sub>Q y"
   shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)"
-  by (metis (full_types) Quant_equiv.rep_eq assms fromUnit mem_Collect_eq)
+  by (metis (full_types) qequiv.rep_eq assms fromUnit mem_Collect_eq)
 
 subsection\<open>Operations on SI-tagged types\<close>
 
 lift_definition 
-  Quant_times :: "('n::times)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
+  qtimes :: "('n::comm_ring_1)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a \<cdot>'b]" (infixl "\<^bold>\<cdot>" 69) is "(*)"
   by (simp add: si_sem_UnitTimes_def times_Quantity_ext_def)
   
 lift_definition 
-  Quant_inverse :: "('n::inverse)['a::si_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
+  qinverse :: "('n::field)['a::si_type] \<Rightarrow> 'n['a\<^sup>-\<^sup>1]" ("(_\<^sup>-\<^sup>\<one>)" [999] 999) is "inverse"
   by (simp add: inverse_Quantity_ext_def si_sem_UnitInv_def)
 
 abbreviation 
-  Quant_divide :: "('n::{times,inverse})['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
-"Quant_divide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
+  qdivide :: "('n::field)['a::si_type] \<Rightarrow> 'n['b::si_type] \<Rightarrow> 'n['a/'b]" (infixl "\<^bold>'/" 70) where
+"qdivide x y \<equiv> x \<^bold>\<cdot> y\<^sup>-\<^sup>\<one>"
 
-abbreviation Quant_sq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
-abbreviation Quant_cube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
-abbreviation Quant_quart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
+abbreviation qsq ("(_)\<^sup>\<two>" [999] 999) where "u\<^sup>\<two> \<equiv> u\<^bold>\<cdot>u"
+abbreviation qcube ("(_)\<^sup>\<three>" [999] 999) where "u\<^sup>\<three> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u"
+abbreviation qquart ("(_)\<^sup>\<four>" [999] 999) where "u\<^sup>\<four> \<equiv> u\<^bold>\<cdot>u\<^bold>\<cdot>u\<^bold>\<cdot>u"
 
-abbreviation Quant_neq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
-abbreviation Quant_neq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
-abbreviation Quant_neq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
+abbreviation qneq_sq ("(_)\<^sup>-\<^sup>\<two>" [999] 999) where "u\<^sup>-\<^sup>\<two> \<equiv> (u\<^sup>\<two>)\<^sup>-\<^sup>\<one>"
+abbreviation qneq_cube ("(_)\<^sup>-\<^sup>\<three>" [999] 999) where "u\<^sup>-\<^sup>\<three> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
+abbreviation qneq_quart ("(_)\<^sup>-\<^sup>\<four>" [999] 999) where "u\<^sup>-\<^sup>\<four> \<equiv> (u\<^sup>\<three>)\<^sup>-\<^sup>\<one>"
 
 instantiation tQuant :: (zero,si_type) zero
 begin
@@ -228,7 +250,7 @@ begin
   instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
 end
 
-lift_definition scaleQ :: "'a \<Rightarrow> 'a::times['u::si_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
+lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['u::si_type] \<Rightarrow> 'a['u]" (infixr "*\<^sub>Q" 63)
   is "\<lambda> r x. \<lparr> magn = r * magn x, unit = SI('u) \<rparr>" by simp
 
 notation scaleQ (infixr "\<odot>" 63)
@@ -241,70 +263,15 @@ translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)"
 
 subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
 
-definition [si_def]: "meter    = UNIT(1, Length)"
-definition [si_def]: "second   = UNIT(1, Time)"
-definition [si_def]: "kilogram = UNIT(1, Mass)"
-definition [si_def]: "ampere   = UNIT(1, Current)"
-definition [si_def]: "kelvin   = UNIT(1, Temperature)"
-definition [si_def]: "mole     = UNIT(1, Amount)"
-definition [si_def]: "candela  = UNIT(1, Intensity)"
+definition [si_def, si_eq]: "meter    = UNIT(1, Length)"
+definition [si_def, si_eq]: "second   = UNIT(1, Time)"
+definition [si_def, si_eq]: "kilogram = UNIT(1, Mass)"
+definition [si_def, si_eq]: "ampere   = UNIT(1, Current)"
+definition [si_def, si_eq]: "kelvin   = UNIT(1, Temperature)"
+definition [si_def, si_eq]: "mole     = UNIT(1, Amount)"
+definition [si_def, si_eq]: "candela  = UNIT(1, Intensity)"
 
 definition dimless ("\<one>") 
-  where [si_def]: "dimless  = UNIT(1, NoDimension)"
-
-subsubsection \<open>The Projection: Stripping the SI-Tags \<close>
-
-definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^sub>Q") where
-"magnQuant x = magn (fromUnit x)"
-
-subsubsection \<open>More Operations \<close>
-
-lemma unit_eq_iff_magn_eq:
-  "x = y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q"
-  by (auto simp add: magnQuant_def, transfer, simp)
-
-lemma unit_equiv_iff:
-  fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]"
-  shows "x \<approx>\<^sub>Q y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^sub>Q \<and> SI('u\<^sub>1) = SI('u\<^sub>2)"
-proof -
-  have "\<forall>t ta. (ta::'a['u\<^sub>2]) = t \<or> magn (fromUnit ta) \<noteq> magn (fromUnit t)"
-    by (simp add: magnQuant_def unit_eq_iff_magn_eq)
-  then show ?thesis
-    by (metis (full_types) Quant_equiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def)
-qed
-
-lemma unit_le_iff_magn_le:
-  "x \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
-  by (auto simp add: magnQuant_def; (transfer, simp))
-
-lemma magnQuant_zero [si_def]: "\<lbrakk>0\<rbrakk>\<^sub>Q = 0"
-  by (simp add: magnQuant_def, transfer, simp)
-
-lemma magnQuant_one [si_def]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
-  by (simp add: magnQuant_def, transfer, simp)
-
-lemma magnQuant_plus [si_def]: "\<lbrakk>x + y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q + \<lbrakk>y\<rbrakk>\<^sub>Q"
-  by (simp add: magnQuant_def, transfer, simp)
-
-lemma magnQuant_scaleQ [si_def]: "\<lbrakk>x *\<^sub>Q y\<rbrakk>\<^sub>Q = x * \<lbrakk>y\<rbrakk>\<^sub>Q"
-  by (simp add: magnQuant_def, transfer, simp)
-
-lemma magnQuant_qinv [si_def]: "\<lbrakk>x\<^sup>-\<^sup>\<one>\<rbrakk>\<^sub>Q = inverse \<lbrakk>x\<rbrakk>\<^sub>Q"
-  by (simp add: magnQuant_def, transfer, simp)
-
-lemma magnQuant_qdiv [si_def]: "\<lbrakk>(x::('a::field)[_]) \<^bold>/ y\<rbrakk>\<^sub>Q = \<lbrakk>x\<rbrakk>\<^sub>Q / \<lbrakk>y\<rbrakk>\<^sub>Q"
-  by (simp add: magnQuant_def, transfer, simp add: field_class.field_divide_inverse)
-
-lemma magnQuant_numeral [si_def]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral n"
-  apply (induct n, simp_all add: si_def)
-  apply (metis magnQuant_plus numeral_code(2))
-  apply (metis magnQuant_one magnQuant_plus numeral_code(3))
-  done
-
-lemma magnQuant_mk [si_def]: "\<lbrakk>UNIT(n, 'u::si_type)\<rbrakk>\<^sub>Q = n"
-  by (simp add: magnQuant_def, transfer, simp)
-
-method si_calc = 
-  (simp add: unit_eq_iff_magn_eq unit_le_iff_magn_le si_def)
+  where [si_def, si_eq]: "dimless  = UNIT(1, NoDimension)"
 
 end
\ No newline at end of file
diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy
index e899f20..710f1e2 100644
--- a/src/SI/SI_Units.thy
+++ b/src/SI/SI_Units.thy
@@ -6,7 +6,7 @@ theory SI_Units
           "HOL-Eisbach.Eisbach"
 begin
 
-named_theorems si_def
+named_theorems si_def and si_eq
 
 text\<open>
 The International System of Units (SI, abbreviated from the French