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, 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).
standard method is also what is invoked when you write
proof without a proof method; in fact,
.. should be equivalent to
Last updated: Dec 07 2023 at 08:19 UTC