Search code examples
isabelle

Some question on the lemma prove in Isabelle

I have defined a lemma like "A ==> B ==>C" and try to use the nitpick, and it give the counterexample, I see the result of A = False , B = False, and C = False.

I just wanna know that how to give a lemma when A and B holds, then C holds.

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
Solution

  • When nitpick says its result is "potentially spurious", that means it might be wrong. And so it is here.