Empty Delta lemma prove in Isabelle

Question

I have defined an inductive predicate as below. And here i want to prove an obvious lemma which called emptyDelta1. But it seems that there exists some questions here.

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:"(q, q'') ∈ Δ' ∧ LTS_is_reachable Δ Δ' q'' l q' ⟹ LTS_is_reachable Δ Δ' q l q'" |
   LTS_Step2[intro!]:"a  ∈ σ ∧ (q, σ, q'') ∈ Δ ∧ LTS_is_reachable Δ Δ' q'' w q' ⟹ LTS_is_reachable Δ Δ' q (a # w) q'"

The lemma is

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof(induction rule:LTS_is_reachable.cases)
case (LTS_Empty Δ Δ' q)
then show ?case by auto
next
  case (LTS_Step1 q q'' Δ' Δ l q')
then show ?case apply simp sorry
next
case (LTS_Step2 a σ q q'' Δ Δ' w q')
then show ?case by auto
qed

Idea: beacause the element in list which comes from the Delta1, so that when the delta1 is empty, that the result of list must be empty.

Any helps will be appreciated!

user_12984990 · Answer

Firstly, there are a couple of improvements that should be made to your definition of LTS_is_reachable:

Note that the parameters Δ and Δ' are fixed parameters (i.e., they do not change). Thus, you should hint Isabelle by using the for clause of the inductive definition. This way, Isabelle is able to generate a simpler induction rule.
You should try to avoid ∧ for compound assumptions and instead use ⟹ or, even better, the Isar constructs if and and. This way, you allow for simpler proofs and better automation.

That is, your improved definition of LTS_is_reachable is the following:

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒  ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" for Δ and Δ' where
  LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q [] q" |
  LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
  LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"

Regarding the proof of your lemma, you should use LTS_is_reachable.induct instead of LTS_is_reachable.cases as the rule for a proof by computation induction. This way, you can easily prove your lemma as follows:

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof (induction rule: LTS_is_reachable.induct)
  case (LTS_Empty q)
  then show ?case by simp
next
  case (LTS_Step1 q q'' l q')
  then show ?case by simp
next
  case (LTS_Step2 a σ q q'' w q')
  then show ?case by simp 
qed

Or, much shorter, as follows:

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
  by (induction rule: LTS_is_reachable.induct) simp_all

Hope this helps.

Empty Delta lemma prove in Isabelle

1 Answers