-- Natural-number exponentiation
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Nat.Pow
import Core

def pow (base exponent : Nat) → Nat
  | base, zero => 1
  | base, succ(n) => mul(base, pow(base, n))

notation infixr 80 "^" => pow for Nat

theorem pow.zero (a : Nat)
  shows a ^ 0 = 1
proof
  simp [pow]

theorem pow.succ (a n : Nat)
  shows a ^ succ(n) = mul(a, a ^ n)
proof
  simp [pow]

theorem pow.closed (a : Nat, n : Nat)
  shows Nat(a ^ n)
proof
  induction n
  | zero => settle with pow, Naturals.constructor.zero, Naturals.constructor.succ
  | succ(k) using ih => settle with pow, mul.closed, ih

theorem pow.add (a n : Nat, m : Nat)
  shows a ^ add(m, n) = mul(a ^ m, a ^ n)
proof
  induction m
  | zero => settle with pow, add, mul, add.right_unit
  | succ(k) using ih => settle with pow, add, mul.associative, pow.closed, ih

lemma pow.sample
  shows 12 ^ 8 = 429981696
proof
  compute

eval 12 ^ 20