author | wenzelm |
Sat, 23 Apr 2011 13:00:19 +0200 | |
changeset 42463 | f270e3e18be5 |
parent 36866 | 426d5781bb25 |
child 46752 | e9e7209eb375 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
1 |
(* Title: HOL/UNITY/Comp/Client.thy |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
6 |
header{*Distributed Resource Management System: the Client*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
7 |
|
36866 | 8 |
theory Client imports "../Rename" AllocBase begin |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
42463 | 10 |
type_synonym |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
11 |
tokbag = nat --{*tokbags could be multisets...or any ordered type?*} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
record state = |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
14 |
giv :: "tokbag list" --{*input history: tokens granted*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
15 |
ask :: "tokbag list" --{*output history: tokens requested*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
16 |
rel :: "tokbag list" --{*output history: tokens released*} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
17 |
tok :: tokbag --{*current token request*} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
record 'a state_d = |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
state + |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
21 |
dummy :: 'a --{*new variables*} |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
(** Release some tokens **) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
|
36866 | 29 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
rel_act :: "('a state_d * 'a state_d) set" |
36866 | 31 |
where "rel_act = {(s,s'). |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
32 |
\<exists>nrel. nrel = size (rel s) & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
33 |
s' = s (| rel := rel s @ [giv s!nrel] |) & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
34 |
nrel < size (giv s) & |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
35 |
ask s!nrel \<le> giv s!nrel}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
37 |
(** Choose a new token requirement **) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
38 |
|
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
(** Including s'=s suppresses fairness, allowing the non-trivial part |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
40 |
of the action to be ignored **) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
|
36866 | 42 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
43 |
tok_act :: "('a state_d * 'a state_d) set" |
36866 | 44 |
where "tok_act = {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
45 |
|
36866 | 46 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
47 |
ask_act :: "('a state_d * 'a state_d) set" |
36866 | 48 |
where "ask_act = {(s,s'). s'=s | |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
49 |
(s' = s (|ask := ask s @ [tok s]|))}" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
|
36866 | 51 |
definition |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
52 |
Client :: "'a state_d program" |
36866 | 53 |
where "Client = |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
11194
diff
changeset
|
54 |
mk_total_program |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
55 |
({s. tok s \<in> atMost NbT & |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
56 |
giv s = [] & ask s = [] & rel s = []}, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
57 |
{rel_act, tok_act, ask_act}, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
58 |
\<Union>G \<in> preserves rel Int preserves ask Int preserves tok. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
59 |
Acts G)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
60 |
|
36866 | 61 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
62 |
(*Maybe want a special theory section to declare such maps*) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
63 |
non_dummy :: "'a state_d => state" |
36866 | 64 |
where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
65 |
|
36866 | 66 |
definition |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
67 |
(*Renaming map to put a Client into the standard form*) |
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
68 |
client_map :: "'a state_d => state*'a" |
36866 | 69 |
where "client_map = funPair non_dummy dummy" |
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
|
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
71 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
72 |
declare Client_def [THEN def_prg_Init, simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
73 |
declare Client_def [THEN def_prg_AllowedActs, simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
74 |
declare rel_act_def [THEN def_act_simp, simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
75 |
declare tok_act_def [THEN def_act_simp, simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
76 |
declare ask_act_def [THEN def_act_simp, simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
77 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
78 |
lemma Client_ok_iff [iff]: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
79 |
"(Client ok G) = |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
80 |
(G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok & |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
81 |
Client \<in> Allowed G)" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
82 |
by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
83 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
84 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
85 |
text{*Safety property 1: ask, rel are increasing*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
86 |
lemma increasing_ask_rel: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
87 |
"Client \<in> UNIV guarantees Increasing ask Int Increasing rel" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
88 |
apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
89 |
apply (auto simp add: Client_def increasing_def) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14089
diff
changeset
|
90 |
apply (safety, auto)+ |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
91 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
92 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
93 |
declare nth_append [simp] append_one_prefix [simp] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
94 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
95 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
96 |
text{*Safety property 2: the client never requests too many tokens. |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
97 |
With no Substitution Axiom, we must prove the two invariants |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
98 |
simultaneously. *} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
99 |
lemma ask_bounded_lemma: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
100 |
"Client ok G |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
101 |
==> Client Join G \<in> |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
102 |
Always ({s. tok s \<le> NbT} Int |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
103 |
{s. \<forall>elt \<in> set (ask s). elt \<le> NbT})" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
104 |
apply auto |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
105 |
apply (rule invariantI [THEN stable_Join_Always2], force) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
106 |
prefer 2 |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
107 |
apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int) |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14089
diff
changeset
|
108 |
apply (simp add: Client_def, safety) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
109 |
apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
110 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
111 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
112 |
text{*export version, with no mention of tok in the postcondition, but |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
113 |
unfortunately tok must be declared local.*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
114 |
lemma ask_bounded: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
115 |
"Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
116 |
apply (rule guaranteesI) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
117 |
apply (erule ask_bounded_lemma [THEN Always_weaken]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
118 |
apply (rule Int_lower2) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
119 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
120 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
121 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
122 |
text{*** Towards proving the liveness property ***} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
123 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
124 |
lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14089
diff
changeset
|
125 |
by (simp add: Client_def, safety, auto) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
126 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
127 |
lemma Join_Stable_rel_le_giv: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
128 |
"[| Client Join G \<in> Increasing giv; G \<in> preserves rel |] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
129 |
==> Client Join G \<in> Stable {s. rel s \<le> giv s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
130 |
by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
131 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
132 |
lemma Join_Always_rel_le_giv: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
133 |
"[| Client Join G \<in> Increasing giv; G \<in> preserves rel |] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
134 |
==> Client Join G \<in> Always {s. rel s \<le> giv s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
135 |
by (force intro: AlwaysI Join_Stable_rel_le_giv) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
136 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
137 |
lemma transient_lemma: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
138 |
"Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
139 |
apply (simp add: Client_def mk_total_program_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
140 |
apply (rule_tac act = rel_act in totalize_transientI) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
141 |
apply (auto simp add: Domain_def Client_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
142 |
apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
143 |
apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
144 |
apply (blast intro: strict_prefix_length_less) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
145 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
146 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
147 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
148 |
lemma induct_lemma: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
149 |
"[| Client Join G \<in> Increasing giv; Client ok G |] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
150 |
==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
151 |
LeadsTo {s. k < rel s & rel s \<le> giv s & |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
152 |
h \<le> giv s & h pfixGe ask s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
153 |
apply (rule single_LeadsTo_I) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
154 |
apply (frule increasing_ask_rel [THEN guaranteesD], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
155 |
apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
156 |
apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
157 |
apply (erule_tac f = giv and x = "giv s" in IncreasingD) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
158 |
apply (erule_tac f = ask and x = "ask s" in IncreasingD) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
159 |
apply (erule_tac f = rel and x = "rel s" in IncreasingD) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
160 |
apply (erule Join_Stable_rel_le_giv, blast) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
161 |
apply (blast intro: order_less_imp_le order_trans) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
162 |
apply (blast intro: sym order_less_le [THEN iffD2] order_trans |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
163 |
prefix_imp_pfixGe pfixGe_trans) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
164 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
165 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
166 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
167 |
lemma rel_progress_lemma: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
168 |
"[| Client Join G \<in> Increasing giv; Client ok G |] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
169 |
==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
170 |
LeadsTo {s. h \<le> rel s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
171 |
apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
172 |
apply (auto simp add: vimage_def) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
173 |
apply (rule single_LeadsTo_I) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
174 |
apply (rule induct_lemma [THEN LeadsTo_weaken], auto) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
175 |
apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
176 |
apply (drule strict_prefix_length_less)+ |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
177 |
apply arith |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
178 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
179 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
180 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
181 |
lemma client_progress_lemma: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
182 |
"[| Client Join G \<in> Increasing giv; Client ok G |] |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
183 |
==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
184 |
LeadsTo {s. h \<le> rel s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
185 |
apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
186 |
apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
187 |
apply (blast intro: rel_progress_lemma) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
188 |
apply (rule subset_refl [THEN subset_imp_LeadsTo]) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
189 |
apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
190 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
191 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
192 |
text{*Progress property: all tokens that are given will be released*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
193 |
lemma client_progress: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
194 |
"Client \<in> |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
195 |
Increasing giv guarantees |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
196 |
(INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
197 |
apply (rule guaranteesI, clarify) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
198 |
apply (blast intro: client_progress_lemma) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
199 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
200 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
201 |
text{*This shows that the Client won't alter other variables in any state |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
202 |
that it is combined with*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
203 |
lemma client_preserves_dummy: "Client \<in> preserves dummy" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14089
diff
changeset
|
204 |
by (simp add: Client_def preserves_def, clarify, safety, auto) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
205 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
206 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
207 |
text{** Obsolete lemmas from first version of the Client **} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
208 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
209 |
lemma stable_size_rel_le_giv: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
210 |
"Client \<in> stable {s. size (rel s) \<le> size (giv s)}" |
16184
80617b8d33c5
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14089
diff
changeset
|
211 |
by (simp add: Client_def, safety, auto) |
14089
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
212 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
213 |
text{*clients return the right number of tokens*} |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
214 |
lemma ok_guar_rel_prefix_giv: |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
215 |
"Client \<in> Increasing giv guarantees Always {s. rel s \<le> giv s}" |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
216 |
apply (rule guaranteesI) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
217 |
apply (rule AlwaysI, force) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
218 |
apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv) |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
219 |
done |
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
220 |
|
7b34f58b1b81
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
paulson
parents:
13812
diff
changeset
|
221 |
|
11194
ea13ff5a26d1
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
222 |
end |