fun 中定义的引理可以工作，但不能在 inductive predicate 中工作

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，即使用 proof (induction rule: LTS_is_reachable.induct).您可以在 Programming and Proving 的第 3.5 节中了解有关规则归纳的更多信息 Isabelle/HOL。作为附带说明，请注意您可以避免使用 inductive_cases，因为如今结构化证明（即 Isar 证明）比非结构化证明（即 apply-脚本）更受青睐。

fun 中定义的引理可以工作，但不能在 inductive predicate 中工作

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

isabelle