author | wenzelm |
Fri, 05 Oct 2001 21:52:39 +0200 | |
changeset 11701 | 3d51fbf81c17 |
parent 11195 | 65ede8dfe304 |
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/Common |
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 |
Common Meeting Time example from Misra (1994) |
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 |
The state is identified with the one variable in existence. |
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 |
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
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 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
(*Misra's property CMT4: t exceeds no common meeting time*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
\ ==> F : Stable (atMost n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
by (asm_full_simp_tac |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
(simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
le_max_iff_disj]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
by (etac Constrains_weaken_R 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
qed "common_stable"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
Goal "[| Init F <= atMost n; \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
\ ALL m. F : {m} Co (maxfg m); n: common |] \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
\ ==> F : Always (atMost n)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
qed "common_safety"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
(*** Some programs that implement the safety property above ***) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
Goal "SKIP : {m} co (maxfg m)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
fasc]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
(*This one is t := ftime t || t := gtime t*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
\ : {m} co (maxfg m)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
42 |
le_max_iff_disj, fasc]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
44 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
(*This one is t := max (ftime t) (gtime t)*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
46 |
Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
\ : {m} co (maxfg m)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
by (simp_tac |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
49 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
51 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
52 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
53 |
Goal "mk_program \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
54 |
\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
55 |
\ : {m} co (maxfg m)"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
56 |
by (simp_tac |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
57 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
58 |
result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
59 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
60 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
61 |
(*It remans to prove that they satisfy CMT3': t does not decrease, |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
and that CMT3' implies that t stops changing once common(t) holds.*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
63 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
64 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
65 |
(*** Progress under weak fairness ***) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
66 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
67 |
Addsimps [atMost_Int_atLeast]; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
68 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
69 |
Goal "[| ALL m. F : {m} Co (maxfg m); \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
71 |
\ n: common |] \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
72 |
\ ==> F : (atMost n) LeadsTo common"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
73 |
by (rtac LeadsTo_weaken_R 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
74 |
by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
75 |
by (ALLGOALS Asm_simp_tac); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
76 |
by (rtac subset_refl 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
77 |
by (blast_tac (claset() addDs [PSP_Stable2] |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
78 |
addIs [common_stable, LeadsTo_weaken_R]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
79 |
val lemma = result(); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
80 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
81 |
(*The "ALL m: -common" form echoes CMT6.*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
82 |
Goal "[| ALL m. F : {m} Co (maxfg m); \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
83 |
\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
84 |
\ n: common |] \ |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
85 |
\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common"; |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
86 |
by (rtac lemma 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
87 |
by (ALLGOALS Asm_simp_tac); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
88 |
by (etac LeastI 2); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
89 |
by (blast_tac (claset() addSDs [not_less_Least]) 1); |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
90 |
qed "leadsTo_common"; |