Search code examples
isabelle

Bad name in Iseabelle, how to fix it

When use the Isar to prove the subgoal:

sem_reg r2 v =
    {w. (Δ' (reg2nfa r2 v) = {} ∨ ℐ (reg2nfa r2 v) ≠ {} ∧ (∃q'∈ℱ (reg2nfa r2 v). ∃x∈Δ' (reg2nfa r2 v). case x of (q, q'') ⇒ LTS_is_reachable (Δ (reg2nfa r2 v)) q'' w q')) ∧
        (Δ' (reg2nfa r2 v) = {} ⟶ (∃q∈ℐ (reg2nfa r2 v). ∃x∈ℱ (reg2nfa r2 v). LTS_is_reachable (Δ (reg2nfa r2 v)) q w x))} ⟹
    sem_reg r1 v = {w. ∃q∈ℐ (reg2nfa r1 v). ∃x∈ℱ (reg2nfa r1 v). LTS_is_reachable (Δ (reg2nfa r1 v)) q w x} ⟹
    ¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r1) x_ Accept ⟹
    ¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r2) x_ Accept ⟹
    Δ' (reg2nfa r1 v) = {} ⟹ q_ ∈ ℐ (reg2nfa r1 v) ⟹ xa_ ∈ ℱ (reg2nfa r1 v) ⟹ LTS_is_reachable (Δ (reg2nfa r1 v)) q_ x_ xa_ ⟹ False

I have written a lemma like that

lemma subGoal1: "sem_reg r2 v =
    {w. (Δ' (reg2nfa r2 v) = {} ∨ ℐ (reg2nfa r2 v) ≠ {} ∧ (∃q'∈ℱ (reg2nfa r2 v). ∃x∈Δ' (reg2nfa r2 v). case x of (q, q'') ⇒ LTS_is_reachable (Δ (reg2nfa r2 v)) q'' w q')) ∧
        (Δ' (reg2nfa r2 v) = {} ⟶ (∃q∈ℐ (reg2nfa r2 v). ∃x∈ℱ (reg2nfa r2 v). LTS_is_reachable (Δ (reg2nfa r2 v)) q w x))} ⟹
    sem_reg r1 v = {w. ∃q∈ℐ (reg2nfa r1 v). ∃x∈ℱ (reg2nfa r1 v). LTS_is_reachable (Δ (reg2nfa r1 v)) q w x} ⟹¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r1) x Accept ⟹
    ¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r2) x Accept ⟹
    Δ' (reg2nfa r1 v) = {} ⟹ q ∈ ℐ (reg2nfa r1 v) ⟹ xa ∈ ℱ (reg2nfa r1 v) ⟹ LTS_is_reachable (Δ (reg2nfa r1 v)) q x xa ⟹ False" 
proof -
  assume "sem_reg r2 v =
    {w. (Δ' (reg2nfa r2 v) = {} ∨ ℐ (reg2nfa r2 v) ≠ {} ∧ (∃q'∈ℱ (reg2nfa r2 v). ∃x∈Δ' (reg2nfa r2 v). case x of (q, q'') ⇒ LTS_is_reachable (Δ (reg2nfa r2 v)) q'' w q')) ∧
        (Δ' (reg2nfa r2 v) = {} ⟶ (∃q∈ℐ (reg2nfa r2 v). ∃x∈ℱ (reg2nfa r2 v). LTS_is_reachable (Δ (reg2nfa r2 v)) q w x))}" and
    "sem_reg r1 v = {w. ∃q∈ℐ (reg2nfa r1 v). ∃x∈ℱ (reg2nfa r1 v). LTS_is_reachable (Δ (reg2nfa r1 v)) q w x}" and a3:"¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r1) x Accept" and 
    "¬ LTS_is_reachable (trans2Del1 r1 v ∪ trans2Del1 r2 v) (Node r2) x Accept" and 
    "Δ' (reg2nfa r1 v) = {}" and "q ∈ ℐ (reg2nfa r1 v)" and a1:"xa ∈ ℱ (reg2nfa r1 v)" and a2:"LTS_is_reachable (Δ (reg2nfa r1 v)) q x xa" 
  then have c1:"q = Node r1" by auto
  from a1 have c2:"xa = Accept" by auto 
  from a2 c1 c2 have c3:"LTS_is_reachable (Δ (reg2nfa r1 v)) (Node r1) x Accept" by auto
  from a3 have c4:"¬ LTS_is_reachable (Δ (reg2nfa r1 v) ∪ Δ (reg2nfa r2 v)) (Node r1) x Accept" by (auto simp:transEqDel)
  from c4 have c5:"¬ LTS_is_reachable (Δ (reg2nfa r1 v)) (Node r1) x Accept" by (auto simp:UnionE)
  from c3 c5 show "False" by auto
qed

But it seems that q_ doesn't match the q. So this proof can not succeed, how to rename it or fix it. And it mentions that bad name q_.

Solution

  • You are dealing with this situation in the wrong way. Copying large amounts of text leads to all sorts of problems. Instead of setting up a separate lemma and copying the text of your subgoal, I suggest you use a built-in command (itself called "subgoal") so that you can have access to your local assumptions directly. It is described in section 7.2 of the reference manual, which you can download here:

    https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2021-1/doc/isar-ref.pdf

    It's clear from your original subgoal that you were already in difficulties. In the last line we see variables called q_, x_, xa_. Variable names with trailing underscores are a warning that you have a fatal variable name clash, so you must have done something wrong before reaching the subgoal at the top of your question.