author | wenzelm |
Fri, 18 Nov 2011 22:32:57 +0100 | |
changeset 45582 | 78f59aaa30ff |
parent 44871 | fbfdc5ac86be |
child 58249 | 180f1b3508ed |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Network.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
5 |
The Communication Network. |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
7 |
From Misra, "A Logic for Concurrent Programming" (1994), section 5.7. |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
44871 | 10 |
theory Network imports "../UNITY" begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
(*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
|
13 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
datatype pvar = Sent | Rcvd | Idle |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
datatype pname = Aproc | Bproc |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
|
42463 | 18 |
type_synonym state = "pname * pvar => nat" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
20 |
locale F_props = |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
21 |
fixes F |
13806 | 22 |
assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}" |
23 |
and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}" |
|
24 |
and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}" |
|
25 |
and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}" |
|
26 |
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
|
27 |
co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}" |
13806 | 28 |
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
|
29 |
co {s. s(proc,Sent) = n}" |
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
30 |
begin |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
31 |
|
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
32 |
lemmas sent_nondec_A = sent_nondec [of _ Aproc] |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
33 |
and sent_nondec_B = sent_nondec [of _ Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
34 |
and rcvd_nondec_A = rcvd_nondec [of _ Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
35 |
and rcvd_nondec_B = rcvd_nondec [of _ Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
36 |
and rcvd_idle_A = rcvd_idle [of Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
37 |
and rcvd_idle_B = rcvd_idle [of Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
38 |
and sent_idle_A = sent_idle [of Aproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
39 |
and sent_idle_B = sent_idle [of Bproc] |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
40 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
41 |
and rs_AB = stable_Int [OF rsA rsB] |
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
42 |
|
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
43 |
lemmas sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B] |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B] |
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
47 |
|
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
48 |
lemmas nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB] |
13785
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 |
|
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
51 |
lemmas nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] idle_AB] |
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
52 |
|
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
53 |
lemma |
13806 | 54 |
shows "F \<in> stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
55 |
s(Aproc,Sent) = s(Bproc,Rcvd) & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
56 |
s(Bproc,Sent) = s(Aproc,Rcvd) & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
57 |
s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}" |
13785
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 |
45582
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
71 |
|
78f59aaa30ff
sequential lemmas to accomodate static rule attributes;
wenzelm
parents:
44871
diff
changeset
|
72 |
end |