Proof that multiplication is commutative; following Rustan's proof in the Dafny demo at POPL 2022 virtual workshop

Mult.thy

begin

fun mult :: "nat ⇒ nat ⇒ nat" where
"mult x 0 = 0" |
"mult x y = x + mult x (y - 1)"

lemma mult_rec[simp]:
  "y ≠ 0 ⟹ mult x y = x + mult x (y - 1)"
  by (cases y) auto

(* this is probably somewhere in the standard library *)
lemma nat_lex_induct:
  fixes x :: nat and y :: nat
  assumes "⋀ x y. (⋀ x' y'. x' < x ⟹ P x' y') ⟹ (⋀ y'. y' < y ⟹ P x y') ⟹ P x y"
  shows "P x y"
  sorry

lemma mult_com:
  shows "mult x y = mult y x"
proof (induction x y rule: nat_lex_induct)
  case (1 x y)
  (* set up four cases that are proven to be exhaustive *)
  consider (a) "x = y" | (b) "x ≠ y" "x = 0" | (c) "y < x" "x ≠ 0" | (d) "x-1 < x" "x < y" "x ≠ 0" "y ≠ 0"
    by linarith
  then show ?case
  proof cases
    case a
    then show ?thesis
      by simp
  next
    case b
    with 1 show ?thesis
      by auto
  next
    case c
    with 1 show ?thesis
      by metis
  next
    case d
    have "mult x y = x + mult x (y-1)"
      using d by simp
    also have "... = x + mult (y-1) x"
      using `x < y` 1  by auto
    also have "... = x + y - 1 + mult (y-1) (x-1)"
      using d by simp
    also have "... = x + y - 1 + mult (x-1) (y-1)"
      using d 1 by metis
    also have "... = y + mult (x-1) y"
      using d by simp
    also have "... = y + mult y (x-1)"
      using `x-1 < x` 1 by simp
    finally show ?thesis
      using d by simp
  qed
qed


(* standard proof *)
lemma mult_com':
  shows "mult x y = mult y x"
proof -
  have "⋀ y. mult 0 y = 0"
  proof -
    fix y
    show "mult 0 y = 0"
      by (induction y) auto
  qed

  moreover have "⋀ x y. y ≠ 0 ⟹ mult y x = x + mult (y - 1) x"
  proof -
    fix x y :: nat
    assume "y ≠ 0"
    then show "mult y x = x + mult (y - 1) x"
      by (induction x) auto
  qed

  ultimately show ?thesis
    by (induction x) auto
qed