Formal Verification course: "personalized" lab

Arithmetic.scala

import fol.Expr
import lcf._
import Theorems._
import fol._
import fol.Expr._

object Arithmetic {

  /* == Theorems 3.2 == */

  /** Theorem (a) `a = a` */
  def equRefl(a: Expr): Theorem = {
    val t1 = axiom5(a)
    val t2 = axiom1(Plus(a, Zero), a, a)
    val t3 = t2(t1)
    val t4 = t3(t1)
    t4
  }

  /** Theorem (b) `a = b => b = a` */
  def equSym(a: Expr, b: Expr): Theorem = {
    val t1 = axiom1(a, b, a)
    val t2 = impliesSwap(t1)
    val t3 = t2(equRefl(a))
    t3
  }

  /** Theorem (c) `a = b => (b = c => a = c)` */
  def equCongruence2(a: Expr, b: Expr, c: Expr): Theorem = {
    val t1 = axiom1(b, a, c)
    val t2 = equSym(a, b)
    val t3 = impliesTrans(t2, t1)
    t3
  }

  /** Theorem (d) `b = a => (c = a => b = c)` */
  def equCongruence3(a: Expr, b: Expr, c: Expr): Theorem = {
    val t1 = equCongruence2(b, a, c)
    val t2 = impliesSwap(t1)
    val t3 = equSym(c, a)
    val t4 = impliesSwap(impliesTrans(t3, t2))
    t4
  }

  /** Theorem (e) `a = b => a + c = b + c` */
  def addRight(a: Expr, b: Expr, c: Expr): Theorem = {
    hypothesis(Equals(a, b)) { hyp =>
      val base = {
        val t1 = axiom5(a)
        val t2 = axiom5(b)
        val t3 = hyp
        val t4 = equCongruence2(Plus(a, Zero), a, b)(t1)(t3)
        val t5 = equCongruence3(b, Plus(a, Zero), Plus(b, Zero))(t4)(t2)
        t5
      }
      val induct = hypothesis(Equals(Plus(a, c), Plus(b, c))) { inductHyp =>
        val t1 = inductHyp
        val t2 = hyp // Unused here
        val t3 = axiom6(a, c)
        val t4 = axiom6(b, c)
        val t5 = t1
        val t6 = axiom2(Plus(a, c), Plus(b, c))(t5)
        val t7 = equCongruence2(Plus(a, Succ(c)), Succ(Plus(a, c)), Succ(Plus(b, c)))(t3)(t6)
        val t8 = equCongruence3(Succ(Plus(b, c)), Plus(a, Succ(c)), Plus(b, Succ(c)))(t7)(t4)
        t8
      }

      axiom9(Equals(Plus(a, InductVar), Plus(b, InductVar)), c)(base)(induct)
    }
  }

  /** Theorem (f) `a = 0 + a` */
  def addIdentityLeft(a: Expr): Theorem = {
    val base = {
      val t1 = equSym(Plus(Zero, Zero), Zero)(axiom5(Zero))
      t1
    }
    val induct = hypothesis(Equals(a, Plus(Zero, a))) { inductHyp =>
      val t1 = inductHyp
      val t2 = axiom6(Zero, a)
      val t3 = axiom2(a, Plus(Zero, a))(t1)
      val t4 = equCongruence3(Succ(Plus(Zero, a)), Succ(a), Plus(Zero, Succ(a)))(t3)(t2)
      t4
    }

    axiom9(Equals(InductVar, Plus(Zero, InductVar)), a)(base)(induct)
  }

  /** Theorem (g) `a' + b = (a + b)'` */
  def addSuccLeft(a: Expr, b: Expr): Theorem = {
    val base = {
      val t1 = axiom5(Succ(a))
      val t2 = axiom5(a)
      val t3 = axiom2(Plus(a, Zero), a)(t2)
      val t4 = equCongruence3(Succ(a), Plus(Succ(a), Zero), Succ(Plus(a, Zero)))(t1)(t3)
      t4
    }
    val induct = hypothesis(Equals(Plus(Succ(a), b), Succ(Plus(a, b)))) { inductHyp =>
      val t1 = inductHyp
      val t2 = axiom6(Succ(a), b)
      val t3 = axiom2(Plus(Succ(a), b), Succ(Plus(a, b)))(t1)
      val t4 = equCongruence2(Plus(Succ(a), Succ(b)), Succ(Plus(Succ(a), b)), Succ(Succ(Plus(a, b))))(t2)(t3)
      val t5 = axiom6(a, b)
      val t6 = axiom2(Plus(a, Succ(b)), Succ(Plus(a, b)))(t5)
      val t7 = equCongruence3(Succ(Succ(Plus(a, b))), Plus(Succ(a), Succ(b)), Succ(Plus(a, Succ(b))))(t4)(t6)
      t7
    }

    axiom9(Equals(Plus(Succ(a), InductVar), Succ(Plus(a, InductVar))), b)(base)(induct)
  }

  /** Theorem (h) `a + b = b + a` */
  def addCommutative(a: Expr, b: Expr): Theorem = {
    val (ab, ba) = (Plus(a, b), Plus(b, a))
    val base = {
      val t1 = axiom5(a)
      val t2 = addIdentityLeft(a)
      val t3 = equCongruence2(Plus(a, Zero), a, Plus(Zero, a))(t1)(t2)
      t3
    }
    val induct = hypothesis(Equals(ab, ba)) { inductHyp =>
      val t1 = inductHyp
      val t2 = axiom6(a, b)
      val t3 = addSuccLeft(b, a)
      val t4 = axiom2(ab, ba)(t1)
      val t5 = equCongruence2(Plus(a, Succ(b)), Succ(ab), Succ(ba))(t2)(t4)
      val t6 = equCongruence3(Succ(ba), Plus(a, Succ(b)), Plus(Succ(b), a))(t5)(t3)
      t6
    }

    axiom9(Equals(Plus(a, InductVar), Plus(InductVar, a)), b)(base)(induct)
  }

  /** Theorem (i) `a = b => c + a = c + b` */
  def addLeft(a: Expr, b: Expr, c: Expr): Theorem = {
    hypothesis(Equals(a, b)) { hyp =>
      val t1 = addRight(a, b, c)
      val t2 = addCommutative(a, c)
      val t3 = addCommutative(b, c)
      val t4 = hyp
      val t5 = t1(t4)
      val t6 = axiom1(Plus(a, c), Plus(c, a), Plus(b, c))(t2)(t5)
      val t7 = equCongruence2(Plus(c, a), Plus(b, c), Plus(c, b))(t6)(t3)
      t7
    }
  }

  // (a, b, c) = (t, r, s)

  /** Theorem (j) `(a + b) + c = a + (b + c)` */
  def addAssociative(a: Expr, b: Expr, c: Expr): Theorem = {
    val base = {
      val t1 = axiom5(Plus(a, b))
      val t2 = axiom5(b)
      val t3 = addLeft(Plus(b, Zero), b, a)(t2) // Note: literature contains a typo, it should be read "(i)" instead of "(j)"
      val t4 = equCongruence3(Plus(a, b), Plus(Plus(a, b), Zero), Plus(a, Plus(b, Zero)))(t1)(t3)
      t4
    }
    val induct = hypothesis(Equals(Plus(Plus(a, b), c), Plus(a, Plus(b, c)))) { inductHyp =>
      val t1 = inductHyp
      val t2 = axiom6(Plus(a, b), c)
      val t3 = axiom2(Plus(Plus(a, b), c), Plus(a, Plus(b, c)))(t1)
      val t4 = equCongruence2(Plus(Plus(a, b), Succ(c)), Succ(Plus(Plus(a, b), c)), Succ(Plus(a, Plus(b, c))))(t2)(t3)
      val t5 = axiom6(b, c)
      val t6 = addLeft(Plus(b, Succ(c)), Succ(Plus(b, c)), a)(t5)
      val t7 = axiom6(a, Plus(b, c))
      val t8 = equCongruence2(Plus(a, Plus(b, Succ(c))), Plus(a, Succ(Plus(b, c))), Succ(Plus(a, Plus(b, c))))(t6)(t7)
      val t9 = equCongruence3(Succ(Plus(a, Plus(b, c))), Plus(Plus(a, b), Succ(c)), Plus(a, Plus(b, Succ(c))))(t4)(t8)
      t9
    }

    axiom9(Equals(Plus(Plus(a, b), InductVar), Plus(a, Plus(b, InductVar))), c)(base)(induct)
  }

  /** Theorem (k) `a = b => a * c = b * c` */
  def timesRight(a: Expr, b: Expr, c: Expr): Theorem = {
    hypothesis(Equals(a, b)) { hyp =>
      val base = {
        val t1 = axiom7(a)
        val t2 = axiom7(b)
        val t3 = equSym(Times(b, Zero), Zero)(t2)
        val t4 = equCongruence2(Times(a, Zero), Zero, Times(b, Zero))(t1)(t3)
        t4
      }
      val induct = hypothesis(Equals(Times(a, c), Times(b, c))) { inductHyp =>
        val t1 = axiom8(a, c)
        val t2 = addRight(Times(a, c), Times(b, c), a)(inductHyp)
        val t3 = addLeft(a, b, Times(b, c))(hyp)
        val t4 = equCongruence2(Plus(Times(a, c), a), Plus(Times(b, c), a), Plus(Times(b, c), b))(t2)(t3)
        val t5 = equCongruence2(Times(a, Succ(c)), Plus(Times(a, c), a), Plus(Times(b, c), b))(t1)(t4)
        val t6 = axiom8(b, c)
        val t7 = equCongruence3(Plus(Times(b, c), b), Times(a, Succ(c)), Times(b, Succ(c)))(t5)(t6)
        t7
      }

      axiom9(Equals(Times(a, InductVar), Times(b, InductVar)), c)(base)(induct)
    }
  }

  /** Theorem (l) `0 * a = 0` */
  def timesNullLeft(a: Expr): Theorem = {
    val base = {
      val t1 = axiom7(Zero)
      t1
    }
    val induct = hypothesis(Equals(Times(Zero, a), Zero)) { inductHyp =>
      val t1 = axiom8(Zero, a)
      val t2 = axiom5(Times(Zero, a))
      val t3 = equCongruence2(Times(Zero, Succ(a)), Plus(Times(Zero, a), Zero), Times(Zero, a))(t1)(t2)
      val t4 = equCongruence2(Times(Zero, Succ(a)), Times(Zero, a), Zero)(t3)(inductHyp)
      t4
    }

    axiom9(Equals(Times(Zero, InductVar), Zero), a)(base)(induct)
  }

  /** Theorem (m) `a' * b = (a * b) + b` */
  def timesSuccLeft(a: Expr, b: Expr): Theorem = {
    val base = {
      val t1 = axiom7(Succ(a))
      val t2 = axiom7(a)
      val t3 = equCongruence3(Zero, Times(Succ(a), Zero), Times(a, Zero))(t1)(t2)
      val t4 = axiom5(Times(a, Zero))
      val t5 = equCongruence3(Times(a, Zero), Times(Succ(a), Zero), Plus(Times(a, Zero), Zero))(t3)(t4)
      t5
    }
    val induct = hypothesis(Equals(Times(Succ(a), b), Plus(Times(a, b), b))) { inductHyp =>
      val t1 = axiom8(Succ(a), b)
      val t2 = addRight(Times(Succ(a), b), Plus(Times(a, b), b), Succ(a))(inductHyp)
      val t3 = addAssociative(Times(a, b), b, Succ(a))
      val t4 = axiom6(b, a)
      val t5 = addSuccLeft(b, a)
      val t6 = equCongruence3(Succ(Plus(b, a)), Plus(b, Succ(a)), Plus(Succ(b), a))(t4)(t5)
      val t7 = addCommutative(Succ(b), a)
      val t8 = equCongruence2(Plus(b, Succ(a)), Plus(Succ(b), a), Plus(a, Succ(b)))(t6)(t7)
      val t9 = addLeft(Plus(b, Succ(a)), Plus(a, Succ(b)), Times(a, b))(t8)
      val t10 = equCongruence2(Plus(Plus(Times(a, b), b), Succ(a)), Plus(Times(a, b), Plus(b, Succ(a))), Plus(Times(a, b), Plus(a, Succ(b))))(t3)(t9)
      val t11 = addAssociative(Times(a, b), a, Succ(b))
      val t12 = equCongruence3(Plus(Times(a, b), Plus(a, Succ(b))), Plus(Plus(Times(a, b), b), Succ(a)), Plus(Plus(Times(a, b), a), Succ(b)))(t10)(t11)
      val t13 = axiom8(a, b)
      val t14 = addRight(Times(a, Succ(b)), Plus(Times(a, b), a), Succ(b))(t13)
      val t15 = equCongruence3(Plus(Plus(Times(a, b), a), Succ(b)), Plus(Plus(Times(a, b), b), Succ(a)), Plus(Times(a, Succ(b)), Succ(b)))(t12)(t14)
      val t16 = equCongruence2(Plus(Times(Succ(a), b), Succ(a)), Plus(Plus(Times(a, b), b), Succ(a)), Plus(Times(a, Succ(b)), Succ(b)))(t2)(t15)
      val t17 = equCongruence2(Times(Succ(a), Succ(b)), Plus(Times(Succ(a), b), Succ(a)), Plus(Times(a, Succ(b)), Succ(b)))(t1)(t16)
      t17
    }

    axiom9(Equals(Times(Succ(a), InductVar), Plus(Times(a, InductVar), InductVar)), b)(base)(induct)
  }

  /** Theorem (n) `a * b = b * a` */
  def timesCommutative(a: Expr, b: Expr): Theorem = {
    lazy val base = {
      val t1 = timesNullLeft(b)
      val t2 = axiom7(b)
      val t3 = equCongruence3(Zero, Times(Zero, b), Times(b, Zero))(t1)(t2)
      t3
    }
    val induct = hypothesis(Equals(Times(a, b), Times(b, a))) { inductHyp =>
      val t1 = timesSuccLeft(a, b)
      val t2 = addRight(Times(a, b), Times(b, a), b)(inductHyp)
      val t3 = equCongruence2(Times(Succ(a), b), Plus(Times(a, b), b), Plus(Times(b, a), b))(t1)(t2)
      val t4 = axiom8(b, a)
      val t5 = equCongruence3(Plus(Times(b, a), b), Times(Succ(a), b), Times(b, Succ(a)))(t3)(t4)
      t5
    }

    axiom9(Equals(Times(InductVar, b), Times(b, InductVar)), a)(base)(induct)
  }

  /** Theorem (o) `a = b => c * a = c * b` */
  def timesLeft(a: Expr, b: Expr, c: Expr): Theorem = {
    hypothesis(Equals(a, b)) { hyp =>
      val t1 = timesRight(a, b, c)(hyp)
      val t2 = timesCommutative(a, c)
      val t3 = axiom1(Times(a, c), Times(b, c), Times(c, a))(t1)(t2)
      val t4 = timesCommutative(b, c)
      val t5 = axiom1(Times(b, c), Times(c, a), Times(c, b))(t3)(t4)
      t5
    }
  }

  /* == Theorems 3.4 == */

  /** Theorem (a) `a * (b + c) = (a * b) + (a * c)` */
  def rightDistributivity(a: Expr, b: Expr, c: Expr): Theorem = {
    val base = {
      val t1 = axiom5(b)
      val t2 = timesLeft(Plus(b, Zero), b, a)(t1)
      val t3 = axiom7(a)
      val t4 = axiom5(Times(a, b))
      val t5 = equCongruence3(Times(a, b), Times(a, Plus(b, Zero)), Plus(Times(a, b), Zero))(t2)(t4)
      val t6 = addLeft(Times(a, Zero), Zero, Times(a, b))(t3)
      val t7 = equCongruence3(Plus(Times(a, b), Zero), Times(a, Plus(b, Zero)), Plus(Times(a, b), Times(a, Zero)))(t5)(t6)
      t7
    }
    val induct = hypothesis(Equals(Times(a, Plus(b, c)), Plus(Times(a, b), Times(a, c)))) { inductHyp =>
      val t1 = axiom6(b, c)
      val t2 = timesLeft(Plus(b, Succ(c)), Succ(Plus(b, c)), a)(t1)
      val t3 = axiom8(a, Plus(b, c))
      val t4 = equCongruence2(Times(a, Plus(b, Succ(c))), Times(a, Succ(Plus(b, c))), Plus(Times(a, Plus(b, c)), a))(t2)(t3)
      val t5 = addRight(Times(a, Plus(b, c)), Plus(Times(a, b), Times(a, c)), a)(inductHyp)
      val t6 = addAssociative(Times(a, b), Times(a, c), a)
      val t7 = equCongruence2(Plus(Times(a, Plus(b, c)), a), Plus(Plus(Times(a, b), Times(a, c)), a), Plus(Times(a, b), Plus(Times(a, c), a)))(t5)(t6)
      val t8 = axiom8(a, c)
      val t9 = addLeft(Plus(Times(a, c), a), Times(a, Succ(c)), Times(a, b))(equSym(Times(a, Succ(c)), Plus(Times(a, c), a))(t8))
      val t10 = equCongruence2(Plus(Times(a, Plus(b, c)), a), Plus(Times(a, b), Plus(Times(a, c), a)), Plus(Times(a, b), Times(a, Succ(c))))(t7)(t9)
      val t11 = equCongruence2(Times(a, Plus(b, Succ(c))), Plus(Times(a, Plus(b, c)), a), Plus(Times(a, b), Times(a, Succ(c))))(t4)(t10)
      t11
    }

    axiom9(Equals(Times(a, Plus(b, InductVar)), Plus(Times(a, b), Times(a, InductVar))), c)(base)(induct)
  }

  /** Theorem (b) `(a + b) * c = (a * c) + (b * c)` */
  def leftDistributivity(a: Expr, b: Expr, c: Expr): Theorem = {
    val t1 = timesCommutative(c, Plus(a, b))
    val t2 = rightDistributivity(c, a, b)
    val t3 = axiom1(Times(c, Plus(a, b)), Times(Plus(a, b), c), Plus(Times(c, a), Times(c, b)))(t1)(t2)
    val t4 = timesCommutative(c, a)
    val t5 = timesCommutative(c, b)
    val t6 = addRight(Times(c, a), Times(a, c), Times(b, c))(t4)
    val t7 = addLeft(Times(c, b), Times(b, c), Times(c, a))(t5)
    val t8 = equCongruence2(Times(Plus(a, b), c), Plus(Times(c, a), Times(c, b)), Plus(Times(c, a), Times(b, c)))(t3)(t7)
    val t9 = equCongruence2(Times(Plus(a, b), c), Plus(Times(c, a), Times(b, c)), Plus(Times(a, c), Times(b, c)))(t8)(t6)
    t9
  }

  /** Theorem (c) `(a * b) * c = a * (b * c)` */
  def timesAssociative(a: Expr, b: Expr, c: Expr): Theorem = {
    val base = {
      val t1 = axiom7(Times(a, b))
      val t2 = axiom7(b)
      val t3 = equCongruence3(Zero, Times(Times(a, b), Zero), Times(b, Zero))(t1)(t2)
      val t4 = equCongruence2(Times(Times(a, b), Zero), Times(b, Zero), Zero)(t3)(t2)
      val t5 = timesLeft(Times(b, Zero), Zero, a)(t2)
      val t6 = axiom7(a)
      val t7 = equCongruence2(Times(a, Times(b, Zero)), Times(a, Zero), Zero)(t5)(t6)
      val t8 = equCongruence3(Zero, Times(Times(a, b), Zero), Times(a, Times(b, Zero)))(t4)(t7)
      t8
    }
    val induct = hypothesis(Equals(Times(Times(a, b), c), Times(a, Times(b, c)))) { inductHyp =>
      val t1 = axiom8(Times(a, b), c)
      val t2 = addRight(Times(Times(a, b), c), Times(a, Times(b, c)), Times(a, b))(inductHyp)
      val t3 = equCongruence2(Times(Times(a, b), Succ(c)), Plus(Times(Times(a, b), c), Times(a, b)), Plus(Times(a, Times(b, c)), Times(a, b)))(t1)(t2)
      val t4 = rightDistributivity(a, Times(b, c), b)
      val t5 = equCongruence3(Plus(Times(a, Times(b, c)), Times(a, b)), Times(Times(a, b), Succ(c)), Times(a, Plus(Times(b, c), b)))(t3)(t4)
      val t6 = axiom8(b, c)
      val t7 = timesLeft(Times(b, Succ(c)), Plus(Times(b, c), b), a)(t6)
      val t8 = equCongruence3(Times(a, Plus(Times(b, c), b)), Times(Times(a, b), Succ(c)), Times(a, Times(b, Succ(c))))(t5)(t7)
      t8
    }

    axiom9(Equals(Times(Times(a, b), InductVar), Times(a, Times(b, InductVar))), c)(base)(induct)
  }

  /** Theorem (d) `a + c = b + c => a = b` */
  def addCancel(a: Expr, b: Expr, c: Expr): Theorem = {
    val base = hypothesis(Equals(Plus(a, Zero), Plus(b, Zero))) { hyp =>
      val t1 = axiom5(a)
      val t2 = axiom5(b)
      val t3 = axiom1(Plus(a, Zero), Plus(b, Zero), a)(hyp)(t1)
      val t4 = axiom1(Plus(b, Zero), a, b)(t3)(t2)
      t4
    }
    val induct = hypothesis(Implies(Equals(Plus(a, c), Plus(b, c)), Equals(a, b))) { inductHyp =>
      hypothesis(Equals(Plus(a, Succ(c)), Plus(b, Succ(c)))) { hyp =>
      val t1 = axiom6(a, c)
      val t2 = axiom6(b, c)
      val t3 = axiom1(Plus(a, Succ(c)), Succ(Plus(a, c)), Plus(b, Succ(c)))(t1)(hyp)
      val t4 = equCongruence2(Succ(Plus(a, c)), Plus(b, Succ(c)), Succ(Plus(b, c)))(t3)(t2)
      val t5 = axiom4(Plus(a, c), Plus(b, c))(t4)
      val t6 = inductHyp(t5)
      t6
    }}

    axiom9(Implies(Equals(Plus(a, InductVar), Plus(b, InductVar)), Equals(a, b)), c)(base)(induct)
  }

  /* == Theorems 3.5 == */

  /** Theorem (a) `a + 1 = a'` */
  def addOne(a: Expr): Theorem = {
    val t1 = axiom6(a, Zero)
    val t2 = axiom5(a)
    val t3 = axiom2(Plus(a, Zero), a)(t2)
    val t4 = equCongruence2(Plus(a, Succ(Zero)), Succ(Plus(a, Zero)), Succ(a))(t1)(t3)
    t4
  }

  /** Theorem (b) `a * 1 = a` */
  def timesIdentity(a: Expr): Theorem = {
    val t1 = axiom8(a, Zero)
    val t2 = axiom7(a)
    val t3 = addRight(Times(a, Zero), Zero, a)(t2)
    val t4 = equCongruence2(Times(a, Succ(Zero)), Plus(Times(a, Zero), a), Plus(Zero, a))(t1)(t3)
    val t5 = equSym(a, Plus(Zero, a))(addIdentityLeft(a))
    val t6 = equCongruence2(Times(a, Succ(Zero)), Plus(Zero, a), a)(t4)(t5)
    t6
  }

  /** Theorem (c) `a * 2 = a + a` */
  def timesTwo(a: Expr): Theorem = {
    val t1 = axiom8(a, Succ(Zero))
    val t2 = timesIdentity(a)
    val t3 = addRight(Times(a, Succ(Zero)), a, a)(t2)
    val t4 = equCongruence2(Times(a, Succ(Succ(Zero))), Plus(Times(a, Succ(Zero)), a), Plus(a, a))(t1)(t3)
    t4
  }

}

Axioms.scala

import fol._
import fol.parser.IRs
import fol.Expr._

object Axioms {
  
/** Axiom S1 `x1 = x2 => (x1 = x3 => x2 = x3)` */
  def axiom1(x1: Expr, x2: Expr, x3: Expr): Theorem =
    Theorem(Implies(Equals(x1, x2), Implies(Equals(x1, x3), Equals(x2, x3))))

  /** Axiom S2 `x1 = x2 => x1' = x2'` */
  def axiom2(x1: Expr, x2: Expr): Theorem =
    Theorem(Implies(Equals(x1, x2), Equals(Succ(x1), Succ(x2))))

  /** Axiom S3 `~(0 = x')` */
  def axiom3(x: Expr): Theorem =
    Theorem(Not(Equals(Zero, Succ(x))))

  /** Axiom S4 `x1' = x2' => x1 = x2` */
  def axiom4(x1: Expr, x2: Expr): Theorem =
    Theorem(Implies(Equals(Succ(x1), Succ(x2)), Equals(x1, x2)))

  /** Axiom S5 `x + 0 = x` */
  def axiom5(x: Expr): Theorem =
    Theorem(Equals(Plus(x, Zero), x))

  /** Axiom S6 `x1 + x2' = (x1 + x2)'` */
  def axiom6(x1: Expr, x2: Expr): Theorem =
    Theorem(Equals(Plus(x1, Succ(x2)), Succ(Plus(x1, x2))))

  /** Axiom S7 `x * 0 = 0` */
  def axiom7(x: Expr): Theorem =
    Theorem(Equals(Times(x, Zero), Zero))

  /** Axiom S8 `x1 * x2' = (x1 * x2) + x1` */
  def axiom8(x1: Expr, x2: Expr): Theorem =
    Theorem(Equals(Times(x1, Succ(x2)), Plus(Times(x1, x2), x1)))

  /** Axiom S9 `p(0) => ((forall x. p(x) => p(x')) => (forall x. p(x)))` */
  def axiom9(p: Formula, x: Expr): Theorem = {
    def subst(f: Formula, by: Expr): Formula = {
      def substExpr(e: Expr): Expr = {
        e match {
          case InductVar => by
          case FunApp(function, args) => FunApp(function, args.map(substExpr))
          case _ => e
        }
      }
      def substFormula(f: Formula): Formula = f match {
        case Not(inner) => Not(substFormula(inner))
        case And(lhs, rhs) => And(substFormula(lhs), substFormula(rhs))
        case Or(lhs, rhs) => Or(substFormula(lhs), substFormula(rhs))
        case Implies(lhs, rhs) => Implies(substFormula(lhs), substFormula(rhs))
        case Iff(lhs, rhs) => Iff(substFormula(lhs), substFormula(rhs))
        case Forall(id, inner) => Forall(id, substFormula(inner))
        case Exists(id, inner) => Exists(id, substFormula(inner))
        case Equals(lhs, rhs) => Equals(substExpr(lhs), substExpr(rhs))
        case PredApp(predicate, args) => PredApp(predicate, args.map(substExpr))
        case _ => f
      }

      substFormula(f)
    }

    Theorem(Implies(subst(p, Zero), Implies(Implies(subst(p, x), subst(p, Succ(x))), subst(p, x))))
  }

  /** `a => b` given `b` in the context of `a` */
  def hypothesis(a: Formula)(certificate: Theorem => Theorem): Theorem = {
    val b = certificate(Theorem(a)).formula
    Theorem(Implies(a, b))
  }
  
}