Nat Nullify Test Athena

nat_exp.ath

module Nat {
    datatype N := zero | (S N)

    declare +: [N N] -> N  [200] # precedence 200
    declare *: [N N] -> N  [300] # precedence 300
    declare **: [N N] -> N [400] # precedence 400

    declare Nul: [N] -> N

    # Some variables to use in definitions & proofs
    define [n m x y] := [?n:N ?m:N ?x:N ?y:N]
    define one := (S zero)
  
  
    # Universally quantified definitions of addition, multiplication and exponentiation
    assert* [ 
             (n + S m = S (n + m))
             (n + zero = n)
             (x * zero = zero)
             (x * (S y) = x * y + x)
             (x ** zero = one)
             (x ** S n = x * x ** n)  
    ]

    # Definitions of Nul function
    assert* nul-axioms := [(Nul S n = Nul n) (Nul zero = zero)]
    define [nul-n nul-z] := nul-axioms


    # 8 ** 3
    define eight-pow-3 := (Nul (** (S (S (S (zero))))  (S (S (S (S (S (S (S (S zero))))))))))



    # Proof that forall Natural numbers, Nul n = zero
    by-induction (forall n . Nul n = zero) {
        zero => (!chain-> [
            (Nul zero) = zero [nul-z]
        ])
        | (S n) => let {ind-hypothesis := (Nul n = zero)}
                        conclude conc := (Nul (S n) = zero)
                            (!chain-> [
                                (Nul S n) = (Nul n) [nul-n]
                                          = zero [ind-hypothesis]
                            ])
    }

    # Proof that Nul 8 ** 3 = zero
    (!chain  [eight-pow-3 = zero [(forall n . Nul n = zero)] ])
    
}