author | paulson |
Tue, 30 Nov 1999 16:54:10 +0100 | |
changeset 8041 | e3237d8c18d6 |
parent 7964 | 6b3e345c47b3 |
child 8055 | bb15396278fb |
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 |
||
16 |
fun invariant_tac i = |
|
17 |
rtac invariantI i THEN |
|
5648 | 18 |
constrains_tac (i+1); |
5636 | 19 |
|
20 |
(*Safety property 1(a): ask is nondecreasing*) |
|
21 |
Goalw [increasing_def] "Cli_prg: increasing ask"; |
|
5648 | 22 |
by (Clarify_tac 1); |
5636 | 23 |
by (constrains_tac 1); |
24 |
by Auto_tac; |
|
25 |
qed "increasing_ask"; |
|
26 |
||
27 |
(*Safety property 1(b): rel is nondecreasing*) |
|
28 |
Goalw [increasing_def] "Cli_prg: increasing rel"; |
|
5648 | 29 |
by (Clarify_tac 1); |
5636 | 30 |
by (constrains_tac 1); |
31 |
by Auto_tac; |
|
32 |
qed "increasing_rel"; |
|
33 |
||
34 |
Addsimps [nth_append, append_one_prefix]; |
|
35 |
||
36 |
Goal "Cli_prg: invariant {s. tok s <= Max}"; |
|
37 |
by (invariant_tac 1); |
|
38 |
by Auto_tac; |
|
39 |
qed "tok_bounded"; |
|
40 |
||
41 |
(*Safety property 3: no client requests "too many" tokens. |
|
42 |
With no Substitution Axiom, we must prove the two invariants |
|
43 |
simultaneously. Could combine tok_bounded, stable_constrains_stable |
|
44 |
and a rule invariant_implies_stable... |
|
45 |
*) |
|
46 |
Goal "Cli_prg: \ |
|
47 |
\ invariant ({s. tok s <= Max} Int \ |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
48 |
\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})"; |
5636 | 49 |
by (invariant_tac 1); |
50 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
51 |
qed "ask_bounded"; |
|
52 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
53 |
(** Several facts used to prove Lemma 1 **) |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
54 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
55 |
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
|
56 |
by (constrains_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
57 |
by Auto_tac; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
58 |
qed "stable_rel_le_giv"; |
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. size (rel s) <= size (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_size_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 (ask s) <= Suc (size (rel 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_ask_le_rel"; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
69 |
|
5636 | 70 |
|
5667 | 71 |
(*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
|
72 |
expanding it is extremely expensive!*) |
5648 | 73 |
program_defs_ref := []; |
74 |
||
5636 | 75 |
(*Safety property 2: clients return the right number of tokens*) |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
76 |
Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg)) \ |
7361 | 77 |
\ guarantees Always {s. rel s <= giv s}"; |
5636 | 78 |
by (rtac guaranteesI 1); |
6570 | 79 |
by (rtac AlwaysI 1); |
5648 | 80 |
by (Force_tac 1); |
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7537
diff
changeset
|
81 |
by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
82 |
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
|
83 |
stable_rel_le_giv]) 1); |
5636 | 84 |
qed "ok_guar_rel_prefix_giv"; |
85 |
||
86 |
||
87 |
(*** Towards proving the liveness property ***) |
|
88 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6018
diff
changeset
|
89 |
Goal "Cli_prg Join G \ |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
90 |
\ : transient {s. size (giv s) = Suc k & \ |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
91 |
\ size (rel s) = k & ask s ! k <= giv s ! k}"; |
8041 | 92 |
by (res_inst_tac [("act", "rel_act")] transientI 1); |
5636 | 93 |
by (auto_tac (claset(), |
7537 | 94 |
simpset() addsimps [Domain_def, Cli_prg_def])); |
5636 | 95 |
qed "transient_lemma"; |
96 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
97 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
98 |
|
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
99 |
val rewrite_o = rewrite_rule [o_def]; |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
100 |
|
6701 | 101 |
val Increasing_length = mono_length RS mono_Increasing_o; |
102 |
||
5636 | 103 |
Goal "Cli_prg : \ |
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
104 |
\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \ |
7361 | 105 |
\ guarantees 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
|
106 |
\ {s. size (rel s) <= size (giv s)})"; |
5636 | 107 |
by (rtac guaranteesI 1); |
108 |
by (Clarify_tac 1); |
|
6701 | 109 |
by (dtac (impOfSubs (rewrite_o Increasing_length)) 1); |
6570 | 110 |
by (rtac AlwaysI 1); |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
111 |
by (Force_tac 1); |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
112 |
by (rtac Stable_Int 1); |
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7537
diff
changeset
|
113 |
by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2); |
7964
6b3e345c47b3
localTo_imp_o_localTo is now really an implication
paulson
parents:
7878
diff
changeset
|
114 |
by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo] |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
115 |
addIs [Increasing_localTo_Stable, |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5758
diff
changeset
|
116 |
stable_size_rel_le_giv]) 2); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
117 |
by (full_simp_tac (simpset() addsimps [Join_localTo]) 1); |
7964
6b3e345c47b3
localTo_imp_o_localTo is now really an implication
paulson
parents:
7878
diff
changeset
|
118 |
by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo] |
5804
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 : \ |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7826
diff
changeset
|
125 |
\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \ |
6570 | 126 |
\ Int Always giv_meets_ask) \ |
7361 | 127 |
\ guarantees ({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); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
137 |
by (force_tac (claset(), |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
138 |
simpset() addsimps [Always_eq_includes_reachable, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
139 |
giv_meets_ask_def]) 1); |
5636 | 140 |
qed "client_correct"; |