Есть ли в Isabelle аддитивная версия Power.thy?

В Изабель я определил функцию f:'a -> nat, где 'a - некоторая алгебраическая структура, которая расширяет моноид (то есть группу, полукольцо, кольцо, область целостности, поле, ...).

Я хотел бы использовать вывод этой функции как «коэффициенты» для моего типа 'a в других конструкциях. То есть, если x:'a и n:nat, я хотел бы иметь возможность использовать некоторую операцию ·:'a -> nat -> 'a, которая позволяет мне сообщить Изабель об этом n·x = x + x + ... + x.

Немного поискав, я нашел "Power.thy "теория и, в некотором смысле, делает то, что я хочу. Однако он делает это для «мультипликативной версии» моей проблемы. Это проблема, если я хочу изменить 'a, например, на целые числа. Его использование означало бы, что вместо вычисления n·x Изабель выполнит x^n. Есть ли аналогичная версия для "Power.thy "это то, что я хочу? Или есть другие способы обойти эту проблему?


theorem-proving isabelle
person Jonathan Julian    schedule 31.10.2017    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Я не знаю какой-либо предопределенной константы, реализующей такую ​​операцию, но ее можно легко реализовать, повторяя добавление, например, используя comppow на nat:

definition scale :: "nat => 'a => 'a" where
  "scale a n = ((plus a) ^^ n) 0"

где plus относится к операции сложения вашей структуры, а 0 - нейтральный элемент. Если вы используете классы арифметических типов от Isabelle / HOL, вы должны добавить ограничение сортировки 'a :: monoid к типу scale.

Существует также операция класса типов scaleR в Complex_Main, которая реализует такую ​​операцию масштабирования коэффициентов, но допускает real чисел, а не только nat, поэтому ваша структура может не удовлетворять всем требуемым аксиомам (класс типа real_vector).

person Andreas Lochbihler    schedule 01.11.2017
comment
Здорово! compow был именно тем, что мне было нужно. Я боялся, что мне может понадобиться доказать что-нибудь об этом, но до сих пор он работал без лишних теорем. Спасибо. - person Jonathan Julian; 02.11.2017

arrow_upward
1
arrow_downward

Совершенно идиоматический способ выразить это умножением и »of_nat«:

context semiring_1
begin

definition scale :: "nat ⇒ 'a ⇒ 'a"
  where "scale n = times (of_nat n)"

lemma [simp]:
  "scale 0 a = 0"
  "scale (Suc n) a = a + scale n a"
  by (simp_all add: scale_def algebra_simps)

lemma
  "((plus a) ^^ n) 0 = scale n a"
  by (induct n) (simp_all)

end
person Florian Haftmann    schedule 24.11.2017