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