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