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