isabelle

How to prove such a lemma that one hold and other holds, the concat of two still holds

For some purpose, I want to prove such a lemma: if one automaton could be reachable and another automaton could be reachable, such that the concat of these two automata could be reachable. The qa is a list and x is an LTS transition.

lemma concat_lemma:"single_LTS_reachable_by_path qa x ⟹ single_LTS_reachable_by_path q xa ⟹ single_LTS_reachable_by_path (qa @ q) (x @ xa)"
sorry

lemma inverse_concat_lemma: "single_LTS_reachable_by_path q (xa @ y) ⟹ ∃p qa. q = qa @ p ∧ single_LTS_reachable_by_path qa xa ∧ single_LTS_reachable_by_path p y"
sorry

The definition of single_LTS_reachable_by_path and others are below:

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


primrec LTS_is_reachable :: "('q, 'a) LTS \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
   "LTS_is_reachable \<Delta> q [] q' = (q = q' ∨ (q, {}, q') ∈ Δ)"|
   "LTS_is_reachable \<Delta> q (a # w) q' =
      (\<exists>q'' \<sigma>. a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q')"

primrec single_LTS_reachable_by_path :: "'a list ⇒ (('q,'a) LTS * 'q * 'q) list  ⇒ bool " where
"single_LTS_reachable_by_path w []= (w = [])"|
"single_LTS_reachable_by_path w (x# xs) = (∃p q. (w = p @ q ∧ LTS_is_reachable (fst x) (fst (snd x)) p (snd (snd x)) ∧ single_LTS_reachable_by_path q xs))"

For the primrec and fun in isabelle, how many tactic could be used.

Solution

  • The first one is just an induction over x with universal quantification over qa, i.e. apply (induction x arbitrary: qa).

    The second is, in a very similar fashion, an induction over xa with q universally quantified.

    Generally, if you want to prove some property of a function/predicate defined recursively, it makes sense to use induction. In particular, an induction whose structure mirrors the structure of the recursion.

    If you do an induction over x in your first lemma here, every step of the induction precisely adds a new list element at the beginning of the list, which is useful because your predicate single_LTS_reachable_by_path strips away the first element of the list in each recursive step.