author | wenzelm |
Tue, 17 Nov 1998 14:07:25 +0100 | |
changeset 5906 | 1f58694fc3e2 |
parent 5648 | fe887910e32e |
child 6012 | 1894bfc4aee9 |
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*) |
|
5648 | 14 |
Goal "[| ALL m. F : Constrains {m} (maxfg m); n: common |] \ |
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; \ |
5648 | 25 |
\ ALL m. F : Constrains {m} (maxfg m); n: common |] \ |
26 |
\ ==> F : Invariant (atMost n)"; |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
27 |
by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
28 |
qed "common_Invariant"; |
4776 | 29 |
|
30 |
||
31 |
(*** Some programs that implement the safety property above ***) |
|
32 |
||
5648 | 33 |
Goal "SKIP : constrains {m} (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*) |
39 |
Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ |
|
40 |
\ : constrains {m} (maxfg m)"; |
|
4776 | 41 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
5648 | 42 |
le_max_iff_disj, fasc]) 1); |
4776 | 43 |
by (Blast_tac 1); |
44 |
result(); |
|
45 |
||
5648 | 46 |
(*This one is t := max (ftime t) (gtime t)*) |
47 |
Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ |
|
48 |
\ : constrains {m} (maxfg m)"; |
|
49 |
by (simp_tac |
|
50 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
|
4776 | 51 |
by (Blast_tac 1); |
52 |
result(); |
|
53 |
||
54 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
|
5648 | 55 |
Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \ |
56 |
\ : constrains {m} (maxfg m)"; |
|
57 |
by (simp_tac |
|
58 |
(simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); |
|
4776 | 59 |
by (blast_tac (claset() addIs [Suc_leI]) 1); |
60 |
result(); |
|
61 |
||
62 |
||
63 |
(*It remans to prove that they satisfy CMT3': t does not decrease, |
|
64 |
and that CMT3' implies that t stops changing once common(t) holds.*) |
|
65 |
||
66 |
||
67 |
(*** Progress under weak fairness ***) |
|
68 |
||
69 |
Addsimps [atMost_Int_atLeast]; |
|
70 |
||
5648 | 71 |
Goal "[| ALL m. F : Constrains {m} (maxfg m); \ |
72 |
\ ALL m: lessThan n. F : LeadsTo {m} (greaterThan m); \ |
|
5584 | 73 |
\ n: common |] \ |
5648 | 74 |
\ ==> F : LeadsTo (atMost n) common"; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
75 |
by (rtac LeadsTo_weaken_R 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
76 |
by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1); |
4776 | 77 |
by (ALLGOALS Asm_simp_tac); |
78 |
by (rtac subset_refl 2); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
79 |
by (blast_tac (claset() addDs [PSP_stable2] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
80 |
addIs [common_stable, LeadsTo_weaken_R]) 1); |
4776 | 81 |
val lemma = result(); |
82 |
||
5490 | 83 |
(*The "ALL m: -common" form echoes CMT6.*) |
5648 | 84 |
Goal "[| ALL m. F : Constrains {m} (maxfg m); \ |
85 |
\ ALL m: -common. F : LeadsTo {m} (greaterThan m); \ |
|
5584 | 86 |
\ n: common |] \ |
5648 | 87 |
\ ==> F : LeadsTo (atMost (LEAST n. n: common)) common"; |
4776 | 88 |
by (rtac lemma 1); |
89 |
by (ALLGOALS Asm_simp_tac); |
|
90 |
by (etac LeastI 2); |
|
91 |
by (blast_tac (claset() addSDs [not_less_Least]) 1); |
|
92 |
qed "leadsTo_common"; |