author | paulson |
Sat, 23 Sep 2000 16:02:01 +0200 | |
changeset 10064 | 1a77667b21ef |
parent 7826 | c6a8b73b6c2a |
permissions | -rw-r--r-- |
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 |
(*Misra's property CMT4: t exceeds no common meeting time*) |
|
6536 | 14 |
Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \ |
5648 | 15 |
\ ==> F : Stable (atMost n)"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
16 |
by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1); |
4776 | 17 |
by (asm_full_simp_tac |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
18 |
(simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def, |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
19 |
le_max_iff_disj]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
20 |
by (etac Constrains_weaken_R 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
21 |
by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1); |
4776 | 22 |
qed "common_stable"; |
23 |
||
5620 | 24 |
Goal "[| Init F <= atMost n; \ |
6536 | 25 |
\ ALL m. F : {m} Co (maxfg m); n: common |] \ |
6570 | 26 |
\ ==> F : Always (atMost n)"; |
27 |
by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1); |
|
28 |
qed "common_safety"; |
|
4776 | 29 |
|
30 |
||
31 |
(*** Some programs that implement the safety property above ***) |
|
32 |
||
6536 | 33 |
Goal "SKIP : {m} co (maxfg m)"; |
4776 | 34 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, |
5648 | 35 |
fasc]) 1); |
4776 | 36 |
result(); |
37 |
||
5648 | 38 |
(*This one is t := ftime t || t := gtime t*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
7826
diff
changeset
|
39 |
Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \ |
6536 | 40 |
\ : {m} co (maxfg m)"; |
4776 | 41 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
5648 | 42 |
le_max_iff_disj, fasc]) 1); |
4776 | 43 |
result(); |
44 |
||
5648 | 45 |
(*This one is t := max (ftime t) (gtime t)*) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
7826
diff
changeset
|
46 |
Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \ |
6536 | 47 |
\ : {m} co (maxfg m)"; |
5648 | 48 |
by (simp_tac |
49 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
|
4776 | 50 |
result(); |
51 |
||
52 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
7826
diff
changeset
|
53 |
Goal "mk_program \ |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
7826
diff
changeset
|
54 |
\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \ |
6536 | 55 |
\ : {m} co (maxfg m)"; |
5648 | 56 |
by (simp_tac |
57 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
|
4776 | 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 |
||
6536 | 69 |
Goal "[| ALL m. F : {m} Co (maxfg m); \ |
70 |
\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \ |
|
5584 | 71 |
\ n: common |] \ |
6536 | 72 |
\ ==> F : (atMost n) LeadsTo common"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
73 |
by (rtac LeadsTo_weaken_R 1); |
7520 | 74 |
by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1); |
4776 | 75 |
by (ALLGOALS Asm_simp_tac); |
76 |
by (rtac subset_refl 2); |
|
6702 | 77 |
by (blast_tac (claset() addDs [PSP_Stable2] |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
78 |
addIs [common_stable, LeadsTo_weaken_R]) 1); |
4776 | 79 |
val lemma = result(); |
80 |
||
5490 | 81 |
(*The "ALL m: -common" form echoes CMT6.*) |
6536 | 82 |
Goal "[| ALL m. F : {m} Co (maxfg m); \ |
83 |
\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \ |
|
5584 | 84 |
\ n: common |] \ |
6536 | 85 |
\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common"; |
4776 | 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"; |