娱乐中定义的引理可以起作用，但不能在归纳谓词中起作用

Question

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

我已经定义了一个有趣的lts_is_reachable，如上所述，并给出一个引理以证明它。但是，为了在LTS系统中引入新的关系，我将形式更改为下面的归纳预期。这种引理无法正常工作，我无法处理。

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

非常感谢您的帮助。

Answer 1

使用lts_is_reachable的归纳定义，您可以证明您的原始引理deltltslemma by 规则诱导，也就是说，使用证明规则：LTS_IS_REACHABLE.IND）。您可以在编程编程并证明
isabelle/hol 。附带说明，请注意，您可以避免使用encuctive_cases，因为如今结构化的证明（即，ISAR证明）比非结构化的证明（即，应用 -scripts）强烈首选。