From b8e347b4c8850d7219f5a7a47ba75f25d1d746d5 Mon Sep 17 00:00:00 2001 From: Simon Foster Date: Tue, 18 Feb 2020 20:31:05 +0000 Subject: [PATCH] Removed the scalar product and associated class instantiations in favour of scaleQ --- src/SI/SI_Constants.thy | 5 +-- src/SI/SI_Derived.thy | 3 +- src/SI/SI_Quantities.thy | 70 ---------------------------------------- 3 files changed, 2 insertions(+), 76 deletions(-) diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy index 71e66d6..8080420 100644 --- a/src/SI/SI_Constants.thy +++ b/src/SI/SI_Constants.thy @@ -56,10 +56,7 @@ theorem Quant_eq_iff_same_dim: "x \\<^sub>Q y \ x = y" by (transfer, simp) -theorem hertz_definition: "1\hertz = \v\<^sub>C\<^sub>s / 9192631770" - by (simp add: unit_eq_iff_magn_eq si_def) - -theorem second_definition: "1\second \\<^sub>Q (9192631770 \ \) \<^bold>/ \v\<^sub>C\<^sub>s" +theorem second_definition: "1 \ second \\<^sub>Q (9192631770 \ \) \<^bold>/ \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 diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index 7408191..b7664d5 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -5,7 +5,7 @@ theory SI_Derived begin definition degree :: "'a::{inverse,real_algebra_1}[L/L]" where -[si_def]: "degree = (2\(UNIT(of_real pi,_)) / 180)\radian" +[si_def]: "degree = (2\(of_real pi) / 180) \ radian" abbreviation degrees ("_\" [999] 999) where "n\ \ n \ degree" @@ -35,7 +35,6 @@ definition "foot = 0.3048 \ meter" definition "yard = 0.9144 \ meter" - text\The full beauty of the approach is perhaps revealed here, with the type of a classical three-dimensional gravitation field:\ type_synonym gravitation_field = "(real\<^sup>3 \ real\<^sup>3)[L \ T\<^sup>-\<^sup>2]" diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index 0da6757..b8d8036 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -221,70 +221,6 @@ instance tQuant :: (numeral,si_type) numeral .. instance tQuant :: (ab_group_add,si_type) ab_group_add by (intro_classes, (transfer, simp)+) -instantiation tQuant :: (times,si_type) times -begin -lift_definition times_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" - is "\ x y. \ magn = magn x * magn y, unit = SI('b) \" - by simp -instance .. -end - -instance tQuant :: (power,si_type) power .. - -instance tQuant :: (semigroup_mult,si_type) semigroup_mult - by (intro_classes, transfer, simp add: mult.assoc) - -instance tQuant :: (ab_semigroup_mult,si_type) ab_semigroup_mult - by (intro_classes, (transfer, simp add: mult.commute)) - -instance tQuant :: (semiring,si_type) semiring - by (intro_classes, (transfer, simp add: distrib_left distrib_right)+) - -instance tQuant :: (semiring_0,si_type) semiring_0 - by (intro_classes, (transfer, simp)+) - -instance tQuant :: (comm_semiring,si_type) comm_semiring - by (intro_classes, transfer, simp add: linordered_field_class.sign_simps(18) mult.commute) - -instance tQuant :: (mult_zero,si_type) mult_zero - by (intro_classes, (transfer, simp)+) - -instance tQuant :: (comm_semiring_0,si_type) comm_semiring_0 - by (intro_classes, (transfer, simp)+) - -instantiation tQuant :: (real_vector,si_type) real_vector -begin - -lift_definition scaleR_tQuant :: "real \ 'a['b] \ 'a['b]" - is "\ r x. \ magn = r *\<^sub>R magn x, unit = unit x \" by simp - -instance - by (intro_classes, (transfer, simp add: scaleR_add_left scaleR_add_right)+) -end - -instance tQuant :: (ring,si_type) ring - by (intro_classes, (transfer, simp)+) - -instance tQuant :: (comm_monoid_mult,si_type) comm_monoid_mult - by (intro_classes, (transfer, simp add: mult.commute)+) - -instance tQuant :: (comm_semiring_1,si_type) comm_semiring_1 - by (intro_classes; (transfer, simp add: semiring_normalization_rules(1-8,24))) - -instantiation tQuant :: (divide,si_type) divide -begin -lift_definition divide_tQuant :: "'a['b] \ 'a['b] \ 'a['b]" - is "\ x y. \ magn = magn x div magn y, unit = SI('b) \" by simp -instance .. -end - -instantiation tQuant :: (inverse,si_type) inverse -begin -lift_definition inverse_tQuant :: "'a['b] \ 'a['b]" - is "\ x. \ magn = inverse (magn x), unit = SI('b) \" by simp -instance .. -end - instantiation tQuant :: (order,si_type) order begin lift_definition less_eq_tQuant :: "'a['b] \ 'a['b] \ bool" is "\ x y. magn x \ magn y" . @@ -350,15 +286,9 @@ lemma magnQuant_one [si_def]: "\1\\<^sub>Q = 1" lemma magnQuant_plus [si_def]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp) -lemma magnQuant_times [si_def]: "\x * y\\<^sub>Q = \x\\<^sub>Q * \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) - lemma magnQuant_scaleQ [si_def]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp) -lemma magnQuant_div [si_def]: "\x / y\\<^sub>Q = \x\\<^sub>Q / \y\\<^sub>Q" - by (simp add: magnQuant_def, transfer, simp) - lemma magnQuant_qinv [si_def]: "\x\<^sup>-\<^sup>\\\<^sub>Q = inverse \x\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp)