Определение отмены права в Изабель / HOL - PullRequest
Новая
       40

Определение отмены права в Изабель / HOL

0 голосов
/ 29 января 2020

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

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

f: A → B обладает свойством отмены права, если ∀ C: (∀ g, h: B → C): g ◦ f = h ◦ f = ⇒ g = h

Возможно ли это? Или, точнее, можно ли определить количество по типу?

Заранее спасибо

1 Ответ

0 голосов
/ 29 января 2020

Невозможно явно определить количество типов. Если вы докажете лемму с переменной типа, она неявно доказана для всех экземпляров типа.

В некоторых случаях вы можете использовать обходной путь и использовать тип V из записи AFP ZFC_in_HOL . Этот тип V в основном является типом с таким количеством элементов, что существует инъективная функция (почти?) Каждого типа HOL в V. Поэтому в некоторых случаях он может использоваться как некий тип Dynami c для экранирования системы типов. 

theory ...
  imports "ZFC_in_HOL.ZFC_Typeclasses"
begin


definition right_cancellation :: "('a ⇒ 'b) ⇒ bool"  where
  "right_cancellation f ≡ (∀g h :: 'b ⇒ V. g ∘ f = h ∘ f ⟶ g = h)"

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

definition right_cancellation :: "'c itself ⇒ ('a ⇒ 'b) ⇒ bool"  where
  "right_cancellation t f ≡ (∀ g h :: 'b ⇒ 'c. g ∘ f = h ∘ f ⟶ g = h)"

lemma 
  fixes f:: "'x ⇒ 'y"
  assumes as: "a1 ≠ (a2::'a)"
    and r: "right_cancellation (A::'a itself) f"
  shows "right_cancellation (B::'b itself) f"
...