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

Some tidying of the proof strategy and derived properties

This commit is contained in:
Simon Foster 2020-02-20 09:53:45 +00:00
parent 1de90a23b2
commit c40088199c
7 changed files with 104 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/SI/SI_Algebra.thy
View File

@ -7,45 +7,37 @@ 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)
by (si_simp add: distrib_left)
lemma scaleQ_add_left: "a + b \<odot> x = (a \<odot> x) + (b \<odot> x)"
by (transfer, simp add: distrib_right)
by (si_simp add: distrib_right)
lemma scaleQ_scaleQ: "a \<odot> b \<odot> x = a \<cdot> b \<odot> x"
by (transfer, simp add: mult.assoc)
by si_simp
lemma scaleQ_one [simp]: "1 \<odot> x = x"
by (transfer, simp)
by si_simp
lemma scaleQ_zero [simp]: "0 \<odot> x = 0"
by (transfer, simp)
by si_simp
lemma scaleQ_inv: "-a \<odot> x = a \<odot> -x"
by (transfer, simp)
by si_calc
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)
by si_calc
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)
by (si_simp add: 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)
by si_simp
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)

14
src/SI/SI_Derived.thy
View File

@ -24,16 +24,18 @@ abbreviation "tesla \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>-\<^sup>\<two>
abbreviation "henry \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<two>"
definition degrees_celcius :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
where [si_def, si_eq]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
definition degrees_celcius :: "'a::field_char_0 \<Rightarrow> 'a[\<Theta>]" ("_\<degree>C" [999] 999)
where [si_eq]: "degrees_celcius x = x + 273.151 \<odot> kelvin"
definition degrees_farenheit :: "'a::field \<Rightarrow> 'a[\<Theta>]" ("_\<degree>F" [999] 999)
where [si_def, si_eq]: "degrees_farenheit x = (x + 459.67)\<cdot>5/9 \<odot> kelvin"
definition [si_def, si_eq]: "gram = milli \<odot> kilogram"
definition [si_eq]: "gram = milli \<odot> kilogram"
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> Properties \<close>
lemma kilogram: "kilo \<odot> gram = kilogram"
by (si_simp)
end

10
src/SI/SI_Imperial.thy
View File

@ -4,6 +4,11 @@ theory SI_Imperial
imports SI_Accepted
begin
subsection \<open> Definition \<close>
definition degrees_farenheit :: "'a::field_char_0 \<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 [si_def, si_eq]: "inch = 25.5 \<odot> milli \<odot> meter"
@ -12,4 +17,9 @@ definition [si_def, si_eq]: "foot = 0.3048 \<odot> meter"
definition [si_def, si_eq]: "yard = 0.9144 \<odot> meter"
subsection \<open> Properties \<close>
lemma celcius_to_farenheit: "(T::rat)\<degree>C = ((T - 32) \<cdot> 5/9)\<degree>F"
oops
end

30
src/SI/SI_Prefix.thy
View File

@ -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

44
src/SI/SI_Proof.thy
View File

@ -4,14 +4,16 @@ theory SI_Proof
imports SI_Quantities
begin
named_theorems si_transfer
definition magnQuant :: "'a['u::si_type] \<Rightarrow> 'a" ("\<lbrakk>_\<rbrakk>\<^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 \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q = \<lbrakk>y\<rbrakk>\<^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 \<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 -
@ -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 \<le> y \<longleftrightarrow> \<lbrakk>x\<rbrakk>\<^sub>Q \<le> \<lbrakk>y\<rbrakk>\<^sub>Q"
by (auto simp add: magnQuant_def; (transfer, simp))
@ -34,6 +36,12 @@ lemma magnQuant_one [si_eq]: "\<lbrakk>1\<rbrakk>\<^sub>Q = 1"
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_minus [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_uminus [si_eq]: "\<lbrakk>- x\<rbrakk>\<^sub>Q = - \<lbrakk>x\<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)
@ -53,12 +61,20 @@ lemma magnQuant_numeral [si_eq]: "\<lbrakk>numeral n\<rbrakk>\<^sub>Q = numeral
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"
lemma magnQuant_mk [si_eq]: "\<lbrakk>UNIT('u::si_type)\<rbrakk>\<^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 \<open> The following tactic breaks an SI conjecture down to numeric and unit properties \<close>
method si_simp uses add =
(simp add: add si_transfer si_eq)
text \<open> The next tactic additionally compiles the semantics of the underlying units \<close>
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\<lparr>Meters := 1\<rparr>" by(simp add: si_def)
lemma "SI(M) = 1\<lparr>Kilograms := 1\<rparr>" by(simp add: si_def)
lemma "SI(T) = 1\<lparr>Seconds := 1\<rparr> " by(simp add: si_def)
lemma "SI(I) = 1\<lparr>Amperes := 1\<rparr>" by(simp add: si_def)
lemma "SI(\<Theta>) = 1\<lparr>Kelvins := 1\<rparr> " by(simp add: si_def)
lemma "SI(N) = 1\<lparr>Moles := 1\<rparr>" by(simp add: si_def)
lemma "SI(J) = 1\<lparr>Candelas := 1\<rparr>" by(simp add: si_def)
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(N \<cdot> \<Theta> \<cdot> N) = SI(\<Theta> \<cdot> N\<^sup>2)" by (simp add: si_eq si_def)
lemma "(meter \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q meter"
by (si_calc)
end

24
src/SI/SI_Quantities.thy
View File

@ -255,23 +255,23 @@ lift_definition scaleQ :: "'a \<Rightarrow> 'a::comm_ring_1['u::si_type] \<Right
notation scaleQ (infixr "\<odot>" 63)
lift_definition mk_unit :: "'a \<Rightarrow> 'u itself \<Rightarrow> ('a::one)['u::si_type]"
is "\<lambda> n u. \<lparr> magn = n, unit = SI('u) \<rparr>" by simp
lift_definition mk_unit :: "'u itself \<Rightarrow> ('a::one)['u::si_type]"
is "\<lambda> u. \<lparr> magn = 1, unit = SI('u) \<rparr>" by simp
syntax "_mk_unit" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("UNIT'(_, _')")
translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)"
syntax "_mk_unit" :: "type \<Rightarrow> logic" ("UNIT'(_')")
translations "UNIT('a)" == "CONST mk_unit TYPE('a)"
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
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 ("\<one>")
where [si_def, si_eq]: "dimless = UNIT(1, NoDimension)"
where [si_eq]: "dimless = UNIT(NoDimension)"
end

39
src/SI/SI_Units.thy
View File

@ -56,13 +56,6 @@ record Unit =
Moles :: int
Candelas :: int
text \<open> Units scaled by a power of 10 \<close>
type_synonym SUnit = "int Unit_ext"
abbreviation scale :: "SUnit \<Rightarrow> int" where
"scale \<equiv> more"
text \<open> We define a commutative monoid for SI units. \<close>
instantiation Unit_ext :: (one) one
@ -109,7 +102,7 @@ definition inverse_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext"
, Candelas = - Candelas x, \<dots> = inverse (more x) \<rparr>"
definition divide_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext \<Rightarrow> '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\<open>We embed the basic SI types into the SI type expressions: \<close>
instantiation Length :: si_baseunit
begin
definition si_sem_Length :: "Length itself \<Rightarrow> Unit" where "si_sem_Length x = 1\<lparr>Meters := 1\<rparr>"
definition si_sem_Length :: "Length itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Length x = 1\<lparr>Meters := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Mass x = 1\<lparr>Kilograms := 1\<rparr>"
definition si_sem_Mass :: "Mass itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Mass x = 1\<lparr>Kilograms := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Time x = 1\<lparr>Seconds := 1\<rparr>"
definition si_sem_Time :: "Time itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Time x = 1\<lparr>Seconds := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Current x = 1\<lparr>Amperes := 1\<rparr>"
definition si_sem_Current :: "Current itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Current x = 1\<lparr>Amperes := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Temperature x = 1\<lparr>Kelvins := 1\<rparr>"
definition si_sem_Temperature :: "Temperature itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Temperature x = 1\<lparr>Kelvins := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Amount x = 1\<lparr>Moles := 1\<rparr>"
definition si_sem_Amount :: "Amount itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Amount x = 1\<lparr>Moles := 1\<rparr>"
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 \<Rightarrow> Unit" where "si_sem_Intensity x = 1\<lparr>Candelas := 1\<rparr>"
definition si_sem_Intensity :: "Intensity itself \<Rightarrow> Unit"
where [si_def]: "si_sem_Intensity x = 1\<lparr>Candelas := 1\<rparr>"
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 \<Rightarrow> 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 \<Rightarrow> 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 \<open> 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 \<cdot> 'b) itself \<Rightarrow> 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 \<Rightarrow> 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