The lemma defined in fun can work, but can not work in inductive predicate

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')"|
   "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')"


lemma DeltLTSlemma:"LTS_is_reachable Δ q x y \<Longrightarrow>LTS_is_reachable {(f a, b, f c)| a b c. (a,b,c)\<in> Δ } (f q) x (f y)"
  apply(induct x arbitrary:q)
   apply auto
  done

I've defined a fun LTS_is_reachable as above, and give a lemma to prove it. But for introduce a new relation in the LTS system, i change the form into the inductive predivate below. This lemma can not work, and I am not able to handle this.

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



inductive LTS_is_reachable :: "('q, 'a) LTS  \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool"  where 
   LTS_Empty:"LTS_is_reachable \<Delta> q [] q"|
   LTS_Step:"(\<exists>q'' \<sigma>. a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q') \<Longrightarrow> LTS_is_reachable \<Delta> q (a # w) q'"|
   LTS_Epi:"(\<exists>q''. (q,{},q'') \<in> \<Delta> \<and>  LTS_is_reachable \<Delta> q'' l q') \<Longrightarrow> LTS_is_reachable \<Delta> q l q'"  

inductive_cases LTS_Step_cases[elim!]:"LTS_is_reachable \<Delta> q (a # w) q'"
inductive_cases LTS_Epi_cases[elim!]:"LTS_is_reachable \<Delta> q l q'"
inductive_cases LTS_Empty_cases[elim!]:"LTS_is_reachable \<Delta> q [] q"




lemma "LTS_is_reachable {(q, v, y)} q x y  ⟹ LTS_is_reachable {(f q, v, f y)} (f q) x (f y)"
proof(induct x arbitrary:q)
  case Nil
  then show ?case
    by (metis (no_types, lifting) LTS_Empty LTS_Epi LTS_Epi_cases Pair_inject list.distinct(1) singletonD singletonI)
next
  case (Cons a x)
  then show ?case 
qed

Thank you very much for your help.

Solution

Using your inductive definition of LTS_is_reachable, you can prove your original lemma DeltLTSlemma by rule induction, that is, by using proof (induction rule: LTS_is_reachable.induct). You can learn more about rule induction in Section 3.5 of Programming and Proving in Isabelle/HOL. As a side remark, note that you can avoid using inductive_cases since nowadays structured proofs (i.e., Isar proofs) are strongly preferred over unstructured proofs (i.e., apply-scripts).