module Int

import Nat
import UInt
import Base

public import IntDefs
public import IntAddSub
public import IntMult

// Need the following for integer literals.

export lit
export zero
export suc
export fromNat

// Properties of Less-Than or Equal

theorem int_less_equal_refl: all n:Int. n ≤ n
proof
  arbitrary n:Int
  switch n {
    case pos(n') {
      expand operator≤
      uint_less_equal_refl
    }
    case negsuc(n') {
      expand operator≤
      uint_less_equal_refl
    }
  }
end

theorem int_less_equal_trans: all m:Int, n:Int, o:Int.
  if m ≤ n and n ≤ o then m ≤ o
proof
  arbitrary m:Int, n:Int, o:Int
  switch m {
    case pos(m') {
      switch n {
        case pos(n') {
          switch o {
            case pos(o') {
              expand operator≤
              uint_less_equal_trans
            }
            case negsuc(o') { expand operator≤. }
          }
        }
        case negsuc(n') { expand operator≤. }
      }
    }
    case negsuc(m') {
      switch n {
        case pos(n') {
          switch o {
            case pos(o') { expand operator≤. }
            case negsuc(o') { expand operator≤. }
          }
        }
        case negsuc(n') {
          switch o {
            case pos(o') { expand operator≤. }
            case negsuc(o') {
              expand operator≤
              //suffices (if (n' ≤ m' and o' ≤ n') then o' ≤ m')
              //  by expand operator≤.
              assume nm_n_on
              apply uint_less_equal_trans[o',n',m'] to nm_n_on
            }
          }
        }
      }
    }
  }
end

theorem int_less_equal_antisymmetric:
  all x:Int, y:Int. 
  if x ≤ y and y ≤ x
  then x = y
proof
  arbitrary x:Int, y:Int
  assume xy_n_yx
  switch x {
    case pos(x') assume x_pos {
      switch y {
        case pos(y') assume y_pos {
          have: x' ≤ y' and y' ≤ x' by expand operator≤ in replace x_pos | y_pos in xy_n_yx
          have: x' = y' by apply uint_less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
          conclude pos(x') = pos(y')  by replace (recall x' = y').
        }
        case negsuc(y') assume y_neg {
          conclude false by expand operator≤ in replace x_pos | y_neg in xy_n_yx
        }
      }
    }
    case negsuc(x') assume x_neg {
      switch y {
        case pos(y') assume y_pos {
          conclude false by expand operator≤ in replace x_neg | y_pos in xy_n_yx
        }
        case negsuc(y') assume y_neg {
          have: x' ≤ y' and y' ≤ x' by expand operator≤ in replace x_neg | y_neg in xy_n_yx
          have: x' = y' by apply uint_less_equal_antisymmetric to (recall x' ≤ y' and y' ≤ x')
          conclude negsuc(x') = negsuc(y')  by replace (recall x' = y').
        }
      }
    }
  }
end

theorem lit_add_pos_pos: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_pos_pos

theorem lit_add_pos_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) + fromNat(lit(y)) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_pos_lit

theorem lit_add_lit_pos: all x:Nat, y:Nat.
  fromNat(lit(x)) + pos(fromNat(lit(y))) = pos(fromNat(lit(x) + lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator+.
end

auto lit_add_lit_pos

postulate lit_add_pos_negsuc_suc: all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(suc(x)))) = pos(fromNat(lit(y))) + negsuc(fromNat(lit(x)))

auto lit_add_pos_negsuc_suc

postulate lit_add_negsuc_pos_suc: all x:Nat, y:Nat. negsuc(fromNat(lit(suc(x)))) + pos(fromNat(lit(suc(y)))) = negsuc(fromNat(lit(x))) + pos(fromNat(lit(y)))

auto lit_add_negsuc_pos_suc

postulate lit_add_pos_suc_negsuc_zero: all x:Nat, y:Nat. pos(fromNat(lit(suc(y)))) + negsuc(fromNat(lit(zero))) = pos(fromNat(lit(y)))

auto lit_add_pos_suc_negsuc_zero

postulate lit_add_negsuc_zero_pos_suc: all x:Nat, y:Nat. negsuc(fromNat(lit(zero))) + pos(fromNat(lit(suc(y)))) = pos(fromNat(lit(y)))

auto lit_add_negsuc_zero_pos_suc

theorem neg_lit_zero: - pos(fromNat(lit(zero))) = pos(fromNat(lit(zero)))
proof
  expand operator-.
end

auto neg_lit_zero

theorem neg_uint_zero: - fromNat(lit(zero)) = pos(fromNat(lit(zero)))
proof
  expand operator-.
end

auto neg_uint_zero

theorem neg_pos_lit_suc: all x:Nat.
  - pos(fromNat(lit(suc(x)))) = negsuc(fromNat(lit(x)))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_pos_lit_suc

theorem neg_lit_suc: all x:Nat.
  - fromNat(lit(suc(x))) = negsuc(fromNat(lit(x)))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_lit_suc

theorem neg_negsuc_lit: all x:Nat.
  - negsuc(fromNat(lit(x))) = pos(fromNat(lit(suc(x))))
proof
  arbitrary x:Nat
  expand operator-.
end

auto neg_negsuc_lit

theorem abs_lit: all x:Nat. abs(pos(fromNat(lit(x)))) = fromNat(lit(x))
proof
  arbitrary x:Nat
  evaluate
end

auto abs_lit

theorem sign_pos_lit: all x:Nat. sign(pos(fromNat(lit(x)))) = positive
proof
  arbitrary x:Nat
  evaluate
end

auto sign_pos_lit

theorem sign_neg_lit: all x:Nat. sign(negsuc(fromNat(lit(x)))) = negative
proof
  arbitrary x:Nat
  evaluate
end

auto sign_neg_lit

theorem mult_pos_lit_pos_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  replace mult_pos_pos.
end

auto mult_pos_lit_pos_lit

theorem mult_lit_pos_lit: all x:Nat, y:Nat.
  fromNat(lit(x)) * pos(fromNat(lit(y))) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_lit_pos_lit

theorem mult_pos_lit_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * fromNat(lit(y)) = pos(fromNat(lit(x) * lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_pos_lit_lit

theorem mult_pos_lit_neg_lit: all x:Nat, y:Nat.
  pos(fromNat(lit(x))) * negsuc(fromNat(lit(y)))
  = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  replace mult_pos_negsuc.
end

auto mult_pos_lit_neg_lit

theorem mult_lit_neg_lit: all x:Nat, y:Nat.
  fromNat(lit(x)) * negsuc(fromNat(lit(y)))
  = - pos(fromNat(lit(x)) + fromNat(lit(x)) * fromNat(lit(y)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_lit_neg_lit

theorem mult_neg_lit_pos: all x:Nat, y:Nat.
  negsuc(fromNat(lit(x))) * pos(fromNat(lit(y)))
  = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x)))
proof
  arbitrary x:Nat, y:Nat
  replace int_mult_commute[negsuc(fromNat(lit(x))), pos(fromNat(lit(y)))].
end

auto mult_neg_lit_pos

theorem mult_neg_lit_lit: all x:Nat, y:Nat.
  negsuc(fromNat(lit(x))) * fromNat(lit(y))
  = - pos(fromNat(lit(y)) + fromNat(lit(y)) * fromNat(lit(x)))
proof
  arbitrary x:Nat, y:Nat
  expand operator*.
end

auto mult_neg_lit_lit