CODEWITHSUNDEEP
isabelletheorem-provinghol
Charlie Parker
Charlie Parker

Reputation: 5301

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

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?

Upvotes: 2

Views: 386

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

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.

Upvotes: 2

Related Questions