src/HOL/Auth/Guard/List_Msg.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/Guard/List_Msg.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2001  University of Cambridge
     4 *)
     5 
     6 section{*Lists of Messages and Lists of Agents*}
     7 
     8 theory List_Msg imports Extensions begin
     9 
    10 subsection{*Implementation of Lists by Messages*}
    11 
    12 subsubsection{*nil is represented by any message which is not a pair*}
    13 
    14 abbreviation (input)
    15   cons :: "msg => msg => msg" where
    16   "cons x l == {|x,l|}"
    17 
    18 subsubsection{*induction principle*}
    19 
    20 lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]
    21 ==> P l"
    22 by (induct l) auto
    23 
    24 subsubsection{*head*}
    25 
    26 primrec head :: "msg => msg" where
    27 "head (cons x l) = x"
    28 
    29 subsubsection{*tail*}
    30 
    31 primrec tail :: "msg => msg" where
    32 "tail (cons x l) = l"
    33 
    34 subsubsection{*length*}
    35 
    36 fun len :: "msg => nat" where
    37 "len (cons x l) = Suc (len l)" |
    38 "len other = 0"
    39 
    40 lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
    41 by (cases l) auto
    42 
    43 subsubsection{*membership*}
    44 
    45 fun isin :: "msg * msg => bool" where
    46 "isin (x, cons y l) = (x=y | isin (x,l))" |
    47 "isin (x, other) = False"
    48 
    49 subsubsection{*delete an element*}
    50 
    51 fun del :: "msg * msg => msg" where
    52 "del (x, cons y l) = (if x=y then l else cons y (del (x,l)))" |
    53 "del (x, other) = other"
    54 
    55 lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
    56 by (induct l) auto
    57 
    58 lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
    59 by (induct l) auto
    60 
    61 subsubsection{*concatenation*}
    62 
    63 fun app :: "msg * msg => msg" where
    64 "app (cons x l, l') = cons x (app (l,l'))" |
    65 "app (other, l') = l'"
    66 
    67 lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
    68 by (induct l) auto
    69 
    70 subsubsection{*replacement*}
    71 
    72 fun repl :: "msg * nat * msg => msg" where
    73 "repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))" |
    74 "repl (cons x l, 0, x') = cons x' l" |
    75 "repl (other, i, M') = other"
    76 
    77 subsubsection{*ith element*}
    78 
    79 fun ith :: "msg * nat => msg" where
    80 "ith (cons x l, Suc i) = ith (l,i)" |
    81 "ith (cons x l, 0) = x" |
    82 "ith (other, i) = other"
    83 
    84 lemma ith_head: "0 < len l ==> ith (l,0) = head l"
    85 by (cases l) auto
    86 
    87 subsubsection{*insertion*}
    88 
    89 fun ins :: "msg * nat * msg => msg" where
    90 "ins (cons x l, Suc i, y) = cons x (ins (l,i,y))" |
    91 "ins (l, 0, y) = cons y l"
    92 
    93 lemma ins_head [simp]: "ins (l,0,y) = cons y l"
    94 by (cases l) auto
    95 
    96 subsubsection{*truncation*}
    97 
    98 fun trunc :: "msg * nat => msg" where
    99 "trunc (l,0) = l" |
   100 "trunc (cons x l, Suc i) = trunc (l,i)"
   101 
   102 lemma trunc_zero [simp]: "trunc (l,0) = l"
   103 by (cases l) auto
   104 
   105 
   106 subsection{*Agent Lists*}
   107 
   108 subsubsection{*set of well-formed agent-list messages*}
   109 
   110 abbreviation
   111   nil :: msg where
   112   "nil == Number 0"
   113 
   114 inductive_set agl :: "msg set"
   115 where
   116   Nil[intro]: "nil:agl"
   117 | Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl"
   118 
   119 subsubsection{*basic facts about agent lists*}
   120 
   121 lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl"
   122 by (erule agl.induct, auto)
   123 
   124 lemma app_in_agl [intro]: "[| I:agl; J:agl |] ==> app (I,J):agl"
   125 by (erule agl.induct, auto)
   126 
   127 lemma no_Key_in_agl: "I:agl ==> Key K ~:parts {I}"
   128 by (erule agl.induct, auto)
   129 
   130 lemma no_Nonce_in_agl: "I:agl ==> Nonce n ~:parts {I}"
   131 by (erule agl.induct, auto)
   132 
   133 lemma no_Key_in_appdel: "[| I:agl; J:agl |] ==>
   134 Key K ~:parts {app (J, del (Agent B, I))}"
   135 by (rule no_Key_in_agl, auto)
   136 
   137 lemma no_Nonce_in_appdel: "[| I:agl; J:agl |] ==>
   138 Nonce n ~:parts {app (J, del (Agent B, I))}"
   139 by (rule no_Nonce_in_agl, auto)
   140 
   141 lemma no_Crypt_in_agl: "I:agl ==> Crypt K X ~:parts {I}"
   142 by (erule agl.induct, auto)
   143 
   144 lemma no_Crypt_in_appdel: "[| I:agl; J:agl |] ==>
   145 Crypt K X ~:parts {app (J, del (Agent B,I))}"
   146 by (rule no_Crypt_in_agl, auto)
   147 
   148 end