Изабель / HOL ограничивают кодомен - PullRequest
Новая
       73

Изабель / HOL ограничивают кодомен

1 голос
/ 27 января 2020

Я прошу прощения за то, что задал так много вопросов Изабель за последнее время. Прямо сейчас у меня есть проблема с типом.

Я хочу использовать синоним типа, введенный в AFP-теории.

type_synonym my_fun = "nat ⇒ real"

В моей собственной теории есть локаль, где:

fixes n :: nat

and f :: "my_fun"

and A :: "nat set"

defines A: "A ≡ {0..n}"

Однако, в моем случае использования, выход функции f всегда является натуральным числом в наборе {0..n}. Я хочу навязать это как условие (или есть ли лучший способ сделать это?). Я нашел только один способ:

assumes "∀v. ∃ i. f v = i ∧ i ∈ A"

, поскольку

assumes "∀v. f v ∈ A"

не работает.

Если Я позволил Изабель показать мне, какие типы шрифтов мне подходят:

∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set)

Но, конечно, теперь я не могу напечатать что-то вроде этого:

have "f ` {0..10} ⊆ A"

Но я должен это доказать. Я понимаю, откуда эта проблема. Однако я не знаю, как поступить в таком случае. Какой нормальный способ с этим справиться? Я хотел бы использовать my_fun, поскольку он имеет то же значение, что и в моей теории.

Спасибо (еще раз).

1 Ответ

1 голос
/ 28 января 2020

Если вы внимательно посмотрите на ∀v::nat. ∃i::nat. (f::nat ⇒ real) v = real i ∧ i ∈ (A::nat set), вы сможете увидеть механизм, который использовался для неявного преобразования типов между nat и real: это сокращение real (это вызывает of_nat определено для semiring_1 в Nat.thy), которое появляется в утверждении предположения в контексте локали.

Конечно, вы можете явно использовать тот же механизм. Например, вы можете определить A::real set как A ≡ image real {0..n} вместо A::nat set как A ≡ {0..n}. Тогда вы можете использовать range f ⊆ A вместо assumes "∀v. ∃ i. f v = i ∧ i ∈ A”. Однако я сомневаюсь, что существует общепринятый правильный способ сделать это: это зависит от того, чего именно вы пытаетесь достичь. Тем не менее, ради аргумента, ваша локаль может выглядеть так: 

type_synonym my_fun = "nat ⇒ real"

locale myloc_basis =
  fixes n :: nat

abbreviation (in myloc_basis) A where "A ≡ image real {0..n}"

locale myloc = myloc_basis +
  fixes f :: "my_fun"
  assumes range: "range f ⊆ A"

lemma (in myloc) "f ` {0..10} ⊆ A"
  using range by auto

Я хочу навязать это как условие (или есть лучший способ сделать это? ).

Ответ зависит от того, что известно о f. Если известно только условие в диапазоне f, как следует из формулировки вашего вопроса, тогда, я полагаю, вы можете утверждать, что это только предположение.

В качестве примечания, насколько мне известно, defines считается устаревшим, и лучше избегать его использования в спецификациях локали: stackoverflow.com /questions/56497678.

...