CODEWITHSUNDEEP
isabelle
Hongjian Jiang
Hongjian Jiang

Reputation: 297

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

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

Upvotes: 1

Views: 69

Answers (1)

Javier Díaz
Javier Díaz

Reputation: 1091

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.

Upvotes: 1

Related Questions