Why is a meta-universally quantified variable renamed and how is it prevented?

Question

Consider the following silly example

theory meta_all
imports Main
begin

lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done

lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
done

lemma "¬ (∃A. A ⊂ A)"
apply(rule notI)
apply(erule exE)

Next I would like to use the strict_subset lemma and substitute A for both A and B, and it will do that, but it will rename the existing A to Aa, totally defeating the purpose of introducing the lemma.

apply(insert strict_subset [where A="A" and B="A"])

If I use the derived lemma strict_subset2 everything works out fine, so I'm confident my reasoning is sound.

apply(insert strict_subset2)
apply(erule_tac x="A" in allE, erule_tac x="A" in allE)
apply(drule mp, assumption)
apply(erule bexE, erule notE, assumption)
done

end

The point is that most standard lemmas are of the form strict_subset and not of the form strict_subset2 and the makers of Isabelle can not have intended me to make my own strict_subset2 myself first, so ergo, I must be doing something wrong.

I would like to understand why A is renamed? I think it has something to do with the typing system, as I think I've also seen examples where meta-universal quantification was not a problem as long as the type was exactly right.

The other question is if I can prevent the renaming of A somehow?

Of course it is very well possible that both questions actually become irrelevant with the really right answer as I'm still quite fresh to Isabelle.

PS. Is it possible to get the nice symbols from Isabelle here too?

Answer 1

This is just a narrow technical answer, without embarking on the question if this path of experimentation makes any sense.

In your situation of

apply(insert strict_subset [where A="A" and B="A"])

the subgoal in question was this:

⋀A. A ⊂ A ⟹ False

but the locally bound (green) A is a so-called "parameter" of the subgoal, which means it is hidden inside the goal context. The use of strict_subset [where A="A" and B="A"] refers to the context of the proof text, not the proof goal. So you get different (free, undeclared) A, which is also indicated by special highlighting in the prover output.

There is a special set of (very old-fashioned) tactics that allow to dive under the implicit goal context and do some instantiation. Here is an example:

apply(cut_tac A = A and B = A in strict_subset)

Now you have the instance for the green A inside the goal state, but that also got split into too subgoals due to the form of your rule, and the way this odd cut_tac works.

Note that there are basically the following catgories of Isabelle/Isar proof methods:

• structured Isar proof steps: notably rule

• weakly structured steps with indication of reasoning direction: erule, drule, frule

• old-style tactic emulations that allow to enter the implicit goal context with its parameters: rule_tac, erule_tac, drule_tac, frule_tac

PS: You can copy-paste unicode output from Isabelle/jEdit into this text editor.

Answer 2

Structured proofs avoid the described naming problems and also allow you to perform single-step reasoning:

lemma  "¬ (∃A :: 'a set. A ⊂ A)"
proof
   assume "∃A :: 'a set. A ⊂ A"
   then obtain A :: "'a set" where "A ⊂ A" ..          (* by (rule exE) *)
   then have "∃a ∈ A. a ∉ A" by (rule strict_subset)
   then obtain a where "a ∉ A" "a ∈ A" ..              (* by (rule bexE) *)
   then show False ..                                  (* by (rule notE) *)
qed

.. is the same as by rule. You can use using [[rule_trace]] (and find_theorems) before a proof step to figure out which rule rule is using.

This structure makes it even more obvious what is happening in the proof. Of course the apply-style has definitely a more exploratory touch (which is why I often prefer it, when trying to find a proof), but structured proofs give you more control.