author | paulson |
Sun, 13 Jun 1999 13:52:26 +0200 | |
changeset 6821 | 350f27e2d649 |
parent 6701 | e84a0b941beb |
child 7179 | 6ffe5067d5cc |
permissions | -rw-r--r-- |
5636 | 1 |
(* Title: HOL/UNITY/Client |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Distributed Resource Management System: the Client |
|
7 |
*) |
|
8 |
||
9 |
||
5648 | 10 |
Addsimps [Cli_prg_def RS def_prg_Init]; |
11 |
program_defs_ref := [Cli_prg_def]; |
|
5636 | 12 |
|
13 |
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); |
|
14 |
||
15 |
(*Simplification for records*) |
|
16 |
Addsimps (thms"state.update_defs"); |
|
17 |
||
18 |
||
19 |
fun invariant_tac i = |
|
20 |
rtac invariantI i THEN |
|
5648 | 21 |
constrains_tac (i+1); |
5636 | 22 |
|
23 |
(*Safety property 1(a): ask is nondecreasing*) |
|
24 |
Goalw [increasing_def] "Cli_prg: increasing ask"; |
|
5648 | 25 |
by (Clarify_tac 1); |
5636 | 26 |
by (constrains_tac 1); |
27 |
by Auto_tac; |
|
28 |
qed "increasing_ask"; |
|
29 |
||
30 |
(*Safety property 1(b): rel is nondecreasing*) |
|
31 |
Goalw [increasing_def] "Cli_prg: increasing rel"; |
|
5648 | 32 |
by (Clarify_tac 1); |
5636 | 33 |
by (constrains_tac 1); |
34 |
by Auto_tac; |
|
35 |
qed "increasing_rel"; |
|
36 |
||
37 |
Addsimps [nth_append, append_one_prefix]; |
|
38 |
||
39 |
Goal "Cli_prg: invariant {s. tok s <= Max}"; |
|
40 |
by (invariant_tac 1); |
|
41 |
by Auto_tac; |
|
42 |
qed "tok_bounded"; |
|
43 |
||
44 |
(*Safety property 3: no client requests "too many" tokens. |
|
45 |
With no Substitution Axiom, we must prove the two invariants |
|
46 |
simultaneously. Could combine tok_bounded, stable_constrains_stable |
|
47 |
and a rule invariant_implies_stable... |
|
48 |
*) |
|
49 |
Goal "Cli_prg: \ |
|
50 |
\ invariant ({s. tok s <= Max} Int \ |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
51 |
\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})"; |
5636 | 52 |
by (invariant_tac 1); |
53 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
54 |
qed "ask_bounded"; |
|
55 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
56 |
(** Several facts used to prove Lemma 1 **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
57 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
58 |
Goal "Cli_prg: stable {s. rel s <= giv s}"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
59 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
60 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
61 |
qed "stable_rel_le_giv"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
62 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
63 |
Goal "Cli_prg: stable {s. size (rel s) <= size (giv s)}"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
64 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
65 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
66 |
qed "stable_size_rel_le_giv"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
67 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
68 |
Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
69 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
70 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
71 |
qed "stable_size_ask_le_rel"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
72 |
|
5636 | 73 |
|
5667 | 74 |
(*We no longer need constrains_tac to expand the program definition, and |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
75 |
expanding it is extremely expensive!*) |
5648 | 76 |
program_defs_ref := []; |
77 |
||
5636 | 78 |
(*Safety property 2: clients return the right number of tokens*) |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
79 |
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \ |
6821 | 80 |
\ guar Always {s. rel s <= giv s}"; |
5636 | 81 |
by (rtac guaranteesI 1); |
6570 | 82 |
by (rtac AlwaysI 1); |
5648 | 83 |
by (Force_tac 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
84 |
by (blast_tac (claset() addIs [Increasing_localTo_Stable, |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
85 |
stable_rel_le_giv]) 1); |
5636 | 86 |
qed "ok_guar_rel_prefix_giv"; |
87 |
||
88 |
||
89 |
(*** Towards proving the liveness property ***) |
|
90 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
91 |
Goal "Cli_prg Join G \ |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
92 |
\ : transient {s. size (giv s) = Suc k & \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
93 |
\ size (rel s) = k & ask s ! k <= giv s ! k}"; |
5636 | 94 |
by (res_inst_tac [("act", "rel_act")] transient_mem 1); |
95 |
by (auto_tac (claset(), |
|
5648 | 96 |
simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def])); |
5636 | 97 |
qed "transient_lemma"; |
98 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
99 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
100 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
101 |
val rewrite_o = rewrite_rule [o_def]; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
102 |
|
6701 | 103 |
val Increasing_length = mono_length RS mono_Increasing_o; |
104 |
||
5636 | 105 |
Goal "Cli_prg : \ |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
106 |
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \ |
6821 | 107 |
\ guar Always ({s. size (ask s) <= Suc (size (rel s))} Int \ |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
108 |
\ {s. size (rel s) <= size (giv s)})"; |
5636 | 109 |
by (rtac guaranteesI 1); |
110 |
by (Clarify_tac 1); |
|
6701 | 111 |
by (dtac (impOfSubs (rewrite_o Increasing_length)) 1); |
6570 | 112 |
by (rtac AlwaysI 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
113 |
by (Force_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
114 |
by (rtac Stable_Int 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
115 |
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)] |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
116 |
addIs [Increasing_localTo_Stable, |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
117 |
stable_size_rel_le_giv]) 2); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
118 |
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)] |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
119 |
addIs [stable_localTo_stable2 RS stable_imp_Stable, |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
120 |
stable_size_ask_le_rel]) 1); |
5636 | 121 |
val lemma1 = result(); |
122 |
||
123 |
||
124 |
Goal "Cli_prg : \ |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
125 |
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ |
6570 | 126 |
\ Int Always giv_meets_ask) \ |
6821 | 127 |
\ guar ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; |
5636 | 128 |
by (rtac guaranteesI 1); |
129 |
by (Clarify_tac 1); |
|
6570 | 130 |
by (rtac Stable_transient_Always_LeadsTo 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
131 |
by (res_inst_tac [("k", "k")] transient_lemma 2); |
6701 | 132 |
by (force_tac (claset() addDs [impOfSubs Increasing_length, |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
133 |
impOfSubs Increasing_Stable_less], |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
134 |
simpset()) 1); |
5636 | 135 |
by (rtac (make_elim (lemma1 RS guaranteesD)) 1); |
6570 | 136 |
by (Blast_tac 1); |
137 |
by (auto_tac (claset(), |
|
138 |
simpset() addsimps [Always_eq_includes_reachable, giv_meets_ask_def])); |
|
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset
|
139 |
by (ALLGOALS Force_tac); |
5636 | 140 |
qed "client_correct"; |