ほげほげ

NK.cpp

#include <iostream>
#include <map>

using namespace std;

typedef enum {
   IMPLIES,
   AND,
   OR,
   NOT,
   ATOMIC,
} PropType;


class Prop {
public:
   virtual PropType type() const = 0;
   friend ostream &operator<<(ostream &stream, const Prop *p) {
      return p->print(stream);
   }
   friend ostream &operator<<(ostream &stream, const Prop &p) {
      return p.print(stream);
   }
private:
   virtual ostream &print(ostream &stream) const = 0;
};

typedef map<char, const Prop*> assumption;

class AtomicProp : public Prop {
   const char ch_;
public:
   explicit AtomicProp(const char ch):ch_(ch){}
   PropType type() const {
      return ATOMIC;
   }
   char name() const {
      return ch_;
   }
private:
   ostream &print(ostream &stream) const {
      stream << ch_;
      return stream;
   }
};

class NotProp : public Prop {
   const Prop *prop_;
public:
   explicit NotProp(const Prop *p):prop_(p){}
   PropType type() const {
      return NOT;
   }
private:
   ostream &print(ostream &stream) const {
      if(NOT > prop_->type()) stream << "¬(" << prop_ << ")";
      else stream << "¬" << prop_;
      return stream;
   }
};

class AndProp : public Prop {
   const Prop *lp_;
   const Prop *rp_;
public:
   explicit AndProp(const Prop *lp, const Prop *rp):lp_(lp),rp_(rp){}
   PropType type() const {
      return AND;
   }
   const Prop *lhs() const {
      return lp_;
   }
   const Prop *rhs() const {
      return rp_;
   }
private:
   ostream &print(ostream &stream) const {
      if(AND >= lp_->type()) stream << "(" << lp_ << ")";
      else stream << lp_;
      stream << " ∧ ";
      if(AND >  rp_->type()) stream << "(" << rp_ << ")";
      else stream << rp_;
      return stream;
   }
};

class OrProp : public Prop {
   const Prop *lp_;
   const Prop *rp_;
public:
   explicit OrProp(const Prop *lp, const Prop *rp):lp_(lp),rp_(rp){}
   PropType type() const {
      return OR;
   }
   const Prop *lhs() const {
      return lp_;
   }
   const Prop *rhs() const {
      return rp_;
   }
private:
   ostream &print(ostream &stream) const {
      if(OR >= lp_->type()) stream << "(" << lp_ << ")";
      else stream << lp_;
      stream << " ∨ ";
      if(OR >  rp_->type()) stream << "(" << rp_ << ")";
      else stream << rp_;
      return stream;
   }
};


class ImpliesProp : public Prop {
   const Prop *lp_;
   const Prop *rp_;
public:
   explicit ImpliesProp(const Prop *lp, const Prop *rp):lp_(lp),rp_(rp){}
   PropType type() const {
      return IMPLIES;
   }
   const Prop *lhs() const {
      return lp_;
   }
   const Prop *rhs() const {
      return rp_;
   }
private:
   ostream &print(ostream &stream) const {
      if(AND >= lp_->type()) stream << "(" << lp_ << ")";
      else stream << lp_;
      stream << " -> ";
      if(AND >  rp_->type()) stream << "(" << rp_ << ")";
      else stream << rp_;
      return stream;
   }
};

class Theorem {
   assumption asp_;
   const Prop *con_; // conclusion
public:
   // law of excluded middle
   explicit Theorem(const Prop *con):con_(con) {}
   // assumption
   explicit Theorem(const Prop *con, const char name):con_(con) {
      assumption::iterator it = asp_.find(name);
      if(it != asp_.end()) asp_.erase(it);
      asp_.insert(pair<char, const Prop*>(name, con_));
   }
   // ordinaly constructor 1
   explicit Theorem(const Prop *con, assumption asp)
    :asp_(asp),con_(con){}
   // ordinaly constructor 2
   explicit Theorem(const Prop *con, assumption asp1, assumption asp2)
    :asp_(asp1),con_(con) {
      asp_.insert(asp2.begin(), asp2.end());
   }
   friend ostream &operator<<(ostream &stream, Theorem *th) {
      assumption::iterator it = th->asp_.begin();
      while(it != th->asp_.end()) {
         stream << it->first << ":" << it->second << endl;
         ++it;
      }
      if(th->asp_.empty()) {
         stream << "no assumptions" << endl;
      }
      stream << "-------------------" << endl;
      stream << th->con_ << endl;
      return stream;
   }
   assumption asp() const {
      return asp_;
   }
   const Prop *con() const {
      return con_;
   }
   const Prop *name2prop(const char name) const {
      assumption::const_iterator it = asp_.find(name);
      if(it == asp_.end()) return NULL;
      return it->second;
   }
};

namespace Rule {
   Theorem *and_intro(Theorem *t1, Theorem *t2) {
      const AndProp *con = new AndProp(t1->con(), t2->con());
      return new Theorem(con, t1->asp(), t2->asp());
   }
   Theorem *and_elim1(Theorem *t) {
      if(t->con()->type() != AND) exit(1);
      const AndProp *p = (AndProp*)t->con();
      const Prop *con = p->lhs();
      return new Theorem(con, t->asp());
   }
   Theorem *and_elim2(Theorem *t) {
      if(t->con()->type() != AND) exit(1);
      const AndProp *p = (AndProp*)t->con();
      const Prop *con = p->rhs();
      return new Theorem(con, t->asp());
   }
   Theorem *implication_intro(Theorem *t, const char name) {
      const Prop *p = t->name2prop(name);
      assumption asp = t->asp();
      asp.erase(name);
      return new Theorem(new ImpliesProp(p, t->con()), asp);
   }
   Theorem *or_intro1(Theorem *t, const Prop *p) {
      return new Theorem(new OrProp(t->con(), p), t->asp());
   }
   Theorem *or_intro2(Theorem *t, const Prop *p) {
      return new Theorem(new OrProp(p, t->con()), t->asp());
   }
   Theorem *lem(const Prop *p) {
      return new Theorem(new OrProp(p, new NotProp(p)));
   }
}

void test1() {
   Theorem *a = new Theorem(new AndProp(new AtomicProp('A'), new AtomicProp('B')), 'a');
   cout << a << endl;
   Theorem *t1 = Rule::and_elim2(a);
   cout << t1 << endl;
   Theorem *t2 = Rule::and_elim1(a);
   cout << t2 << endl;
   Theorem *t3 = Rule::and_intro(t1, t2);
   cout << t3 << endl;
   Theorem *con = Rule::implication_intro(t3, 'a');
   cout << con << endl;
}

void test2() {
   Theorem *a = new Theorem(new AtomicProp('B'), 'b');
   Theorem *b = Rule::or_intro2(a, new AtomicProp('A'));
   Theorem *con = Rule::implication_intro(b, 'b');
   cout << con;
}

int main(void) {
   // A ∧ B -> B ∧ A
   test1();
   cout << endl << endl;
   // B -> A ∨ B
   test2();
   return 0;
}