Re: [isabelle] cross product in Isabelle
As Johannes says, there is no cross product formalized in
Multivariate_Analysis. But you can easily define one yourself, like
theory Cross imports Multivariate_Analysis begin
definition cross2 :: "real × real ⇒ real × real ⇒ real" where
"cross2 = (λ(a1,a2). λ(b1,b2). a1 * b2 - a2 * b1)"
definition cross3 :: "real × real × real ⇒ real × real × real ⇒ real ×
real × real" where
"cross3 = (λ(a1,a2,a3). λ(b1,b2,b3). (a2 * b3 - a3 * b2, a3 * b1 -
a1 * b3, a1 * b2 - a2 * b1))"
It is then a simple matter to prove that the cross product is a
bounded bilinear operator. By interpreting the "bounded_bilinear"
locale you can obtain many useful lemmas automatically.
lemma bounded_bilinear_cross3: "bounded_bilinear cross3"
apply (rule bilinear_conv_bounded_bilinear [THEN iffD1])
apply (auto simp add: bilinear_def cross_def algebra_simps intro!: linearI)
interpretation cross: bounded_bilinear cross3
by (rule bounded_bilinear_cross3)
print_theorems (* this shows lemmas about distributivity, continuity,
limits, etc. *)
Hope this helps,
On Thu, Jun 12, 2014 at 11:13 AM, Johannes Hölzl <hoelzl at in.tum.de> wrote:
> Hi Lyj,
> there isn't yet a formalization of the cross product of two vectors in
> Isabelle/HOL. At least not in Multivariate_Analysis. But I'm also not
> aware of any other formalization.
> - Johannes
> Am Donnerstag, den 12.06.2014, 12:08 +0800 schrieb lyj238:
>> Dear experts:
>> The cross product in Euclide-space is directly defined in the multivariate lib in Isabelle?
This archive was generated by a fusion of
Pipermail (Mailman edition) and