author | paulson |
Tue, 29 Sep 1998 15:58:47 +0200 | |
changeset 5584 | aad639e56d4e |
parent 5490 | 85855f65d0c6 |
child 5608 | a82a038a3e7a |
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*) |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
14 |
Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
15 |
\ ==> Stable prg (atMost n)"; |
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 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
24 |
Goal "[| Init prg <= atMost n; \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
25 |
\ ALL m. Constrains prg {m} (maxfg m); n: common |] \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
26 |
\ ==> Invariant prg (atMost n)"; |
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 |
||
33 |
(*This one is just Skip*) |
|
5069 | 34 |
Goal "constrains {id} {m} (maxfg m)"; |
4776 | 35 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, |
36 |
fasc, gasc]) 1); |
|
37 |
result(); |
|
38 |
||
39 |
(*This one is t := ftime t || t := gtime t really needs Skip too*) |
|
5069 | 40 |
Goal "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \ |
4776 | 41 |
\ {m} (maxfg m)"; |
42 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, |
|
43 |
le_max_iff_disj]) 1); |
|
44 |
by (Blast_tac 1); |
|
45 |
result(); |
|
46 |
||
47 |
(*This one is t := max (ftime t) (gtime t) really needs Skip too*) |
|
5069 | 48 |
Goal "constrains {range(%t.(t, max (ftime t) (gtime t)))} \ |
4776 | 49 |
\ {m} (maxfg m)"; |
50 |
by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1); |
|
51 |
by (Blast_tac 1); |
|
52 |
result(); |
|
53 |
||
54 |
(*This one is t := t+1 if t <max (ftime t) (gtime t) *) |
|
5069 | 55 |
Goalw [constrains_def, maxfg_def] |
4776 | 56 |
"constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \ |
57 |
\ {m} (maxfg m)"; |
|
58 |
by (blast_tac (claset() addIs [Suc_leI]) 1); |
|
59 |
result(); |
|
60 |
||
61 |
||
62 |
(*It remans to prove that they satisfy CMT3': t does not decrease, |
|
63 |
and that CMT3' implies that t stops changing once common(t) holds.*) |
|
64 |
||
65 |
||
66 |
(*** Progress under weak fairness ***) |
|
67 |
||
68 |
Addsimps [atMost_Int_atLeast]; |
|
69 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
70 |
Goal "[| ALL m. Constrains prg {m} (maxfg m); \ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
71 |
\ ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \ |
5584 | 72 |
\ n: common |] \ |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
73 |
\ ==> LeadsTo prg (atMost n) common"; |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
74 |
by (rtac LeadsTo_weaken_R 1); |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
75 |
by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1); |
4776 | 76 |
by (ALLGOALS Asm_simp_tac); |
77 |
by (rtac subset_refl 2); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
78 |
by (blast_tac (claset() addDs [PSP_stable2] |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
79 |
addIs [common_stable, LeadsTo_weaken_R]) 1); |
4776 | 80 |
val lemma = result(); |
81 |
||
5490 | 82 |
(*The "ALL m: -common" form echoes CMT6.*) |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
83 |
Goal "[| ALL m. Constrains prg {m} (maxfg m); \ |
5490 | 84 |
\ ALL m: -common. LeadsTo prg {m} (greaterThan m); \ |
5584 | 85 |
\ n: common |] \ |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
86 |
\ ==> LeadsTo prg (atMost (LEAST n. n: common)) common"; |
4776 | 87 |
by (rtac lemma 1); |
88 |
by (ALLGOALS Asm_simp_tac); |
|
89 |
by (etac LeastI 2); |
|
90 |
by (blast_tac (claset() addSDs [not_less_Least]) 1); |
|
91 |
qed "leadsTo_common"; |