关于 Isabelle 引理证明的一些问题

Question

我已经定义了一个像“A ==> B ==>C”这样的引理并尝试使用挑剔，它给出了反例，我看到了 A = False ，B = False 和 C 的结果= 错误。

我只想知道当A和B成立，然后C成立时如何给出引理。

lemma "LTS_is_reachable (Δ (reg2nfa r1 v)) [] x y ⟹
       y ∈ ℱ (reg2nfa r1 v) ⟹
       LTS_is_reachable (Δ (reg2nfa r1 v)) [] y x"
  nitpick

Nitpicking formula... 
Nitpick found a potentially spurious counterexample for card 'a = 1:

  Free variables:
    r1 = LChr a⇩1?
    v = {a⇩1}
    x = [a⇩1]
    y = []

lemma "LTS_is_reachable (Δ (reg2nfa (LChr a1) {a1})) [] [a1] [] == False"
  by auto

lemma "[] \<in> ℱ (reg2nfa (LChr a1) {a1}) == False"
  by auto

lemma "LTS_is_reachable (Δ (reg2nfa (LChr a⇩1) {a⇩1})) []  []   [a⇩1] == False"
  by auto

Answer 1

当 nitpick 说它的结果“可能是虚假的”时，这意味着它可能是错误的。所以它就在这里。

关于 Isabelle 引理证明的一些问题

Some question on the lemma prove in Isabelle

isabelle