Email Gateway (Aug 22 2022 at 20:15): Email Gateway (Aug 22 2022 at 20:15):From: Christopher Hoskin <christopher.hoskin@gmail.com>
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
Email Gateway (Aug 22 2022 at 20:15):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 20:15):From: Christopher Hoskin <christopher.hoskin@gmail.com>
Thanks. After experimenting a bit more I found I could move the definition of the quadratic operator to the body of the class as:
definition quad :: "'a ⇒ ('a ⇒ 'a)" ("Q _ " [100] 900) where "(Q a) b = ⦃ a b a ⦄"
(A more standard notation would be Q(a)b rather than (Q a) b, but this caused a Type unification error.)
Isabelle can then correctly prove:
lemma cube1:
assumes "tripotent u"
shows "( Q(u) ∘ Q(u) ∘ Q(u) ) a = (Q u) a"
However, what I'd then like to conclude is:
lemma cube2:
assumes "tripotent u"
shows "Q(u) ∘ Q(u) ∘ Q(u) = Q(u)"
which I was hoping would be an immediate consequence of fun_eq_iff from HOL.thy, but it seems not?
Thanks for any pointers you can give.
Christopher
Last updated: Apr 19 2024 at 20:15 UTC