# Re: [isabelle] surprising behavior of schematic_lemma

```On Mon, 15 Apr 2013, Ondřej Kunčar wrote:

```
```Recently I've experienced a bit odd behavior of schematic_lemma.
Let's consider this minimal example:

schematic_lemma surprise:
"?A ⟹ ?B ⟹ ?C"
proof -
fix a1 :: 'a
fix a2 :: 'a
fix A :: "'a set"
show "a1 ∈ A ⟹ a2 ∈ A ⟹ a1 = a1 ∧ a2 = a2" by auto
qed

Then what I get as a lemma surprise is the following theorem:
?a1.0 ∈ ?A ⟹ ?B ⟹ ?a1.0 = ?a1.0 ∧ ?a1.0 = ?a1.0
```
```
```
I am still trying to see what you are trying to do, to understand better from where the actual surprise is coming from.
```
```
Maybe it is just a misunderstanding about the scope of a1, a2, A. As written above, they become arbitrary in the goal context, and unification gets lots of freedom -- the details of it are explained in the usual foundational papers about Isabelle/Pure and Isar.
```

This one might be closer to what you intend:

schematic_lemma no_surprise:
fixes a1 :: 'a
fixes a2 :: 'a
fixes A :: "'a set"
shows "?A ⟹ ?B ⟹ ?C"
proof -
assume "a1 ∈ A" and "a2 ∈ A"
then show "a1 = a1 ∧ a2 = a2" by auto
qed

Makarius```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.