diff --git a/src/SI/SI_Algebra.thy b/src/SI/SI_Algebra.thy index 69f7007..82095fc 100644 --- a/src/SI/SI_Algebra.thy +++ b/src/SI/SI_Algebra.thy @@ -7,45 +7,37 @@ begin subsection \ Quantity Scale \ lemma scaleQ_add_right: "a \ x + y = (a \ x) + (a \ y)" - by (transfer, simp add: distrib_left) + by (si_simp add: distrib_left) lemma scaleQ_add_left: "a + b \ x = (a \ x) + (b \ x)" - by (transfer, simp add: distrib_right) + by (si_simp add: distrib_right) lemma scaleQ_scaleQ: "a \ b \ x = a \ b \ x" - by (transfer, simp add: mult.assoc) + by si_simp lemma scaleQ_one [simp]: "1 \ x = x" - by (transfer, simp) + by si_simp lemma scaleQ_zero [simp]: "0 \ x = 0" - by (transfer, simp) + by si_simp lemma scaleQ_inv: "-a \ x = a \ -x" - by (transfer, simp) + by si_calc lemma scaleQ_as_qprod: "a \ x \\<^sub>Q (a \ \) \<^bold>\ x" - unfolding si_def - by (transfer, simp add: si_sem_NoDimension_def) + by si_calc lemma mult_scaleQ_left [simp]: "(a \ x) \<^bold>\ y = a \ x \<^bold>\ y" - by (transfer, simp add: si_sem_UnitTimes_def mult.assoc) + by (si_simp add: mult.assoc) lemma mult_scaleQ_right [simp]: "x \<^bold>\ (a \ y) = a \ x \<^bold>\ y" - by (transfer, simp add: si_sem_UnitTimes_def times_Quantity_ext_def mult.assoc) + by si_simp subsection \ Field Laws \ lemma qtimes_commute: "x \<^bold>\ y \\<^sub>Q y \<^bold>\ x" by si_calc -text\Observe that this commutation law also commutes the types.\ - -(* just a check that instantiation works for special cases ... *) -lemma " (UNIT(x, J) \<^bold>\ UNIT(y::'a::comm_ring_1, N)) - \\<^sub>Q (UNIT(y, N) \<^bold>\ UNIT(x, J)) " - by(simp add: qtimes_commute) - lemma qtimes_assoc: "(x \<^bold>\ y) \<^bold>\ z \\<^sub>Q x \<^bold>\ (y \<^bold>\ z)" by (si_calc) diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy index 15a1067..5640f75 100644 --- a/src/SI/SI_Derived.thy +++ b/src/SI/SI_Derived.thy @@ -24,16 +24,18 @@ abbreviation "tesla \ kilogram \<^bold>\ meter\<^sup>-\<^sup>\ abbreviation "henry \ kilogram \<^bold>\ meter\<^sup>\ \<^bold>\ second\<^sup>-\<^sup>\ \<^bold>\ ampere\<^sup>-\<^sup>\" -definition degrees_celcius :: "'a::field \ 'a[\]" ("_\C" [999] 999) - where [si_def, si_eq]: "degrees_celcius x = x + 273.151 \ kelvin" +definition degrees_celcius :: "'a::field_char_0 \ 'a[\]" ("_\C" [999] 999) + where [si_eq]: "degrees_celcius x = x + 273.151 \ kelvin" -definition degrees_farenheit :: "'a::field \ 'a[\]" ("_\F" [999] 999) - where [si_def, si_eq]: "degrees_farenheit x = (x + 459.67)\5/9 \ kelvin" - -definition [si_def, si_eq]: "gram = milli \ kilogram" +definition [si_eq]: "gram = milli \ kilogram" 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]" +subsection \ Properties \ + +lemma kilogram: "kilo \ gram = kilogram" + by (si_simp) + end \ No newline at end of file diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy index bd20fcf..45eef91 100644 --- a/src/SI/SI_Imperial.thy +++ b/src/SI/SI_Imperial.thy @@ -4,6 +4,11 @@ theory SI_Imperial imports SI_Accepted begin +subsection \ Definition \ + +definition degrees_farenheit :: "'a::field_char_0 \ 'a[\]" ("_\F" [999] 999) + where [si_eq]: "degrees_farenheit x = (x + 459.67)\5/9 \ kelvin" + definition [si_def, si_eq]: "pint = 0.56826125 \ litre" definition [si_def, si_eq]: "inch = 25.5 \ milli \ meter" @@ -12,4 +17,9 @@ definition [si_def, si_eq]: "foot = 0.3048 \ meter" definition [si_def, si_eq]: "yard = 0.9144 \ meter" +subsection \ Properties \ + +lemma celcius_to_farenheit: "(T::rat)\C = ((T - 32) \ 5/9)\F" + oops + end \ No newline at end of file diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy index 0ed5bd9..a53ce1e 100644 --- a/src/SI/SI_Prefix.thy +++ b/src/SI/SI_Prefix.thy @@ -4,28 +4,34 @@ theory SI_Prefix imports SI_Constants begin -definition [si_def]: "deca = 10^1" +default_sort ring_char_0 -definition [si_def]: "hecto = 10^2" +definition deca :: "'a" where [si_eq]: "deca = 10^1" -definition [si_def]: "kilo = 10^3" +definition hecto :: "'a" where [si_eq]: "hecto = 10^2" -definition [si_def]: "mega = 10^6" +definition kilo :: "'a" where [si_eq]: "kilo = 10^3" -definition [si_def]: "giga = 10^9" +definition mega :: "'a" where [si_eq]: "mega = 10^6" -definition [si_def]: "tera = 10^12" +definition giga :: "'a" where [si_eq]: "giga = 10^9" -definition [si_def]: "peta = 10^15" +definition tera :: "'a" where [si_eq]: "tera = 10^12" -definition [si_def]: "deci = 1/10^1" +definition peta :: "'a" where [si_eq]: "peta = 10^15" -definition [si_def]: "centi = 1/10^2" +default_sort field_char_0 -definition [si_def]: "milli = 1/10^3" +definition deci :: "'a" where [si_eq]: "deci = 1/10^1" -definition [si_def]: "micro = 1/10^6" +definition centi :: "'a" where [si_eq]: "centi = 1/10^2" -definition [si_def]: "nano = 1/10^9" +definition milli :: "'a" where [si_eq]: "milli = 1/10^3" + +definition micro :: "'a" where [si_eq]: "micro = 1/10^6" + +definition nano :: "'a" where [si_eq]: "nano = 1/10^9" + +default_sort type end \ No newline at end of file diff --git a/src/SI/SI_Proof.thy b/src/SI/SI_Proof.thy index dcc424f..c558fca 100644 --- a/src/SI/SI_Proof.thy +++ b/src/SI/SI_Proof.thy @@ -4,14 +4,16 @@ theory SI_Proof imports SI_Quantities begin +named_theorems si_transfer + definition magnQuant :: "'a['u::si_type] \ 'a" ("\_\\<^sub>Q") where [si_def]: "magnQuant x = magn (fromQ x)" -lemma unit_eq_iff_magn_eq: +lemma unit_eq_iff_magn_eq [si_transfer]: "x = y \ \x\\<^sub>Q = \y\\<^sub>Q" by (auto simp add: magnQuant_def, transfer, simp) -lemma unit_equiv_iff: +lemma unit_equiv_iff [si_transfer]: fixes x :: "'a['u\<^sub>1::si_type]" and y :: "'a['u\<^sub>2::si_type]" shows "x \\<^sub>Q y \ \x\\<^sub>Q = \y\\<^sub>Q \ SI('u\<^sub>1) = SI('u\<^sub>2)" proof - @@ -21,7 +23,7 @@ proof - by (metis (full_types) qequiv.rep_eq coerceQuant_eq_iff2 eq_ magnQuant_def) qed -lemma unit_le_iff_magn_le: +lemma unit_le_iff_magn_le [si_transfer]: "x \ y \ \x\\<^sub>Q \ \y\\<^sub>Q" by (auto simp add: magnQuant_def; (transfer, simp)) @@ -34,6 +36,12 @@ lemma magnQuant_one [si_eq]: "\1\\<^sub>Q = 1" lemma magnQuant_plus [si_eq]: "\x + y\\<^sub>Q = \x\\<^sub>Q + \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp) +lemma magnQuant_minus [si_eq]: "\x - y\\<^sub>Q = \x\\<^sub>Q - \y\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + +lemma magnQuant_uminus [si_eq]: "\- x\\<^sub>Q = - \x\\<^sub>Q" + by (simp add: magnQuant_def, transfer, simp) + lemma magnQuant_scaleQ [si_eq]: "\x *\<^sub>Q y\\<^sub>Q = x * \y\\<^sub>Q" by (simp add: magnQuant_def, transfer, simp) @@ -53,12 +61,20 @@ lemma magnQuant_numeral [si_eq]: "\numeral n\\<^sub>Q = numeral apply (metis magnQuant_def magnQuant_one magnQuant_plus numeral_code(3)) done -lemma magnQuant_mk [si_eq]: "\UNIT(n, 'u::si_type)\\<^sub>Q = n" +lemma magnQuant_mk [si_eq]: "\UNIT('u::si_type)\\<^sub>Q = 1" 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) +text \ The following tactic breaks an SI conjecture down to numeric and unit properties \ +method si_simp uses add = + (simp add: add si_transfer si_eq) + +text \ The next tactic additionally compiles the semantics of the underlying units \ + +method si_calc uses add = + (si_simp add: add; simp add: si_def add) + +(* 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 @@ -71,17 +87,11 @@ lemmas [si_def] = si_sem_Length_def si_sem_Mass_def si_sem_Time_def si_sem_UnitTimes_def si_sem_UnitInv_def times_Unit_ext_def one_Unit_ext_def - -(* renaming and putting defs into the rewrite set (which is usually not a good idea) *) -lemma "SI(L) = 1\Meters := 1\" by(simp add: si_def) -lemma "SI(M) = 1\Kilograms := 1\" by(simp add: si_def) -lemma "SI(T) = 1\Seconds := 1\ " by(simp add: si_def) -lemma "SI(I) = 1\Amperes := 1\" by(simp add: si_def) -lemma "SI(\) = 1\Kelvins := 1\ " by(simp add: si_def) -lemma "SI(N) = 1\Moles := 1\" by(simp add: si_def) -lemma "SI(J) = 1\Candelas := 1\" by(simp add: si_def) -lemma "SI(\) = 1" by(simp add: si_def) +*) -lemma "SI(N \ \ \ N) = SI(\ \ N\<^sup>2)" by(simp add: si_def) +lemma "SI(N \ \ \ N) = SI(\ \ N\<^sup>2)" by (simp add: si_eq si_def) + +lemma "(meter \<^bold>\ second\<^sup>-\<^sup>\) \<^bold>\ second \\<^sub>Q meter" + by (si_calc) end \ No newline at end of file diff --git a/src/SI/SI_Quantities.thy b/src/SI/SI_Quantities.thy index 0677f49..3b7a250 100644 --- a/src/SI/SI_Quantities.thy +++ b/src/SI/SI_Quantities.thy @@ -255,23 +255,23 @@ lift_definition scaleQ :: "'a \ 'a::comm_ring_1['u::si_type] \" 63) -lift_definition mk_unit :: "'a \ 'u itself \ ('a::one)['u::si_type]" - is "\ n u. \ magn = n, unit = SI('u) \" by simp +lift_definition mk_unit :: "'u itself \ ('a::one)['u::si_type]" + is "\ u. \ magn = 1, unit = SI('u) \" by simp -syntax "_mk_unit" :: "logic \ type \ logic" ("UNIT'(_, _')") -translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)" +syntax "_mk_unit" :: "type \ logic" ("UNIT'(_')") +translations "UNIT('a)" == "CONST mk_unit TYPE('a)" subsection \Polymorphic Operations for Elementary SI Units \ -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 [si_eq]: "meter = UNIT(Length)" +definition [si_eq]: "second = UNIT(Time)" +definition [si_eq]: "kilogram = UNIT(Mass)" +definition [si_eq]: "ampere = UNIT(Current)" +definition [si_eq]: "kelvin = UNIT(Temperature)" +definition [si_eq]: "mole = UNIT(Amount)" +definition [si_eq]: "candela = UNIT(Intensity)" definition dimless ("\") - where [si_def, si_eq]: "dimless = UNIT(1, NoDimension)" + where [si_eq]: "dimless = UNIT(NoDimension)" end \ No newline at end of file diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index 5882ef1..8b4c998 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -56,13 +56,6 @@ record Unit = Moles :: int Candelas :: int -text \ Units scaled by a power of 10 \ - -type_synonym SUnit = "int Unit_ext" - -abbreviation scale :: "SUnit \ int" where -"scale \ more" - text \ We define a commutative monoid for SI units. \ instantiation Unit_ext :: (one) one @@ -109,7 +102,7 @@ definition inverse_Unit_ext :: "'a Unit_ext \ 'a Unit_ext" , Candelas = - Candelas x, \ = inverse (more x) \" definition divide_Unit_ext :: "'a Unit_ext \ 'a Unit_ext \ 'a Unit_ext" - where [code_unfold]: + where [code_unfold, si_def]: "divide_Unit_ext x y = x * (inverse y)" instance .. end @@ -226,50 +219,58 @@ text\We embed the basic SI types into the SI type expressions: \ instantiation Length :: si_baseunit begin - definition si_sem_Length :: "Length itself \ Unit" where "si_sem_Length x = 1\Meters := 1\" +definition si_sem_Length :: "Length itself \ Unit" + where [si_def]: "si_sem_Length x = 1\Meters := 1\" instance by (intro_classes, auto simp add: si_sem_Length_def is_BaseUnit_def, (transfer, simp)+) end instantiation Mass :: si_baseunit begin - definition si_sem_Mass :: "Mass itself \ Unit" where "si_sem_Mass x = 1\Kilograms := 1\" +definition si_sem_Mass :: "Mass itself \ Unit" + where [si_def]: "si_sem_Mass x = 1\Kilograms := 1\" instance by (intro_classes, auto simp add: si_sem_Mass_def is_BaseUnit_def, (transfer, simp)+) end instantiation Time :: si_baseunit begin - definition si_sem_Time :: "Time itself \ Unit" where "si_sem_Time x = 1\Seconds := 1\" +definition si_sem_Time :: "Time itself \ Unit" + where [si_def]: "si_sem_Time x = 1\Seconds := 1\" instance by (intro_classes, auto simp add: si_sem_Time_def is_BaseUnit_def, (transfer, simp)+) end instantiation Current :: si_baseunit begin - definition si_sem_Current :: "Current itself \ Unit" where "si_sem_Current x = 1\Amperes := 1\" +definition si_sem_Current :: "Current itself \ Unit" + where [si_def]: "si_sem_Current x = 1\Amperes := 1\" instance by (intro_classes, auto simp add: si_sem_Current_def is_BaseUnit_def, (transfer, simp)+) end instantiation Temperature :: si_baseunit begin - definition si_sem_Temperature :: "Temperature itself \ Unit" where "si_sem_Temperature x = 1\Kelvins := 1\" +definition si_sem_Temperature :: "Temperature itself \ Unit" + where [si_def]: "si_sem_Temperature x = 1\Kelvins := 1\" instance by (intro_classes, auto simp add: si_sem_Temperature_def is_BaseUnit_def, (transfer, simp)+) end instantiation Amount :: si_baseunit begin - definition si_sem_Amount :: "Amount itself \ Unit" where "si_sem_Amount x = 1\Moles := 1\" +definition si_sem_Amount :: "Amount itself \ Unit" + where [si_def]: "si_sem_Amount x = 1\Moles := 1\" instance by (intro_classes, auto simp add: si_sem_Amount_def is_BaseUnit_def, (transfer, simp)+) end instantiation Intensity :: si_baseunit begin - definition si_sem_Intensity :: "Intensity itself \ Unit" where "si_sem_Intensity x = 1\Candelas := 1\" +definition si_sem_Intensity :: "Intensity itself \ Unit" + where [si_def]: "si_sem_Intensity x = 1\Candelas := 1\" instance by (intro_classes, auto simp add: si_sem_Intensity_def is_BaseUnit_def, (transfer, simp)+) end instantiation NoDimension :: si_type begin - definition si_sem_NoDimension :: "NoDimension itself \ Unit" where "si_sem_NoDimension x = 1" - instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseUnit_def, (transfer, simp)+) +definition si_sem_NoDimension :: "NoDimension itself \ Unit" + where [si_def]: "si_sem_NoDimension x = 1" +instance by (intro_classes, auto simp add: si_sem_NoDimension_def is_BaseUnit_def, (transfer, simp)+) end lemma base_units [simp]: @@ -289,7 +290,7 @@ text \ We can prove that multiplication of two SI types yields an SI type. instantiation UnitTimes :: (si_type, si_type) si_type begin definition si_sem_UnitTimes :: "('a \ 'b) itself \ Unit" where - "si_sem_UnitTimes x = SI('a) * SI('b)" + [si_eq]: "si_sem_UnitTimes x = SI('a) * SI('b)" instance by (intro_classes, simp_all add: si_sem_UnitTimes_def, (transfer, simp)+) end @@ -300,7 +301,7 @@ setup_lifting type_definition_UnitInv instantiation UnitInv :: (si_type) si_type begin definition si_sem_UnitInv :: "('a\<^sup>-\<^sup>1) itself \ Unit" where - "si_sem_UnitInv x = inverse SI('a)" + [si_eq]: "si_sem_UnitInv x = inverse SI('a)" instance by (intro_classes, simp_all add: si_sem_UnitInv_def, (transfer, simp)+) end