How can we force Isabelle to reveal to us what rule it's applying in the background in Isar when a proof starts?

Question

I was trying to prove:

lemma
  shows "¬ ev (Suc 0)"

I did:

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof

and it gave me really pretty goals:

proof (state)
goal (2 subgoals):
 1. Suc 0 = 0 ⟹ False
 2. ⋀n. ⟦Suc 0 = Suc (Suc n); ev n⟧ ⟹ False

that could probably make my proof readable.

It seems it applied some sort of cases in the background. But when I wrote cases the proof finished immediately instead of showing the above rule inversion cases explicitly. See:

lemma
  shows "¬ ev (Suc 0)"
proof (rule notI)
  assume "ev (Suc 0)"
  then show False 
  proof (cases)

which shows:

proof (state)
goal:
No subgoals!

which means I can just place a qed.

How can I figure out exactly what (introduction?) rules Isar is doing automatically in Isabelle?

From Section 6.4.2 in Isar-ref: "Unless given explicitly by the user, the default initial method is standard, which subsumes at least rule or its classical variant rule. These methods apply a single standard elimination or introduction rule according to the topmost logical connective involved. There is no separate default terminal method. Any remaining goals are always solved by assumption in the very last step." I am not certain if there is an easy way to get the name of the fact though. — user9716869 - supports Ukraine, May 20 '20 at 21:01

score 2 · Answer 1 · answered May 21 '20 at 08:13

As noted in the comment to your question, in your case, proof boils down to proof rule. The rule method (without any parameters) applies some fitting introduction/elimination rule. You can find out which one it is using the rule_trace attribute:

    using [[rule_trace]] apply rule

(or you could have done declare [[rule_trace]] globally somewhere above or note [[rule_trace]] in your Isar proof)

This says

    proof (prove)
    goal (2 subgoals):
     1. Suc 0 = 0 ⟹ False
     2. ⋀n. Suc 0 = Suc (Suc n) ⟹ ev n ⟹ False 
    rules:
        ev ?a ⟹ (?a = 0 ⟹ ?P) ⟹ (⋀n. ?a = Suc (Suc n) ⟹ ev n ⟹ ?P) ⟹ ?P

so it doesn't give you the name, unfortunately. But it is clear that this rule must come from the inductive command, because you didn't prove it yourself. If you do a print_theorems command right after the inductive command, you find that this is the theorem ev.cases, which is also the one that the cases method uses (except that the cases method also does some postprocessing simplification of the goal, as mentioned here).

The inductive command registers the ev.cases rule as an elim? rule, which means that the automation will not use it, but if you do something like apply rule, it will be considered.

How can we force Isabelle to reveal to us what rule it's applying in the background in Isar when a proof starts?

1 Answers1