Усилитель Изабеллы: как он выбирает, какие правила применять? [Конкретный пример]

Question

Недавно я начал использовать Isabelle, и сейчас я заинтересован в изучении и понимании того, как работает упроститель.

Итак, я начал с простых доказательств и анализа трассировок упростителя.

Мой вопрос связан с тем, как упроститель выбирает, какие правила применять во время доказательства.

Вот конкретный пример у меня сомнения:

я доказать по индукции, что сумма первых п натуральных чисел равно N * (N + 1)/2. В случае п = 0, [здесь мой код для этого случая]

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 . 

[И соответствующая часть Simplifier следа для линии "также" ... = 0 * (0 + 1) ДИВ 2" , используя [[simp_trace_new режим = полный]] по простофиля "]

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** 

Я не понимаю, почему это с помощью правила

Nat.mult_Suc_right:" м * SUc п = m + (m * n) "

, чтобы доказать, что 0 * Suc 0 ≡ 0 + 0 * 0, вместо того, чтобы использовать правило

Nat.times_nat.mult_0: "0 * п = (0 :: физ)"

и заключая непосредственно, что 0 * Suc 0 ≡ 0?

Answer 1

Упрощение в этом отношении довольно упрощенное: оно по существу выбирает первое правило, которое оно встречает, которое соответствует и применяет это.

Answer 2

Исходный код, как представляется, в файле Nat.thy (строки 265-273), внутри 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) 

и правило mult_0 в определении times_nat, появляясь первым. Таким образом, реализация ML не соответствует порядку декларации при доступе к правилам.