Re: [isabelle] Defining operators



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




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