author | wenzelm |
Tue, 05 Aug 2014 12:01:32 +0200 | |
changeset 57859 | 29e728588163 |
parent 46953 | 2b6e55924af3 |
child 58860 | fee7cfa69c50 |
permissions | -rw-r--r-- |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/UNITY/ClientImpl.thy |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
2 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
3 |
Copyright 2002 University of Cambridge |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
4 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26289
diff
changeset
|
5 |
Distributed Resource Management System: Client Implementation. |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
6 |
*) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
7 |
|
16417 | 8 |
theory ClientImpl imports AllocBase Guar begin |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
9 |
|
24892 | 10 |
abbreviation "ask == Var(Nil)" (* input history: tokens requested *) |
11 |
abbreviation "giv == Var([0])" (* output history: tokens granted *) |
|
12 |
abbreviation "rel == Var([1])" (* input history: tokens released *) |
|
13 |
abbreviation "tok == Var([2])" (* the number of available tokens *) |
|
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
14 |
|
41779 | 15 |
axiomatization where |
14061 | 16 |
type_assumes: |
46953 | 17 |
"type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & |
41779 | 18 |
type_of(rel) = list(tokbag) & type_of(tok) = nat" and |
14061 | 19 |
default_val_assumes: |
46953 | 20 |
"default_val(ask) = Nil & default_val(giv) = Nil & |
41779 | 21 |
default_val(rel) = Nil & default_val(tok) = 0" |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
22 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
23 |
|
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
24 |
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
25 |
|
24893 | 26 |
definition |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
27 |
(** Release some client_tokens **) |
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
28 |
"client_rel_act == |
14061 | 29 |
{<s,t> \<in> state*state. |
30 |
\<exists>nrel \<in> nat. nrel = length(s`rel) & |
|
14057 | 31 |
t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) & |
32 |
nrel < length(s`giv) & |
|
14061 | 33 |
nth(nrel, s`ask) \<le> nth(nrel, s`giv)}" |
46953 | 34 |
|
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
35 |
(** Choose a new token requirement **) |
14057 | 36 |
(** Including t=s suppresses fairness, allowing the non-trivial part |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
37 |
of the action to be ignored **) |
24893 | 38 |
definition |
39 |
"client_tok_act == {<s,t> \<in> state*state. t=s | |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26289
diff
changeset
|
40 |
t = s(tok:=succ(s`tok mod NbT))}" |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
41 |
|
24893 | 42 |
definition |
14061 | 43 |
"client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
46953 | 44 |
|
24893 | 45 |
definition |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
46 |
"client_prog == |
14061 | 47 |
mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil & |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26289
diff
changeset
|
48 |
s`ask = Nil & s`rel = Nil}, |
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff
changeset
|
49 |
{client_rel_act, client_tok_act, client_ask_act}, |
14061 | 50 |
\<Union>G \<in> preserves(lift(rel)) Int |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26289
diff
changeset
|
51 |
preserves(lift(ask)) Int |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26289
diff
changeset
|
52 |
preserves(lift(tok)). Acts(G))" |
14061 | 53 |
|
54 |
||
55 |
declare type_assumes [simp] default_val_assumes [simp] |
|
56 |
(* This part should be automated *) |
|
57 |
||
58 |
lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)" |
|
59 |
apply (unfold state_def) |
|
60 |
apply (drule_tac a = ask in apply_type, auto) |
|
61 |
done |
|
62 |
||
63 |
lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)" |
|
64 |
apply (unfold state_def) |
|
65 |
apply (drule_tac a = giv in apply_type, auto) |
|
66 |
done |
|
67 |
||
68 |
lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)" |
|
69 |
apply (unfold state_def) |
|
70 |
apply (drule_tac a = rel in apply_type, auto) |
|
71 |
done |
|
72 |
||
73 |
lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat" |
|
74 |
apply (unfold state_def) |
|
75 |
apply (drule_tac a = tok in apply_type, auto) |
|
76 |
done |
|
77 |
||
78 |
(** The Client Program **) |
|
79 |
||
80 |
lemma client_type [simp,TC]: "client_prog \<in> program" |
|
81 |
apply (unfold client_prog_def) |
|
82 |
apply (simp (no_asm)) |
|
83 |
done |
|
84 |
||
85 |
declare client_prog_def [THEN def_prg_Init, simp] |
|
86 |
declare client_prog_def [THEN def_prg_AllowedActs, simp] |
|
24051
896fb015079c
replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents:
16417
diff
changeset
|
87 |
declare client_prog_def [program] |
14061 | 88 |
|
89 |
declare client_rel_act_def [THEN def_act_simp, simp] |
|
90 |
declare client_tok_act_def [THEN def_act_simp, simp] |
|
91 |
declare client_ask_act_def [THEN def_act_simp, simp] |
|
92 |
||
93 |
lemma client_prog_ok_iff: |
|
46953 | 94 |
"\<forall>G \<in> program. (client_prog ok G) \<longleftrightarrow> |
95 |
(G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) & |
|
14061 | 96 |
G \<in> preserves(lift(tok)) & client_prog \<in> Allowed(G))" |
97 |
by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed]) |
|
98 |
||
99 |
lemma client_prog_preserves: |
|
100 |
"client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))" |
|
101 |
apply (rule Inter_var_DiffI, force) |
|
102 |
apply (rule ballI) |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
103 |
apply (rule preservesI, safety, auto) |
14061 | 104 |
done |
105 |
||
106 |
||
107 |
lemma preserves_lift_imp_stable: |
|
108 |
"G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"; |
|
109 |
apply (drule preserves_imp_stable) |
|
46953 | 110 |
apply (simp add: lift_def) |
14061 | 111 |
done |
112 |
||
113 |
lemma preserves_imp_prefix: |
|
46953 | 114 |
"G \<in> preserves(lift(ff)) |
14061 | 115 |
==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"; |
46953 | 116 |
by (erule preserves_lift_imp_stable) |
14061 | 117 |
|
46953 | 118 |
(*Safety property 1 \<in> ask, rel are increasing: (24) *) |
119 |
lemma client_prog_Increasing_ask_rel: |
|
46823 | 120 |
"client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))" |
14061 | 121 |
apply (unfold guar_def) |
46953 | 122 |
apply (auto intro!: increasing_imp_Increasing |
26289 | 123 |
simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix) |
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
124 |
apply (safety, force, force)+ |
14061 | 125 |
done |
126 |
||
127 |
declare nth_append [simp] append_one_prefix [simp] |
|
128 |
||
129 |
lemma NbT_pos2: "0<NbT" |
|
130 |
apply (cut_tac NbT_pos) |
|
131 |
apply (rule Ord_0_lt, auto) |
|
132 |
done |
|
133 |
||
46953 | 134 |
(*Safety property 2 \<in> the client never requests too many tokens. |
14061 | 135 |
With no Substitution Axiom, we must prove the two invariants simultaneously. *) |
136 |
||
46953 | 137 |
lemma ask_Bounded_lemma: |
138 |
"[| client_prog ok G; G \<in> program |] |
|
139 |
==> client_prog \<squnion> G \<in> |
|
140 |
Always({s \<in> state. s`tok \<le> NbT} \<inter> |
|
14061 | 141 |
{s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})" |
142 |
apply (rotate_tac -1) |
|
143 |
apply (auto simp add: client_prog_ok_iff) |
|
46953 | 144 |
apply (rule invariantI [THEN stable_Join_Always2], force) |
14061 | 145 |
prefer 2 |
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
146 |
apply (fast intro: stable_Int preserves_lift_imp_stable, safety) |
14061 | 147 |
apply (auto dest: ActsD) |
148 |
apply (cut_tac NbT_pos) |
|
149 |
apply (rule NbT_pos2 [THEN mod_less_divisor]) |
|
150 |
apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append) |
|
151 |
done |
|
152 |
||
153 |
(* Export version, with no mention of tok in the postcondition, but |
|
154 |
unfortunately tok must be declared local.*) |
|
46953 | 155 |
lemma client_prog_ask_Bounded: |
156 |
"client_prog \<in> program guarantees |
|
14061 | 157 |
Always({s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})" |
158 |
apply (rule guaranteesI) |
|
159 |
apply (erule ask_Bounded_lemma [THEN Always_weaken], auto) |
|
160 |
done |
|
161 |
||
162 |
(*** Towards proving the liveness property ***) |
|
163 |
||
46953 | 164 |
lemma client_prog_stable_rel_le_giv: |
14061 | 165 |
"client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
166 |
by (safety, auto) |
14061 | 167 |
|
46953 | 168 |
lemma client_prog_Join_Stable_rel_le_giv: |
169 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |] |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
170 |
==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
14061 | 171 |
apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable]) |
172 |
apply (auto simp add: lift_def) |
|
173 |
done |
|
174 |
||
175 |
lemma client_prog_Join_Always_rel_le_giv: |
|
46953 | 176 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |] |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
177 |
==> client_prog \<squnion> G \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})" |
14061 | 178 |
by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv) |
179 |
||
180 |
lemma def_act_eq: |
|
181 |
"A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}" |
|
182 |
by auto |
|
183 |
||
184 |
lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state" |
|
185 |
by auto |
|
186 |
||
46953 | 187 |
lemma transient_lemma: |
188 |
"client_prog \<in> |
|
189 |
transient({s \<in> state. s`rel = k & <k, h> \<in> strict_prefix(nat) |
|
14061 | 190 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask})" |
191 |
apply (rule_tac act = client_rel_act in transientI) |
|
192 |
apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts]) |
|
193 |
apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset]) |
|
194 |
apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def) |
|
195 |
apply (rule ReplaceI) |
|
196 |
apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI) |
|
197 |
apply (auto intro!: state_update_type app_type length_type nth_type, auto) |
|
198 |
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) |
|
199 |
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) |
|
200 |
apply (simp (no_asm_use) add: gen_prefix_iff_nth) |
|
201 |
apply (subgoal_tac "h \<in> list(nat)") |
|
202 |
apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1]) |
|
203 |
apply (auto simp add: prefix_def Ge_def) |
|
204 |
apply (drule strict_prefix_length_lt) |
|
205 |
apply (drule_tac x = "length (x`rel) " in spec) |
|
206 |
apply auto |
|
207 |
apply (simp (no_asm_use) add: gen_prefix_iff_nth) |
|
208 |
apply (auto simp add: id_def lam_def) |
|
209 |
done |
|
210 |
||
46953 | 211 |
lemma strict_prefix_is_prefix: |
46823 | 212 |
"<xs, ys> \<in> strict_prefix(A) \<longleftrightarrow> <xs, ys> \<in> prefix(A) & xs\<noteq>ys" |
14061 | 213 |
apply (unfold strict_prefix_def id_def lam_def) |
214 |
apply (auto dest: prefix_type [THEN subsetD]) |
|
215 |
done |
|
216 |
||
46953 | 217 |
lemma induct_lemma: |
218 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
|
219 |
==> client_prog \<squnion> G \<in> |
|
220 |
{s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat) |
|
221 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
|
222 |
LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat) |
|
223 |
& <s`rel, s`giv> \<in> prefix(nat) & |
|
224 |
<h, s`giv> \<in> prefix(nat) & |
|
14061 | 225 |
h pfixGe s`ask}" |
226 |
apply (rule single_LeadsTo_I) |
|
227 |
prefer 2 apply simp |
|
228 |
apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD]) |
|
229 |
apply (rotate_tac [3] 2) |
|
230 |
apply (auto simp add: client_prog_ok_iff) |
|
231 |
apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken]) |
|
232 |
apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int]) |
|
233 |
apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable) |
|
234 |
apply (simp (no_asm_simp)) |
|
235 |
apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable) |
|
236 |
apply (simp (no_asm_simp)) |
|
237 |
apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable) |
|
238 |
apply (simp (no_asm_simp)) |
|
239 |
apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all) |
|
240 |
prefer 2 |
|
241 |
apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans) |
|
46953 | 242 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1] |
14061 | 243 |
prefix_trans) |
244 |
done |
|
245 |
||
46953 | 246 |
lemma rel_progress_lemma: |
247 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
|
248 |
==> client_prog \<squnion> G \<in> |
|
249 |
{s \<in> state. <s`rel, h> \<in> strict_prefix(nat) |
|
250 |
& <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
|
14061 | 251 |
LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}" |
46953 | 252 |
apply (rule_tac f = "\<lambda>x \<in> state. length(h) #- length(x`rel)" |
14061 | 253 |
in LessThan_induct) |
254 |
apply (auto simp add: vimage_def) |
|
46953 | 255 |
prefer 2 apply (force simp add: lam_def) |
14061 | 256 |
apply (rule single_LeadsTo_I) |
46953 | 257 |
prefer 2 apply simp |
14061 | 258 |
apply (subgoal_tac "h \<in> list(nat)") |
46953 | 259 |
prefer 2 apply (blast dest: prefix_type [THEN subsetD]) |
14061 | 260 |
apply (rule induct_lemma [THEN LeadsTo_weaken]) |
261 |
apply (simp add: length_type lam_def) |
|
262 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD2] |
|
263 |
dest: common_prefix_linear prefix_type [THEN subsetD]) |
|
264 |
apply (erule swap) |
|
265 |
apply (rule imageI) |
|
46953 | 266 |
apply (force dest!: simp add: lam_def) |
267 |
apply (simp add: length_type lam_def, clarify) |
|
14061 | 268 |
apply (drule strict_prefix_length_lt)+ |
269 |
apply (drule less_imp_succ_add, simp)+ |
|
46953 | 270 |
apply clarify |
271 |
apply simp |
|
14061 | 272 |
apply (erule diff_le_self [THEN ltD]) |
273 |
done |
|
274 |
||
46953 | 275 |
lemma progress_lemma: |
276 |
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] |
|
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
277 |
==> client_prog \<squnion> G |
46953 | 278 |
\<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask} |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
279 |
LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}" |
46953 | 280 |
apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], |
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
281 |
assumption) |
14061 | 282 |
apply (force simp add: client_prog_ok_iff) |
46953 | 283 |
apply (rule LeadsTo_weaken_L) |
284 |
apply (rule LeadsTo_Un [OF rel_progress_lemma |
|
14061 | 285 |
subset_refl [THEN subset_imp_LeadsTo]]) |
286 |
apply (auto intro: strict_prefix_is_prefix [THEN iffD2] |
|
287 |
dest: common_prefix_linear prefix_type [THEN subsetD]) |
|
288 |
done |
|
289 |
||
290 |
(*Progress property: all tokens that are given will be released*) |
|
46953 | 291 |
lemma client_prog_progress: |
292 |
"client_prog \<in> Incr(lift(giv)) guarantees |
|
293 |
(\<Inter>h \<in> list(nat). {s \<in> state. <h, s`giv> \<in> prefix(nat) & |
|
14061 | 294 |
h pfixGe s`ask} LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)})" |
295 |
apply (rule guaranteesI) |
|
296 |
apply (blast intro: progress_lemma, auto) |
|
297 |
done |
|
298 |
||
299 |
lemma client_prog_Allowed: |
|
46953 | 300 |
"Allowed(client_prog) = |
46823 | 301 |
preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))" |
14061 | 302 |
apply (cut_tac v = "lift (ask)" in preserves_type) |
46953 | 303 |
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed] |
14061 | 304 |
cons_Int_distrib safety_prop_Acts_iff) |
305 |
done |
|
306 |
||
14072
f932be305381
Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents:
14061
diff
changeset
|
307 |
end |