空的三角洲引理证明在伊莎贝尔（Isabelle）

Question

我已经定义了下文的归纳谓词。在这里，我想证明一个称为emptydelta1的显而易见的引理。但是这里似乎存在一些问题。

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

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒  ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" where
   LTS_Empty[intro!]:"LTS_is_reachable Δ Δ' q [] q"|
   LTS_Step1:"(q, q'') ∈ Δ' ∧ LTS_is_reachable Δ Δ' q'' l q' ⟹ LTS_is_reachable Δ Δ' q l q'" |
   LTS_Step2[intro!]:"a  ∈ σ ∧ (q, σ, q'') ∈ Δ ∧ LTS_is_reachable Δ Δ' q'' w q' ⟹ LTS_is_reachable Δ Δ' q (a # w) q'"

引理是

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof(induction rule:LTS_is_reachable.cases)
case (LTS_Empty Δ Δ' q)
then show ?case by auto
next
  case (LTS_Step1 q q'' Δ' Δ l q')
then show ?case apply simp sorry
next
case (LTS_Step2 a σ q q'' Δ Δ' w q')
then show ?case by auto
qed

想法：BeaCause来自Delta1的列表中的元素，因此当Delta1为空时，列表的结果必须为空。

任何帮助将不胜感激！

Answer 1

首先，您应该对您的定义进行一些改进，以lts_is_reachable：

1. 请注意，参数Δ和Δ'是固定参数（即它们不会更改）。因此，您应该通过使用子句的encuctive定义的子句来提示isabelle。这样，伊莎贝尔能够生成更简单的归纳规则。

2. 您应该尝试避免使用进行复合假设，而是使用或更好的是，ISAR构造如果 和>和。这样，您允许更简单的证据和更好的自动化。

也就是说，您改进的lts_is_reachable的定义如下：

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒  ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" for Δ and Δ' where
  LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q [] q" |
  LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
  LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"

关于引理的证明，您应使用lts_is_reachable.indable.induct.induct而不是lts_is_reachable.cases作为通过计算诱导进行证明的规则。这样，您可以轻松地证明自己的引理如下：

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
proof (induction rule: LTS_is_reachable.induct)
  case (LTS_Empty q)
  then show ?case by simp
next
  case (LTS_Step1 q q'' l q')
  then show ?case by simp
next
  case (LTS_Step2 a σ q q'' w q')
  then show ?case by simp 
qed

或者，较短，如下所示：

lemma "LTS_is_reachable {} Δ' p x q ⟹ x = []"
  by (induction rule: LTS_is_reachable.induct) simp_all

希望这会有所帮助。