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

user_1601580 0
Viewed 185

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?

theorem-proving hol isabelle
1 Answers

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.

user_21442270
Related