src/ZF/UNITY/ClientImpl.thy
author wenzelm
Sat Oct 10 22:02:23 2015 +0200 (2015-10-10)
changeset 61392 331be2820f90
parent 58860 fee7cfa69c50
permissions -rw-r--r--
tuned syntax -- more symbols;
     1 (*  Title:      ZF/UNITY/ClientImpl.thy
     2     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3     Copyright   2002  University of Cambridge
     4 
     5 Distributed Resource Management System:  Client Implementation.
     6 *)
     7 
     8 theory ClientImpl imports AllocBase Guar begin
     9 
    10 abbreviation "ask == Var(Nil)" (* input history:  tokens requested *)
    11 abbreviation "giv == Var([0])" (* output history: tokens granted *)
    12 abbreviation "rel == Var([1])" (* input history: tokens released *)
    13 abbreviation "tok == Var([2])" (* the number of available tokens *)
    14 
    15 axiomatization where
    16   type_assumes:
    17   "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
    18    type_of(rel) = list(tokbag) & type_of(tok) = nat" and
    19   default_val_assumes:
    20   "default_val(ask) = Nil & default_val(giv) = Nil &
    21    default_val(rel) = Nil & default_val(tok) = 0"
    22 
    23 
    24 (*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
    25 
    26 definition
    27  (** Release some client_tokens **)
    28     "client_rel_act ==
    29      {<s,t> \<in> state*state.
    30       \<exists>nrel \<in> nat. nrel = length(s`rel) &
    31                    t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
    32                    nrel < length(s`giv) &
    33                    nth(nrel, s`ask) \<le> nth(nrel, s`giv)}"
    34 
    35   (** Choose a new token requirement **)
    36   (** Including t=s suppresses fairness, allowing the non-trivial part
    37       of the action to be ignored **)
    38 definition
    39   "client_tok_act == {<s,t> \<in> state*state. t=s |
    40                      t = s(tok:=succ(s`tok mod NbT))}"
    41 
    42 definition
    43   "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
    44 
    45 definition
    46   "client_prog ==
    47    mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil &
    48                        s`ask = Nil & s`rel = Nil},
    49                     {client_rel_act, client_tok_act, client_ask_act},
    50                    \<Union>G \<in> preserves(lift(rel)) Int
    51                          preserves(lift(ask)) Int
    52                          preserves(lift(tok)).  Acts(G))"
    53 
    54 
    55 declare type_assumes [simp] default_val_assumes [simp]
    56 (* This part should be automated *)
    57 
    58 lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
    59 apply (unfold state_def)
    60 apply (drule_tac a = ask in apply_type, auto)
    61 done
    62 
    63 lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)"
    64 apply (unfold state_def)
    65 apply (drule_tac a = giv in apply_type, auto)
    66 done
    67 
    68 lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)"
    69 apply (unfold state_def)
    70 apply (drule_tac a = rel in apply_type, auto)
    71 done
    72 
    73 lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat"
    74 apply (unfold state_def)
    75 apply (drule_tac a = tok in apply_type, auto)
    76 done
    77 
    78 (** The Client Program **)
    79 
    80 lemma client_type [simp,TC]: "client_prog \<in> program"
    81 apply (unfold client_prog_def)
    82 apply (simp (no_asm))
    83 done
    84 
    85 declare client_prog_def [THEN def_prg_Init, simp]
    86 declare client_prog_def [THEN def_prg_AllowedActs, simp]
    87 declare client_prog_def [program]
    88 
    89 declare  client_rel_act_def [THEN def_act_simp, simp]
    90 declare  client_tok_act_def [THEN def_act_simp, simp]
    91 declare  client_ask_act_def [THEN def_act_simp, simp]
    92 
    93 lemma client_prog_ok_iff:
    94   "\<forall>G \<in> program. (client_prog ok G) \<longleftrightarrow>
    95    (G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) &
    96     G \<in> preserves(lift(tok)) &  client_prog \<in> Allowed(G))"
    97 by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed])
    98 
    99 lemma client_prog_preserves:
   100     "client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))"
   101 apply (rule Inter_var_DiffI, force)
   102 apply (rule ballI)
   103 apply (rule preservesI, safety, auto)
   104 done
   105 
   106 
   107 lemma preserves_lift_imp_stable:
   108      "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
   109 apply (drule preserves_imp_stable)
   110 apply (simp add: lift_def)
   111 done
   112 
   113 lemma preserves_imp_prefix:
   114      "G \<in> preserves(lift(ff))
   115       ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
   116 by (erule preserves_lift_imp_stable)
   117 
   118 (*Safety property 1 \<in> ask, rel are increasing: (24) *)
   119 lemma client_prog_Increasing_ask_rel:
   120 "client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))"
   121 apply (unfold guar_def)
   122 apply (auto intro!: increasing_imp_Increasing
   123             simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
   124 apply (safety, force, force)+
   125 done
   126 
   127 declare nth_append [simp] append_one_prefix [simp]
   128 
   129 lemma NbT_pos2: "0<NbT"
   130 apply (cut_tac NbT_pos)
   131 apply (rule Ord_0_lt, auto)
   132 done
   133 
   134 (*Safety property 2 \<in> the client never requests too many tokens.
   135 With no Substitution Axiom, we must prove the two invariants simultaneously. *)
   136 
   137 lemma ask_Bounded_lemma:
   138 "[| client_prog ok G; G \<in> program |]
   139       ==> client_prog \<squnion> G \<in>
   140               Always({s \<in> state. s`tok \<le> NbT}  \<inter>
   141                       {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
   142 apply (rotate_tac -1)
   143 apply (auto simp add: client_prog_ok_iff)
   144 apply (rule invariantI [THEN stable_Join_Always2], force)
   145  prefer 2
   146  apply (fast intro: stable_Int preserves_lift_imp_stable, safety)
   147 apply (auto dest: ActsD)
   148 apply (cut_tac NbT_pos)
   149 apply (rule NbT_pos2 [THEN mod_less_divisor])
   150 apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append)
   151 done
   152 
   153 (* Export version, with no mention of tok in the postcondition, but
   154   unfortunately tok must be declared local.*)
   155 lemma client_prog_ask_Bounded:
   156     "client_prog \<in> program guarantees
   157                    Always({s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
   158 apply (rule guaranteesI)
   159 apply (erule ask_Bounded_lemma [THEN Always_weaken], auto)
   160 done
   161 
   162 (*** Towards proving the liveness property ***)
   163 
   164 lemma client_prog_stable_rel_le_giv:
   165     "client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
   166 by (safety, auto)
   167 
   168 lemma client_prog_Join_Stable_rel_le_giv:
   169 "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
   170     ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
   171 apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
   172 apply (auto simp add: lift_def)
   173 done
   174 
   175 lemma client_prog_Join_Always_rel_le_giv:
   176      "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
   177     ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
   178 by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
   179 
   180 lemma def_act_eq:
   181      "A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}"
   182 by auto
   183 
   184 lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state"
   185 by auto
   186 
   187 lemma transient_lemma:
   188 "client_prog \<in>
   189   transient({s \<in> state. s`rel = k & <k, h> \<in> strict_prefix(nat)
   190    & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask})"
   191 apply (rule_tac act = client_rel_act in transientI)
   192 apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts])
   193 apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset])
   194 apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def)
   195 apply (rule ReplaceI)
   196 apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI)
   197 apply (auto intro!: state_update_type app_type length_type nth_type, auto)
   198 apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
   199 apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
   200 apply (simp (no_asm_use) add: gen_prefix_iff_nth)
   201 apply (subgoal_tac "h \<in> list(nat)")
   202  apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1])
   203 apply (auto simp add: prefix_def Ge_def)
   204 apply (drule strict_prefix_length_lt)
   205 apply (drule_tac x = "length (x`rel) " in spec)
   206 apply auto
   207 apply (simp (no_asm_use) add: gen_prefix_iff_nth)
   208 apply (auto simp add: id_def lam_def)
   209 done
   210 
   211 lemma strict_prefix_is_prefix:
   212     "<xs, ys> \<in> strict_prefix(A) \<longleftrightarrow>  <xs, ys> \<in> prefix(A) & xs\<noteq>ys"
   213 apply (unfold strict_prefix_def id_def lam_def)
   214 apply (auto dest: prefix_type [THEN subsetD])
   215 done
   216 
   217 lemma induct_lemma:
   218 "[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
   219   ==> client_prog \<squnion> G \<in>
   220   {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)
   221    & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
   222         \<longmapsto>w {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)
   223                           & <s`rel, s`giv> \<in> prefix(nat) &
   224                                   <h, s`giv> \<in> prefix(nat) &
   225                 h pfixGe s`ask}"
   226 apply (rule single_LeadsTo_I)
   227  prefer 2 apply simp
   228 apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD])
   229 apply (rotate_tac [3] 2)
   230 apply (auto simp add: client_prog_ok_iff)
   231 apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
   232 apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
   233 apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable)
   234 apply (simp (no_asm_simp))
   235 apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable)
   236 apply (simp (no_asm_simp))
   237 apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable)
   238 apply (simp (no_asm_simp))
   239 apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all)
   240  prefer 2
   241  apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans)
   242 apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1]
   243                    prefix_trans)
   244 done
   245 
   246 lemma rel_progress_lemma:
   247 "[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
   248   ==> client_prog \<squnion> G  \<in>
   249      {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)
   250            & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
   251                       \<longmapsto>w {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
   252 apply (rule_tac f = "\<lambda>x \<in> state. length(h) #- length(x`rel)"
   253        in LessThan_induct)
   254 apply (auto simp add: vimage_def)
   255  prefer 2 apply (force simp add: lam_def)
   256 apply (rule single_LeadsTo_I)
   257  prefer 2 apply simp
   258 apply (subgoal_tac "h \<in> list(nat)")
   259  prefer 2 apply (blast dest: prefix_type [THEN subsetD])
   260 apply (rule induct_lemma [THEN LeadsTo_weaken])
   261     apply (simp add: length_type lam_def)
   262 apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
   263             dest: common_prefix_linear  prefix_type [THEN subsetD])
   264 apply (erule swap)
   265 apply (rule imageI)
   266  apply (force dest!: simp add: lam_def)
   267 apply (simp add: length_type lam_def, clarify)
   268 apply (drule strict_prefix_length_lt)+
   269 apply (drule less_imp_succ_add, simp)+
   270 apply clarify
   271 apply simp
   272 apply (erule diff_le_self [THEN ltD])
   273 done
   274 
   275 lemma progress_lemma:
   276 "[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
   277  ==> client_prog \<squnion> G
   278        \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
   279          \<longmapsto>w  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
   280 apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI],
   281        assumption)
   282 apply (force simp add: client_prog_ok_iff)
   283 apply (rule LeadsTo_weaken_L)
   284 apply (rule LeadsTo_Un [OF rel_progress_lemma
   285                            subset_refl [THEN subset_imp_LeadsTo]])
   286 apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
   287             dest: common_prefix_linear prefix_type [THEN subsetD])
   288 done
   289 
   290 (*Progress property: all tokens that are given will be released*)
   291 lemma client_prog_progress:
   292 "client_prog \<in> Incr(lift(giv))  guarantees
   293       (\<Inter>h \<in> list(nat). {s \<in> state. <h, s`giv> \<in> prefix(nat) &
   294               h pfixGe s`ask} \<longmapsto>w {s \<in> state. <h, s`rel> \<in> prefix(nat)})"
   295 apply (rule guaranteesI)
   296 apply (blast intro: progress_lemma, auto)
   297 done
   298 
   299 lemma client_prog_Allowed:
   300      "Allowed(client_prog) =
   301       preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
   302 apply (cut_tac v = "lift (ask)" in preserves_type)
   303 apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
   304                       cons_Int_distrib safety_prop_Acts_iff)
   305 done
   306 
   307 end