How to submit an argument to keyword proof?

Question

I would like to understand how keyword proof works in an Isar proof. I consulted the Isabelle/Isar reference, section 6.3.2 and Programming and Proving in Isabelle/HOL, section 4.1.

To summarise what I have learned, there are three ways of beginning a proof by the keyword proof:

• without any argument Isabelle finds a suitable introduction rule to the lemma being proved and applies it in a forward mode

• if a hyphen: - is supplied as an argument, then proof does nothing to the goal, avoiding any automatic rule being applied when it would lead to a blind alley

• if a specific rule, like rule name, unfold true_def, clarify or induct n is supplied, then it is applied to the goal in a forward mode

Am I right that the third case is like using apply with the argument supplied?

How is the automatic introduction rule in the first case picked by the system?

And, does the above fully describe the usage of proof?

Answer 1

Andreas gave a good description of how proof without a method argument works; I'll just cover some other parts of the question.

First, proof (method) is like apply (method) except for one thing: While apply leaves you in "prove" mode, where you can continue with more apply statements, proof transitions into "state" mode, where you must use a have or show statement to continue proving. Otherwise the effect on the goal state is the same.

I'd also like to point out that case 2 (proof -) is really an instance of case 3, because - is actually an ordinary proof method just like rule name or induct (you can also write apply -, for example). The hyphen - proof method does nothing, except that it will insert chained facts into the current goal, if it is given any chained facts.

Answer 2

The command proof without a method specification applies the method default. The method default is almost like rule, but if rule fails, then it tries next intro_classes and then unfold_locales. The method rule without being given a list of theorems tries all rules that are declared to the classical reasoner (intro, elim, and dest). If no facts are chained in, only intro rules are considered. Otherwise, all types of rules are tried. All chained-in facts must unify with the rules. dest rules are transformed into elim rules before they are applied.

You can print all declared rules with print_rules. Safe rules (intro!, elim!, ...) are preferred over normal rules (intro, elim, ...) and extra rules (intro?, elim?) come last.

You can also use rule without giving any rules. Then, it behaves like default, but without the fallbacks intro_classes and unfold_locales.