src/HOL/UNITY/Comp/Client.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      HOL/UNITY/Client.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 *)
     6 
     7 header{*Distributed Resource Management System: the Client*}
     8 
     9 theory Client imports Rename AllocBase begin
    10 
    11 types
    12   tokbag = nat	   --{*tokbags could be multisets...or any ordered type?*}
    13 
    14 record state =
    15   giv :: "tokbag list" --{*input history: tokens granted*}
    16   ask :: "tokbag list" --{*output history: tokens requested*}
    17   rel :: "tokbag list" --{*output history: tokens released*}
    18   tok :: tokbag	       --{*current token request*}
    19 
    20 record 'a state_d =
    21   state +  
    22   dummy :: 'a          --{*new variables*}
    23 
    24 
    25 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
    26 
    27 constdefs
    28   
    29   (** Release some tokens **)
    30   
    31   rel_act :: "('a state_d * 'a state_d) set"
    32     "rel_act == {(s,s').
    33 		  \<exists>nrel. nrel = size (rel s) &
    34 		         s' = s (| rel := rel s @ [giv s!nrel] |) &
    35 		         nrel < size (giv s) &
    36 		         ask s!nrel \<le> giv s!nrel}"
    37 
    38   (** Choose a new token requirement **)
    39 
    40   (** Including s'=s suppresses fairness, allowing the non-trivial part
    41       of the action to be ignored **)
    42 
    43   tok_act :: "('a state_d * 'a state_d) set"
    44      "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
    45   
    46   ask_act :: "('a state_d * 'a state_d) set"
    47     "ask_act == {(s,s'). s'=s |
    48 		         (s' = s (|ask := ask s @ [tok s]|))}"
    49 
    50   Client :: "'a state_d program"
    51     "Client ==
    52        mk_total_program
    53             ({s. tok s \<in> atMost NbT &
    54 		 giv s = [] & ask s = [] & rel s = []},
    55 	     {rel_act, tok_act, ask_act},
    56 	     \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
    57 		   Acts G)"
    58 
    59   (*Maybe want a special theory section to declare such maps*)
    60   non_dummy :: "'a state_d => state"
    61     "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
    62 
    63   (*Renaming map to put a Client into the standard form*)
    64   client_map :: "'a state_d => state*'a"
    65     "client_map == funPair non_dummy dummy"
    66 
    67 
    68 declare Client_def [THEN def_prg_Init, simp]
    69 declare Client_def [THEN def_prg_AllowedActs, simp]
    70 declare rel_act_def [THEN def_act_simp, simp]
    71 declare tok_act_def [THEN def_act_simp, simp]
    72 declare ask_act_def [THEN def_act_simp, simp]
    73 
    74 lemma Client_ok_iff [iff]:
    75      "(Client ok G) =  
    76       (G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok & 
    77        Client \<in> Allowed G)"
    78 by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
    79 
    80 
    81 text{*Safety property 1: ask, rel are increasing*}
    82 lemma increasing_ask_rel:
    83      "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
    84 apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
    85 apply (auto simp add: Client_def increasing_def)
    86 apply (safety, auto)+
    87 done
    88 
    89 declare nth_append [simp] append_one_prefix [simp]
    90 
    91 
    92 text{*Safety property 2: the client never requests too many tokens.
    93       With no Substitution Axiom, we must prove the two invariants 
    94       simultaneously. *}
    95 lemma ask_bounded_lemma:
    96      "Client ok G   
    97       ==> Client Join G \<in>   
    98               Always ({s. tok s \<le> NbT}  Int   
    99                       {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
   100 apply auto
   101 apply (rule invariantI [THEN stable_Join_Always2], force) 
   102  prefer 2
   103  apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int) 
   104 apply (simp add: Client_def, safety)
   105 apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
   106 done
   107 
   108 text{*export version, with no mention of tok in the postcondition, but
   109   unfortunately tok must be declared local.*}
   110 lemma ask_bounded:
   111      "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
   112 apply (rule guaranteesI)
   113 apply (erule ask_bounded_lemma [THEN Always_weaken])
   114 apply (rule Int_lower2)
   115 done
   116 
   117 
   118 text{*** Towards proving the liveness property ***}
   119 
   120 lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
   121 by (simp add: Client_def, safety, auto)
   122 
   123 lemma Join_Stable_rel_le_giv:
   124      "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
   125       ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
   126 by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
   127 
   128 lemma Join_Always_rel_le_giv:
   129      "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
   130       ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
   131 by (force intro: AlwaysI Join_Stable_rel_le_giv)
   132 
   133 lemma transient_lemma:
   134      "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
   135 apply (simp add: Client_def mk_total_program_def)
   136 apply (rule_tac act = rel_act in totalize_transientI)
   137   apply (auto simp add: Domain_def Client_def)
   138  apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
   139 apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
   140 apply (blast intro: strict_prefix_length_less)
   141 done
   142 
   143 
   144 lemma induct_lemma:
   145      "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   146   ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
   147                       LeadsTo {s. k < rel s & rel s \<le> giv s &  
   148                                   h \<le> giv s & h pfixGe ask s}"
   149 apply (rule single_LeadsTo_I)
   150 apply (frule increasing_ask_rel [THEN guaranteesD], auto)
   151 apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
   152   apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
   153      apply (erule_tac f = giv and x = "giv s" in IncreasingD)
   154     apply (erule_tac f = ask and x = "ask s" in IncreasingD)
   155    apply (erule_tac f = rel and x = "rel s" in IncreasingD)
   156   apply (erule Join_Stable_rel_le_giv, blast)
   157  apply (blast intro: order_less_imp_le order_trans)
   158 apply (blast intro: sym order_less_le [THEN iffD2] order_trans
   159                     prefix_imp_pfixGe pfixGe_trans)
   160 done
   161 
   162 
   163 lemma rel_progress_lemma:
   164      "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   165   ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
   166                       LeadsTo {s. h \<le> rel s}"
   167 apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
   168 apply (auto simp add: vimage_def)
   169 apply (rule single_LeadsTo_I)
   170 apply (rule induct_lemma [THEN LeadsTo_weaken], auto)
   171  apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
   172 apply (drule strict_prefix_length_less)+
   173 apply arith
   174 done
   175 
   176 
   177 lemma client_progress_lemma:
   178      "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   179       ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
   180                           LeadsTo {s. h \<le> rel s}"
   181 apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
   182 apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
   183   apply (blast intro: rel_progress_lemma) 
   184  apply (rule subset_refl [THEN subset_imp_LeadsTo])
   185 apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
   186 done
   187 
   188 text{*Progress property: all tokens that are given will be released*}
   189 lemma client_progress:
   190      "Client \<in>  
   191        Increasing giv  guarantees   
   192        (INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})"
   193 apply (rule guaranteesI, clarify)
   194 apply (blast intro: client_progress_lemma)
   195 done
   196 
   197 text{*This shows that the Client won't alter other variables in any state
   198   that it is combined with*}
   199 lemma client_preserves_dummy: "Client \<in> preserves dummy"
   200 by (simp add: Client_def preserves_def, clarify, safety, auto)
   201 
   202 
   203 text{** Obsolete lemmas from first version of the Client **}
   204 
   205 lemma stable_size_rel_le_giv:
   206      "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
   207 by (simp add: Client_def, safety, auto)
   208 
   209 text{*clients return the right number of tokens*}
   210 lemma ok_guar_rel_prefix_giv:
   211      "Client \<in> Increasing giv  guarantees  Always {s. rel s \<le> giv s}"
   212 apply (rule guaranteesI)
   213 apply (rule AlwaysI, force)
   214 apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv)
   215 done
   216 
   217 
   218 end