src/HOL/Auth/Guard/List_Msg.thy
author krauss
Mon Mar 01 16:42:45 2010 +0100 (2010-03-01)
changeset 35418 83b0f75810f0
parent 23746 a455e69c31cc
child 41775 6214816d79d3
permissions -rw-r--r--
killed recdefs in HOL-Auth
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@21404
    21
  cons :: "msg => msg => msg" where
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
krauss@35418
    32
primrec head :: "msg => msg" where
paulson@13508
    33
"head (cons x l) = x"
paulson@13508
    34
paulson@13508
    35
subsubsection{*tail*}
paulson@13508
    36
krauss@35418
    37
primrec tail :: "msg => msg" where
paulson@13508
    38
"tail (cons x l) = l"
paulson@13508
    39
paulson@13508
    40
subsubsection{*length*}
paulson@13508
    41
krauss@35418
    42
fun len :: "msg => nat" where
krauss@35418
    43
"len (cons x l) = Suc (len l)" |
paulson@13508
    44
"len other = 0"
paulson@13508
    45
paulson@13508
    46
lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
wenzelm@20768
    47
by (cases l) auto
paulson@13508
    48
paulson@13508
    49
subsubsection{*membership*}
paulson@13508
    50
krauss@35418
    51
fun isin :: "msg * msg => bool" where
krauss@35418
    52
"isin (x, cons y l) = (x=y | isin (x,l))" |
paulson@13508
    53
"isin (x, other) = False"
paulson@13508
    54
paulson@13508
    55
subsubsection{*delete an element*}
paulson@13508
    56
krauss@35418
    57
fun del :: "msg * msg => msg" where
krauss@35418
    58
"del (x, cons y l) = (if x=y then l else cons y (del (x,l)))" |
paulson@13508
    59
"del (x, other) = other"
paulson@13508
    60
paulson@13508
    61
lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
wenzelm@20768
    62
by (induct l) auto
paulson@13508
    63
paulson@13508
    64
lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
wenzelm@20768
    65
by (induct l) auto
paulson@13508
    66
paulson@13508
    67
subsubsection{*concatenation*}
paulson@13508
    68
krauss@35418
    69
fun app :: "msg * msg => msg" where
krauss@35418
    70
"app (cons x l, l') = cons x (app (l,l'))" |
paulson@13508
    71
"app (other, l') = l'"
paulson@13508
    72
paulson@13508
    73
lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
wenzelm@20768
    74
by (induct l) auto
paulson@13508
    75
paulson@13508
    76
subsubsection{*replacement*}
paulson@13508
    77
krauss@35418
    78
fun repl :: "msg * nat * msg => msg" where
krauss@35418
    79
"repl (cons x l, Suc i, x') = cons x (repl (l,i,x'))" |
krauss@35418
    80
"repl (cons x l, 0, x') = cons x' l" |
paulson@13508
    81
"repl (other, i, M') = other"
paulson@13508
    82
paulson@13508
    83
subsubsection{*ith element*}
paulson@13508
    84
krauss@35418
    85
fun ith :: "msg * nat => msg" where
krauss@35418
    86
"ith (cons x l, Suc i) = ith (l,i)" |
krauss@35418
    87
"ith (cons x l, 0) = x" |
paulson@13508
    88
"ith (other, i) = other"
paulson@13508
    89
paulson@13508
    90
lemma ith_head: "0 < len l ==> ith (l,0) = head l"
wenzelm@20768
    91
by (cases l) auto
paulson@13508
    92
paulson@13508
    93
subsubsection{*insertion*}
paulson@13508
    94
krauss@35418
    95
fun ins :: "msg * nat * msg => msg" where
krauss@35418
    96
"ins (cons x l, Suc i, y) = cons x (ins (l,i,y))" |
paulson@13508
    97
"ins (l, 0, y) = cons y l"
paulson@13508
    98
paulson@13508
    99
lemma ins_head [simp]: "ins (l,0,y) = cons y l"
wenzelm@20768
   100
by (cases l) auto
paulson@13508
   101
paulson@13508
   102
subsubsection{*truncation*}
paulson@13508
   103
krauss@35418
   104
fun trunc :: "msg * nat => msg" where
krauss@35418
   105
"trunc (l,0) = l" |
paulson@13508
   106
"trunc (cons x l, Suc i) = trunc (l,i)"
paulson@13508
   107
paulson@13508
   108
lemma trunc_zero [simp]: "trunc (l,0) = l"
wenzelm@20768
   109
by (cases l) auto
paulson@13508
   110
paulson@13508
   111
paulson@13508
   112
subsection{*Agent Lists*}
paulson@13508
   113
paulson@13508
   114
subsubsection{*set of well-formed agent-list messages*}
paulson@13508
   115
wenzelm@20768
   116
abbreviation
wenzelm@21404
   117
  nil :: msg where
wenzelm@20768
   118
  "nil == Number 0"
paulson@13508
   119
berghofe@23746
   120
inductive_set agl :: "msg set"
berghofe@23746
   121
where
berghofe@23746
   122
  Nil[intro]: "nil:agl"
berghofe@23746
   123
| Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl"
paulson@13508
   124
paulson@13508
   125
subsubsection{*basic facts about agent lists*}
paulson@13508
   126
paulson@13508
   127
lemma del_in_agl [intro]: "I:agl ==> del (a,I):agl"
paulson@13508
   128
by (erule agl.induct, auto)
paulson@13508
   129
paulson@13508
   130
lemma app_in_agl [intro]: "[| I:agl; J:agl |] ==> app (I,J):agl"
paulson@13508
   131
by (erule agl.induct, auto)
paulson@13508
   132
paulson@13508
   133
lemma no_Key_in_agl: "I:agl ==> Key K ~:parts {I}"
paulson@13508
   134
by (erule agl.induct, auto)
paulson@13508
   135
paulson@13508
   136
lemma no_Nonce_in_agl: "I:agl ==> Nonce n ~:parts {I}"
paulson@13508
   137
by (erule agl.induct, auto)
paulson@13508
   138
paulson@13508
   139
lemma no_Key_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   140
Key K ~:parts {app (J, del (Agent B, I))}"
paulson@13508
   141
by (rule no_Key_in_agl, auto)
paulson@13508
   142
paulson@13508
   143
lemma no_Nonce_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   144
Nonce n ~:parts {app (J, del (Agent B, I))}"
paulson@13508
   145
by (rule no_Nonce_in_agl, auto)
paulson@13508
   146
paulson@13508
   147
lemma no_Crypt_in_agl: "I:agl ==> Crypt K X ~:parts {I}"
paulson@13508
   148
by (erule agl.induct, auto)
paulson@13508
   149
paulson@13508
   150
lemma no_Crypt_in_appdel: "[| I:agl; J:agl |] ==>
paulson@13508
   151
Crypt K X ~:parts {app (J, del (Agent B,I))}"
paulson@13508
   152
by (rule no_Crypt_in_agl, auto)
paulson@13508
   153
paulson@13508
   154
end