// Like in class 15, we work with a very simple (even simpler than in class)
// type of logical-formula syntax trees.

module Defs {
  // Expressions are just variables.
  type Variable = string
  datatype Exp =
    Var(x: Variable)

  // And predicates are just less-than comparisons.
  datatype Pred =
    LT(a: Exp, b: Exp)

  // We also assign a simple semantics (interpreter) to syntax.

  // Associate each variable with an integer value:
  type Assgn = Variable -> int

  ghost function InterpExp(asgn: Assgn, e: Exp): int {
    match e
    case Var(x) => asgn(x)
  }

  ghost predicate InterpPred(asgn: Assgn, p: Pred) {
    match p
    case LT(a, b) => InterpExp(asgn, a) < InterpExp(asgn, b)
  }

  // In general, we will be concerned with the meanings of implications from many
  // hypotheses to single conclusion predicates.  Let's represent a set of many
  // hypotheses with a set.
  type Preds = set<Pred>

  ghost predicate InterpPreds(asgn: Assgn, ps: Preds) {
    forall p :: p in ps ==> InterpPred(asgn, p)
  }

  // Hypotheses are *contradictory* when they can't possibly be true.
  ghost predicate Contradictory(ps: Preds) {
    forall asgn :: !InterpPreds(asgn, ps)
  }

  // Here is the right notion of logical entailment that we use to capture
  // correctness of our automated theorem prover.  Note that Implies can be used
  // to restate Contradictory with a 'p' value that can never be true, like one
  // variable being less than itself.
  ghost predicate Implies(ps: Preds, p: Pred) {
    forall asgn :: InterpPreds(asgn, ps) ==> InterpPred(asgn, p)
  }
}