Отображение закона группы при допущениях

Question

Предположим, что add является функцией и {(x,y). e x y = 0} является определенным набором. Я хочу показать (схематично), что:

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

поэтому при определенных условиях набор и операция дают группу. Я сомневаюсь, как сформулировать это в Изабель. Я читал руководство по локализации документации, но не очень хорошо понимаю, как ее написать.

Answer 1

Вот способ написать это:

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)⦈" 

Вы также можете увидеть общую теорию и как доказать результат здесь:

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