{0,1} as function type in Isabelle

I'm trying to write a function that takes a second parameter that can be either 0 or 1:

typedef f_2 = "{0::nat,1}"

function proj_add :: "(real × real) × f_2 ⇒ (real × real) × f_2 ⇒ (real × real) × f_2" where
  "proj_add ((x1,y1),l) ((x2,y2),j) = ((add (x1,y1) (x2,y2)), (l+j) mod 2)" 
    if "delta x1 y1 x2 y2 ≠ 0"
| "proj_add ((x1,y1),l) ((x2,y2),j) = ((ext_add (x1,y1) (x2,y2)), (l+j) mod 2)" 
    if "delta' x1 y1 x2 y2 ≠ 0"

If I write directly {0::nat,1} I get the error inner syntax error.

If I write f_2 I get the error undefined type name f_2.

What is the right way to write this definition in Isabelle?

Solution

There is the type bit in the theory HOL-Library.Bit with the two elements 0 and 1. This contains all the setup that's needed to make the 0 and 1 notation work for bits including pattern matching.