(NOTE: If I can get rid of the warning, which I will show below, then I say a bunch of extraneous things. As part of the asked question, I also express some doubts. I assume this question asks the question “Why am I wrong here, what am I say? ")
It seems that 6 characters used for operators boolshould be assigned to classes of a syntactic type, and boolfor these type classes. In particular, they:
~, &, |, \<not>, \<and>, \<or>.
Since annotation of type terms is a frequent requirement for HOL statements, I don’t think it would be a big burden to use annotations boolfor these 6 statements.
I would like to overload these 6 characters for other logical operators. The absence of the usual characters for the application can lead to the fact that there will not be a good solution for the designation.
In the following source example, if I can get rid of the warnings, the problem is resolved (unless I set a trap for myself):
definition natOP :: "nat => nat => nat" where
"natOP x y = x"
definition natlistOP :: "nat list => nat list => nat list" where
"natlistOP x y = x"
notation
natOP (infixr "&" 35)
notation
natlistOP (infixr "&" 35)
term "True & False"
term "2 & (2::nat)"
term "[2] & [(2::nat)]" (*
OUTPUT: Ambiguous input produces 3 parse trees:
...
Fortunately, only one parse tree is well-formed and type-correct,
but you may still want to disambiguate your grammar or your input.*)
Can I get rid of warnings? It seems that since the correct type term exists, there should be no problem.
There are actually other characters, such as those !used for list:
term "[1,2,3] ! 1"
Here is the application for which I need the characters:
Update
, & & . , , . - " Isabelle/HOL".
(*|Unnotate; switch to a type class; see someday why this is a bad idea.|*)
no_notation conj (infixr "&" 35)
class conj =
fixes syntactic_type_classes_are_awesome :: "'a => 'a => 'a" (infixr "&" 35)
instantiation bool :: conj
begin
definition syntactic_type_classes_are_awesome_bool :: "bool => bool => bool"
where "p & q == conj p q"
instance ..
end
term "True & False"
value "True & False"
declare[[show_sorts]]
term "p & q" (* "(p::'a::conj) & (q::'a::conj)" :: "'a::conj" *)