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