theorem or_not: all P:bool, Q:bool.
  if (P or Q) and not P
  then Q
proof
  arbitrary P:bool, Q:bool
  suppose prem
  cases conjunct 0 of prem
  case p {
    conclude false  by apply (conjunct 1 of prem) to p
  }
  case q {
    q
  }
end

theorem ex_mid: all b:bool. b or not b
proof
  arbitrary b:bool
  switch b {
    case true { . }
    case false { . }
  }
end

theorem or_sym: all P:bool, Q:bool.  (P or Q) = (Q or P)
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

theorem and_sym: all P:bool, Q:bool.  (P and Q) = (Q and P)
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true { . }
    case false { . }
  }
end

theorem eq_true: all P:bool. P ⇔ (P = true)
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

theorem eq_false: all P:bool. not P ⇔ P = false
proof
  arbitrary P:bool
  switch P {
    case true { . }
    case false { . }
  }
end

theorem iff_equal: all P:bool, Q:bool.
  if (P ⇔ Q)  
  then P = Q
proof
  arbitrary P:bool, Q:bool
  switch P {
    case true {
      suppose q
      replace (apply eq_true to q).
    }
    case false {
      suppose not_q
      replace (apply eq_false to not_q).
    }
  }
end

theorem iff_symm: all P:bool, Q:bool.
  if (P ⇔ Q) then (Q ⇔ P)
proof
  arbitrary P:bool, Q:bool
  assume: P ⇔ Q
  have fwd: if Q then P by assume: Q apply (recall P ⇔ Q) to (recall Q)
  have bkwd: if P then Q by assume: P apply (recall P ⇔ Q) to (recall P)
  fwd, bkwd
end

theorem iff_trans: all P:bool, Q:bool, R:bool.
  if (P ⇔ Q) and (Q ⇔ R) then (P ⇔ R)
proof
  arbitrary P:bool, Q:bool, R:bool
  assume prem: (P ⇔ Q) and (Q ⇔ R)
  have fwd: if P then R by {
    assume: P
    have: Q by apply prem to recall P
    conclude R by apply prem to recall Q
  }
  have bkwd: if R then P by {
    assume: R
    have: Q by apply prem to recall R
    conclude P by apply prem to recall Q
  }
  fwd, bkwd
end

theorem contrapositive: all P : bool, Q : bool.
  if (if P then Q) and not Q then not P
proof
  arbitrary P : bool, Q : bool
  switch Q {
    case true { . }
    case false { . }
  }
end

theorem double_neg: all P: bool.
  (not (not P)) = P
proof
  arbitrary P:bool
  switch P {
    case true {
      evaluate
    }
    case false {
      evaluate
    }
  }
end

fun xor(x : bool, y : bool) {
  if x then not y
  else y
}

theorem xor_true: all b:bool. xor(true, b) = not b
proof
  arbitrary b:bool
  switch b {
    case true {
      evaluate
    }
    case false {
      evaluate
    }
  }
end

theorem xor_false: all b:bool. xor(false, b) = b
proof
  arbitrary b:bool
  switch b {
    case true {
      evaluate
    }
    case false {
      evaluate
    }
  }
end

theorem xor_commute: all a:bool, b:bool. xor(a,b) = xor(b,a)
proof
  arbitrary a:bool, b:bool
  switch a {
    case true {
      switch b {
        case true {
          evaluate
        }
        case false {
          evaluate
        }
      }
    }
    case false {
      switch b {
        case true {
          evaluate
        }
        case false {
          evaluate
        }
      }
    }
  }
end