Subato

Aussagenlogische Formel: Negationen nach innen

package name.panitz.util;
import java.util.function.Function;

public interface Logic{
  static record Var(String n) implements Logic{
    public String toString(){return n;}
  }
  static record Neg(Logic f) implements Logic{
    public String toString(){return "¬"+f;}
  }
  static record Implication(Logic l,Logic r) implements Logic{
    public String toString(){return "("+l+"→"+r+")";}
  }
  static record And(Logic l,Logic r) implements Logic{
    public String toString(){return "("+l+"∧"+r+")";}
  }
  static record Or(Logic l,Logic r) implements Logic{
    public String toString(){return "("+l+"∨"+r+")";}
  }

  default Logic everywhere(Function<Logic,Logic> f){
    var result = f.apply(this);
    if (result instanceof Neg n) return f.apply(new Neg(n.f.everywhere(f)));
    if (result instanceof Or n) return  f.apply(new Or(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof And n) return f.apply(new And(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Implication n) return f.apply(new Implication(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Var v) return v;
    throw new RuntimeException("unknown Logic class: "+this);
  }

  default Logic negationsInside(){
    return everywhere(x->x.moveTopLevelNegation());
  }

  default Logic moveTopLevelNegation(){
    if (this instanceof Neg n){
      if (n.f instanceof Neg n2) return n2.f;
      if (n.f instanceof And n2) return new Or(new Neg(n2.l),new Neg(n2.r));
      if (n.f instanceof Or n2) return new And(new Neg(n2.l),new Neg(n2.r));
      if (n.f instanceof Implication n2) return new And(n2.l,new Neg(n2.r));
    }
    return this;
  }
  default Logic and(Logic that){return new And(this,that);}
  default Logic or(Logic that){return new Or(this,that);}
  default Logic implication(Logic that){return new Implication(this,that);}
  default Logic neg(){return new Neg(this);}
}