src/HOL/Auth/Guard/List_Msg.thy
author wenzelm
Thu Sep 28 23:42:35 2006 +0200 (2006-09-28)
changeset 20768 1d478c2d621f
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
permissions -rw-r--r--
replaced syntax/translations by abbreviation;
paulson@13508
     1
(******************************************************************************
paulson@13508
     2
date: november 2001
paulson@13508
     3
author: Frederic Blanqui
paulson@13508
     4
email: blanqui@lri.fr
paulson@13508
     5
webpage: http://www.lri.fr/~blanqui/
paulson@13508
     6
paulson@13508
     7
University of Cambridge, Computer Laboratory
paulson@13508
     8
William Gates Building, JJ Thomson Avenue
paulson@13508
     9
Cambridge CB3 0FD, United Kingdom
paulson@13508
    10
******************************************************************************)
paulson@13508
    11
paulson@13508
    12
header{*Lists of Messages and Lists of Agents*}
paulson@13508
    13
haftmann@16417
    14
theory List_Msg imports Extensions begin
paulson@13508
    15
paulson@13508
    16
subsection{*Implementation of Lists by Messages*}
paulson@13508
    17
paulson@13508
    18
subsubsection{*nil is represented by any message which is not a pair*}
paulson@13508
    19
wenzelm@20768
    20
abbreviation (input)
wenzelm@20768
    21
  cons :: "msg => msg => msg"
wenzelm@20768
    22
  "cons x l == {|x,l|}"
paulson@13508
    23
paulson@13508
    24
subsubsection{*induction principle*}
paulson@13508
    25
paulson@13508
    26
lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]
paulson@13508
    27
==> P l"
wenzelm@20768
    28
by (induct l) auto
paulson@13508
    29
paulson@13508
    30
subsubsection{*head*}
paulson@13508
    31
paulson@13508
    32
consts head :: "msg => msg"
paulson@13508
    33
paulson@13508
    34
recdef head "measure size"
paulson@13508
    35
"head (cons x l) = x"
paulson@13508
    36
paulson@13508
    37
subsubsection{*tail*}
paulson@13508
    38
paulson@13508
    39
consts tail :: "msg => msg"
paulson@13508
    40
paulson@13508
    41
recdef tail "measure size"
paulson@13508
    42
"tail (cons x l) = l"
paulson@13508
    43
paulson@13508
    44
subsubsection{*length*}
paulson@13508
    45
paulson@13508
    46
consts len :: "msg => nat"
paulson@13508
    47
paulson@13508
    48
recdef len "measure size"
paulson@13508
    49
"len (cons x l) = Suc (len l)"
paulson@13508
    50
"len other = 0"
paulson@13508
    51
paulson@13508
    52
lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
wenzelm@20768
    53
by (cases l) auto
paulson@13508
    54
paulson@13508
    55
subsubsection{*membership*}
paulson@13508
    56
paulson@13508
    57
consts isin :: "msg * msg => bool"
paulson@13508
    58
paulson@13508
    59
recdef isin "measure (%(x,l). size l)"
paulson@13508
    60
"isin (x, cons y l) = (x=y | isin (x,l))"
paulson@13508
    61
"isin (x, other) = False"
paulson@13508
    62
paulson@13508
    63
subsubsection{*delete an element*}
paulson@13508
    64
paulson@13508
    65
consts del :: "msg * msg => msg"
paulson@13508
    66
paulson@13508
    67
recdef del "measure (%(x,l). size l)"
paulson@13508
    68
"del (x, cons y l) = (if x=y then l else cons y (del (x,l)))"
paulson@13508
    69
"del (x, other) = other"
paulson@13508
    70
paulson@13508
    71
lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
wenzelm@20768
    72
by (induct l) auto
paulson@13508
    73
paulson@13508
    74
lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
wenzelm@20768
    75
by (induct l) auto
paulson@13508
    76
paulson@13508
    77
subsubsection{*concatenation*}
paulson@13508
    78
paulson@13508
    79
consts app :: "msg * msg => msg"
paulson@13508
    80
paulson@13508
    81
recdef app "measure (%(l,l'). size l)"
paulson@13508
    82
"app (cons x l, l') = cons x (app (l,l'))"
paulson@13508
    83
"app (other, l') = l'"
paulson@13508
    84
paulson@13508
    85
lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
wenzelm@20768
    86
by (induct l) auto
paulson@13508
    87
paulson@13508
    88
subsubsection{*replacement*}
paulson@13508
    89
paulson@13508
    90
consts repl :: "msg * nat * msg => msg"
paulson@13508
    91
paulson@13508
    92
recdef repl "measure (%(l,i,x'). i)"
paulson@13508
    93
"repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))"
paulson@13508
    94
"repl (cons x l, 0, x') = cons x' l"
paulson@13508
    95
"repl (other, i, M') = other"
paulson@13508
    96
paulson@13508
    97
subsubsection{*ith element*}
paulson@13508
    98
paulson@13508
    99
consts ith :: "msg * nat => msg"
paulson@13508
   100
paulson@13508
   101
recdef ith "measure (%(l,i). i)"
paulson@13508
   102
"ith (cons x l, Suc i) = ith (l,i)"
paulson@13508
   103
"ith (cons x l, 0) = x"
paulson@13508
   104
"ith (other, i) = other"
paulson@13508
   105
paulson@13508
   106
lemma ith_head: "0 < len l ==> ith (l,0) = head l"
wenzelm@20768
   107
by (cases l) auto
paulson@13508
   108
paulson@13508
   109
subsubsection{*insertion*}
paulson@13508
   110
paulson@13508
   111
consts ins :: "msg * nat * msg => msg"
paulson@13508
   112
paulson@13508
   113
recdef ins "measure (%(l,i,x). i)"
paulson@13508
   114
"ins (cons x l, Suc i, y) = cons x (ins (l,i,y))"
paulson@13508
   115
"ins (l, 0, y) = cons y l"
paulson@13508
   116
paulson@13508
   117
lemma ins_head [simp]: "ins (l,0,y) = cons y l"
wenzelm@20768
   118
by (cases l) auto
paulson@13508
   119
paulson@13508
   120
subsubsection{*truncation*}
paulson@13508
   121
paulson@13508
   122
consts trunc :: "msg * nat => msg"
paulson@13508
   123
paulson@13508
   124
recdef trunc "measure (%(l,i). i)"
paulson@13508
   125
"trunc (l,0) = l"
paulson@13508
   126
"trunc (cons x l, Suc i) = trunc (l,i)"
paulson@13508
   127
paulson@13508
   128
lemma trunc_zero [simp]: "trunc (l,0) = l"
wenzelm@20768
   129
by (cases l) auto
paulson@13508
   130
paulson@13508
   131
paulson@13508
   132
subsection{*Agent Lists*}
paulson@13508
   133
paulson@13508
   134
subsubsection{*set of well-formed agent-list messages*}
paulson@13508
   135
wenzelm@20768
   136
abbreviation
wenzelm@20768
   137
  nil :: msg
wenzelm@20768
   138
  "nil == Number 0"
paulson@13508
   139
paulson@13508
   140
consts agl :: "msg set"
paulson@13508
   141
paulson@13508
   142
inductive agl
paulson@13508
   143
intros
paulson@13508
   144
Nil[intro]: "nil:agl"
paulson@13508
   145
Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl"
paulson@13508
   146
paulson@13508
   147
subsubsection{*basic facts about agent lists*}
paulson@13508
   148
paulson@13508
   149
lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl"
paulson@13508
   150
by (erule agl.induct, auto)
paulson@13508
   151
paulson@13508
   152
lemma app_in_agl [intro]: "[| I:agl; J:agl |] ==> app (I,J):agl"
paulson@13508
   153
by (erule agl.induct, auto)
paulson@13508
   154
paulson@13508
   155
lemma no_Key_in_agl: "I:agl ==> Key K ~:parts {I}"
paulson@13508
   156
by (erule agl.induct, auto)
paulson@13508
   157
paulson@13508
   158
lemma no_Nonce_in_agl: "I:agl ==> Nonce n ~:parts {I}"
paulson@13508
   159
by (erule agl.induct, auto)
paulson@13508
   160
paulson@13508
   161
lemma no_Key_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   162
Key K ~:parts {app (J, del (Agent B, I))}"
paulson@13508
   163
by (rule no_Key_in_agl, auto)
paulson@13508
   164
paulson@13508
   165
lemma no_Nonce_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   166
Nonce n ~:parts {app (J, del (Agent B, I))}"
paulson@13508
   167
by (rule no_Nonce_in_agl, auto)
paulson@13508
   168
paulson@13508
   169
lemma no_Crypt_in_agl: "I:agl ==> Crypt K X ~:parts {I}"
paulson@13508
   170
by (erule agl.induct, auto)
paulson@13508
   171
paulson@13508
   172
lemma no_Crypt_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   173
Crypt K X ~:parts {app (J, del (Agent B,I))}"
paulson@13508
   174
by (rule no_Crypt_in_agl, auto)
paulson@13508
   175
paulson@13508
   176
end