I have the following:

```
lemma "¬¬A ⟹ A"
proof -
assume "¬¬A"
from this have "¬A ⟹ False" unfolding not_def ..
```

I am trying to explain what .. does.

It does unification of ¬¬A and ¬A ⟶ False, and then converts object level implication to meta implication.

In Isabelle/Isar Reference, .. is explained as "by standard". But what automation is there in "standard", what it tries to do?

Gergely Buday said:

In Isabelle/Isar Reference,

`..`

is explained as`by standard`

. But what automation is there in`standard`

, what it tries to do?

Look a bit further on the same page. There it says:

In Isabelle/Pure,

standardperforms elementary introduction / elimination steps (rule), introduction of type classes (intro_classes) and locales (intro_locales).In Isabelle/HOL,

standardalso takes classical rules into account (cf. §9.4).

The `standard`

method is also what is invoked when you write `proof`

without a proof method; in fact, `..`

should be equivalent to `proof qed`

.

Last updated: Nov 11 2024 at 04:22 UTC