1 theory Says

     2 imports Main

     3 begin

     4 

     5 typedecl principal

     6 

     7 consts Admin :: principal

     8 consts Alice :: principal

     9 

    10 consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _")

    11 consts del_file :: "bool"

    12 

    13 axiomatization where

    14   saysI[intro]: "F \<Longrightarrow> P says F" and

    15   saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2"

    16 

    17 lemma

    18   assumes a1: "(Admin says del_file) \<longrightarrow> del_file"

    19   and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"

    20   and     a3: "Alice says del_file"

    21   shows "del_file"

    22 proof -

    23   from a3 have "Admin says (Alice says del_file)" by (rule saysI)

    24   with a2 have "Admin says del_file" by (rule saysE)

    25   with a1 show "del_file" by (rule mp)

    26 qed

    27 

    28 lemma

    29   assumes a1: "(Admin says del_file) \<longrightarrow> del_file"

    30   and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"

    31   and     a3: "Alice says del_file"

    32   shows "del_file"

    33 using a1 a2 a3 by auto

    34 

    35 

    36 end