diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy index 819393b..d0e0259 100644 --- a/src/SI/Groups_mult.thy +++ b/src/SI/Groups_mult.thy @@ -1,4 +1,4 @@ -section \ Multiplication Group Classes \ +chapter \ Multiplicative Groups \ theory Groups_mult imports Main diff --git a/src/SI/ISQ.thy b/src/SI/ISQ.thy new file mode 100644 index 0000000..53f6142 --- /dev/null +++ b/src/SI/ISQ.thy @@ -0,0 +1,3 @@ +theory ISQ + imports ISQ_Dimensions ISQ_Quantities ISQ_Proof ISQ_Algebra +begin end \ No newline at end of file diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy index 39b2185..8439e77 100644 --- a/src/SI/ISQ_Dimensions.thy +++ b/src/SI/ISQ_Dimensions.thy @@ -1,4 +1,6 @@ -section \ Dimensions \ +chapter \ International System of Quantities \ + +section \ Quantity Dimensions \ theory ISQ_Dimensions imports Groups_mult diff --git a/src/SI/ROOT b/src/SI/ROOT index a475f2a..714c21a 100644 --- a/src/SI/ROOT +++ b/src/SI/ROOT @@ -43,14 +43,14 @@ (* $Id:$ *) session "SI" = Main + - description {* SI Unit Support *} + description \ SI Unit Support \ options [document = pdf, document_output = "document/output", document_variants="document:outline=/proof,/ML"] sessions "HOL-Eisbach" theories - "SI_Accepted" - "SI_Imperial" + "ISQ" + "SI" document_files "root.tex" "adb-long.bib" diff --git a/src/SI/SI.thy b/src/SI/SI.thy index ad547e1..c3d961b 100644 --- a/src/SI/SI.thy +++ b/src/SI/SI.thy @@ -1,148 +1,3 @@ -theory SI - imports Main -begin - - -section\SI's as Values.\ - -record SI = - Second :: int - Meter :: int - Kilogram :: int - Ampere :: int - Kelvin :: int - Mole :: int - Candela :: int - - -definition ONE_SI::"SI" ("1\<^sub>S\<^sub>I") - where "1\<^sub>S\<^sub>I = (\ Second = 0::int, Meter = 0::int, Kilogram = 0::int, - Ampere = 0::int, Kelvin = 0::int, Mole = 0::int, - Candela = 0::int, \ = () \)" - - -text\Example: Watt is \kg\m\<^sup>2\s\<^sup>−\<^sup>3\. Joule is \kg\m\<^sup>2\s\<^sup>−\<^sup>2\. \ -definition "Watt \ \ Second = -3, Meter = 2, Kilogram = 1, - Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \" -definition "Joule\ \ Second = -2, Meter = 2, Kilogram = 1, - Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \" -definition "Hertz\ 1\<^sub>S\<^sub>I\Second := -1\" - -value " Watt = \ Second = -2, Meter = 1, Kilogram = 7, - Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0\" - -class unit\<^sub>C = - fixes id :: "'a \ 'a" (* hack *) - assumes endo: "\x\(UNIV::'a set). \y\(UNIV::'a set). x = y" - -instantiation unit :: unit\<^sub>C -begin -definition "id = (\x::unit. x) " -instance proof(intro_classes) - show " \x\(UNIV:: unit set). \y\UNIV. x = y" - by auto - qed -end - - -instantiation SI_ext :: (unit\<^sub>C) one -begin -definition "(1::('a::unit\<^sub>C)SI_ext) = - \ Second = 0::int, Meter = 0::int, Kilogram = 0::int, - Ampere = 0::int, Kelvin = 0::int, Mole = 0::int, - Candela = 0::int, - \ = undefined \" -instance .. -end - - -lemma XXX [code_unfold] : "(1::SI) = 1\<^sub>S\<^sub>I " - by (simp add: one_SI_ext_def ONE_SI_def) - -term "one ::('a::unit\<^sub>C)SI_ext " -term "1 ::('a::unit\<^sub>C)SI_ext " -term "(1::SI)\ more := () \ \Second := -1\ " -value "1\<^sub>S\<^sub>I \Second := -1\ " - -instantiation SI_ext :: (unit\<^sub>C) times -begin -definition "(X::('a::unit\<^sub>C)SI_ext) * Y = - \ Second = Second X + Second Y, - Meter = Meter X + Meter Y, - Kilogram = Kilogram X + Kilogram Y, - Ampere = Ampere X + Ampere Y, - Kelvin = Kelvin X + Kelvin Y, - Mole = Mole X + Mole Y, - Candela = Candela X + Candela Y, - \ = undefined \" -instance .. -end - -term "set" -lemma YYY [code_unfold] : - "(X::SI) * Y = \ Second = Second X + Second Y, - Meter = Meter X + Meter Y, - Kilogram = Kilogram X + Kilogram Y, - Ampere = Ampere X + Ampere Y, - Kelvin = Kelvin X + Kelvin Y, - Mole = Mole X + Mole Y, - Candela = Candela X + Candela Y, - \ = () \ " - by (simp add: times_SI_ext_def) - - -instantiation SI_ext :: (unit\<^sub>C) comm_monoid_mult -begin -instance proof(intro_classes) - fix a b c show "(a:: ('a)SI_ext) * b * c = a * (b * c)" - unfolding times_SI_ext_def - by (auto simp: mult.assoc ) -next - fix a b show "(a:: ('a)SI_ext) * b = b * a" - unfolding times_SI_ext_def - by (auto simp: mult.commute ) -next - fix a::"('a::unit\<^sub>C)SI_ext" show "1 * a = a" - unfolding times_SI_ext_def one_SI_ext_def - apply (auto simp: mult.commute, rule sym) - apply(subst surjective) - by (metis UNIV_I endo) - qed -end - -value "Hertz * 1\<^sub>S\<^sub>I " -value "Watt = Joule * Hertz" - - -section\SI's as Types.\ - - -class si = one + ab_semigroup_mult + - fixes second :: "'a \ int" - fixes meter :: "'a \ int" - fixes kilogram :: "'a \ int" - fixes ampere :: "'a \ int" - fixes kelvin :: "'a \ int" - fixes mole :: "'a \ int" - fixes candela :: "'a \ int" - -definition si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e :: "'a::si \ 'b::si \ bool" - where "si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e X Y = (second X = second Y \ meter X = meter Y \ - kilogram X = kilogram Y \ ampere X = ampere Y \ - kelvin X = kelvin Y \ mole X = mole Y \ candela X = candela Y )" - -text\SI's as Value are perfectly compatible with this type interface.\ -instantiation SI_ext :: (unit\<^sub>C) si -begin - definition second where "second = Second" - definition meter where "meter = Meter" - definition kilogram where "kilogram = Kilogram" - definition ampere where "ampere = Ampere" - definition kelvin where "kelvin = Kelvin" - definition mole where "mole = Mole" - definition candela where "candela = Candela" -instance .. -end - - -end \ No newline at end of file +theory SI + imports SI_Units SI_Constants SI_Prefix SI_Derived SI_Accepted SI_Imperial +begin end \ No newline at end of file diff --git a/src/SI/SIOld.thy b/src/SI/SIOld.thy new file mode 100644 index 0000000..ad547e1 --- /dev/null +++ b/src/SI/SIOld.thy @@ -0,0 +1,148 @@ +theory SI + imports Main +begin + + +section\SI's as Values.\ + +record SI = + Second :: int + Meter :: int + Kilogram :: int + Ampere :: int + Kelvin :: int + Mole :: int + Candela :: int + + +definition ONE_SI::"SI" ("1\<^sub>S\<^sub>I") + where "1\<^sub>S\<^sub>I = (\ Second = 0::int, Meter = 0::int, Kilogram = 0::int, + Ampere = 0::int, Kelvin = 0::int, Mole = 0::int, + Candela = 0::int, \ = () \)" + + +text\Example: Watt is \kg\m\<^sup>2\s\<^sup>−\<^sup>3\. Joule is \kg\m\<^sup>2\s\<^sup>−\<^sup>2\. \ +definition "Watt \ \ Second = -3, Meter = 2, Kilogram = 1, + Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \" +definition "Joule\ \ Second = -2, Meter = 2, Kilogram = 1, + Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0 \" +definition "Hertz\ 1\<^sub>S\<^sub>I\Second := -1\" + +value " Watt = \ Second = -2, Meter = 1, Kilogram = 7, + Ampere = 0, Kelvin = 0, Mole = 0, Candela = 0\" + +class unit\<^sub>C = + fixes id :: "'a \ 'a" (* hack *) + assumes endo: "\x\(UNIV::'a set). \y\(UNIV::'a set). x = y" + +instantiation unit :: unit\<^sub>C +begin +definition "id = (\x::unit. x) " +instance proof(intro_classes) + show " \x\(UNIV:: unit set). \y\UNIV. x = y" + by auto + qed +end + + +instantiation SI_ext :: (unit\<^sub>C) one +begin +definition "(1::('a::unit\<^sub>C)SI_ext) = + \ Second = 0::int, Meter = 0::int, Kilogram = 0::int, + Ampere = 0::int, Kelvin = 0::int, Mole = 0::int, + Candela = 0::int, + \ = undefined \" +instance .. +end + + +lemma XXX [code_unfold] : "(1::SI) = 1\<^sub>S\<^sub>I " + by (simp add: one_SI_ext_def ONE_SI_def) + +term "one ::('a::unit\<^sub>C)SI_ext " +term "1 ::('a::unit\<^sub>C)SI_ext " +term "(1::SI)\ more := () \ \Second := -1\ " +value "1\<^sub>S\<^sub>I \Second := -1\ " + +instantiation SI_ext :: (unit\<^sub>C) times +begin +definition "(X::('a::unit\<^sub>C)SI_ext) * Y = + \ Second = Second X + Second Y, + Meter = Meter X + Meter Y, + Kilogram = Kilogram X + Kilogram Y, + Ampere = Ampere X + Ampere Y, + Kelvin = Kelvin X + Kelvin Y, + Mole = Mole X + Mole Y, + Candela = Candela X + Candela Y, + \ = undefined \" +instance .. +end + +term "set" +lemma YYY [code_unfold] : + "(X::SI) * Y = \ Second = Second X + Second Y, + Meter = Meter X + Meter Y, + Kilogram = Kilogram X + Kilogram Y, + Ampere = Ampere X + Ampere Y, + Kelvin = Kelvin X + Kelvin Y, + Mole = Mole X + Mole Y, + Candela = Candela X + Candela Y, + \ = () \ " + by (simp add: times_SI_ext_def) + + +instantiation SI_ext :: (unit\<^sub>C) comm_monoid_mult +begin +instance proof(intro_classes) + fix a b c show "(a:: ('a)SI_ext) * b * c = a * (b * c)" + unfolding times_SI_ext_def + by (auto simp: mult.assoc ) +next + fix a b show "(a:: ('a)SI_ext) * b = b * a" + unfolding times_SI_ext_def + by (auto simp: mult.commute ) +next + fix a::"('a::unit\<^sub>C)SI_ext" show "1 * a = a" + unfolding times_SI_ext_def one_SI_ext_def + apply (auto simp: mult.commute, rule sym) + apply(subst surjective) + by (metis UNIV_I endo) + qed +end + +value "Hertz * 1\<^sub>S\<^sub>I " +value "Watt = Joule * Hertz" + + +section\SI's as Types.\ + + +class si = one + ab_semigroup_mult + + fixes second :: "'a \ int" + fixes meter :: "'a \ int" + fixes kilogram :: "'a \ int" + fixes ampere :: "'a \ int" + fixes kelvin :: "'a \ int" + fixes mole :: "'a \ int" + fixes candela :: "'a \ int" + +definition si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e :: "'a::si \ 'b::si \ bool" + where "si\<^sub>c\<^sub>o\<^sub>m\<^sub>p\<^sub>a\<^sub>t\<^sub>i\<^sub>b\<^sub>l\<^sub>e X Y = (second X = second Y \ meter X = meter Y \ + kilogram X = kilogram Y \ ampere X = ampere Y \ + kelvin X = kelvin Y \ mole X = mole Y \ candela X = candela Y )" + +text\SI's as Value are perfectly compatible with this type interface.\ +instantiation SI_ext :: (unit\<^sub>C) si +begin + definition second where "second = Second" + definition meter where "meter = Meter" + definition kilogram where "kilogram = Kilogram" + definition ampere where "ampere = Ampere" + definition kelvin where "kelvin = Kelvin" + definition mole where "mole = Mole" + definition candela where "candela = Candela" +instance .. +end + + +end \ No newline at end of file diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy index a996157..c817560 100644 --- a/src/SI/SI_Units.thy +++ b/src/SI/SI_Units.thy @@ -1,4 +1,6 @@ -section \ SI Units \ +chapter \ International System of Units \ + +section \ SI Units Semantics \ theory SI_Units imports ISQ_Proof diff --git a/src/SI/document/root.tex b/src/SI/document/root.tex index 8d99481..078bfb2 100644 --- a/src/SI/document/root.tex +++ b/src/SI/document/root.tex @@ -162,9 +162,6 @@ to support formal and automated deduction on Si unit equivalences. MORE TO COME. -% generated text of all theories -\chapter{Appendix: The Theories} - \input{session} % optional bibliography