author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 13806 | fd40c9d9076b |
child 32960 | 69916a850301 |
permissions | -rw-r--r-- |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Network |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
The Communication Network |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
16417 | 11 |
theory Network imports UNITY begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
(*The state assigns a number to each process variable*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
datatype pvar = Sent | Rcvd | Idle |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
datatype pname = Aproc | Bproc |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
types state = "pname * pvar => nat" |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
21 |
locale F_props = |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
22 |
fixes F |
13806 | 23 |
assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}" |
24 |
and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}" |
|
25 |
and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}" |
|
26 |
and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}" |
|
27 |
and rcvd_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m} |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
28 |
co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}" |
13806 | 29 |
and sent_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n} |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
30 |
co {s. s(proc,Sent) = n}" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
31 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
32 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
33 |
lemmas (in F_props) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
34 |
sent_nondec_A = sent_nondec [of _ Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
35 |
and sent_nondec_B = sent_nondec [of _ Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
36 |
and rcvd_nondec_A = rcvd_nondec [of _ Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
37 |
and rcvd_nondec_B = rcvd_nondec [of _ Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
38 |
and rcvd_idle_A = rcvd_idle [of Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
39 |
and rcvd_idle_B = rcvd_idle [of Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
40 |
and sent_idle_A = sent_idle [of Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
41 |
and sent_idle_B = sent_idle [of Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
42 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
43 |
and rs_AB = stable_Int [OF rsA rsB] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
44 |
and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
45 |
and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
46 |
and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
47 |
and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
48 |
and nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
49 |
and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
50 |
and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
51 |
idle_AB] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
52 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
53 |
lemma (in F_props) |
13806 | 54 |
shows "F \<in> stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
55 |
s(Aproc,Sent) = s(Bproc,Rcvd) & |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
56 |
s(Bproc,Sent) = s(Aproc,Rcvd) & |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
57 |
s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
58 |
apply (unfold stable_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
59 |
apply (rule constrainsI) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
60 |
apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
61 |
THEN constrainsD], assumption) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
62 |
apply simp_all |
13806 | 63 |
apply (blast del: le0, clarify) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
64 |
apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
65 |
apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
66 |
apply simp |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
67 |
apply (blast intro: order_antisym le_trans eq_imp_le)+ |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
68 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
69 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
end |