diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Says.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Says.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,36 @@
+theory Says
+imports Main
+begin
+
+typedecl principal
+
+consts Admin :: principal
+consts Alice :: principal
+
+consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _")
+consts del_file :: "bool"
+
+axiomatization where
+  saysI[intro]: "F \<Longrightarrow> P says F" and
+  saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2"
+
+lemma
+  assumes a1: "(Admin says del_file) \<longrightarrow> del_file"
+  and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"
+  and     a3: "Alice says del_file"
+  shows "del_file"
+proof -
+  from a3 have "Admin says (Alice says del_file)" by (rule saysI)
+  with a2 have "Admin says del_file" by (rule saysE)
+  with a1 show "del_file" by (rule mp)
+qed
+
+lemma
+  assumes a1: "(Admin says del_file) \<longrightarrow> del_file"
+  and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"
+  and     a3: "Alice says del_file"
+  shows "del_file"
+using a1 a2 a3 by auto
+
+
+end