4776
|
1 |
(* Title: HOL/UNITY/Common
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Common Meeting Time example from Misra (1994)
|
|
7 |
|
|
8 |
The state is identified with the one variable in existence.
|
|
9 |
|
|
10 |
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
|
|
11 |
*)
|
|
12 |
|
|
13 |
|
|
14 |
open Common;
|
|
15 |
|
|
16 |
(*Misra's property CMT4: t exceeds no common meeting time*)
|
5069
|
17 |
Goal
|
4776
|
18 |
"!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
|
|
19 |
\ ==> stable Acts (atMost n)";
|
|
20 |
by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
|
|
21 |
by (asm_full_simp_tac
|
|
22 |
(simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
|
|
23 |
constrains_def, le_max_iff_disj]) 1);
|
|
24 |
by (Clarify_tac 1);
|
|
25 |
by (dtac bspec 1);
|
|
26 |
by (assume_tac 1);
|
|
27 |
by (blast_tac (claset() addSEs [subsetCE]
|
|
28 |
addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
|
|
29 |
qed "common_stable";
|
|
30 |
|
5069
|
31 |
Goal
|
4776
|
32 |
"!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
|
|
33 |
\ ==> reachable {0} Acts <= atMost n";
|
|
34 |
by (rtac strongest_invariant 1);
|
|
35 |
by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
|
|
36 |
by (simp_tac (simpset() addsimps [atMost_def]) 1);
|
|
37 |
qed "common_invariant";
|
|
38 |
|
|
39 |
|
|
40 |
(*** Some programs that implement the safety property above ***)
|
|
41 |
|
|
42 |
(*This one is just Skip*)
|
5069
|
43 |
Goal "constrains {id} {m} (maxfg m)";
|
4776
|
44 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
|
|
45 |
fasc, gasc]) 1);
|
|
46 |
result();
|
|
47 |
|
|
48 |
(*This one is t := ftime t || t := gtime t really needs Skip too*)
|
5069
|
49 |
Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
|
4776
|
50 |
\ {m} (maxfg m)";
|
|
51 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
|
|
52 |
le_max_iff_disj]) 1);
|
|
53 |
by (Blast_tac 1);
|
|
54 |
result();
|
|
55 |
|
|
56 |
(*This one is t := max (ftime t) (gtime t) really needs Skip too*)
|
5069
|
57 |
Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
|
4776
|
58 |
\ {m} (maxfg m)";
|
|
59 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
|
|
60 |
by (Blast_tac 1);
|
|
61 |
result();
|
|
62 |
|
|
63 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
|
5069
|
64 |
Goalw [constrains_def, maxfg_def]
|
4776
|
65 |
"constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
|
|
66 |
\ {m} (maxfg m)";
|
|
67 |
by (blast_tac (claset() addIs [Suc_leI]) 1);
|
|
68 |
result();
|
|
69 |
|
|
70 |
|
|
71 |
(*It remans to prove that they satisfy CMT3': t does not decrease,
|
|
72 |
and that CMT3' implies that t stops changing once common(t) holds.*)
|
|
73 |
|
|
74 |
|
|
75 |
(*** Progress under weak fairness ***)
|
|
76 |
|
|
77 |
Addsimps [atMost_Int_atLeast];
|
|
78 |
|
5069
|
79 |
Goal
|
4776
|
80 |
"!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
|
|
81 |
\ ALL m: lessThan n. leadsTo Acts {m} (greaterThan m); \
|
|
82 |
\ n: common; id: Acts |] \
|
|
83 |
\ ==> leadsTo Acts (atMost n) common";
|
|
84 |
by (rtac leadsTo_weaken_R 1);
|
|
85 |
by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
|
|
86 |
by (ALLGOALS Asm_simp_tac);
|
|
87 |
by (rtac subset_refl 2);
|
|
88 |
by (blast_tac (claset() addDs [PSP_stable2]
|
|
89 |
addIs [common_stable, leadsTo_weaken_R]) 1);
|
|
90 |
val lemma = result();
|
|
91 |
|
|
92 |
(*The "ALL m: Compl common" form echoes CMT6.*)
|
5069
|
93 |
Goal
|
4776
|
94 |
"!!Acts. [| ALL m. constrains Acts {m} (maxfg m); \
|
|
95 |
\ ALL m: Compl common. leadsTo Acts {m} (greaterThan m); \
|
|
96 |
\ n: common; id: Acts |] \
|
|
97 |
\ ==> leadsTo Acts (atMost (LEAST n. n: common)) common";
|
|
98 |
by (rtac lemma 1);
|
|
99 |
by (ALLGOALS Asm_simp_tac);
|
|
100 |
by (etac LeastI 2);
|
|
101 |
by (blast_tac (claset() addSDs [not_less_Least]) 1);
|
|
102 |
qed "leadsTo_common";
|