author | huffman |
Sat, 08 Jan 2011 09:30:52 -0800 | |
changeset 41476 | 0fa9629aa399 |
parent 40774 | 0437dbc127b3 |
child 42151 | 4da4fc77664b |
permissions | -rw-r--r-- |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/IOA/NTP/Packet.thy |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow & Konrad Slind |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
17244 | 5 |
theory Packet |
6 |
imports Multiset |
|
7 |
begin |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
|
41476 | 9 |
type_synonym |
17244 | 10 |
'msg packet = "bool * 'msg" |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19739
diff
changeset
|
12 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19739
diff
changeset
|
13 |
hdr :: "'msg packet => bool" where |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
"hdr == fst" |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19739
diff
changeset
|
16 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19739
diff
changeset
|
17 |
msg :: "'msg packet => 'msg" where |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
"msg == snd" |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
|
19739 | 20 |
|
21 |
text {* Instantiation of a tautology? *} |
|
22 |
lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)" |
|
23 |
by simp |
|
24 |
||
25 |
declare hdr_def [simp] msg_def [simp] |
|
17244 | 26 |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
end |