Gergely Buday (Aug 01 2023 at 14:24): Gergely Buday (Aug 01 2023 at 14:24):I am to type in the monoid with left neutral element definition from the Type Class Tutorial:
class monoidl = semigroup +
fixes neutral :: α (1)
assumes neutl: 1 ⊗ x = x
with the special "one" symbol from Symbols -> Digit in jEdit. I used
class monoidleft = semigroup +
fixes neutral :: "'a" (𝟭)
assumes neutrality_left: "𝟭 ⊗ x = x"
but this resulted in
Outer syntax error⌂: keyword "infix" expected,
but symbolic identifier 𝟭⌂ was found
What is the correct concrete syntax for introducing a special symbol for a scalar, i.e. not an infix operator?
Gergely Buday (Aug 01 2023 at 14:30):The answer is
class monoidleft = semigroup +
fixes neutral :: "'a" ("𝟭")
assumes neutrality_left: "𝟭 ⊗ x = x"
so using quotes inside the parentheses.
Wolfgang Jeltsch (Aug 01 2023 at 14:50):Yes, it’s inner syntax (the syntax for terms and types); so you have to delimit it. This can be done by quotation marks or by cartouches.
Gergely Buday (Aug 01 2023 at 15:11):How about this one?
class group = monoid +
fixes inverse :: "'a ⇒ 'a" ("_÷")
assumes inverse_left: "x÷ ⊗ x = 𝟭"
works but the Type Class Tutorial would give
((_÷) [1000] 999)
for precedences but I cannot find a concrete syntax for it. Is there one?
Gergely Buday (Aug 01 2023 at 15:24):@Wolfgang Jeltsch do you ask your question for this topic? It is not clear for me how could I add [1000] 999 as the precedence for the left inverse in the above example.
Wolfgang Jeltsch (Aug 01 2023 at 15:26):Yes, my question referred to your question regarding concrete syntax. It wasn’t clear to me whether you talked about concrete syntax for group inverses or concrete syntax for defining such concrete syntax.
Wolfgang Jeltsch (Aug 01 2023 at 15:27):Oh, I see: wrong thread. Maybe some new question sneaked in while I was typing or whatever.
Wolfgang Jeltsch (Aug 01 2023 at 15:30):This kind of syntax definitions is described in the Isabelle/Isar Reference Manual in Section 8.2: Mixfix annotations.
Gergely Buday (Aug 02 2023 at 09:02):@Wolfgang Jeltsch
The Isabelle/Isar Reference Manual is complicated, but searching for examples in Isabelle/src resulted in working examples:
Isabelle2022/src/HOL/Groups.thy: fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
Isabelle2022/src/HOL/Complete_Lattices.thy: fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter> _" [900] 900)
Isabelle2022/src/HOL/Complete_Lattices.thy: fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion> _" [900] 900)
Isabelle2022/src/HOL/Boolean_Algebras.thy: fixes compl :: \<open>'a \<Rightarrow> 'a\<close> (\<open>\<^bold>- _\<close> [81] 80)
Isabelle2022/src/Doc/Tutorial/Types/Axioms.thy: fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
Isabelle2022/src/Doc/Classes/Classes.thy: fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
which instructed me to omit the inner parentheses:
fixes inverse :: "'a ⇒ 'a" ("_ ÷" [1000] 999)
The Type Class Tutorial has it wrong:
class group = monoidl +
fixes inverse :: α ⇒ α ((-÷) [1000] 999)
assumes invl: x÷ ⊗ x = 1
How should I report this typo?
Wolfgang Jeltsch (Aug 02 2023 at 11:52):The Type Class Tutorial has it wrong: […]
Yes, I guess the inner parentheses should be quotation marks or cartouches.
Maybe report it directly to the authors by e-mail.
Last updated: Apr 27 2024 at 12:25 UTC