Stream: Beginner Questions

Topic: Understanding the automation in ..

Gergely Buday (Aug 01 2023 at 10:57):

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?

Wolfgang Jeltsch (Aug 01 2023 at 12:07):

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, standard performs elementary introduction / elimination steps (rule), introduction of type classes (intro_classes) and locales (intro_locales).

In Isabelle/HOL, standard also 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: Apr 28 2024 at 08:19 UTC