Использование правил внутри локали (группы) Изабель - PullRequest
Новая
       24

Использование правил внутри локали (группы) Изабель

1 голос
/ 04 октября 2019

Предположим, у меня есть следующая теорема: 

comm_group ⦇carrier = e_aff, mult = add, one = (1, 0)⦈

, и я хочу показать, что: 

add (add (x1,y1) (x2,y2)) (i (x2,y2)) = (x1,y1)

, где i - обратная операция группы. Это obviously имеет место в группе. Как я могу извлечь эти знания из предположения?

1 Ответ

2 голосов
/ 04 октября 2019

comm_group … - это предикат локали, т. Е. Вещь, которая показывает, что у вас действительно есть экземпляр локали. Чтобы фактически использовать его, обычно интерпретирует локаль: 

interpret comm_group "⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
  by (fact <insert your theorem here>)

После этого вам становятся доступны все теоремы, доказанные в контексте comm_group локали (например, m_assoc). При желании вы можете добавить префикс к этим именам (особенно полезно, если есть столкновения имен, особенно если у вас есть несколько интерпретаций одного и того же языка): 

interpret G: comm_group "⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
  by (fact <insert your theorem here>)

Тогда теорема будет называться G.m_assoc. Это описано в разделе 5 руководства по языку .

Кстати, вы можете рассмотреть возможность введения сокращения для вашей группы, например, 

define G where "G = ⦇carrier = e_aff, mult = add, one = (1, 0)⦈"

длясделать записи об этом менее громоздкими. Вы также можете заставить упрощатель Изабель автоматически развернуть это определение, выполнив 

define G where [simp]: "G = ⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
...