6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

     7 where

     7 where

     8   "intrel (x, y) (u, v) = (x + v = u + y)"

     8   "intrel (x, y) (u, v) = (x + v = u + y)"

     9 

     9 

    10 quotient my_int = "nat \<times> nat" / intrel

    10 quotient my_int = "nat \<times> nat" / intrel

    12   apply(unfold EQUIV_def)

    11   apply(unfold EQUIV_def)

    13   apply(auto simp add: mem_def expand_fun_eq)

    12   apply(auto simp add: mem_def expand_fun_eq)

    14   done

    13   done

    15 

    14 

    16 thm my_int_equiv

    15 thm my_int_equiv