Can I overload the notation for operators that are assigned to bool and list?

Question

(NOTE: If I can get rid of the warning I show below, then I say a bunch of extraneous stuff. As part of asking a question, I also do some opinionating. I guess that's sort of asking the question "Why am I wrong here in what I say?")

It seems that 6 of the symbols used for bool operators should have been assigned to syntactic type classes, and bool instantiated for those type classes. In particular, these:

~, &, |, \<not>, \<and>, \<or>. 

Because type annotation of terms is a frequent requirement for HOL operators, I don't think it would be a great burden to have to use bool annotations for those 6 operators.

I would like to overload those 6 symbols for other logical operators. Not having the usual symbols for an application can result in there being no good solution for notation.

In the following example source, if I can get rid of the warnings, then the problem is solved (unless I would be setting 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 the warnings? It seems that since there's a type correct term, there shouldn't be a problem.

There are actually other symbols I also want, such as !, used for list:

term "[1,2,3] ! 1"

Here's the application for which I want the symbols:

• Verilog HDL Operators.

Update

Based on Brian Huffman's answer, I unnotate &, and switch & to a syntactic type class. It'll work out, or it won't, indeed, binary logic, so diversely applicable. My general rule is "don't mess with default 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" *)

Answer 1

You can "undeclare" special syntax using the no_notation command, e.g.

no_notation conj (infixr "\<and>" 35)

This infix operator is then available to be used with your own functions:

notation myconj (infixr "\<and>" 35)

From here on, \<and> refers to the constant myconj instead of the HOL library's standard conjunction operator for type bool. You should have no warnings about ambiguous syntax. The original HOL boolean operator is still accessible by name (conj), or you can give it a different syntax if you want with another notation command.

For the no_notation command to work, the pattern and fixities must be exactly the same as they were declared originally. See src/HOL/HOL.thy for the declarations of the operators you are interested in.

I should warn about a potential pitfall: Subsequent theory merges can bring the original syntax back into scope, causing ambiguous syntax again. For example, say your theory A.thy imports Main and redeclares the \<and> syntax. Then your theory B.thy imports both A and another library theory, say Complex_Main. Then in theory B, \<and> will be ambiguous. To prevent this, make sure to put all your external theory imports in the one theory file where you change the syntax; then have all of your other theories import this one.