src/HOL/UNITY/Client.ML
author paulson
Fri, 18 Feb 2000 15:20:44 +0100
changeset 8251 9be357df93d4
parent 8216 e4b3192dfefa
child 8311 6218522253e7
permissions -rw-r--r--
New treatment of "guarantees" with polymorphic components and bijections. Works EXCEPT FOR Alloc.
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
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
     9
Addsimps [Client_def RS def_prg_Init];
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    10
program_defs_ref := [Client_def];
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    11
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    12
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    13
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    14
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    15
fun invariant_tac i = 
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    16
    rtac invariantI i  THEN
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
    17
    constrains_tac (i+1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    18
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    19
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    20
(*Safety property 1: ask, rel are increasing*)
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    21
Goal "Client: UNIV guarantees[funPair rel ask] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    22
\             Increasing ask Int Increasing rel";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    23
by (safe_tac (claset() addSIs [guaranteesI,increasing_imp_Increasing]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    24
by (auto_tac
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    25
    (claset(),
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    26
     simpset() addsimps [impOfSubs preserves_subset_increasing,
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    27
			 Join_increasing]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    28
by (auto_tac (claset(), simpset() addsimps [increasing_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    29
by (ALLGOALS constrains_tac);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    30
by Auto_tac;
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    31
qed "increasing_ask_rel";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    32
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
    33
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
*)
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    41
Goal "G : preserves (funPair ask tok)  \
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})";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    45
by (rtac (invariantI RS stable_Join_Always2) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    46
by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    47
		       addSIs [stable_Int]) 3);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    48
by (constrains_tac 2);
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
    49
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
    50
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    51
qed "ask_bounded_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    52
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
    53
(*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
    54
  unfortunately tok must be declared local.*)
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    55
Goal "Client: UNIV guarantees[funPair ask tok] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    56
\             Always {s. ALL elt : set (ask s). elt <= NbT}";
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}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    78
by (rtac AlwaysI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    79
by (rtac Join_Stable_rel_le_giv 2);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    80
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    81
qed "Join_Always_rel_le_giv";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    82
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    83
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
    84
by (res_inst_tac [("act", "rel_act")] transientI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    85
by (auto_tac (claset(),
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    86
	      simpset() addsimps [Domain_def, Client_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    87
by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    88
			       strict_prefix_length_less]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    89
by (auto_tac (claset(), 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    90
	      simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    91
by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    92
qed "transient_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    93
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    94
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    95
Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    96
\ ==> 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
    97
\                     LeadsTo {s. k < rel s & rel s <= giv s & \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    98
\                                 h <= giv s & h pfixGe ask s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
    99
by (rtac single_LeadsTo_I 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   100
by (ftac (increasing_ask_rel RS guaranteesD) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   101
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   102
by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   103
	  leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   104
by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   105
by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   106
by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   107
by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   108
by (etac Join_Stable_rel_le_giv 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   109
by (Blast_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   110
by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   111
			       order_trans, prefix_imp_pfixGe, 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   112
			       pfixGe_trans]) 2);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   113
by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   114
qed "induct_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   115
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   116
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   117
Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   118
\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   119
\                     LeadsTo {s. h <= rel s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   120
by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   121
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   122
by (rtac single_LeadsTo_I 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   123
by (rtac (induct_lemma RS LeadsTo_weaken) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   124
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   125
by (blast_tac (claset() addIs [order_less_le RS iffD2]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   126
			addDs [common_prefix_linear]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   127
by (REPEAT (dtac strict_prefix_length_less 1));
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   128
by (arith_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   129
qed "rel_progress_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   130
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   131
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   132
Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   133
\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   134
\                     LeadsTo {s. h <= rel s}";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   135
by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   136
by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   137
    LeadsTo_Un RS LeadsTo_weaken_L) 3);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   138
by Auto_tac;
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   139
by (blast_tac (claset() addIs [order_less_le RS iffD2]
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   140
			addDs [common_prefix_linear]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   141
qed "client_progress_lemma";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   142
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   143
(*Progress property: all tokens that are given will be released*)
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   144
Goal "Client : \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   145
\      Increasing giv  guarantees[funPair rel ask]  \
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   146
\      (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
   147
by (rtac guaranteesI 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   148
by (Clarify_tac 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   149
by (blast_tac (claset() addIs [client_progress_lemma]) 1);
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   150
qed "client_progress";
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   151
8251
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   152
Goal "Client : preserves extra";
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;
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   157
qed "client_preserves_extra";
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   158
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   159
Goal "bij client_map";
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   160
by (auto_tac (claset() addSWrapper record_split_wrapper, 
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   161
	      simpset() addsimps [client_map_def, non_extra_def, bij_def, 
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   162
				  inj_on_def, surj_def]));
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   163
by (res_inst_tac 
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   164
    [("x", "(|giv=?a, ask=?b, rel=?c, tok=?d, extra=?e|)")] exI 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   165
by (Force_tac 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   166
qed "bij_client_map";
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   167
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   168
Goal "rename client_map Client : preserves snd";
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   169
by (asm_simp_tac (simpset() addsimps [bij_client_map RS rename_preserves]) 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   170
by (asm_simp_tac (simpset() addsimps [client_map_def]) 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   171
by (rtac client_preserves_extra 1);
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   172
qed "client_preserves_extra";
9be357df93d4 New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents: 8216
diff changeset
   173
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   174
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   175
(** Obsolete lemmas from first version of the Client **)
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   176
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   177
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
   178
by (constrains_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   179
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   180
qed "stable_size_rel_le_giv";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5758
diff changeset
   181
8216
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   182
(*clients return the right number of tokens*)
e4b3192dfefa updated the Client example
paulson
parents: 8055
diff changeset
   183
Goal "Client : Increasing giv  guarantees[rel]  Always {s. rel s <= giv s}";
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   184
by (rtac guaranteesI 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   185
by (rtac AlwaysI 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5636
diff changeset
   186
by (Force_tac 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   187
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
   188
			       stable_rel_le_giv]) 1);
5636
dd8f30780fa9 Addition of HOL/UNITY/Client
paulson
parents:
diff changeset
   189
qed "ok_guar_rel_prefix_giv";