(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Exponential.ma: Exponential (raising to a power) over the natural numbers. *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "Nat.ma".

include "Equality.ma".
include "Connectives.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Syntax.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

notation "hvbox(n^m)"
  left associative with precedence 52
  for @{ 'exponential $n $m }.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Exponential.                                                               *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec exponential (m: Nat) (n: Nat) on n ≝
  match n with
    [ Z ⇒ S (Z)
    | S o ⇒ m * (exponential m o)
    ].
    
(* DPM Bug: Matita's standard notation gets in the way here.  Cannot use
            'exponential instead of 'exp.                                     *)
interpretation "Nat exponential" 'exp n m = (exponential n m).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlemma exponential_zero_succ_zero:
  ∀n: Nat.
    ¬(n = Z) → n^Z = (S Z).
  #n.
  nelim n.
  //.
  #N H.
  //.
nqed.

nlemma exponential_succ_zero_neutral:
  ∀n: Nat.
    n^(S Z) = n.
  #n.
  nelim n.
  //.
  #N H.
  nnormalize.
  nrewrite > (multiplication_succ_zero_right_neutral ?).
  @.
nqed.

nlemma succ_zero_exponential_succ_zero:
  ∀m: Nat.
    (S Z)^m = S Z.
  #m.
  nelim m.
  //.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite > (plus_zero ?).
  @.
nqed.

naxiom exponential_addition_exponential_multiplication:
  ∀m, n, o: Nat.
    (m^n) * (m^o) = m^(n + o).

(*
nlemma exponential_exponential_multiplication:
  ∀m, n, o: Nat.
    (m^n)^o = m^(n × o).
  #m n o.
  nelim n.
  nnormalize.
  //.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (exponential_addition_exponential_multiplication m o (N × o)).
  nrewrite < H.
*)