Consider the following inductive predicate:
inductive terminating where
"(⋀ s'. s → s' ⟹ terminating s') ⟹ terminating s"
I would like to prove that if a node s is not terminating then there exists an infinite chain of the form s0 → s1 → s2 → .... Something among the lines of:
lemma "¬ terminating (c,s) ⟹
∃ cfs. (cfs 0 = (c,s) ∧ (∀ n. (cfs n) → (cfs (n+1))))"
How can I prove this in Isabelle?
Edit
The final goal is to prove the following goal:
lemma "(∀s t. (c, s) ⇒ t = (c', s) ⇒ t) ⟹
terminating (c, s) = terminating (c', s) "
where ⇒ is the big step semantics of the GCL. Perhaps another method is needed to prove this theorem.
If you are comfortable using the choice operator, you can easily construct a witness using SOME, for instance:
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)›
(I was not sure about the types of your s and (c,s) values—so I just used 's for that.)
Obviously, the witness construction would fail if at some point SOME cannot pick a value satisfying the constraint. So, one still has to prove that the non-termination indeed propagates (as is quite obvious from the definition):
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)+)
Proving your existential quantification using infinite_trace (c,s) as a witness is straight-forward.