converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
authorpaulson
Thu Jul 03 18:07:50 2003 +0200 (2003-07-03)
changeset 140897b34f58b1b81
parent 14088 61bd46feb919
child 14090 f24b2818c1e7
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
src/HOL/IsaMakefile
src/HOL/UNITY/Comp/AllocImpl.ML
src/HOL/UNITY/Comp/AllocImpl.thy
src/HOL/UNITY/Comp/Client.ML
src/HOL/UNITY/Comp/Client.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Jul 03 12:56:48 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jul 03 18:07:50 2003 +0200
     1.3 @@ -389,8 +389,7 @@
     1.4    UNITY/Simple/Network.thy\
     1.5    UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
     1.6    UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
     1.7 -  UNITY/Comp/AllocBase.thy \
     1.8 -  UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
     1.9 +  UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
    1.10    UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
    1.11    UNITY/Comp/PriorityAux.thy \
    1.12    UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
     2.1 --- a/src/HOL/UNITY/Comp/AllocImpl.ML	Thu Jul 03 12:56:48 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,191 +0,0 @@
     2.4 -(*  Title:      HOL/UNITY/AllocImpl
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   2000  University of Cambridge
     2.8 -
     2.9 -Implementation of a multiple-client allocator from a single-client allocator
    2.10 -*)
    2.11 -
    2.12 -AddIs [impOfSubs subset_preserves_o];
    2.13 -Addsimps [funPair_o_distrib];
    2.14 -Addsimps [Always_INT_distrib];
    2.15 -Delsimps [o_apply];
    2.16 -
    2.17 -Open_locale "Merge";
    2.18 -
    2.19 -val Merge = thm "Merge_spec";
    2.20 -
    2.21 -Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
    2.22 -by (cut_facts_tac [Merge] 1);
    2.23 -by (auto_tac (claset(), 
    2.24 -              simpset() addsimps [merge_spec_def, merge_allowed_acts_def, 
    2.25 -                                  Allowed_def, safety_prop_Acts_iff]));  
    2.26 -qed "Merge_Allowed";
    2.27 -
    2.28 -Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
    2.29 -\                    M : Allowed G)";
    2.30 -by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));  
    2.31 -qed "M_ok_iff";
    2.32 -AddIffs [M_ok_iff];
    2.33 -
    2.34 -Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
    2.35 -\     ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
    2.36 -by (cut_facts_tac [Merge] 1);
    2.37 -by (force_tac (claset() addDs [guaranteesD], 
    2.38 -               simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); 
    2.39 -qed "Merge_Always_Out_eq_iOut";
    2.40 -
    2.41 -Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
    2.42 -\     ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
    2.43 -by (cut_facts_tac [Merge] 1);
    2.44 -by (force_tac (claset() addDs [guaranteesD], 
    2.45 -               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
    2.46 -qed "Merge_Bounded";
    2.47 -
    2.48 -Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
    2.49 -\ ==> M Join G : Always \
    2.50 -\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
    2.51 -\                                 {k. k < length (iOut s) & iOut s ! k = i})) = \
    2.52 -\             (bag_of o merge.Out) s}";
    2.53 -by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
    2.54 -	   UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
    2.55 -     by Auto_tac; 
    2.56 -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
    2.57 -  by (Simp_tac 1);
    2.58 - by (Blast_tac 1); 
    2.59 -by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); 
    2.60 -by (subgoal_tac
    2.61 -    "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
    2.62 -\    lessThan (length (iOut x))" 1);
    2.63 - by (Blast_tac 2); 
    2.64 -by (asm_simp_tac (simpset() addsimps [o_def]) 1); 
    2.65 -qed "Merge_Bag_Follows_lemma";
    2.66 -
    2.67 -Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
    2.68 -\         guarantees  \
    2.69 -\            (bag_of o merge.Out) Fols \
    2.70 -\            (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
    2.71 -by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
    2.72 -by Auto_tac;  
    2.73 -by (rtac Follows_setsum 1);
    2.74 -by (cut_facts_tac [Merge] 1);
    2.75 -by (auto_tac (claset(), 
    2.76 -              simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
    2.77 -by (dtac guaranteesD 1); 
    2.78 -by (best_tac
    2.79 -    (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
    2.80 -by Auto_tac;  
    2.81 -qed "Merge_Bag_Follows";
    2.82 -
    2.83 -Close_locale "Merge";
    2.84 -
    2.85 -
    2.86 -(** Distributor **)
    2.87 -
    2.88 -Open_locale "Distrib";
    2.89 -
    2.90 -val Distrib = thm "Distrib_spec";
    2.91 -  
    2.92 -
    2.93 -Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
    2.94 -\         Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
    2.95 -\         guarantees \
    2.96 -\         (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
    2.97 -by (cut_facts_tac [Distrib] 1);
    2.98 -by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
    2.99 -by (Clarify_tac 1); 
   2.100 -by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
   2.101 -                        addDs [guaranteesD]) 1);
   2.102 -qed "Distr_Increasing_Out";
   2.103 -
   2.104 -Goal "[| G : preserves distr.Out; \
   2.105 -\        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
   2.106 -\ ==> D Join G : Always \
   2.107 -\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
   2.108 -\                                 {k. k < length (iIn s) & iIn s ! k = i})) = \
   2.109 -\             bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
   2.110 -by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
   2.111 -by Auto_tac; 
   2.112 -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
   2.113 -  by (Simp_tac 1);
   2.114 - by (Blast_tac 1); 
   2.115 -by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); 
   2.116 -by (subgoal_tac
   2.117 -    "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
   2.118 -\    lessThan (length (iIn x))" 1);
   2.119 - by (Blast_tac 2); 
   2.120 -by (Asm_simp_tac 1); 
   2.121 -qed "Distr_Bag_Follows_lemma";
   2.122 -
   2.123 -Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
   2.124 -by (cut_facts_tac [Distrib] 1);
   2.125 -by (auto_tac (claset(), 
   2.126 -     simpset() addsimps [distr_spec_def, distr_allowed_acts_def, 
   2.127 -                         Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
   2.128 -qed "D_ok_iff";
   2.129 -AddIffs [D_ok_iff];
   2.130 -
   2.131 -Goal
   2.132 - "D : Increasing distr.In Int Increasing distr.iIn Int \
   2.133 -\     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
   2.134 -\     guarantees  \
   2.135 -\      (INT i : lessThan Nclients. \
   2.136 -\       (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
   2.137 -\       Fols \
   2.138 -\       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
   2.139 -by (rtac guaranteesI 1);
   2.140 -by (Clarify_tac 1); 
   2.141 -by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
   2.142 -by Auto_tac;  
   2.143 -by (rtac Follows_setsum 1);
   2.144 -by (cut_facts_tac [Distrib] 1);
   2.145 -by (auto_tac (claset(), 
   2.146 -              simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
   2.147 -by (dtac guaranteesD 1); 
   2.148 -by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
   2.149 -by Auto_tac;  
   2.150 -qed "Distr_Bag_Follows";
   2.151 -
   2.152 -Close_locale "Distrib";
   2.153 -
   2.154 -
   2.155 -Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s})  \
   2.156 -\     <= {s. (\\<Sum>x: lessThan n. f x) <= (\\<Sum>x: lessThan n. g x s)}";
   2.157 -by (induct_tac "n" 1);
   2.158 -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
   2.159 -qed "alloc_refinement_lemma";
   2.160 -
   2.161 -Goal
   2.162 -"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int  \
   2.163 -\                            Increasing (sub i o allocRel))     \
   2.164 -\ Int   \
   2.165 -\ Always {s. ALL i. i<Nclients -->      \
   2.166 -\             (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}       \
   2.167 -\ Int   \
   2.168 -\ (INT i : lessThan Nclients.   \
   2.169 -\  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}  \
   2.170 -\          LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})        \
   2.171 -\ <=     \
   2.172 -\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int  \
   2.173 -\                            Increasing (sub i o allocRel))     \
   2.174 -\ Int   \
   2.175 -\ Always {s. ALL i. i<Nclients -->      \
   2.176 -\             (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}       \
   2.177 -\ Int   \
   2.178 -\ (INT hf. (INT i : lessThan Nclients.  \
   2.179 -\        {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
   2.180 -\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <=         \
   2.181 -\   (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
   2.182 -by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));  
   2.183 -by (rename_tac "F hf" 1);
   2.184 -by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
   2.185 -          MRS LeadsTo_weaken_R) 1);
   2.186 -  by (Blast_tac 1); 
   2.187 - by (Blast_tac 1); 
   2.188 -by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1);
   2.189 - by (blast_tac
   2.190 -     (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2);
   2.191 -by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1);
   2.192 -qed "alloc_refinement";
   2.193 -
   2.194 -
     3.1 --- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 03 12:56:48 2003 +0200
     3.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 03 18:07:50 2003 +0200
     3.3 @@ -2,42 +2,42 @@
     3.4      ID:         $Id$
     3.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.6      Copyright   1998  University of Cambridge
     3.7 -
     3.8 -Implementation of a multiple-client allocator from a single-client allocator
     3.9  *)
    3.10  
    3.11 -AllocImpl = AllocBase + Follows + PPROD + 
    3.12 +header{*Implementation of a multiple-client allocator from a single-client allocator*}
    3.13 +
    3.14 +theory AllocImpl = AllocBase + Follows + PPROD:
    3.15  
    3.16  
    3.17  (** State definitions.  OUTPUT variables are locals **)
    3.18  
    3.19  (*Type variable 'b is the type of items being merged*)
    3.20  record 'b merge =
    3.21 -  In   :: nat => 'b list   (*merge's INPUT histories: streams to merge*)
    3.22 -  Out  :: 'b list          (*merge's OUTPUT history: merged items*)
    3.23 -  iOut :: nat list         (*merge's OUTPUT history: origins of merged items*)
    3.24 +  In   :: "nat => 'b list"   (*merge's INPUT histories: streams to merge*)
    3.25 +  Out  :: "'b list"          (*merge's OUTPUT history: merged items*)
    3.26 +  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)
    3.27  
    3.28  record ('a,'b) merge_d =
    3.29 -  'b merge +
    3.30 +  "'b merge" +
    3.31    dummy :: 'a       (*dummy field for new variables*)
    3.32  
    3.33  constdefs
    3.34 -  non_dummy :: ('a,'b) merge_d => 'b merge
    3.35 +  non_dummy :: "('a,'b) merge_d => 'b merge"
    3.36      "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
    3.37  
    3.38  record 'b distr =
    3.39 -  In  :: 'b list          (*items to distribute*)
    3.40 -  iIn :: nat list         (*destinations of items to distribute*)
    3.41 -  Out :: nat => 'b list   (*distributed items*)
    3.42 +  In  :: "'b list"          (*items to distribute*)
    3.43 +  iIn :: "nat list"         (*destinations of items to distribute*)
    3.44 +  Out :: "nat => 'b list"   (*distributed items*)
    3.45  
    3.46  record ('a,'b) distr_d =
    3.47 -  'b distr +
    3.48 +  "'b distr" +
    3.49    dummy :: 'a       (*dummy field for new variables*)
    3.50  
    3.51  record allocState =
    3.52 -  giv :: nat list   (*OUTPUT history: source of tokens*)
    3.53 -  ask :: nat list   (*INPUT: tokens requested from allocator*)
    3.54 -  rel :: nat list   (*INPUT: tokens released to allocator*)
    3.55 +  giv :: "nat list"   (*OUTPUT history: source of tokens*)
    3.56 +  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
    3.57 +  rel :: "nat list"   (*INPUT: tokens released to allocator*)
    3.58  
    3.59  record 'a allocState_d =
    3.60    allocState +
    3.61 @@ -45,9 +45,9 @@
    3.62  
    3.63  record 'a systemState =
    3.64    allocState +
    3.65 -  mergeRel :: nat merge
    3.66 -  mergeAsk :: nat merge
    3.67 -  distr    :: nat distr
    3.68 +  mergeRel :: "nat merge"
    3.69 +  mergeAsk :: "nat merge"
    3.70 +  distr    :: "nat distr"
    3.71    dummy    :: 'a                  (*dummy field for new variables*)
    3.72  
    3.73  
    3.74 @@ -56,154 +56,152 @@
    3.75  (** Merge specification (the number of inputs is Nclients) ***)
    3.76  
    3.77    (*spec (10)*)
    3.78 -  merge_increasing :: ('a,'b) merge_d program set
    3.79 +  merge_increasing :: "('a,'b) merge_d program set"
    3.80      "merge_increasing ==
    3.81           UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
    3.82  
    3.83    (*spec (11)*)
    3.84 -  merge_eqOut :: ('a,'b) merge_d program set
    3.85 +  merge_eqOut :: "('a,'b) merge_d program set"
    3.86      "merge_eqOut ==
    3.87           UNIV guarantees
    3.88           Always {s. length (merge.Out s) = length (merge.iOut s)}"
    3.89  
    3.90    (*spec (12)*)
    3.91 -  merge_bounded :: ('a,'b) merge_d program set
    3.92 +  merge_bounded :: "('a,'b) merge_d program set"
    3.93      "merge_bounded ==
    3.94           UNIV guarantees
    3.95 -         Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
    3.96 +         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
    3.97  
    3.98    (*spec (13)*)
    3.99 -  merge_follows :: ('a,'b) merge_d program set
   3.100 +  merge_follows :: "('a,'b) merge_d program set"
   3.101      "merge_follows ==
   3.102 -	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
   3.103 +	 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
   3.104  	 guarantees
   3.105 -	 (INT i : lessThan Nclients. 
   3.106 +	 (\<Inter>i \<in> lessThan Nclients. 
   3.107  	  (%s. sublist (merge.Out s) 
   3.108                         {k. k < size(merge.iOut s) & merge.iOut s! k = i})
   3.109  	  Fols (sub i o merge.In))"
   3.110  
   3.111    (*spec: preserves part*)
   3.112 -  merge_preserves :: ('a,'b) merge_d program set
   3.113 +  merge_preserves :: "('a,'b) merge_d program set"
   3.114      "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
   3.115  
   3.116    (*environmental constraints*)
   3.117 -  merge_allowed_acts :: ('a,'b) merge_d program set
   3.118 +  merge_allowed_acts :: "('a,'b) merge_d program set"
   3.119      "merge_allowed_acts ==
   3.120         {F. AllowedActs F =
   3.121  	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
   3.122  
   3.123 -  merge_spec :: ('a,'b) merge_d program set
   3.124 +  merge_spec :: "('a,'b) merge_d program set"
   3.125      "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
   3.126                     merge_follows Int merge_allowed_acts Int merge_preserves"
   3.127  
   3.128  (** Distributor specification (the number of outputs is Nclients) ***)
   3.129  
   3.130    (*spec (14)*)
   3.131 -  distr_follows :: ('a,'b) distr_d program set
   3.132 +  distr_follows :: "('a,'b) distr_d program set"
   3.133      "distr_follows ==
   3.134  	 Increasing distr.In Int Increasing distr.iIn Int
   3.135 -	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
   3.136 +	 Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
   3.137  	 guarantees
   3.138 -	 (INT i : lessThan Nclients. 
   3.139 +	 (\<Inter>i \<in> lessThan Nclients. 
   3.140  	  (sub i o distr.Out) Fols
   3.141  	  (%s. sublist (distr.In s) 
   3.142                         {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
   3.143  
   3.144 -  distr_allowed_acts :: ('a,'b) distr_d program set
   3.145 +  distr_allowed_acts :: "('a,'b) distr_d program set"
   3.146      "distr_allowed_acts ==
   3.147         {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
   3.148  
   3.149 -  distr_spec :: ('a,'b) distr_d program set
   3.150 +  distr_spec :: "('a,'b) distr_d program set"
   3.151      "distr_spec == distr_follows Int distr_allowed_acts"
   3.152  
   3.153  (** Single-client allocator specification (required) ***)
   3.154  
   3.155    (*spec (18)*)
   3.156 -  alloc_increasing :: 'a allocState_d program set
   3.157 +  alloc_increasing :: "'a allocState_d program set"
   3.158      "alloc_increasing == UNIV  guarantees  Increasing giv"
   3.159  
   3.160    (*spec (19)*)
   3.161 -  alloc_safety :: 'a allocState_d program set
   3.162 +  alloc_safety :: "'a allocState_d program set"
   3.163      "alloc_safety ==
   3.164  	 Increasing rel
   3.165           guarantees  Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
   3.166  
   3.167    (*spec (20)*)
   3.168 -  alloc_progress :: 'a allocState_d program set
   3.169 +  alloc_progress :: "'a allocState_d program set"
   3.170      "alloc_progress ==
   3.171  	 Increasing ask Int Increasing rel Int
   3.172 -         Always {s. ALL elt : set (ask s). elt <= NbT}
   3.173 +         Always {s. \<forall>elt \<in> set (ask s). elt <= NbT}
   3.174           Int
   3.175 -         (INT h. {s. h <= giv s & h pfixGe (ask s)}
   3.176 +         (\<Inter>h. {s. h <= giv s & h pfixGe (ask s)}
   3.177  		 LeadsTo
   3.178  	         {s. tokens h <= tokens (rel s)})
   3.179 -         guarantees  (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
   3.180 +         guarantees  (\<Inter>h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
   3.181  
   3.182    (*spec: preserves part*)
   3.183 -  alloc_preserves :: 'a allocState_d program set
   3.184 +  alloc_preserves :: "'a allocState_d program set"
   3.185      "alloc_preserves == preserves rel Int
   3.186                          preserves ask Int
   3.187                          preserves allocState_d.dummy"
   3.188    
   3.189  
   3.190    (*environmental constraints*)
   3.191 -  alloc_allowed_acts :: 'a allocState_d program set
   3.192 +  alloc_allowed_acts :: "'a allocState_d program set"
   3.193      "alloc_allowed_acts ==
   3.194         {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
   3.195  
   3.196 -  alloc_spec :: 'a allocState_d program set
   3.197 +  alloc_spec :: "'a allocState_d program set"
   3.198      "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
   3.199                     alloc_allowed_acts Int alloc_preserves"
   3.200  
   3.201  locale Merge =
   3.202 -  fixes 
   3.203 -    M   :: ('a,'b::order) merge_d program
   3.204 +  fixes M :: "('a,'b::order) merge_d program"
   3.205    assumes
   3.206 -    Merge_spec  "M  : merge_spec"
   3.207 +    Merge_spec:  "M  \<in> merge_spec"
   3.208  
   3.209  locale Distrib =
   3.210 -  fixes 
   3.211 -    D   :: ('a,'b::order) distr_d program
   3.212 +  fixes D :: "('a,'b::order) distr_d program"
   3.213    assumes
   3.214 -    Distrib_spec  "D : distr_spec"
   3.215 +    Distrib_spec:  "D \<in> distr_spec"
   3.216  
   3.217  
   3.218  (****
   3.219 -#  (** Network specification ***)
   3.220 +#  {** Network specification ***}
   3.221  
   3.222 -#    (*spec (9.1)*)
   3.223 -#    network_ask :: 'a systemState program set
   3.224 -#	"network_ask == INT i : lessThan Nclients.
   3.225 +#    {*spec (9.1)*}
   3.226 +#    network_ask :: "'a systemState program set
   3.227 +#	"network_ask == \<Inter>i \<in> lessThan Nclients.
   3.228  #			    Increasing (ask o sub i o client)
   3.229  #			    guarantees[ask]
   3.230  #			    (ask  Fols (ask o sub i o client))"
   3.231  
   3.232 -#    (*spec (9.2)*)
   3.233 -#    network_giv :: 'a systemState program set
   3.234 -#	"network_giv == INT i : lessThan Nclients.
   3.235 +#    {*spec (9.2)*}
   3.236 +#    network_giv :: "'a systemState program set
   3.237 +#	"network_giv == \<Inter>i \<in> lessThan Nclients.
   3.238  #			    Increasing giv 
   3.239  #			    guarantees[giv o sub i o client]
   3.240 -#			    ((giv o sub i o client) Fols giv )"
   3.241 +#			    ((giv o sub i o client) Fols giv)"
   3.242  
   3.243 -#    (*spec (9.3)*)
   3.244 -#    network_rel :: 'a systemState program set
   3.245 -#	"network_rel == INT i : lessThan Nclients.
   3.246 +#    {*spec (9.3)*}
   3.247 +#    network_rel :: "'a systemState program set
   3.248 +#	"network_rel == \<Inter>i \<in> lessThan Nclients.
   3.249  #			    Increasing (rel o sub i o client)
   3.250  #			    guarantees[rel]
   3.251  #			    (rel  Fols (rel o sub i o client))"
   3.252  
   3.253 -#    (*spec: preserves part*)
   3.254 -#	network_preserves :: 'a systemState program set
   3.255 +#    {*spec: preserves part*}
   3.256 +#	network_preserves :: "'a systemState program set
   3.257  #	"network_preserves == preserves giv  Int
   3.258 -#			      (INT i : lessThan Nclients.
   3.259 +#			      (\<Inter>i \<in> lessThan Nclients.
   3.260  #			       preserves (funPair rel ask o sub i o client))"
   3.261  
   3.262 -#    network_spec :: 'a systemState program set
   3.263 +#    network_spec :: "'a systemState program set
   3.264  #	"network_spec == network_ask Int network_giv Int
   3.265  #			 network_rel Int network_preserves"
   3.266  
   3.267  
   3.268 -#  (** State mappings **)
   3.269 +#  {** State mappings **}
   3.270  #    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
   3.271  #	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
   3.272  #			   in (| giv = giv s,
   3.273 @@ -221,4 +219,171 @@
   3.274  #				     systemState.dummy = allocState_d.dummy al|)"
   3.275  ****)
   3.276  
   3.277 +
   3.278 +declare subset_preserves_o [THEN subsetD, intro]
   3.279 +declare funPair_o_distrib [simp]
   3.280 +declare Always_INT_distrib [simp]
   3.281 +declare o_apply [simp del]
   3.282 +
   3.283 +
   3.284 +subsection{*Theorems for Merge*}
   3.285 +
   3.286 +lemma (in Merge) Merge_Allowed:
   3.287 +     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
   3.288 +apply (cut_tac Merge_spec)
   3.289 +apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
   3.290 +done
   3.291 +
   3.292 +lemma (in Merge) M_ok_iff [iff]:
   3.293 +     "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &  
   3.294 +                     M \<in> Allowed G)"
   3.295 +by (auto simp add: Merge_Allowed ok_iff_Allowed)
   3.296 +
   3.297 +
   3.298 +lemma (in Merge) Merge_Always_Out_eq_iOut:
   3.299 +     "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]  
   3.300 +      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
   3.301 +apply (cut_tac Merge_spec)
   3.302 +apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
   3.303 +done
   3.304 +
   3.305 +lemma (in Merge) Merge_Bounded:
   3.306 +     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]  
   3.307 +      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
   3.308 +apply (cut_tac Merge_spec)
   3.309 +apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
   3.310 +done
   3.311 +
   3.312 +lemma (in Merge) Merge_Bag_Follows_lemma:
   3.313 +     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]  
   3.314 +  ==> M Join G \<in> Always  
   3.315 +          {s. (\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s)  
   3.316 +                                  {k. k < length (iOut s) & iOut s ! k = i})) =  
   3.317 +              (bag_of o merge.Out) s}"
   3.318 +apply (rule Always_Compl_Un_eq [THEN iffD1]) 
   3.319 +apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded]) 
   3.320 +apply (rule UNIV_AlwaysI, clarify) 
   3.321 +apply (subst bag_of_sublist_UN_disjoint [symmetric])
   3.322 +  apply (simp)
   3.323 + apply blast
   3.324 +apply (simp add: set_conv_nth)
   3.325 +apply (subgoal_tac
   3.326 +       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
   3.327 +       lessThan (length (iOut x))")
   3.328 + apply (simp (no_asm_simp) add: o_def)
   3.329 +apply blast
   3.330 +done
   3.331 +
   3.332 +lemma (in Merge) Merge_Bag_Follows:
   3.333 +     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))  
   3.334 +          guarantees   
   3.335 +             (bag_of o merge.Out) Fols  
   3.336 +             (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)"
   3.337 +apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
   3.338 +apply (rule Follows_setsum)
   3.339 +apply (cut_tac Merge_spec)
   3.340 +apply (auto simp add: merge_spec_def merge_follows_def o_def)
   3.341 +apply (drule guaranteesD) 
   3.342 +  prefer 3
   3.343 +  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
   3.344 +done
   3.345 +
   3.346 +
   3.347 +subsection{*Theorems for Distributor*}
   3.348 +
   3.349 +lemma (in Distrib) Distr_Increasing_Out:
   3.350 +     "D \<in> Increasing distr.In Int Increasing distr.iIn Int  
   3.351 +          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}  
   3.352 +          guarantees  
   3.353 +          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
   3.354 +apply (cut_tac Distrib_spec)
   3.355 +apply (simp add: distr_spec_def distr_follows_def)
   3.356 +apply clarify
   3.357 +apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
   3.358 +done
   3.359 +
   3.360 +lemma (in Distrib) Distr_Bag_Follows_lemma:
   3.361 +     "[| G \<in> preserves distr.Out;  
   3.362 +         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]  
   3.363 +  ==> D Join G \<in> Always  
   3.364 +          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)  
   3.365 +                                  {k. k < length (iIn s) & iIn s ! k = i})) =  
   3.366 +              bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
   3.367 +apply (erule Always_Compl_Un_eq [THEN iffD1])
   3.368 +apply (rule UNIV_AlwaysI, clarify)
   3.369 +apply (subst bag_of_sublist_UN_disjoint [symmetric])
   3.370 +  apply (simp (no_asm))
   3.371 + apply blast
   3.372 +apply (simp add: set_conv_nth)
   3.373 +apply (subgoal_tac
   3.374 +       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = 
   3.375 +        lessThan (length (iIn x))")
   3.376 + apply (simp (no_asm_simp))
   3.377 +apply blast
   3.378 +done
   3.379 +
   3.380 +lemma (in Distrib) D_ok_iff [iff]:
   3.381 +     "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
   3.382 +apply (cut_tac Distrib_spec)
   3.383 +apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def 
   3.384 +                      safety_prop_Acts_iff ok_iff_Allowed)
   3.385 +done
   3.386 +
   3.387 +lemma (in Distrib) Distr_Bag_Follows: 
   3.388 + "D \<in> Increasing distr.In Int Increasing distr.iIn Int  
   3.389 +      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}  
   3.390 +      guarantees   
   3.391 +       (\<Inter>i \<in> lessThan Nclients.  
   3.392 +        (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s)  
   3.393 +        Fols  
   3.394 +        (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
   3.395 +apply (rule guaranteesI, clarify)
   3.396 +apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
   3.397 +apply (rule Follows_setsum)
   3.398 +apply (cut_tac Distrib_spec)
   3.399 +apply (auto simp add: distr_spec_def distr_follows_def o_def)
   3.400 +apply (drule guaranteesD)
   3.401 +  prefer 3
   3.402 +  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
   3.403 +done
   3.404 +
   3.405 +
   3.406 +subsection{*Theorems for Allocator*}
   3.407 +
   3.408 +lemma alloc_refinement_lemma:
   3.409 +     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i <= g i s})   
   3.410 +      <= {s. (\<Sum>x \<in> lessThan n. f x) <= (\<Sum>x: lessThan n. g x s)}"
   3.411 +apply (induct_tac "n")
   3.412 +apply (auto simp add: lessThan_Suc)
   3.413 +done
   3.414 +
   3.415 +lemma alloc_refinement: 
   3.416 +"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int   
   3.417 +                             Increasing (sub i o allocRel))      
   3.418 +  Int    
   3.419 +  Always {s. \<forall>i. i<Nclients -->       
   3.420 +              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}        
   3.421 +  Int    
   3.422 +  (\<Inter>i \<in> lessThan Nclients.    
   3.423 +   \<Inter>h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}   
   3.424 +           LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})         
   3.425 +  <=      
   3.426 + (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int   
   3.427 +                             Increasing (sub i o allocRel))      
   3.428 +  Int    
   3.429 +  Always {s. \<forall>i. i<Nclients -->       
   3.430 +              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}        
   3.431 +  Int    
   3.432 +  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.   
   3.433 +         {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})  
   3.434 +  LeadsTo {s. (\<Sum>i: lessThan Nclients. tokens (hf i)) <=          
   3.435 +    (\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})"
   3.436 +apply (auto simp add: ball_conj_distrib)
   3.437 +apply (rename_tac F hf)
   3.438 +apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
   3.439 +apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
   3.440 + apply (simp add: Increasing_def o_assoc)
   3.441 +apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
   3.442 +done
   3.443 +
   3.444  end
     4.1 --- a/src/HOL/UNITY/Comp/Client.ML	Thu Jul 03 12:56:48 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,176 +0,0 @@
     4.4 -(*  Title:      HOL/UNITY/Client
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1998  University of Cambridge
     4.8 -
     4.9 -Distributed Resource Management System: the Client
    4.10 -*)
    4.11 -
    4.12 -Addsimps [Client_def RS def_prg_Init, 
    4.13 -          Client_def RS def_prg_AllowedActs];
    4.14 -Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
    4.15 -
    4.16 -Goal "(Client ok G) = \
    4.17 -\     (G : preserves rel & G : preserves ask & G : preserves tok &\
    4.18 -\      Client : Allowed G)";
    4.19 -by (auto_tac (claset(), 
    4.20 -    simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
    4.21 -qed "Client_ok_iff";
    4.22 -AddIffs [Client_ok_iff];
    4.23 -
    4.24 -
    4.25 -(*Safety property 1: ask, rel are increasing*)
    4.26 -Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
    4.27 -by (auto_tac
    4.28 -    (claset() addSIs [increasing_imp_Increasing],
    4.29 -     simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
    4.30 -by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def]));
    4.31 -by (ALLGOALS constrains_tac);
    4.32 -by Auto_tac;
    4.33 -qed "increasing_ask_rel";
    4.34 -
    4.35 -Addsimps [nth_append, append_one_prefix];
    4.36 -
    4.37 -
    4.38 -(*Safety property 2: the client never requests too many tokens.
    4.39 -      With no Substitution Axiom, we must prove the two invariants 
    4.40 -  simultaneously.
    4.41 -*)
    4.42 -Goal "Client ok G  \
    4.43 -\     ==> Client Join G :  \
    4.44 -\             Always ({s. tok s <= NbT}  Int  \
    4.45 -\                     {s. ALL elt : set (ask s). elt <= NbT})";
    4.46 -by Auto_tac;  
    4.47 -by (rtac (invariantI RS stable_Join_Always2) 1);
    4.48 -by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
    4.49 -		       addSIs [stable_Int]) 3);
    4.50 -by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2);
    4.51 -by (constrains_tac 2);
    4.52 -by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
    4.53 -by Auto_tac;
    4.54 -qed "ask_bounded_lemma";
    4.55 -
    4.56 -(*export version, with no mention of tok in the postcondition, but
    4.57 -  unfortunately tok must be declared local.*)
    4.58 -Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
    4.59 -by (rtac guaranteesI 1);
    4.60 -by (etac (ask_bounded_lemma RS Always_weaken) 1);
    4.61 -by (rtac Int_lower2 1);
    4.62 -qed "ask_bounded";
    4.63 -
    4.64 -
    4.65 -(*** Towards proving the liveness property ***)
    4.66 -
    4.67 -Goal "Client: stable {s. rel s <= giv s}";
    4.68 -by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1); 
    4.69 -by (constrains_tac 1);
    4.70 -by Auto_tac;
    4.71 -qed "stable_rel_le_giv";
    4.72 -
    4.73 -Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
    4.74 -\     ==> Client Join G : Stable {s. rel s <= giv s}";
    4.75 -by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
    4.76 -by Auto_tac;
    4.77 -qed "Join_Stable_rel_le_giv";
    4.78 -
    4.79 -Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
    4.80 -\     ==> Client Join G : Always {s. rel s <= giv s}";
    4.81 -by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
    4.82 -qed "Join_Always_rel_le_giv";
    4.83 -
    4.84 -Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
    4.85 -by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
    4.86 -by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
    4.87 -by (auto_tac (claset(),
    4.88 -	      simpset() addsimps [Domain_def, Client_def]));
    4.89 -by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
    4.90 -			       strict_prefix_length_less]) 1);
    4.91 -by (auto_tac (claset(), 
    4.92 -	      simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
    4.93 -by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
    4.94 -qed "transient_lemma";
    4.95 -
    4.96 -
    4.97 -Goal "[| Client Join G : Increasing giv;  Client ok G |] \
    4.98 -\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
    4.99 -\                     LeadsTo {s. k < rel s & rel s <= giv s & \
   4.100 -\                                 h <= giv s & h pfixGe ask s}";
   4.101 -by (rtac single_LeadsTo_I 1);
   4.102 -by (ftac (increasing_ask_rel RS guaranteesD) 1);
   4.103 -by Auto_tac;
   4.104 -by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
   4.105 -	  leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
   4.106 -by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
   4.107 -by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
   4.108 -by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
   4.109 -by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
   4.110 -by (etac Join_Stable_rel_le_giv 1);
   4.111 -by (Blast_tac 1);
   4.112 -by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, 
   4.113 -			       order_trans, prefix_imp_pfixGe, 
   4.114 -			       pfixGe_trans]) 2);
   4.115 -by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
   4.116 -qed "induct_lemma";
   4.117 -
   4.118 -
   4.119 -Goal "[| Client Join G : Increasing giv;  Client ok G |] \
   4.120 -\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
   4.121 -\                     LeadsTo {s. h <= rel s}";
   4.122 -by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
   4.123 -by (auto_tac (claset(), simpset() addsimps [vimage_def]));
   4.124 -by (rtac single_LeadsTo_I 1);
   4.125 -by (rtac (induct_lemma RS LeadsTo_weaken) 1);
   4.126 -by Auto_tac;
   4.127 -by (blast_tac (claset() addIs [order_less_le RS iffD2]
   4.128 -			addDs [common_prefix_linear]) 1);
   4.129 -by (REPEAT (dtac strict_prefix_length_less 1));
   4.130 -by (arith_tac 1);
   4.131 -qed "rel_progress_lemma";
   4.132 -
   4.133 -
   4.134 -Goal "[| Client Join G : Increasing giv;  Client ok G |] \
   4.135 -\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
   4.136 -\                     LeadsTo {s. h <= rel s}";
   4.137 -by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
   4.138 -by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
   4.139 -    LeadsTo_Un RS LeadsTo_weaken_L) 3);
   4.140 -by Auto_tac;
   4.141 -by (blast_tac (claset() addIs [order_less_le RS iffD2]
   4.142 -			addDs [common_prefix_linear]) 1);
   4.143 -qed "client_progress_lemma";
   4.144 -
   4.145 -(*Progress property: all tokens that are given will be released*)
   4.146 -Goal "Client : \
   4.147 -\      Increasing giv  guarantees  \
   4.148 -\      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
   4.149 -by (rtac guaranteesI 1);
   4.150 -by (Clarify_tac 1);
   4.151 -by (blast_tac (claset() addIs [client_progress_lemma]) 1);
   4.152 -qed "client_progress";
   4.153 -
   4.154 -(*This shows that the Client won't alter other variables in any state
   4.155 -  that it is combined with*)
   4.156 -Goal "Client : preserves dummy";
   4.157 -by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1);
   4.158 -by (Clarify_tac 1); 
   4.159 -by (constrains_tac 1);
   4.160 -by Auto_tac;
   4.161 -qed "client_preserves_dummy";
   4.162 -
   4.163 -
   4.164 -(** Obsolete lemmas from first version of the Client **)
   4.165 -
   4.166 -Goal "Client: stable {s. size (rel s) <= size (giv s)}";
   4.167 -by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
   4.168 -by (constrains_tac 1);
   4.169 -by Auto_tac;
   4.170 -qed "stable_size_rel_le_giv";
   4.171 -
   4.172 -(*clients return the right number of tokens*)
   4.173 -Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
   4.174 -by (rtac guaranteesI 1);
   4.175 -by (rtac AlwaysI 1);
   4.176 -by (Force_tac 1);
   4.177 -by (blast_tac (claset() addIs [Increasing_preserves_Stable, 
   4.178 -			       stable_rel_le_giv]) 1);
   4.179 -qed "ok_guar_rel_prefix_giv";
     5.1 --- a/src/HOL/UNITY/Comp/Client.thy	Thu Jul 03 12:56:48 2003 +0200
     5.2 +++ b/src/HOL/UNITY/Comp/Client.thy	Thu Jul 03 18:07:50 2003 +0200
     5.3 @@ -2,24 +2,24 @@
     5.4      ID:         $Id$
     5.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.6      Copyright   1998  University of Cambridge
     5.7 -
     5.8 -Distributed Resource Management System: the Client
     5.9  *)
    5.10  
    5.11 -Client = Rename + AllocBase +
    5.12 +header{*Distributed Resource Management System: the Client*}
    5.13 +
    5.14 +theory Client = Rename + AllocBase:
    5.15  
    5.16  types
    5.17 -  tokbag = nat	   (*tokbags could be multisets...or any ordered type?*)
    5.18 +  tokbag = nat	   --{*tokbags could be multisets...or any ordered type?*}
    5.19  
    5.20  record state =
    5.21 -  giv :: tokbag list   (*input history: tokens granted*)
    5.22 -  ask :: tokbag list   (*output history: tokens requested*)
    5.23 -  rel :: tokbag list   (*output history: tokens released*)
    5.24 -  tok :: tokbag	       (*current token request*)
    5.25 +  giv :: "tokbag list" --{*input history: tokens granted*}
    5.26 +  ask :: "tokbag list" --{*output history: tokens requested*}
    5.27 +  rel :: "tokbag list" --{*output history: tokens released*}
    5.28 +  tok :: tokbag	       --{*current token request*}
    5.29  
    5.30  record 'a state_d =
    5.31    state +  
    5.32 -  dummy :: 'a          (*new variables*)
    5.33 +  dummy :: 'a          --{*new variables*}
    5.34  
    5.35  
    5.36  (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
    5.37 @@ -30,10 +30,10 @@
    5.38    
    5.39    rel_act :: "('a state_d * 'a state_d) set"
    5.40      "rel_act == {(s,s').
    5.41 -		  \\<exists>nrel. nrel = size (rel s) &
    5.42 +		  \<exists>nrel. nrel = size (rel s) &
    5.43  		         s' = s (| rel := rel s @ [giv s!nrel] |) &
    5.44  		         nrel < size (giv s) &
    5.45 -		         ask s!nrel <= giv s!nrel}"
    5.46 +		         ask s!nrel \<le> giv s!nrel}"
    5.47  
    5.48    (** Choose a new token requirement **)
    5.49  
    5.50 @@ -47,21 +47,172 @@
    5.51      "ask_act == {(s,s'). s'=s |
    5.52  		         (s' = s (|ask := ask s @ [tok s]|))}"
    5.53  
    5.54 -  Client :: 'a state_d program
    5.55 +  Client :: "'a state_d program"
    5.56      "Client ==
    5.57         mk_total_program
    5.58 -            ({s. tok s : atMost NbT &
    5.59 +            ({s. tok s \<in> atMost NbT &
    5.60  		 giv s = [] & ask s = [] & rel s = []},
    5.61  	     {rel_act, tok_act, ask_act},
    5.62 -	     \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
    5.63 +	     \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
    5.64  		   Acts G)"
    5.65  
    5.66    (*Maybe want a special theory section to declare such maps*)
    5.67 -  non_dummy :: 'a state_d => state
    5.68 +  non_dummy :: "'a state_d => state"
    5.69      "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
    5.70  
    5.71    (*Renaming map to put a Client into the standard form*)
    5.72    client_map :: "'a state_d => state*'a"
    5.73      "client_map == funPair non_dummy dummy"
    5.74  
    5.75 +
    5.76 +declare Client_def [THEN def_prg_Init, simp]
    5.77 +declare Client_def [THEN def_prg_AllowedActs, simp]
    5.78 +declare rel_act_def [THEN def_act_simp, simp]
    5.79 +declare tok_act_def [THEN def_act_simp, simp]
    5.80 +declare ask_act_def [THEN def_act_simp, simp]
    5.81 +
    5.82 +lemma Client_ok_iff [iff]:
    5.83 +     "(Client ok G) =  
    5.84 +      (G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok & 
    5.85 +       Client \<in> Allowed G)"
    5.86 +by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
    5.87 +
    5.88 +
    5.89 +text{*Safety property 1: ask, rel are increasing*}
    5.90 +lemma increasing_ask_rel:
    5.91 +     "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
    5.92 +apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
    5.93 +apply (auto simp add: Client_def increasing_def)
    5.94 +apply (constrains, auto)+
    5.95 +done
    5.96 +
    5.97 +declare nth_append [simp] append_one_prefix [simp]
    5.98 +
    5.99 +
   5.100 +text{*Safety property 2: the client never requests too many tokens.
   5.101 +      With no Substitution Axiom, we must prove the two invariants 
   5.102 +      simultaneously. *}
   5.103 +lemma ask_bounded_lemma:
   5.104 +     "Client ok G   
   5.105 +      ==> Client Join G \<in>   
   5.106 +              Always ({s. tok s \<le> NbT}  Int   
   5.107 +                      {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
   5.108 +apply auto
   5.109 +apply (rule invariantI [THEN stable_Join_Always2], force) 
   5.110 + prefer 2
   5.111 + apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int) 
   5.112 +apply (simp add: Client_def, constrains)
   5.113 +apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
   5.114 +done
   5.115 +
   5.116 +text{*export version, with no mention of tok in the postcondition, but
   5.117 +  unfortunately tok must be declared local.*}
   5.118 +lemma ask_bounded:
   5.119 +     "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
   5.120 +apply (rule guaranteesI)
   5.121 +apply (erule ask_bounded_lemma [THEN Always_weaken])
   5.122 +apply (rule Int_lower2)
   5.123 +done
   5.124 +
   5.125 +
   5.126 +text{*** Towards proving the liveness property ***}
   5.127 +
   5.128 +lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
   5.129 +by (simp add: Client_def, constrains, auto)
   5.130 +
   5.131 +lemma Join_Stable_rel_le_giv:
   5.132 +     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
   5.133 +      ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
   5.134 +by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
   5.135 +
   5.136 +lemma Join_Always_rel_le_giv:
   5.137 +     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
   5.138 +      ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
   5.139 +by (force intro: AlwaysI Join_Stable_rel_le_giv)
   5.140 +
   5.141 +lemma transient_lemma:
   5.142 +     "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
   5.143 +apply (simp add: Client_def mk_total_program_def)
   5.144 +apply (rule_tac act = rel_act in totalize_transientI)
   5.145 +  apply (auto simp add: Domain_def Client_def)
   5.146 + apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
   5.147 +apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
   5.148 +apply (blast intro: strict_prefix_length_less)
   5.149 +done
   5.150 +
   5.151 +
   5.152 +lemma induct_lemma:
   5.153 +     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   5.154 +  ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
   5.155 +                      LeadsTo {s. k < rel s & rel s \<le> giv s &  
   5.156 +                                  h \<le> giv s & h pfixGe ask s}"
   5.157 +apply (rule single_LeadsTo_I)
   5.158 +apply (frule increasing_ask_rel [THEN guaranteesD], auto)
   5.159 +apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
   5.160 +  apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
   5.161 +     apply (erule_tac f = giv and x = "giv s" in IncreasingD)
   5.162 +    apply (erule_tac f = ask and x = "ask s" in IncreasingD)
   5.163 +   apply (erule_tac f = rel and x = "rel s" in IncreasingD)
   5.164 +  apply (erule Join_Stable_rel_le_giv, blast)
   5.165 + apply (blast intro: order_less_imp_le order_trans)
   5.166 +apply (blast intro: sym order_less_le [THEN iffD2] order_trans
   5.167 +                    prefix_imp_pfixGe pfixGe_trans)
   5.168 +done
   5.169 +
   5.170 +
   5.171 +lemma rel_progress_lemma:
   5.172 +     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   5.173 +  ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
   5.174 +                      LeadsTo {s. h \<le> rel s}"
   5.175 +apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
   5.176 +apply (auto simp add: vimage_def)
   5.177 +apply (rule single_LeadsTo_I)
   5.178 +apply (rule induct_lemma [THEN LeadsTo_weaken], auto)
   5.179 + apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
   5.180 +apply (drule strict_prefix_length_less)+
   5.181 +apply arith
   5.182 +done
   5.183 +
   5.184 +
   5.185 +lemma client_progress_lemma:
   5.186 +     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
   5.187 +      ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
   5.188 +                          LeadsTo {s. h \<le> rel s}"
   5.189 +apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
   5.190 +apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
   5.191 +  apply (blast intro: rel_progress_lemma) 
   5.192 + apply (rule subset_refl [THEN subset_imp_LeadsTo])
   5.193 +apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
   5.194 +done
   5.195 +
   5.196 +text{*Progress property: all tokens that are given will be released*}
   5.197 +lemma client_progress:
   5.198 +     "Client \<in>  
   5.199 +       Increasing giv  guarantees   
   5.200 +       (INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})"
   5.201 +apply (rule guaranteesI, clarify)
   5.202 +apply (blast intro: client_progress_lemma)
   5.203 +done
   5.204 +
   5.205 +text{*This shows that the Client won't alter other variables in any state
   5.206 +  that it is combined with*}
   5.207 +lemma client_preserves_dummy: "Client \<in> preserves dummy"
   5.208 +by (simp add: Client_def preserves_def, clarify, constrains, auto)
   5.209 +
   5.210 +
   5.211 +text{** Obsolete lemmas from first version of the Client **}
   5.212 +
   5.213 +lemma stable_size_rel_le_giv:
   5.214 +     "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
   5.215 +by (simp add: Client_def, constrains, auto)
   5.216 +
   5.217 +text{*clients return the right number of tokens*}
   5.218 +lemma ok_guar_rel_prefix_giv:
   5.219 +     "Client \<in> Increasing giv  guarantees  Always {s. rel s \<le> giv s}"
   5.220 +apply (rule guaranteesI)
   5.221 +apply (rule AlwaysI, force)
   5.222 +apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv)
   5.223 +done
   5.224 +
   5.225 +
   5.226  end