Доступ к элементам типов данных

Question

Возможно ли в Изабель доступ к отдельным элементам типа данных? Допустим, у меня есть следующий тип данных:

datatype foo = mat int int int int 

и (например, в лемме)

fixes A :: foo

Можно ли получить доступ к отдельным элементам A? Или, в качестве альтернативы, исправить отдельные элементы (fix a b c d :: int), а затем определить A как mat a b c d?

Answer 1

В качестве альтернативы можно определить пользовательские функции экстрактора при указании типа данных. В вашем случае, например

datatype foo = Mat (mat_a : int) (mat_b : int) (mat_c : int) (mat_d : int)

должно сработать.

Затем вы можете получить доступ к первому элементу foo значение x от mat_a xвторой по mat_b x, и так далее.

Пример:

 value "mat_a (Mat 1 2 3 4)"

"1":: "int"

Answer 2

На логическом уровне вы можете использовать case синтаксис для деконструкции типа данных (т.е. case A of mat a b c d ⇒ …). Вы также можете определить свои собственные функции проекции, используя fun или же primrecнапример,

primrec foo1 where "foo1 (mat a b c d) = a"

В доказательство, вы можете получить доступ к значениям с помощью obtain и cases команда, например

obtain a b c d where "A = mat a b c d" by (cases A) auto

Что касается ваших вопросов об определениях, вы можете сделать локальные определения в доказательствах Изара следующим образом:

define A where "A = mat a b c d"

и вы можете развернуть это определение с помощью теоремы A_def,

Если вы хотите использовать свое определение уже в помещении или цели (и раскрыть его в теореме после его доказательства), вы можете использовать defines:

lemma
  defines "A ≡ mat a b c d"
  shows   …

Опять же, это дает вам факт A_def что вы можете использовать, чтобы развернуть определение.

Вы также можете использовать let ?A = mat a b c d или сопоставление с шаблоном is ввести сокращения. В отличие от предыдущих определений, они только на синтаксическом уровне, т.е. вы вводите ?A, но после разбора у вас есть mat a b c d, и вы также увидите mat a b c d на выходе. is работает так:

lemma
  shows "P (mat a b c d)" (is "P ?A")
proof -
  term ?A

Это также работает после "предполагает".