Доказательство над случаями, для которых заданный элемент включен в - PullRequest
Новая
       19

Доказательство над случаями, для которых заданный элемент включен в

2 голосов
/ 24 апреля 2020

Я хочу подтвердить следующую теорему, для которой у меня уже есть доказательство на бумаге, в Изабель: 

theorem 
  assumes "(X :: 'a set) ∩ (Y :: 'a set) = {}"
    and "trans (r :: 'a rel) ∧ total_in X r"
    and "trans (r' :: 'a rel) ∧ total_in Y r'"
  shows "∃ m. m ⊇ (r ∪ r') ∧ trans m ∧ total_in (X ∪ Y) m"
proof
  have 1: "(r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) ⊇ (r ∪ r')" by simp
  have 2: "trans (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" sorry
  have 3: "total_in (X ∪ Y) (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" sorry
  from 1 2 3 show "
      r ∪ r' ⊆ (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) 
    ∧ trans (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) 
    ∧ total_in (X ∪ Y) (r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" by auto
qed

Чтобы доказать 2 и 3, я хотел бы использовать различие в регистре какие подмножества сторон в данном члене нового отношения включаются в:

(a, b) ∈ (r ∪ r '∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y}) где (a ∈ X, b ∈ X) или (a ∈ X, b ∈ Y) и т. Д. c.

Для каждого из возможных случаев я бы хотел доказать подцели .

Есть ли какое-нибудь автоматическое c правило доказательства, которое может помочь мне формализовать это? Я совершенно новичок в Изабель и не уверен, что я бы даже искал в справочнике, чтобы найти это.

Кроме того, я недоволен необходимостью копировать "(r ∪ r' ∪ {(x, y) | x y. x ∈ X ∧ y ∈ Y})" повсюду. Как идиоматический c способ извлечь это новое отношение в какое-то определение, чтобы избежать копирования?

1 Ответ

3 голосов
/ 24 апреля 2020

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

definition total_in :: "'a set ⇒ 'a rel ⇒ bool"
  where "total_in X r ⟷ total_on X r ∧ r ⊆ X × X"
―‹I could not find the definition of ‹total_in› in the source code of
Isabelle/HOL. Please let me know if my guess is wrong.›

lemma total_inI[intro]:
  assumes "total_on X r" and "r ⊆ X × X"
  shows "total_in X r"
  using assms unfolding total_in_def by simp

lemma total_inE[elim]:
  assumes "total_in X r"
  obtains "total_on X r" and "r ⊆ X × X"
  using assms unfolding total_in_def by simp

lemma my_thm:
   ―‹In this case, there does not seem to be any need to specify the types 
  explicitly: type inference does not seem to struggle to infer the types 
  that you suggested.›
  ―‹There is rarely a need to combine assumptions using HOL's conjunction.›
  ―‹Some of the assumptions seem to be redundant. Of course, given that I
am not certain as to what is the meaning of ‹total_in›, I might be wrong.›
  assumes "total_in X r" and "total_in Y r'"
  shows "∃m. m ⊇ r ∪ r' ∧ trans m ∧ total_in (X ∪ Y) m"
proof(intro exI conjI) 
  ―‹Use the introduction of the existential quantifier and conjunction to
  start the proof.›
  let ?m = "(X ∪ Y) × (X ∪ Y)"
  ―‹Syntactic abbreviation.›
  ―‹Alternatively you can use ‹define› to provide a new definition inside
  the proof context, e.g. ‹define m where "m = (X ∪ Y) × (X ∪ Y)"››
  show "r ∪ r' ⊆ ?m" using assms by auto
  show "trans ?m" by (intro transI) auto
  show "total_in (X ∪ Y) ?m" by (auto simp: total_on_def)
qed

Дополнительные замечания:

  • Я не уверен, что именно подразумевается под total_in в формулировке вашего вопроса. Я не смог найти эту константу в исходном коде Изабель / HOL. Я позволил себе угадать его значение и дать свое собственное определение (пожалуйста, дайте мне знать, если мое предположение было неверным).
  • Мое доказательство не совсем идентично доказательству, которое вы предложили. Тем не менее, надеюсь, вы сможете изменить его в соответствии с вашими потребностями.

Я новичок в Изабель и не уверен, что я бы даже искал в ссылка, чтобы найти это.

Моей собственной отправной точкой для изучения Изабель была книга "Конкретная семантика" Тобиаса Нипкова и Джервина Кляйна. Когда вы освоитесь с основами, лучший способ приступить к поиску информации - начать поиск в официальной документации, то есть в учебниках и документе «isar-ref».

В этом конкретном случае , вполне вероятно, что вы бы sh посмотрели «Раздел 6: Доказательства» в «isar-ref».

...