CODEWITHSUNDEEP
isabelle
MarciaNogueira
MarciaNogueira

Reputation: 21

Isabelle's Simplifier: How does it choose which rules to apply? [Specific Example]

I started using Isabelle recently and I am currently interested in studying and understanding how the simplifier works.

So, I started by doing some simple proofs and analysing the simplifier traces.

My question is related with the way the simplifier chooses which rules to apply during a proof.

Here is the specific example I have doubts about:

I was proving, by induction, that the sum of the first n naturals is equal to n*(n+1)/2. On case n=0, [here is my code for this case]

    lemma
    fixes n :: nat
    shows "(∑ i=0..n. i) = n * (n + 1) div 2"
    proof (induct n)
    case 0
    have "(∑ i=0..0. i) = (0::nat)" using [[simp_trace_new mode=full]] by simp
    also have " ... = 0 * (0 + 1) div 2" using [[simp_trace_new mode=full]] by simp
    finally show ?case .

[And the relevant part of the simplifier trace for the line "also have " ... = 0 * (0 + 1) div 2" using [[simp_trace_new mode=full]] by simp"]

Simplifier invoked 
  0 = 0 * (0 + 1) div 2 
    Apply rewrite rule? 
      Instance of Nat.One_nat_def: 1 ≡ Suc 0
      Trying to rewrite: 1 
        Successfully rewrote 
          1 ≡ Suc 0 
    Apply rewrite rule? 
      Instance of Nat.add_Suc_right: 0 + Suc 0 ≡ Suc (0 + 0)
      Trying to rewrite: 0 + Suc 0 
        Successfully rewrote 
          0 + Suc 0 ≡ Suc (0 + 0) 
    Apply rewrite rule? 
      Instance of Groups.monoid_add_class.add.right_neutral: 0 + 0 ≡ 0
      Trying to rewrite: 0 + 0 
        Successfully rewrote 
          0 + 0 ≡ 0 
    **Apply rewrite rule? 
      Instance of Nat.mult_Suc_right: 0 * Suc 0 ≡ 0 + 0 * 0
      Trying to rewrite: 0 * Suc 0 
        Successfully rewrote 
          0 * Suc 0 ≡ 0 + 0 * 0**

I don't understand why is it using the rule

Nat.mult_Suc_right: "m * Suc n = m + (m * n)"

to prove that 0 * Suc 0 ≡ 0 + 0 * 0, instead of using the rule

Nat.times_nat.mult_0: "0 * n = (0::nat)"

and concluding directly that 0 * Suc 0 ≡ 0?

Upvotes: 2

Views: 241

Answers (2)

Pedro
Pedro

Reputation: 81

The source code appears to be in the file Nat.thy (lines 265-273), inside HOL:

primrec times_nat where
  mult_0: "0 * n = (0::nat)"
| mult_Suc: "Suc m * n = n + (m * n)"

lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
  by (induct m) simp_all

lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
 by (induct m) (simp_all add: add.left_commute)

and the rule mult_0 is in the definition of times_nat, appearing first. So the ML implementation does not follow order of declaration in accessing the rules.

Upvotes: 2

Manuel Eberl
Manuel Eberl

Reputation: 8298

The simplifier is quite simplistic in this respect: it essentially chooses the first rule that it comes across that matches and applies that.

Upvotes: 0

Related Questions