src/HOL/UNITY/Alloc.ML
author paulson
Thu Aug 26 11:46:04 1999 +0200 (1999-08-26)
changeset 7365 b5bb32e0861c
parent 7347 ad0ce67e4eb6
child 7399 cf780c2bcccf
permissions -rw-r--r--
a bit further with property (1)
paulson@6828
     1
(*  Title:      HOL/UNITY/Alloc
paulson@6828
     2
    ID:         $Id$
paulson@6828
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6828
     4
    Copyright   1998  University of Cambridge
paulson@6828
     5
paulson@6828
     6
Specification of Chandy and Charpentier's Allocator
paulson@6828
     7
*)
paulson@6828
     8
paulson@6840
     9
(*Generalized version allowing different clients*)
paulson@6840
    10
Goal "[| Alloc : alloc_spec;  \
paulson@6840
    11
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6840
    12
\        Network : network_spec |] \
paulson@6840
    13
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
    14
\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
paulson@6840
    15
\         Join Network : system_spec";
paulson@6840
    16
paulson@6840
    17
Goal "System : system_spec";
paulson@6840
    18
paulson@6840
    19
paulson@6828
    20
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    21
by (rtac injI 1);
paulson@7347
    22
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    23
qed "inj_sysOfAlloc";
paulson@6828
    24
paulson@6828
    25
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    26
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    27
\                                allocAsk = allocAsk s,    \
paulson@6828
    28
\                                allocRel = allocRel s |), \
paulson@6828
    29
\                             client s)")] surjI 1);
paulson@7347
    30
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    31
qed "surj_sysOfAlloc";
paulson@6828
    32
paulson@6828
    33
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    34
paulson@7365
    35
(**SHOULD NOT BE NECESSARY: The various injections into the system
paulson@7365
    36
   state need to be treated symmetrically or done automatically*)
paulson@7347
    37
Goalw [sysOfClient_def] "inj sysOfClient";
paulson@7347
    38
by (rtac injI 1);
paulson@7347
    39
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
paulson@7347
    40
		       addSWrapper record_split_wrapper, simpset()));
paulson@7347
    41
qed "inj_sysOfClient";
paulson@7347
    42
paulson@7347
    43
Goalw [sysOfClient_def] "surj sysOfClient";
paulson@7347
    44
by (cut_facts_tac [surj_sysOfAlloc] 1);
paulson@7347
    45
by (rewtac surj_def);
paulson@7347
    46
by Auto_tac;
paulson@7347
    47
by (Blast_tac 1);
paulson@7347
    48
qed "surj_sysOfClient";
paulson@7347
    49
paulson@7347
    50
AddIffs [inj_sysOfClient, surj_sysOfClient];
paulson@7347
    51
paulson@6828
    52
paulson@7347
    53
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7347
    54
Goal "!!s. inv sysOfClient s = \
paulson@7347
    55
\            (client s, \
paulson@7347
    56
\             (| allocGiv = allocGiv s, \
paulson@7347
    57
\                allocAsk = allocAsk s, \
paulson@7347
    58
\                allocRel = allocRel s|) )";
paulson@7347
    59
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
paulson@7347
    60
by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
paulson@7347
    61
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@7365
    62
qed "inv_sysOfClient_eq";
paulson@6837
    63
paulson@6837
    64
paulson@7365
    65
Open_locale "System";
paulson@7365
    66
paulson@7365
    67
val Alloc = thm "Alloc";
paulson@7365
    68
val Client = thm "Client";
paulson@7365
    69
val Network = thm "Network";
paulson@7365
    70
val System_def = thm "System_def";
paulson@7365
    71
paulson@7365
    72
AddIffs [finite_lessThan];
paulson@7365
    73
paulson@7365
    74
(*Client : <unfolded specification> *)
paulson@7365
    75
val Client_Spec =
paulson@7365
    76
    rewrite_rule [client_spec_def, client_increasing_def,
paulson@7365
    77
		  client_bounded_def, client_progress_def] Client;
paulson@7365
    78
paulson@7365
    79
Goal "Client : UNIV guarantees Increasing ask";
paulson@7365
    80
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
    81
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
    82
qed "Client_Increasing_ask";
paulson@7365
    83
paulson@7365
    84
Goal "Client : UNIV guarantees Increasing rel";
paulson@7365
    85
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
    86
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
    87
qed "Client_Increasing_rel";
paulson@7365
    88
paulson@7365
    89
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
paulson@7365
    90
paulson@7365
    91
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
paulson@7365
    92
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
    93
by Auto_tac;
paulson@7365
    94
qed "Client_Bounded";
paulson@7365
    95
paulson@7365
    96
(*Client_Progress is cumbersome to state*)
paulson@7365
    97
val Client_Progress = Client_Spec RS IntD2;
paulson@6828
    98
paulson@6828
    99
paulson@7365
   100
(*Network : <unfolded specification> *)
paulson@7365
   101
val Network_Spec =
paulson@7365
   102
    rewrite_rule [network_spec_def, network_ask_def,
paulson@7365
   103
		  network_giv_def, network_rel_def] Network;
paulson@7365
   104
paulson@7365
   105
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
paulson@7365
   106
  exporting it from the locale*)
paulson@7365
   107
val Network_Ask = Network_Spec RS IntD1 RS IntD1;
paulson@7365
   108
val Network_Giv = Network_Spec RS IntD1 RS IntD2;
paulson@7365
   109
val Network_Rel = Network_Spec RS IntD2 RS INT_D;
paulson@7365
   110
paulson@7365
   111
paulson@7365
   112
(*Alloc : <unfolded specification> *)
paulson@7365
   113
val Alloc_Spec =
paulson@7365
   114
    rewrite_rule [alloc_spec_def, alloc_increasing_def,
paulson@7365
   115
		  alloc_safety_def, alloc_progress_def] Alloc;
paulson@7365
   116
paulson@7365
   117
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocAsk)";
paulson@7365
   118
by (cut_facts_tac [Alloc_Spec] 1);
paulson@7365
   119
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
paulson@7365
   120
qed "Alloc_Increasing";
paulson@7365
   121
paulson@7365
   122
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2;
paulson@7365
   123
val Alloc_Progress = (Alloc_Spec RS IntD2
paulson@7365
   124
                      |> simplify (simpset() addsimps [guarantees_INT_right]))
paulson@7365
   125
                     RS bspec RS spec;
paulson@7365
   126
		     
paulson@7365
   127
paulson@7347
   128
paulson@7365
   129
(*Not sure what to say about the other components because they involve
paulson@7365
   130
  extend*)
paulson@7365
   131
Goalw [System_def] "Network component System";
paulson@7365
   132
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7365
   133
qed "Network_component_System";
paulson@7365
   134
paulson@7365
   135
AddIffs [Network_component_System];
paulson@7365
   136
paulson@7365
   137
paulson@7365
   138
val project_guarantees' =
paulson@7365
   139
  [surj_sysOfClient, inj_sysOfClient] MRS export project_guarantees;
paulson@7365
   140
paulson@7365
   141
(* F : UNIV guarantees Increasing func
paulson@7365
   142
   ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
paulson@7365
   143
val extend_guar_Increasing' =
paulson@7365
   144
  [surj_sysOfClient, inj_sysOfClient] MRS export extend_guar_Increasing
paulson@7365
   145
  |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
paulson@7365
   146
paulson@7365
   147
paulson@7365
   148
(** Proof of property (1) **)
paulson@7365
   149
paulson@7365
   150
(*step 1*)
paulson@7365
   151
Goalw [System_def]
paulson@7365
   152
     "i < Nclients ==> System : Increasing (rel o sub i o client)";
paulson@7365
   153
by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] 
paulson@7365
   154
	  MRS guaranteesD) 1);
paulson@7365
   155
by (asm_simp_tac 
paulson@7365
   156
    (simpset() addsimps [guarantees_PLam_I, 
paulson@7365
   157
			 extend_guar_Increasing' RS guaranteesD,
paulson@7365
   158
			 lift_prog_guar_Increasing]) 1);
paulson@7347
   159
qed "System_Increasing_rel";
paulson@6828
   160
paulson@7365
   161
(*Note: the first step above performs simple quantifier reasoning.  It could
paulson@7365
   162
  be replaced by a proof mentioning no guarantees primitives*)
paulson@6828
   163
paulson@6828
   164
paulson@7365
   165
(*step 2*)
paulson@7365
   166
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@7365
   167
by (rtac Follows_Increasing1 1);
paulson@7365
   168
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
paulson@7365
   169
			       System_Increasing_rel, Network]) 1);
paulson@7365
   170
qed "System_Increasing_allocRel";
paulson@6828
   171
paulson@7365
   172
Goal "i < Nclients \
paulson@7365
   173
\ ==> System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
paulson@7365
   174
\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
paulson@7365
   175
fr component_guaranteesD;
paulson@7347
   176
paulson@7365
   177
val extend_guar_Increasing'' =
paulson@7365
   178
  [surj_sysOfAlloc, inj_sysOfAlloc] MRS export extend_guar_Increasing
paulson@7365
   179
  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
paulson@6828
   180
paulson@7365
   181
by (rtac (Alloc_Safety RS component_guaranteesD) 1);