Split out SI units into several files, and began adapting proof automation
This commit is contained in:
parent
ec32ed0486
commit
9199bc3109
|
|
@ -30,7 +30,10 @@ begin
|
|||
|
||||
lemma mult_distrib_inverse' [simp]: "(a * b) / a = b"
|
||||
using local.mult_distrib_inverse mult_commute by fastforce
|
||||
|
||||
|
||||
lemma inverse_distrib: "inverse (a * b) = (inverse a) * (inverse b)"
|
||||
by (simp add: local.mult.inverse_distrib_swap mult_commute)
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,35 @@
|
|||
section \<open> Derived Units\<close>
|
||||
|
||||
theory SI_Derived
|
||||
imports SI_Prefix
|
||||
begin
|
||||
|
||||
definition "radian = 1 \<cdot> (meter \<^bold>\<cdot> meter\<^sup>-\<^sup>\<one>)"
|
||||
|
||||
definition degree :: "real[meter / meter]" where
|
||||
[si_def]: "degree = (2\<cdot>(UNIT(pi,_)) / 180)\<cdot>radian"
|
||||
|
||||
abbreviation degrees ("_\<degree>" [999] 999) where "n\<degree> \<equiv> n\<cdot>degree"
|
||||
|
||||
definition [si_def]: "litre = 1/1000 \<cdot> meter\<^sup>\<three>"
|
||||
|
||||
definition [si_def]: "pint = 0.56826125 \<cdot> litre"
|
||||
|
||||
definition [si_def]: "hour = 3600 \<cdot> second"
|
||||
|
||||
abbreviation "tonne \<equiv> kilo\<cdot>kilogram"
|
||||
|
||||
abbreviation "newton \<equiv> (kilogram \<^bold>\<cdot> meter) \<^bold>/ second\<^sup>\<two>"
|
||||
|
||||
abbreviation "volt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three> \<^bold>\<cdot> ampere\<^sup>-\<^sup>\<one>"
|
||||
|
||||
abbreviation "watt \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<three>"
|
||||
|
||||
abbreviation "joule \<equiv> kilogram \<^bold>\<cdot> meter\<^sup>\<two> \<^bold>\<cdot> second\<^sup>-\<^sup>\<two>"
|
||||
|
||||
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)[meter \<cdot> (second)\<^sup>-\<^sup>2]"
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,27 @@
|
|||
section \<open> SI Prefixes \<close>
|
||||
|
||||
theory SI_Prefix
|
||||
imports SI_Quantities
|
||||
begin
|
||||
|
||||
definition [si_def]: "giga = UNIT(1000000000, _)"
|
||||
|
||||
definition [si_def]: "mega = UNIT(1000000, _)"
|
||||
|
||||
definition [si_def]: "kilo = UNIT(1000, _)"
|
||||
|
||||
definition [si_def]: "hecto = UNIT(100, _)"
|
||||
|
||||
definition [si_def]: "deca = UNIT(10, _)"
|
||||
|
||||
definition [si_def]: "deci = UNIT(0.1, _)"
|
||||
|
||||
definition [si_def]: "centi = UNIT(0.01, _)"
|
||||
|
||||
definition [si_def]: "milli = UNIT(0.001, _)"
|
||||
|
||||
definition [si_def]: "micro = UNIT(0.000001, _)"
|
||||
|
||||
definition [si_def]: "nano = UNIT(0.000000001, _)"
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,160 @@
|
|||
theory SI_Proof
|
||||
imports SI_Derived
|
||||
begin
|
||||
|
||||
section \<open> Tactic Support for SI type expressions. \<close>
|
||||
|
||||
lemmas [si_def] = si_sem_meter_def si_sem_kilogram_def si_sem_second_def
|
||||
si_sem_ampere_def si_sem_kelvin_def si_sem_mole_def
|
||||
si_sem_candela_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(meter) = 1\<lparr>Meters := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(kilogram)= 1\<lparr>Kilograms := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(second) = 1\<lparr>Seconds := 1\<rparr> " by(simp add: si_def)
|
||||
lemma "SI(ampere) = 1\<lparr>Amperes := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(kelvin) = 1\<lparr>Kelvins := 1\<rparr> " by(simp add: si_def)
|
||||
lemma "SI(mole) = 1\<lparr>Moles := 1\<rparr>" by(simp add: si_def)
|
||||
lemma "SI(candela) = 1\<lparr>Candelas := 1\<rparr>" by(simp add: si_def)
|
||||
|
||||
lemma "SI(mole \<cdot> kelvin \<cdot> mole) = SI(kelvin \<cdot> (mole)\<^sup>2)" by(simp add: si_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, second) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 1, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_second_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, meter) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 1, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_meter_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, kilogram) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 1, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_kilogram_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, ampere) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 1,
|
||||
Kelvins = 0, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_ampere_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, kelvin) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 1, Moles = 0, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_kelvin_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, mole) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 1, Candelas = 0\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_mole_def)
|
||||
|
||||
lemma [si_def]:"fromUnit UNIT(x::'a::one, candela) =
|
||||
\<lparr>magn = x,
|
||||
unit = \<lparr>Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0,
|
||||
Kelvins = 0, Moles = 0, Candelas = 1\<rparr>\<rparr>"
|
||||
by (simp add: mk_unit.rep_eq one_Unit_ext_def si_sem_candela_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, candela) \<^bold>\<cdot> UNIT(y::'a::{one,ab_semigroup_mult}, mole))
|
||||
\<approx>\<^sub>Q (UNIT(y, mole) \<^bold>\<cdot> UNIT(x, candela)) "
|
||||
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"
|
||||
apply (transfer)
|
||||
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
|
||||
|
|
@ -0,0 +1,297 @@
|
|||
section \<open> SI Quantities \<close>
|
||||
|
||||
theory SI_Quantities
|
||||
imports SI_Units
|
||||
begin
|
||||
|
||||
subsection \<open> The \<^theory_text>\<open>Quantity\<close>-type and its operations \<close>
|
||||
|
||||
record 'a Quantity =
|
||||
magn :: 'a \<comment> \<open> Magnitude of the quantity \<close>
|
||||
unit :: Unit \<comment> \<open> Unit of the quantity \<close>
|
||||
|
||||
lemma Quantity_eq_intro:
|
||||
assumes "magn x = magn y" "unit x = unit y" "more x = more y"
|
||||
shows "x = y"
|
||||
by (simp add: assms)
|
||||
|
||||
instantiation Quantity_ext :: (times, times) times
|
||||
begin
|
||||
definition "times_Quantity_ext x y = \<lparr> magn = magn x \<cdot> magn y, unit = unit x \<cdot> unit y, \<dots> = more x \<cdot> more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Quantity_ext :: (zero, zero) zero
|
||||
begin
|
||||
definition "zero_Quantity_ext = \<lparr> magn = 0, unit = 1, \<dots> = 0 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Quantity_ext :: (one, one) one
|
||||
begin
|
||||
definition "one_Quantity_ext = \<lparr> magn = 1, unit = 1, \<dots> = 1 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Quantity_ext :: (inverse, inverse) inverse
|
||||
begin
|
||||
definition "inverse_Quantity_ext x = \<lparr> magn = inverse (magn x), unit = inverse (unit x), \<dots> = inverse (more x) \<rparr>"
|
||||
definition "divide_Quantity_ext x y = \<lparr> magn = magn x / magn y, unit = unit x / unit y, \<dots> = more x / more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance Quantity_ext :: (comm_monoid_mult, comm_monoid_mult) comm_monoid_mult
|
||||
by (intro_classes, simp_all add: one_Quantity_ext_def
|
||||
times_Quantity_ext_def mult.assoc, simp add: mult.commute)
|
||||
|
||||
instance Quantity_ext :: (ab_group_mult, ab_group_mult) ab_group_mult
|
||||
oops
|
||||
|
||||
subsection \<open> SI Tagged Types \<close>
|
||||
text\<open>We 'lift' SI type expressions to SI tagged type expressions as follows:\<close>
|
||||
|
||||
typedef (overloaded) ('n, 'u::si_type) tQuant ("_[_]" [999,0] 999)
|
||||
= "{x :: 'n Quantity. unit x = SI('u)}"
|
||||
morphisms fromUnit toUnit by (rule_tac x="\<lparr> magn = undefined, unit = SI('u) \<rparr>" in exI, simp)
|
||||
|
||||
setup_lifting type_definition_tQuant
|
||||
|
||||
text \<open> Coerce values when their units are equivalent \<close>
|
||||
|
||||
definition coerceUnit :: "'u\<^sub>2 itself \<Rightarrow> 'a['u\<^sub>1::si_type] \<Rightarrow> 'a['u\<^sub>2::si_type]" where
|
||||
"SI('u\<^sub>1) = SI('u\<^sub>2) \<Longrightarrow> coerceUnit t x = (toUnit (fromUnit x))"
|
||||
|
||||
section\<open>Operations SI-tagged types via their Semantic Domains\<close>
|
||||
|
||||
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
|
||||
"(=)" .
|
||||
|
||||
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 Quant_equiv_sym: "a \<approx>\<^sub>Q b \<Longrightarrow> b \<approx>\<^sub>Q a"
|
||||
by (simp add: Quant_equiv_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)
|
||||
|
||||
(* 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)
|
||||
|
||||
(* 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
|
||||
|
||||
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"
|
||||
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>
|
||||
|
||||
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"
|
||||
shows "SI('u\<^sub>1) = SI('u\<^sub>2::si_type)"
|
||||
by (metis (full_types) Quant_equiv.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 "(*)"
|
||||
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"
|
||||
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>"
|
||||
|
||||
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_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>"
|
||||
|
||||
instantiation tQuant :: (zero,si_type) zero
|
||||
begin
|
||||
lift_definition zero_tQuant :: "('a, 'b) tQuant" is "\<lparr> magn = 0, unit = SI('b) \<rparr>"
|
||||
by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (one,si_type) one
|
||||
begin
|
||||
lift_definition one_tQuant :: "('a, 'b) tQuant" is "\<lparr> magn = 1, unit = SI('b) \<rparr>"
|
||||
by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (plus,si_type) plus
|
||||
begin
|
||||
lift_definition plus_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x + magn y, unit = SI('b) \<rparr>"
|
||||
by (simp)
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance tQuant :: (semigroup_add,si_type) semigroup_add
|
||||
by (intro_classes, transfer, simp add: add.assoc)
|
||||
|
||||
instance tQuant :: (ab_semigroup_add,si_type) ab_semigroup_add
|
||||
by (intro_classes, transfer, simp add: add.commute)
|
||||
|
||||
instance tQuant :: (monoid_add,si_type) monoid_add
|
||||
by (intro_classes; (transfer, simp))
|
||||
|
||||
instance tQuant :: (comm_monoid_add,si_type) comm_monoid_add
|
||||
by (intro_classes; transfer, simp)
|
||||
|
||||
instantiation tQuant :: (uminus,si_type) uminus
|
||||
begin
|
||||
lift_definition uminus_tQuant :: "'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x. \<lparr> magn = - magn x, unit = unit x \<rparr>" by (simp)
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (minus,si_type) minus
|
||||
begin
|
||||
lift_definition minus_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x - magn y, unit = unit x \<rparr>" by (simp)
|
||||
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance tQuant :: (numeral,si_type) numeral ..
|
||||
|
||||
instantiation tQuant :: (times,si_type) times
|
||||
begin
|
||||
lift_definition times_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x * magn y, unit = SI('b) \<rparr>"
|
||||
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 :: (comm_semiring,si_type) comm_semiring
|
||||
by (intro_classes, transfer, simp add: linordered_field_class.sign_simps(18) mult.commute)
|
||||
|
||||
instance tQuant :: (comm_semiring_0,si_type) comm_semiring_0
|
||||
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] \<Rightarrow> 'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x y. \<lparr> magn = magn x div magn y, unit = SI('b) \<rparr>" by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (inverse,si_type) inverse
|
||||
begin
|
||||
lift_definition inverse_tQuant :: "'a['b] \<Rightarrow> 'a['b]"
|
||||
is "\<lambda> x. \<lparr> magn = inverse (magn x), unit = SI('b) \<rparr>" by simp
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation tQuant :: (order,si_type) order
|
||||
begin
|
||||
lift_definition less_eq_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. magn x \<le> magn y" .
|
||||
lift_definition less_tQuant :: "'a['b] \<Rightarrow> 'a['b] \<Rightarrow> bool" is "\<lambda> x y. magn x < magn y" .
|
||||
instance by (intro_classes, (transfer, simp add: less_le_not_le)+)
|
||||
end
|
||||
|
||||
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
|
||||
|
||||
syntax "_mk_unit" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("UNIT'(_, _')")
|
||||
translations "UNIT(n, 'a)" == "CONST mk_unit n TYPE('a)"
|
||||
|
||||
subsection \<open>Polymorphic Operations for Elementary SI Units \<close>
|
||||
|
||||
named_theorems si_def
|
||||
|
||||
definition [si_def]: "meter = UNIT(1, meter)"
|
||||
definition [si_def]: "second = UNIT(1, second)"
|
||||
definition [si_def]: "kilogram = UNIT(1, kilogram)"
|
||||
definition [si_def]: "ampere = UNIT(1, ampere)"
|
||||
definition [si_def]: "kelvin = UNIT(1, kelvin)"
|
||||
definition [si_def]: "mole = UNIT(1, mole)"
|
||||
definition [si_def]: "candela = UNIT(1, candela)"
|
||||
|
||||
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_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_times [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_div [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_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)
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,299 @@
|
|||
section \<open> SI Units \<close>
|
||||
|
||||
theory SI_Units
|
||||
imports Groups_mult
|
||||
HOL.Transcendental
|
||||
"HOL-Eisbach.Eisbach"
|
||||
begin
|
||||
|
||||
text\<open>
|
||||
The International System of Units (SI, abbreviated from the French
|
||||
Système international (d'unités)) is the modern form of the metric
|
||||
system and is the most widely used system of measurement. It comprises
|
||||
a coherent system of units of measurement built on seven base units,
|
||||
which are the second, metre, kilogram, ampere, kelvin, mole, candela,
|
||||
and a set of twenty prefixes to the unit names and unit symbols that
|
||||
may be used when specifying multiples and fractions of the units.
|
||||
The system also specifies names for 22 derived units, such as lumen and
|
||||
watt, for other common physical quantities.
|
||||
|
||||
(cited from \<^url>\<open>https://en.wikipedia.org/wiki/International_System_of_Units\<close>).\<close>
|
||||
|
||||
text\<open> This is an attempt to model the system and its derived entities (cf.
|
||||
\<^url>\<open>https://www.quora.com/What-are-examples-of-SI-units\<close>) in Isabelle/HOL.
|
||||
The design objective are twofold (and for the case of Isabelle somewhat
|
||||
contradictory, see below)
|
||||
|
||||
The construction proceeds in three phases:
|
||||
\<^enum> We construct a generic type \<^theory_text>\<open>Unit\<close> which is basically an "inner representation" or
|
||||
"semantic domain" of all SI types. Since SI-types have an interpretation in this domain,
|
||||
it serves to give semantics to type-constructors by operations on this domain, too.
|
||||
We construct a multiplicative group on it.
|
||||
\<^enum> From \<^theory_text>\<open>Unit\<close> we build a \<^theory_text>\<open>'a SI_tagged_domain\<close> types, i.e. a polymorphic family of values
|
||||
tagged with values from \<^theory_text>\<open>Unit\<close>. We construct multiplicative and additive
|
||||
groups over it.
|
||||
\<^enum> We construct a type-class characterizing SI - type expressions
|
||||
and types tagged with SI - type expressions; this construction paves the
|
||||
way to overloaded interpretation functions from SI type-expressions to
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open>The Domains of SI types and SI-tagged types\<close>
|
||||
|
||||
subsection \<open> The \<^theory_text>\<open>Unit\<close>-type and its operations \<close>
|
||||
|
||||
text \<open> An SI unit associates with each of the seven base unit an integer that denotes the power
|
||||
to which it is raised. We use a record to represent this 7-tuple, to enable code generation. \<close>
|
||||
|
||||
record Unit =
|
||||
Seconds :: int
|
||||
Meters :: int
|
||||
Kilograms :: int
|
||||
Amperes :: int
|
||||
Kelvins :: int
|
||||
Moles :: int
|
||||
Candelas :: int
|
||||
|
||||
text \<open> We define a commutative monoid for SI units. \<close>
|
||||
|
||||
instantiation Unit_ext :: (one) one
|
||||
begin
|
||||
\<comment> \<open> Here, $1$ is the dimensionless unit \<close>
|
||||
definition one_Unit_ext :: "'a Unit_ext"
|
||||
where [code_unfold]: "1 = \<lparr> Seconds = 0, Meters = 0, Kilograms = 0, Amperes = 0
|
||||
, Kelvins = 0, Moles = 0, Candelas = 0, \<dots> = 1 \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instantiation Unit_ext :: (times) times
|
||||
begin
|
||||
\<comment> \<open> Multiplication is defined by adding together the powers \<close>
|
||||
definition times_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext \<Rightarrow> 'a Unit_ext"
|
||||
where [code_unfold]:
|
||||
"x * y = \<lparr> Seconds = Seconds x + Seconds y, Meters = Meters x + Meters y
|
||||
, Kilograms = Kilograms x + Kilograms y, Amperes = Amperes x + Amperes y
|
||||
, Kelvins = Kelvins x + Kelvins y, Moles = Moles x + Moles y
|
||||
, Candelas = Candelas x + Candelas y, \<dots> = more x * more y \<rparr>"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance Unit_ext :: (comm_monoid_mult) comm_monoid_mult
|
||||
proof
|
||||
fix a b c :: "'a Unit_ext"
|
||||
show "a * b * c = a * (b * c)"
|
||||
by (simp add: times_Unit_ext_def mult.assoc)
|
||||
show "a * b = b * a"
|
||||
by (simp add: times_Unit_ext_def mult.commute)
|
||||
show "1 * a = a"
|
||||
by (simp add: times_Unit_ext_def one_Unit_ext_def)
|
||||
qed
|
||||
|
||||
text \<open> We also define the inverse and division operations, and an abelian group. \<close>
|
||||
|
||||
instantiation Unit_ext :: ("{times,inverse}") inverse
|
||||
begin
|
||||
definition inverse_Unit_ext :: "'a Unit_ext \<Rightarrow> 'a Unit_ext"
|
||||
where [code_unfold]:
|
||||
"inverse x = \<lparr> Seconds = - Seconds x , Meters = - Meters x
|
||||
, Kilograms = - Kilograms x, Amperes = - Amperes x
|
||||
, Kelvins = - Kelvins x, Moles = - Moles x
|
||||
, 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]:
|
||||
"divide_Unit_ext x y = x * (inverse y)"
|
||||
instance ..
|
||||
end
|
||||
|
||||
instance Unit_ext :: (ab_group_mult) ab_group_mult
|
||||
proof
|
||||
fix a b :: "'a Unit_ext"
|
||||
show "inverse a \<cdot> a = 1"
|
||||
by (simp add: inverse_Unit_ext_def times_Unit_ext_def one_Unit_ext_def)
|
||||
show "a \<cdot> inverse b = a div b"
|
||||
by (simp add: divide_Unit_ext_def)
|
||||
qed
|
||||
|
||||
instantiation unit :: comm_monoid_add
|
||||
begin
|
||||
definition "zero_unit = ()"
|
||||
definition "plus_unit (x::unit) (y::unit) = ()"
|
||||
instance proof qed (simp_all)
|
||||
end
|
||||
|
||||
instantiation unit :: comm_monoid_mult
|
||||
begin
|
||||
definition "one_unit = ()"
|
||||
definition "times_unit (x::unit) (y::unit) = ()"
|
||||
instance proof qed (simp_all)
|
||||
end
|
||||
|
||||
instantiation unit :: inverse
|
||||
begin
|
||||
definition "inverse_unit (x::unit) = ()"
|
||||
definition "divide_unit (x::unit) (y::unit) = ()"
|
||||
instance ..
|
||||
end
|
||||
|
||||
text \<open> A base unit is an SI_tagged_domain unit here precisely one unit has power 1. \<close>
|
||||
|
||||
definition is_BaseUnit :: "Unit \<Rightarrow> bool" where
|
||||
"is_BaseUnit u = (\<exists> n. u = 1\<lparr>Meters := n\<rparr> \<or> u = 1\<lparr>Kilograms := n\<rparr> \<or> u = 1\<lparr>Seconds := n\<rparr>
|
||||
\<or> u = 1\<lparr>Amperes := n\<rparr> \<or> u = 1\<lparr>Kelvins := n\<rparr> \<or> u = 1\<lparr>Moles := n\<rparr>
|
||||
\<or> u = 1\<lparr>Candelas := n\<rparr>)"
|
||||
|
||||
section\<open>The Syntax and Semantics of SI types and SI-tagged types\<close>
|
||||
|
||||
subsection \<open> Basic SI-types \<close>
|
||||
|
||||
text \<open> We provide a syntax for type-expressions; The definition of
|
||||
the basic type constructors is straight-forward via a one-elementary set. \<close>
|
||||
|
||||
typedef meter = "UNIV :: unit set" .. setup_lifting type_definition_meter
|
||||
typedef kilogram = "UNIV :: unit set" .. setup_lifting type_definition_kilogram
|
||||
typedef second = "UNIV :: unit set" .. setup_lifting type_definition_second
|
||||
typedef ampere = "UNIV :: unit set" .. setup_lifting type_definition_ampere
|
||||
typedef kelvin = "UNIV :: unit set" .. setup_lifting type_definition_kelvin
|
||||
typedef mole = "UNIV :: unit set" .. setup_lifting type_definition_mole
|
||||
typedef candela = "UNIV :: unit set" .. setup_lifting type_definition_candela
|
||||
|
||||
subsection \<open> SI-type expressions and SI-type interpretation \<close>
|
||||
|
||||
text \<open> The case for the construction of the multiplicative and inverse operators requires ---
|
||||
thus, the unary and binary operators on our SI type language --- require that their arguments
|
||||
are restricted to the set of SI-type expressions.
|
||||
|
||||
The mechanism in Isabelle to characterize a certain sub-class of Isabelle-type expressions
|
||||
are \<^emph>\<open>type classes\<close>. We therefore need such a sub-class; for reasons of convenience,
|
||||
we combine its construction also with the "semantics" of SI types in terms of
|
||||
@{typ Unit}. \<close>
|
||||
|
||||
subsubsection \<open> SI-type expression definition as type-class \<close>
|
||||
|
||||
class si_type = finite +
|
||||
fixes si_sem :: "'a itself \<Rightarrow> Unit"
|
||||
assumes unitary_unit_pres: "card (UNIV::'a set) = 1"
|
||||
|
||||
syntax
|
||||
"_SI" :: "type \<Rightarrow> logic" ("SI'(_')")
|
||||
|
||||
translations
|
||||
"SI('a)" == "CONST si_sem TYPE('a)"
|
||||
|
||||
text \<open> The sub-set of basic SI type expressions can be characterized by the following
|
||||
operation: \<close>
|
||||
|
||||
class si_baseunit = si_type +
|
||||
assumes is_BaseUnit: "is_BaseUnit SI('a)"
|
||||
|
||||
subsubsection \<open> SI base type constructors \<close>
|
||||
|
||||
text\<open>We embed the basic SI types into the SI type expressions: \<close>
|
||||
declare [[show_sorts]]
|
||||
|
||||
instantiation meter :: si_baseunit
|
||||
begin
|
||||
definition si_sem_meter :: "meter itself \<Rightarrow> Unit" where "si_sem_meter x = 1\<lparr>Meters := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_meter_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation kilogram :: si_baseunit
|
||||
begin
|
||||
definition si_sem_kilogram :: "kilogram itself \<Rightarrow> Unit" where "si_sem_kilogram x = 1\<lparr>Kilograms := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_kilogram_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation second :: si_baseunit
|
||||
begin
|
||||
definition si_sem_second :: "second itself \<Rightarrow> Unit" where "si_sem_second x = 1\<lparr>Seconds := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_second_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation ampere :: si_baseunit
|
||||
begin
|
||||
definition si_sem_ampere :: "ampere itself \<Rightarrow> Unit" where "si_sem_ampere x = 1\<lparr>Amperes := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_ampere_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation kelvin :: si_baseunit
|
||||
begin
|
||||
definition si_sem_kelvin :: "kelvin itself \<Rightarrow> Unit" where "si_sem_kelvin x = 1\<lparr>Kelvins := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_kelvin_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation mole :: si_baseunit
|
||||
begin
|
||||
definition si_sem_mole :: "mole itself \<Rightarrow> Unit" where "si_sem_mole x = 1\<lparr>Moles := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_mole_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
instantiation candela :: si_baseunit
|
||||
begin
|
||||
definition si_sem_candela :: "candela itself \<Rightarrow> Unit" where "si_sem_candela x = 1\<lparr>Candelas := 1\<rparr>"
|
||||
instance by (intro_classes, auto simp add: si_sem_candela_def is_BaseUnit_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
lemma base_units [simp]:
|
||||
"is_BaseUnit SI(meter)" "is_BaseUnit SI(kilogram)" "is_BaseUnit SI(second)"
|
||||
"is_BaseUnit SI(ampere)" "is_BaseUnit SI(kelvin)" "is_BaseUnit SI(mole)"
|
||||
"is_BaseUnit SI(candela)" by (simp_all add: is_BaseUnit)
|
||||
|
||||
subsubsection \<open> Higher SI Type Constructors: Inner Product and Inverse \<close>
|
||||
text\<open>On the class of SI-types (in which we have already inserted the base SI types),
|
||||
the definitions of the type constructors for inner product and inverse is straight) forward.\<close>
|
||||
|
||||
typedef ('a::si_type, 'b::si_type) UnitTimes (infixl "\<cdot>" 69) = "UNIV :: unit set" ..
|
||||
setup_lifting type_definition_UnitTimes
|
||||
|
||||
text \<open> We can prove that multiplication of two SI types yields an SI type. \<close>
|
||||
|
||||
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)"
|
||||
instance by (intro_classes, simp_all add: si_sem_UnitTimes_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
text \<open> Similarly, we define division of two SI types and prove that SI types are closed under this. \<close>
|
||||
|
||||
typedef 'a UnitInv ("(_\<^sup>-\<^sup>1)" [999] 999) = "UNIV :: unit set" ..
|
||||
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)"
|
||||
instance by (intro_classes, simp_all add: si_sem_UnitInv_def, (transfer, simp)+)
|
||||
end
|
||||
|
||||
|
||||
subsubsection \<open> Syntactic Support for SI type expressions. \<close>
|
||||
|
||||
text\<open>A number of type-synonyms allow for more compact notation: \<close>
|
||||
type_synonym ('a, 'b) UnitDiv = "'a \<cdot> ('b\<^sup>-\<^sup>1)" (infixl "'/" 69)
|
||||
|
||||
type_synonym 'a UnitSquare = "'a \<cdot> 'a" ("(_)\<^sup>2" [999] 999)
|
||||
type_synonym 'a UnitCube = "'a \<cdot> 'a \<cdot> 'a" ("(_)\<^sup>3" [999] 999)
|
||||
type_synonym 'a UnitInvSquare = "('a\<^sup>2)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>2" [999] 999)
|
||||
type_synonym 'a UnitInvCube = "('a\<^sup>3)\<^sup>-\<^sup>1" ("(_)\<^sup>-\<^sup>3" [999] 999)
|
||||
|
||||
translations (type) "'a\<^sup>-\<^sup>2" <= (type) "('a\<^sup>2)\<^sup>-\<^sup>1"
|
||||
translations (type) "'a\<^sup>-\<^sup>3" <= (type) "('a\<^sup>3)\<^sup>-\<^sup>1"
|
||||
|
||||
print_translation \<open>
|
||||
[(@{type_syntax UnitTimes},
|
||||
fn ctx => fn [a, b] =>
|
||||
if (a = b)
|
||||
then Const (@{type_syntax UnitSquare}, dummyT) $ a
|
||||
else case a of
|
||||
Const (@{type_syntax UnitTimes}, _) $ a1 $ a2 =>
|
||||
if (a1 = a2 andalso a2 = b)
|
||||
then Const (@{type_syntax UnitCube}, dummyT) $ a1
|
||||
else raise Match |
|
||||
Const (@{type_syntax UnitSquare}, _) $ a' =>
|
||||
if (@{print} a' = b)
|
||||
then Const (@{type_syntax UnitCube}, dummyT) $ a'
|
||||
else raise Match |
|
||||
_ => raise Match)]
|
||||
\<close>
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue