I want to use the nat type in Isabelle but I want to overload some existing definitions like for example addition. I wrote the following code:
theory Prueba
imports Main HOL
begin
primrec suma::"nat ⇒ nat ⇒ nat" where
"suma 0 n = 0" |
"suma (Suc x) n = 0"
no_notation suma (infix "+" 65)
value "2 + (1 :: nat)"
I tried to overload addition with a new definition that always outputs 0. However when I evaluate 2 + (1 :: nat) I get "Suc (Suc (Suc 0))" :: "nat", which means Isabelle is still using the plus definition from Nat. How can I get it to use my new definition of +?
Thank you
Your must use no_notation to remove the default plus-syntax which comes from the plus type class of the Groups theory.
no_notation Groups.plus_class.plus (infixl "+" 65)
Then you can use
notation suma (infixl "+" 65)
to add your own syntax.
(I have never tried to override such basic parts of the definitions. I guess it might lead to strange situations – especially for other people trying to work with your theory afterwards.)