英文:
How to prove such a lemma that one hold and other holds, the concat of two still holds
问题
以下是代码部分的中文翻译：
sorry
lemma inverse_concat_lemma: "如果一个自动机通过路径可达到 q (xa @ y)，那么存在 p 和 qa，使得 q = qa @ p 且 qa 可以通过路径可达到 xa，p 可以通过路径可达到 y。"
sorry
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') ∈ \<Delta>)"|
"LTS_is_reachable \<Delta> q (a # w) q' =
(\<exists>q'' \<sigma>. a \<in> \<sigma> ∧ (q, \<sigma>, q'') ∈ \<Delta> ∧ 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))";
至于你的最后一个问题，你问到 primrec 和 fun 在 Isabelle 中可以使用多少策略。然而，这个问题并不是很明确，因为 primrec 和 fun 是定义函数的关键词，而策略是用于证明和推理的步骤。如果你有更具体的问题或需要进一步的解释，请提供更多上下文，我将很乐意帮助你。
英文:
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.
答案1
得分: 2
第一个部分是对变量 x 进行归纳，其中普遍量化应用于变量 qa，即 apply (induction x arbitrary: qa)。
第二部分类似地，对变量 xa 进行归纳，其中普遍量化应用于变量 q。
一般来说，如果您想要证明一个递归定义的函数/谓词的性质，使用归纳法是有意义的。特别是，归纳法的结构应该反映递归的结构。
如果您在第一个引理中对变量 x 进行归纳，那么归纳的每一步都会精确地在列表的开头添加一个新的列表元素，这很有用，因为您的谓词 single_LTS_reachable_by_path 在每个递归步骤中会剥离列表的第一个元素。
英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论