equal
deleted
inserted
replaced
72 expanding it is extremely expensive!*) |
72 expanding it is extremely expensive!*) |
73 program_defs_ref := []; |
73 program_defs_ref := []; |
74 |
74 |
75 (*Safety property 2: clients return the right number of tokens*) |
75 (*Safety property 2: clients return the right number of tokens*) |
76 Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \ |
76 Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \ |
77 \ guar Always {s. rel s <= giv s}"; |
77 \ guarantees Always {s. rel s <= giv s}"; |
78 by (rtac guaranteesI 1); |
78 by (rtac guaranteesI 1); |
79 by (rtac AlwaysI 1); |
79 by (rtac AlwaysI 1); |
80 by (Force_tac 1); |
80 by (Force_tac 1); |
81 by (blast_tac (claset() addIs [Increasing_localTo_Stable, |
81 by (blast_tac (claset() addIs [Increasing_localTo_Stable, |
82 stable_rel_le_giv]) 1); |
82 stable_rel_le_giv]) 1); |
99 |
99 |
100 val Increasing_length = mono_length RS mono_Increasing_o; |
100 val Increasing_length = mono_length RS mono_Increasing_o; |
101 |
101 |
102 Goal "Cli_prg : \ |
102 Goal "Cli_prg : \ |
103 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \ |
103 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \ |
104 \ guar Always ({s. size (ask s) <= Suc (size (rel s))} Int \ |
104 \ guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \ |
105 \ {s. size (rel s) <= size (giv s)})"; |
105 \ {s. size (rel s) <= size (giv s)})"; |
106 by (rtac guaranteesI 1); |
106 by (rtac guaranteesI 1); |
107 by (Clarify_tac 1); |
107 by (Clarify_tac 1); |
108 by (dtac (impOfSubs (rewrite_o Increasing_length)) 1); |
108 by (dtac (impOfSubs (rewrite_o Increasing_length)) 1); |
109 by (rtac AlwaysI 1); |
109 by (rtac AlwaysI 1); |
119 |
119 |
120 |
120 |
121 Goal "Cli_prg : \ |
121 Goal "Cli_prg : \ |
122 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ |
122 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ |
123 \ Int Always giv_meets_ask) \ |
123 \ Int Always giv_meets_ask) \ |
124 \ guar ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; |
124 \ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; |
125 by (rtac guaranteesI 1); |
125 by (rtac guaranteesI 1); |
126 by (Clarify_tac 1); |
126 by (Clarify_tac 1); |
127 by (rtac Stable_transient_Always_LeadsTo 1); |
127 by (rtac Stable_transient_Always_LeadsTo 1); |
128 by (res_inst_tac [("k", "k")] transient_lemma 2); |
128 by (res_inst_tac [("k", "k")] transient_lemma 2); |
129 by (force_tac (claset() addDs [impOfSubs Increasing_length, |
129 by (force_tac (claset() addDs [impOfSubs Increasing_length, |