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