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