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