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