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