[isabelle] Defining operators



Hello,

I'm trying to teach myself Isabelle, and have come across something I
don't understand. I'm trying to model Jordan *-triples (e.g. the
complex numbers equipped with the ternary product {a b c} =
1/2(ab^*c+cb^*a) where ^* denotes conjugation. The triple product has
a quadratic operator associated with it defined by Q(a)b = {a b a}.

I can model the ternary multiplication as:

class triple = ab_group_add +
  fixes triple :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("⦃ _ _ _ ⦄" [100,100,100] 1000)

(There are other axioms which I have omitted for simplicity as
removing them doesn't affect the outcome described below.)

I then attempt to define the quadratic operator as:

  fixes Qsig :: "'a ⇒ 'a ⇒ 'a" ("Q⇩_ _ " 1000)
  assumes Qdef: "Q⇩a b = ⦃ a b a ⦄"

Clearly I have introduced some rules beyond what I intended, as
Isabelle is then able to prove statements which aren't in general true
in the mathematical theory. e.g.

lemma Qop: "Q⇩u (Q⇩u (Q⇩u a)) = ⦃ u a u ⦄" by (rule local.Qdef)

is considered true. (This should require the additional assumption
that u is a tripotent i.e. ⦃ u u u ⦄ = u along with the omitted axioms
on the multiplication.)

How is Isabelle actually interpreting what I have entered, and what
should I have put?

(Sorry if this is a very basic question. I am still new to this and
finding it hard going.)

Thank you for any help you are able to offer.

Christopher Hoskin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.