Доказательство существования бесконечного пути в Изабель - PullRequest
Новая
       12

Доказательство существования бесконечного пути в Изабель

0 голосов
/ 05 января 2019

Рассмотрим следующий индуктивный предикат: 

inductive terminating where
 "(⋀ s'. s → s' ⟹ terminating s') ⟹ terminating s"

Я бы хотел доказать, что если узел s не заканчивается, существует бесконечная цепочка вида s0 → s1 → s2 → .... Что-то среди строк: 

 lemma "¬ terminating (c,s) ⟹ 
       ∃ cfs. (cfs 0 = (c,s) ∧ (∀ n. (cfs n) → (cfs (n+1))))"

Как я могу доказать это в Изабель?

Редактировать

Конечная цель - доказать следующую цель: 

lemma "(∀s t. (c, s) ⇒ t = (c', s) ⇒ t) ⟹
       terminating (c, s) = terminating (c', s) "

где ⇒ - семантика большого шага GCL. Возможно, для доказательства этой теоремы необходим другой метод.

1 Ответ

0 голосов
/ 05 января 2019

Если вам удобно использовать оператор выбора, вы можете легко создать свидетеля, используя SOME, например: 

primrec infinite_trace :: ‹'s ⇒ nat ⇒ 's› where 
  ‹infinite_trace c0 0 = c0›
| ‹infinite_trace c0 (Suc n) =
    (SOME c. infinite_trace c0 n → c ∧ ¬ terminating c)›

(я не был уверен в типах ваших значений s и (c,s) - поэтому я просто использовал 's для этого.)

Очевидно, что конструкция свидетеля потерпит неудачу, если в какой-то момент SOME не сможет выбрать значение, удовлетворяющее ограничению. Таким образом, еще нужно доказать, что не прекращение действительно распространяется (как это совершенно очевидно из определения): 

lemma terminating_suc:
  assumes ‹¬ terminating c›
  obtains c' where ‹c → c'› ‹¬ terminating c'›
  using assms terminating.intros by blast

lemma nontermination_implies_infinite_trace:
  assumes ‹¬ terminating c0›
  shows  ‹¬ terminating (infinite_trace c0 n) 
    ∧ infinite_trace c0 n → infinite_trace c0 (Suc n)›
  by (induct n,
     (simp, metis (mono_tags, lifting) terminating_suc assms exE_some)+)

Доказать свою экзистенциальную количественную оценку, используя infinite_trace (c,s) в качестве свидетеля, просто.

...