Re: [isabelle] Defining operators



The problem is that ⇩ (\<^sub>) is considered part of an identifier,
e.g. when you type Q⇩a, it gets parsed as a single identifier. You can
see that by inspecting the theorem "Qdef": It contains a universally
quantified variable Q⇩a.

The best solution to this would probably be to use \<^bsub> and \<^esub>
instead of \<^sub>. That also has the additional advantage of allowing
you to have parameters for a that are more than a single character long
without looking ugly.

class triple = ab_group_add +
  fixes triple :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("⦃ _ _ _ ⦄" [100,100,100] 1000)
  fixes Qsig :: "'a ⇒ 'a ⇒ 'a" ("Q⇘_⇙ _ " [100,100] 1000)
  assumes Qdef: "Q⇘a⇙ b = ⦃ a b a ⦄"
begin

(I also adjusted the precedences a little bit to avoid ambiguous parse
trees)


However, I would also suggest to reconsider whether you really need that
much custom syntax. Syntax /can/ be useful to increase readability, but
in this case I'm not sure if it's not easier to just write e.g. "Q a b".

Cheers,

Manuel


On 13/07/2019 10:50, Christopher Hoskin wrote:
> 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.