How to define a lemma towards inductive predicate that can not hold

user_13276122 0
Viewed 44

Recently, I have learned the inductive predicate of Isabelle, like even and the reflexive transitive clousre. It seems that we can easily derive the cases that the predicate hold, but when we need to prove some case that inductive predicate not hold, it can not work easily.

And I have done a case like below, a LTS system is used to accept list which can finally arrived. The notJoinLTSlemma lemma is hard for me to prove. Any help would be appreciated.

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

inductive LTS_is_reachable :: "(('q, 'a) LTS * ('q * 'q) set) ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" where
   LTS_Empty[intro!]:"LTS_is_reachable Δ q [] q"|
   LTS_Step1[intro!]:"(∃q''. (q, q'') ∈ snd Δ ∧ LTS_is_reachable Δ q'' l q') ⟹ LTS_is_reachable Δ q l q'" |
   LTS_Step2[intro!]:"(∃q'' σ. a ∈ σ ∧ (q, σ, q'') ∈ fst Δ ∧ LTS_is_reachable Δ q'' w q') ⟹ LTS_is_reachable Δ q (a # w) q'"

lemma joinLTSlemma:"LTS_is_reachable l q x p ⟹  LTS_is_reachable l p y q''⟹ LTS_is_reachable l q (x@y) q''"
  proof (induction rule: LTS_is_reachable.induct)
    case (LTS_Empty Δ q)
    then show ?case by auto
  next
    case (LTS_Step1 q Δ l q')
    then show ?case by auto
  next
    case (LTS_Step2 a q Δ w q')
    then show ?case by auto
  qed

lemma notJoinLTSlemma:"LTS_is_reachable l q x p ⟹  ¬ LTS_is_reachable l p y q''⟹ ¬ LTS_is_reachable l q (x@y) q''"
  nitpick
isabelle
1 Answers

Your lemma notJoinLTSlemma does not hold, as nitpick already points out. Intuitively, the reason is that you're stating that "For some p, if p is reachable from q via x, and q'' is not reachable from p via y, then q'' is not reachable from q via x@y", which clearly is not true, since there may be another path in the LTS to reach q'' from q via x@y. In order to see that, you can inspect the counter-example given by nitpick. Therefore, the correct statement is "For all p, ...", that is:

lemma notJoinLTSlemma:"∀p. LTS_is_reachable l q x p ∧ ¬ LTS_is_reachable l p y q'' ⟹ ¬ LTS_is_reachable l q (x@y) q''"

Hope this helps.

user_129849900
Related