author | paulson |
Thu, 29 Apr 1999 10:51:58 +0200 | |
changeset 6536 | 281d44905cab |
parent 6295 | 351b3c2b0d83 |
child 6570 | a7d7985050a9 |
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 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
10 |
claset_ref() := claset(); |
5636 | 11 |
|
5648 | 12 |
Addsimps [Cli_prg_def RS def_prg_Init]; |
13 |
program_defs_ref := [Cli_prg_def]; |
|
5636 | 14 |
|
15 |
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); |
|
16 |
||
17 |
(*Simplification for records*) |
|
18 |
Addsimps (thms"state.update_defs"); |
|
19 |
||
20 |
||
21 |
fun invariant_tac i = |
|
22 |
rtac invariantI i THEN |
|
5648 | 23 |
constrains_tac (i+1); |
5636 | 24 |
|
25 |
(*Safety property 1(a): ask is nondecreasing*) |
|
26 |
Goalw [increasing_def] "Cli_prg: increasing ask"; |
|
5648 | 27 |
by (Clarify_tac 1); |
5636 | 28 |
by (constrains_tac 1); |
29 |
by Auto_tac; |
|
30 |
qed "increasing_ask"; |
|
31 |
||
32 |
(*Safety property 1(b): rel is nondecreasing*) |
|
33 |
Goalw [increasing_def] "Cli_prg: increasing rel"; |
|
5648 | 34 |
by (Clarify_tac 1); |
5636 | 35 |
by (constrains_tac 1); |
36 |
by Auto_tac; |
|
37 |
qed "increasing_rel"; |
|
38 |
||
39 |
Addsimps [nth_append, append_one_prefix]; |
|
40 |
||
41 |
Goal "Cli_prg: invariant {s. tok s <= Max}"; |
|
42 |
by (invariant_tac 1); |
|
43 |
by Auto_tac; |
|
44 |
qed "tok_bounded"; |
|
45 |
||
46 |
(*Safety property 3: no client requests "too many" tokens. |
|
47 |
With no Substitution Axiom, we must prove the two invariants |
|
48 |
simultaneously. Could combine tok_bounded, stable_constrains_stable |
|
49 |
and a rule invariant_implies_stable... |
|
50 |
*) |
|
51 |
Goal "Cli_prg: \ |
|
52 |
\ invariant ({s. tok s <= Max} Int \ |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
53 |
\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})"; |
5636 | 54 |
by (invariant_tac 1); |
55 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
56 |
qed "ask_bounded"; |
|
57 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
58 |
(** Several facts used to prove Lemma 1 **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
59 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
60 |
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
|
61 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
62 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
63 |
qed "stable_rel_le_giv"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
64 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
65 |
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
|
66 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
67 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
68 |
qed "stable_size_rel_le_giv"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
69 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
70 |
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
|
71 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
72 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
73 |
qed "stable_size_ask_le_rel"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
74 |
|
5636 | 75 |
|
5667 | 76 |
(*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
|
77 |
expanding it is extremely expensive!*) |
5648 | 78 |
program_defs_ref := []; |
79 |
||
5636 | 80 |
(*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
|
81 |
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
82 |
\ guarantees Invariant {s. rel s <= giv s}"; |
5636 | 83 |
by (rtac guaranteesI 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
84 |
by (rtac InvariantI 1); |
5648 | 85 |
by (Force_tac 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
86 |
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
|
87 |
stable_rel_le_giv]) 1); |
5636 | 88 |
qed "ok_guar_rel_prefix_giv"; |
89 |
||
90 |
||
91 |
(*** Towards proving the liveness property ***) |
|
92 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
93 |
Goal "Cli_prg Join G \ |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
94 |
\ : transient {s. size (giv s) = Suc k & \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
95 |
\ size (rel s) = k & ask s ! k <= giv s ! k}"; |
5636 | 96 |
by (res_inst_tac [("act", "rel_act")] transient_mem 1); |
97 |
by (auto_tac (claset(), |
|
5648 | 98 |
simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def])); |
5636 | 99 |
qed "transient_lemma"; |
100 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
101 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
102 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
103 |
val rewrite_o = rewrite_rule [o_def]; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
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)) \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
107 |
\ guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \ |
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); |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
111 |
by (dtac (impOfSubs (rewrite_o Increasing_size)) 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
112 |
by (rtac InvariantI 1); |
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) \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
126 |
\ Int Invariant giv_meets_ask) \ |
6536 | 127 |
\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; |
5636 | 128 |
by (rtac guaranteesI 1); |
129 |
by (Clarify_tac 1); |
|
130 |
by (rtac Stable_transient_reachable_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); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
132 |
by (force_tac (claset() addDs [impOfSubs Increasing_size, |
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); |
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5706
diff
changeset
|
136 |
by (Blast_tac 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
137 |
by (auto_tac (claset(), |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
138 |
simpset() addsimps [Invariant_eq_always, 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"; |