src/HOL/UNITY/Client.ML
author paulson
Sat, 23 Sep 2000 16:02:01 +0200
changeset 10064 1a77667b21ef
parent 9403 aad13b59b8d9
permissions -rw-r--r--
added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Client
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     2
    ID:         $Id$
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     5
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     6
Distributed Resource Management System: the Client
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     7
*)
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
     8
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
     9
Addsimps [Client_def RS def_prg_Init, 
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    10
          Client_def RS def_prg_AllowedActs];
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    11
program_defs_ref := [Client_def];
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    12
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    13
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    14
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    15
Goal "(Client ok G) = \
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    16
\     (G : preserves rel & G : preserves ask & G : preserves tok &\
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    17
\      Client : Allowed G)";
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    18
by (auto_tac (claset(), 
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    19
      simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));  
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    20
qed "Client_ok_iff";
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    21
AddIffs [Client_ok_iff];
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    22
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    23
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    24
(*Safety property 1: ask, rel are increasing*)
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    25
Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    26
by (auto_tac
9403
aad13b59b8d9 much tidying in connection with the 2nd UNITY paper
paulson
parents: 8948
diff changeset
    27
    (claset() addSIs [increasing_imp_Increasing],
aad13b59b8d9 much tidying in connection with the 2nd UNITY paper
paulson
parents: 8948
diff changeset
    28
     simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    29
by (auto_tac (claset(), simpset() addsimps [increasing_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    30
by (ALLGOALS constrains_tac);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    31
by Auto_tac;
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    32
qed "increasing_ask_rel";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    33
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    34
Addsimps [nth_append, append_one_prefix];
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    35
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    36
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    37
(*Safety property 2: the client never requests too many tokens.
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    38
      With no Substitution Axiom, we must prove the two invariants 
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    39
  simultaneously.
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    40
*)
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    41
Goal "Client ok G  \
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    42
\     ==> Client Join G :  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    43
\             Always ({s. tok s <= NbT}  Int  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    44
\                     {s. ALL elt : set (ask s). elt <= NbT})";
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    45
by Auto_tac;  
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    46
by (rtac (invariantI RS stable_Join_Always2) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    47
by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    48
		       addSIs [stable_Int]) 3);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    49
by (constrains_tac 2);
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
    50
by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    51
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    52
qed "ask_bounded_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    53
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
    54
(*export version, with no mention of tok in the postcondition, but
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
    55
  unfortunately tok must be declared local.*)
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    56
Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    57
by (rtac guaranteesI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    58
by (etac (ask_bounded_lemma RS Always_weaken) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    59
by (rtac Int_lower2 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    60
qed "ask_bounded";
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    61
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    62
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    63
(*** Towards proving the liveness property ***)
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    64
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    65
Goal "Client: stable {s. rel s <= giv s}";
5804
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_rel_le_giv";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
    69
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    70
Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    71
\     ==> Client Join G : Stable {s. rel s <= giv s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    72
by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    73
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    74
qed "Join_Stable_rel_le_giv";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    75
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    76
Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    77
\     ==> Client Join G : Always {s. rel s <= giv s}";
9403
aad13b59b8d9 much tidying in connection with the 2nd UNITY paper
paulson
parents: 8948
diff changeset
    78
by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    79
qed "Join_Always_rel_le_giv";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    80
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    81
Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    82
by (res_inst_tac [("act", "rel_act")] transientI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    83
by (auto_tac (claset(),
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    84
	      simpset() addsimps [Domain_def, Client_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    85
by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    86
			       strict_prefix_length_less]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    87
by (auto_tac (claset(), 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    88
	      simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    89
by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    90
qed "transient_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    91
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    92
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
    93
Goal "[| Client Join G : Increasing giv;  Client ok G |] \
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    94
\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    95
\                     LeadsTo {s. k < rel s & rel s <= giv s & \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    96
\                                 h <= giv s & h pfixGe ask s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    97
by (rtac single_LeadsTo_I 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    98
by (ftac (increasing_ask_rel RS guaranteesD) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    99
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   100
by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   101
	  leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   102
by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   103
by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   104
by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   105
by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   106
by (etac Join_Stable_rel_le_giv 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   107
by (Blast_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   108
by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   109
			       order_trans, prefix_imp_pfixGe, 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   110
			       pfixGe_trans]) 2);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   111
by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   112
qed "induct_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   113
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   114
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
   115
Goal "[| Client Join G : Increasing giv;  Client ok G |] \
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   116
\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   117
\                     LeadsTo {s. h <= rel s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   118
by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   119
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   120
by (rtac single_LeadsTo_I 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   121
by (rtac (induct_lemma RS LeadsTo_weaken) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   122
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   123
by (blast_tac (claset() addIs [order_less_le RS iffD2]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   124
			addDs [common_prefix_linear]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   125
by (REPEAT (dtac strict_prefix_length_less 1));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   126
by (arith_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   127
qed "rel_progress_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   128
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   129
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
   130
Goal "[| Client Join G : Increasing giv;  Client ok G |] \
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   131
\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   132
\                     LeadsTo {s. h <= rel s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   133
by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   134
by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   135
    LeadsTo_Un RS LeadsTo_weaken_L) 3);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   136
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   137
by (blast_tac (claset() addIs [order_less_le RS iffD2]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   138
			addDs [common_prefix_linear]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   139
qed "client_progress_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   140
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   141
(*Progress property: all tokens that are given will be released*)
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   142
Goal "Client : \
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
   143
\      Increasing giv  guarantees  \
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   144
\      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   145
by (rtac guaranteesI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   146
by (Clarify_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   147
by (blast_tac (claset() addIs [client_progress_lemma]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   148
qed "client_progress";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   149
8311
6218522253e7 new mostly working version; Alloc nearly converted to "Rename"
paulson
parents: 8251
diff changeset
   150
(*This shows that the Client won't alter other variables in any state
6218522253e7 new mostly working version; Alloc nearly converted to "Rename"
paulson
parents: 8251
diff changeset
   151
  that it is combined with*)
9403
aad13b59b8d9 much tidying in connection with the 2nd UNITY paper
paulson
parents: 8948
diff changeset
   152
Goal "Client : preserves dummy";
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   153
by (rewtac preserves_def);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   154
by Auto_tac;
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   155
by (constrains_tac 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   156
by Auto_tac;
9403
aad13b59b8d9 much tidying in connection with the 2nd UNITY paper
paulson
parents: 8948
diff changeset
   157
qed "client_preserves_dummy";
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   158
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   159
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   160
(** Obsolete lemmas from first version of the Client **)
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   161
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   162
Goal "Client: stable {s. size (rel s) <= size (giv s)}";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   163
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   164
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   165
qed "stable_size_rel_le_giv";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   166
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   167
(*clients return the right number of tokens*)
10064
1a77667b21ef added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents: 9403
diff changeset
   168
Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   169
by (rtac guaranteesI 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   170
by (rtac AlwaysI 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
   171
by (Force_tac 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   172
by (blast_tac (claset() addIs [Increasing_preserves_Stable, 
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   173
			       stable_rel_le_giv]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   174
qed "ok_guar_rel_prefix_giv";