--- a/progs/prove.scala	Sat Oct 04 00:36:51 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-import scala.language.implicitConversions
-import scala.language.reflectiveCalls
-import scala.util._
-
-abstract class Term 
-case class Var(s: String) extends Term 
-case class Const(s: String) extends Term 
-case class Fun(s: String, ts: List[Term]) extends Term
-
-abstract class Form
-case object True extends Form
-case object False extends Form
-case class Pred(s: String, ts: List[Term]) extends Form
-case class Imp(f1: Form, f2: Form) extends Form
-case class Says(p: String, f: Form) extends Form 
-case class And(f1: Form, f2: Form) extends Form 
-case class Or(f1: Form, f2: Form) extends Form 
-case class Sends(p: String, q: String, f: Form) extends Form
-case class Enc(f1: Form, f2: Form) extends Form
-
-case class Judgement(gamma: Set[Form], f: Form) {
-  def lhs = gamma
-  def rhs = f
-}
-
-// some syntactic sugar
-implicit def FormOps(f1: Form) = new {
-  def -> (f2: Form) = Imp(f1, f2)
-}
-implicit def StringOps(p: String) = new {
-  def says (f: Form) = Says(p, f)
-}
-implicit def SetFormOps(gamma: Set[Form]) = new {
-  def |- (f: Form) : Judgement = Judgement(gamma, f)
-}
-
-val Admin = "Admin"
-val Bob = "Bob"
-val Del = Pred("del_file", Nil)
-
-val Gamma: Set[Form] = 
-  Set( (Admin says Del) -> Del,
-       Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal = Gamma |- Del // request: provable or not?
-
-def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
-  s.map (e => (e, s - e))
-
-
-def prove(j: Judgement, sc: () => Unit) : Unit = {
-  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
-  else { 
-    prove1(j, sc);
-    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
-  }
-}
-
-def prove1(j: Judgement, sc: () => Unit) : Unit = 
-  j.rhs match {
-    case True => sc ()
-    case False => ()
-    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
-    case Says(p, Enc(f1, f2)) => 
-      prove(j.lhs |- Says(p, f1), 
-            () => prove(j.lhs |- Says(p, f2), sc))
-    case Says(p, f1) => prove(j.lhs |- f1, sc) 
-    case Or(f1, f2) => 
-      { prove(j.lhs |- f1, sc);
-        prove(j.lhs |- f2, sc) }
-    case And(f1, f2) => 
-      prove(j.lhs |- f1, 
-            () => prove(j.lhs |- f2, sc))
-    case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
-    case _ => ()
-  }
-
-def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
-  f match {
-    case True => prove(lhs_rest |- rhs, sc)
-    case False => sc ()
-    case And(f1, f2) =>
-      prove(lhs_rest + f1 + f2 |- rhs, sc)
-    case Imp(f1, f2) => 
-      prove(lhs_rest |- f1, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Sends(p, q, f) => 
-      prove(lhs_rest |- (p says f), 
-            () => prove(lhs_rest + (q says f) |- rhs, sc))
-    case Enc(f1, f2) => 
-      prove(lhs_rest |- f1, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Or(f1, f2) => 
-      prove(lhs_rest + f1 |- rhs, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Says(p, Enc(f1, f2)) => 
-      prove(lhs_rest |- Says(p, f2), 
-            () => prove(lhs_rest + Says(p, f1) |- rhs, sc))
-    case Says(p, Imp(f1, f2)) => 
-      prove(lhs_rest |- Says(p, f1), 
-            () => prove(lhs_rest + Says(p, f2) |- rhs, sc))
-     
-    case _ => ()
-  }
-
-// function that calls prove and returns immediately once a proof is found
-def run (j : Judgement) : Unit = {
-  def sc () = { println ("Yes!"); throw new Exception }
-  Try(prove(j, sc)) getOrElse ()
-} 
-
-run (goal)
-
-run (Set[Form]() |- False -> Del)
-run (Set[Form]() |- True -> Del)
-run (Set[Form]() |- Del -> True)
-run (Set[Form]() |- Del -> Del)
-run (Set[Form]() |- Del -> Or(False, Del))
-
-
-val Gamma1 : Set[Form] = 
-  Set( Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal1 = Gamma1 |- Del // not provable
-run (goal1)
-
-
-val f1 = "P" says Pred("F1", Nil)
-val f2 = "Q" says Pred("F2", Nil)
-run (Set[Form](And(f1, f2)) |- And(f2, f1))
-
-
-val Chr = "Christian"
-val HoD = "Peter"
-val Email = Pred("may_obtain_email", List(Const(Chr)))
-val AtLib = Pred("is_at_library", List(Const(Chr)))
-val Chr_Staff = Pred("is_staff", List(Const(Chr)))
-
-val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
-val Policy_Lib = And(Chr_Staff, AtLib) -> Email
-val HoD_says = HoD says Chr_Staff
-
-run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email)
-
-println("Server Example")
-
-def Connect(p: String, q: String) : Form =
-  Pred("Connect", List(Var(p), Var(q)))
-
-
-val A = "A"
-val B = "B"
-val S = "S"
-val CAB = Connect(A, B)
-val Msg = Pred("Msg", Nil)
-val KAS = Pred("Kas", Nil)
-val KBS = Pred("Kbs", Nil)
-val KAB = Pred("Kab", Nil)
-
-val Gamma_big : Set[Form] = 
-  Set( A says CAB,
-       Sends(A, S, CAB), 
-       S says (CAB -> Enc(KAB, KAS)),
-       S says (CAB -> Enc(Enc(KAB, KBS), KAS)),
-       Sends(S, A, Enc(KAB, KAS)),
-       Sends(S, A, Enc(Enc(KAB, KBS), KAS)),
-       Sends(A, B, Enc(KAB, KBS)),
-       Sends(A, B, Enc(Msg, KAB)),
-       A says KAS,
-       B says KBS,
-       S says KAS,
-       A says (Enc(Msg, KAB))
-     )
-
-run (Gamma_big |- (B says Msg))
-
-