src/HOL/UNITY/Comp/Client.ML
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 (*  Title:      HOL/UNITY/Client
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Distributed Resource Management System: the Client
     7 *)
     8 
     9 Addsimps [Client_def RS def_prg_Init, 
    10           Client_def RS def_prg_AllowedActs];
    11 Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    12 
    13 Goal "(Client ok G) = \
    14 \     (G : preserves rel & G : preserves ask & G : preserves tok &\
    15 \      Client : Allowed G)";
    16 by (auto_tac (claset(), 
    17     simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
    18 qed "Client_ok_iff";
    19 AddIffs [Client_ok_iff];
    20 
    21 
    22 (*Safety property 1: ask, rel are increasing*)
    23 Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
    24 by (auto_tac
    25     (claset() addSIs [increasing_imp_Increasing],
    26      simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
    27 by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def]));
    28 by (ALLGOALS constrains_tac);
    29 by Auto_tac;
    30 qed "increasing_ask_rel";
    31 
    32 Addsimps [nth_append, append_one_prefix];
    33 
    34 
    35 (*Safety property 2: the client never requests too many tokens.
    36       With no Substitution Axiom, we must prove the two invariants 
    37   simultaneously.
    38 *)
    39 Goal "Client ok G  \
    40 \     ==> Client Join G :  \
    41 \             Always ({s. tok s <= NbT}  Int  \
    42 \                     {s. ALL elt : set (ask s). elt <= NbT})";
    43 by Auto_tac;  
    44 by (rtac (invariantI RS stable_Join_Always2) 1);
    45 by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
    46 		       addSIs [stable_Int]) 3);
    47 by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2);
    48 by (constrains_tac 2);
    49 by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
    50 by Auto_tac;
    51 qed "ask_bounded_lemma";
    52 
    53 (*export version, with no mention of tok in the postcondition, but
    54   unfortunately tok must be declared local.*)
    55 Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
    56 by (rtac guaranteesI 1);
    57 by (etac (ask_bounded_lemma RS Always_weaken) 1);
    58 by (rtac Int_lower2 1);
    59 qed "ask_bounded";
    60 
    61 
    62 (*** Towards proving the liveness property ***)
    63 
    64 Goal "Client: stable {s. rel s <= giv s}";
    65 by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1); 
    66 by (constrains_tac 1);
    67 by Auto_tac;
    68 qed "stable_rel_le_giv";
    69 
    70 Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
    71 \     ==> Client Join G : Stable {s. rel s <= giv s}";
    72 by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
    73 by Auto_tac;
    74 qed "Join_Stable_rel_le_giv";
    75 
    76 Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
    77 \     ==> Client Join G : Always {s. rel s <= giv s}";
    78 by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
    79 qed "Join_Always_rel_le_giv";
    80 
    81 Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
    82 by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
    83 by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
    84 by (auto_tac (claset(),
    85 	      simpset() addsimps [Domain_def, Client_def]));
    86 by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
    87 			       strict_prefix_length_less]) 1);
    88 by (auto_tac (claset(), 
    89 	      simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
    90 by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
    91 qed "transient_lemma";
    92 
    93 
    94 Goal "[| Client Join G : Increasing giv;  Client ok G |] \
    95 \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
    96 \                     LeadsTo {s. k < rel s & rel s <= giv s & \
    97 \                                 h <= giv s & h pfixGe ask s}";
    98 by (rtac single_LeadsTo_I 1);
    99 by (ftac (increasing_ask_rel RS guaranteesD) 1);
   100 by Auto_tac;
   101 by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
   102 	  leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
   103 by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
   104 by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
   105 by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
   106 by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
   107 by (etac Join_Stable_rel_le_giv 1);
   108 by (Blast_tac 1);
   109 by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, 
   110 			       order_trans, prefix_imp_pfixGe, 
   111 			       pfixGe_trans]) 2);
   112 by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
   113 qed "induct_lemma";
   114 
   115 
   116 Goal "[| Client Join G : Increasing giv;  Client ok G |] \
   117 \ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
   118 \                     LeadsTo {s. h <= rel s}";
   119 by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
   120 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
   121 by (rtac single_LeadsTo_I 1);
   122 by (rtac (induct_lemma RS LeadsTo_weaken) 1);
   123 by Auto_tac;
   124 by (blast_tac (claset() addIs [order_less_le RS iffD2]
   125 			addDs [common_prefix_linear]) 1);
   126 by (REPEAT (dtac strict_prefix_length_less 1));
   127 by (arith_tac 1);
   128 qed "rel_progress_lemma";
   129 
   130 
   131 Goal "[| Client Join G : Increasing giv;  Client ok G |] \
   132 \ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
   133 \                     LeadsTo {s. h <= rel s}";
   134 by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
   135 by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
   136     LeadsTo_Un RS LeadsTo_weaken_L) 3);
   137 by Auto_tac;
   138 by (blast_tac (claset() addIs [order_less_le RS iffD2]
   139 			addDs [common_prefix_linear]) 1);
   140 qed "client_progress_lemma";
   141 
   142 (*Progress property: all tokens that are given will be released*)
   143 Goal "Client : \
   144 \      Increasing giv  guarantees  \
   145 \      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
   146 by (rtac guaranteesI 1);
   147 by (Clarify_tac 1);
   148 by (blast_tac (claset() addIs [client_progress_lemma]) 1);
   149 qed "client_progress";
   150 
   151 (*This shows that the Client won't alter other variables in any state
   152   that it is combined with*)
   153 Goal "Client : preserves dummy";
   154 by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1);
   155 by (Clarify_tac 1); 
   156 by (constrains_tac 1);
   157 by Auto_tac;
   158 qed "client_preserves_dummy";
   159 
   160 
   161 (** Obsolete lemmas from first version of the Client **)
   162 
   163 Goal "Client: stable {s. size (rel s) <= size (giv s)}";
   164 by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
   165 by (constrains_tac 1);
   166 by Auto_tac;
   167 qed "stable_size_rel_le_giv";
   168 
   169 (*clients return the right number of tokens*)
   170 Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
   171 by (rtac guaranteesI 1);
   172 by (rtac AlwaysI 1);
   173 by (Force_tac 1);
   174 by (blast_tac (claset() addIs [Increasing_preserves_Stable, 
   175 			       stable_rel_le_giv]) 1);
   176 qed "ok_guar_rel_prefix_giv";