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