Showing group law under assumptions

Question

Assume that add is a function and {(x,y). e x y = 0} is certain set. I want to show (schematically) that:

lemma 
  assumes "∃ b. 1/c = b^2" "¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)"
  shows "group {(x,y). e x y = 0} add"

so under certain conditions the set and the operation give a group. My doubt is how to phrase this in Isabelle. I was reading the locale tutorial of the documentation but I don't see very well how to write it.

Answer 1

Here is the way to write it:

lemma group_law:
  assumes "∃ b. 1/c = b^2" "¬ (∃ b. b ≠ 0 ∧ 1/d = b^2)"
  shows "comm_group ⦇carrier = {(x,y). e x y = 0}, mult = add, one = (1,0)⦈" 

you may also see the general theory and how does one prove the result here:

https://github.com/rjraya/Isabelle/blob/master/curves/Hales.thy