AddMul.dfy

datatype Expr =
  | Num(nat)
  | Add(Expr, Expr)
  | Mul(Expr, Expr)

function eval (e : Expr) : nat
{
  match e
  case Num(n) => n
  case Add(e1, e2) => eval(e1) + eval(e2)
  case Mul(e1, e2) => eval(e1) * eval(e2)
}

function optimise (e : Expr) : Expr 
{
  match e
  case Num(n) => Num(n)
  case Mul(x,y) => Mul (optimise(x), optimise(y))
  case Add(x,y) =>
    match x
    case Num(x_) => Add(optimise(x), optimise(y))
    case Add(x1,y1) => Add (optimise(x), optimise(y))
    case Mul (k,x_) =>
      match y
      case Num(y_) => Add(optimise(x),optimise(y))
      case Add(y1,y2) => Add(optimise(x), optimise(y))
      case Mul (k',y_) => 
        if k == k' then Mul(k, Add(optimise(x_), optimise(y_)))
        else Add(optimise(x), optimise(y))
}

method optimise_corect (e : Expr)
  ensures eval(e) == eval(optimise(e))
{
  match e{
    case Num(n) => {}
    case Mul(x,y) => { optimise_corect(x); optimise_corect(y); }
    case Add(x,y) => {
      optimise_corect(y);
      match x {
        case Num(x_) => {}
        case Add(x1,x2) => {optimise_corect(x); }
        case Mul(k,x_) => {
          optimise_corect(k);
          optimise_corect(x_);
          match y {
            case Num(y_) => {}
            case Add(y1,y2) => {optimise_corect(y1); optimise_corect(y2);}
            case Mul(k',y_) => {optimise_corect(k'); optimise_corect(y_);}
          }
        }
      }
    }
  }
}