src/HOL/UNITY/Alloc.ML
author paulson
Wed Aug 25 11:09:24 1999 +0200 (1999-08-25)
changeset 7347 ad0ce67e4eb6
parent 7188 2bc63a44721b
child 7365 b5bb32e0861c
permissions -rw-r--r--
another snapshot
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@7347
     9
		Goal "(%(x,y). f(x,y)) = f";
paulson@7347
    10
		by (rtac ext 1);
paulson@7347
    11
		by (pair_tac "x" 1);
paulson@7347
    12
		by (Simp_tac 1);
paulson@7347
    13
		qed "split_Pair_apply";
paulson@7347
    14
paulson@7347
    15
		Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
paulson@7347
    16
		by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
paulson@7347
    17
		qed "split_paired_Eps";
paulson@7347
    18
paulson@7347
    19
		Goal "[| inj(f);  f x = y |] ==> inv f y = x";
paulson@7347
    20
		by (etac subst 1);
paulson@7347
    21
		by (etac inv_f_f 1);
paulson@7347
    22
		qed "inv_f_eq";
paulson@6837
    23
paulson@6840
    24
(*Generalized version allowing different clients*)
paulson@6840
    25
Goal "[| Alloc : alloc_spec;  \
paulson@6840
    26
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6840
    27
\        Network : network_spec |] \
paulson@6840
    28
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
    29
\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
paulson@6840
    30
\         Join Network : system_spec";
paulson@6840
    31
paulson@6840
    32
Goal "System : system_spec";
paulson@6840
    33
paulson@6840
    34
paulson@6828
    35
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    36
by (rtac injI 1);
paulson@7347
    37
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    38
qed "inj_sysOfAlloc";
paulson@6828
    39
paulson@6828
    40
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    41
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    42
\                                allocAsk = allocAsk s,    \
paulson@6828
    43
\                                allocRel = allocRel s |), \
paulson@6828
    44
\                             client s)")] surjI 1);
paulson@7347
    45
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    46
qed "surj_sysOfAlloc";
paulson@6828
    47
paulson@6828
    48
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    49
paulson@7347
    50
(**THESE SHOULD NOT BE NECESSARY...THE VARIOUS INJECTIONS INTO THE SYSTEM
paulson@7347
    51
   STATE NEED TO BE TREATED SYMMETRICALLY OR DONE AUTOMATICALLY*)
paulson@7347
    52
Goalw [sysOfClient_def] "inj sysOfClient";
paulson@7347
    53
by (rtac injI 1);
paulson@7347
    54
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
paulson@7347
    55
		       addSWrapper record_split_wrapper, simpset()));
paulson@7347
    56
qed "inj_sysOfClient";
paulson@7347
    57
paulson@7347
    58
Goalw [sysOfClient_def] "surj sysOfClient";
paulson@7347
    59
by (cut_facts_tac [surj_sysOfAlloc] 1);
paulson@7347
    60
by (rewtac surj_def);
paulson@7347
    61
by Auto_tac;
paulson@7347
    62
by (Blast_tac 1);
paulson@7347
    63
qed "surj_sysOfClient";
paulson@7347
    64
paulson@7347
    65
AddIffs [inj_sysOfClient, surj_sysOfClient];
paulson@7347
    66
paulson@6828
    67
paulson@6828
    68
Open_locale "System";
paulson@6828
    69
paulson@6828
    70
val Alloc = thm "Alloc";
paulson@6828
    71
val Client = thm "Client";
paulson@6828
    72
val Network = thm "Network";
paulson@6828
    73
val System_def = thm "System_def";
paulson@6828
    74
paulson@6828
    75
AddIffs [finite_lessThan];
paulson@6828
    76
paulson@6828
    77
paulson@7347
    78
Goal "Client : UNIV guar Increasing ask";
paulson@7347
    79
by (cut_facts_tac [Client] 1);
paulson@7347
    80
by (asm_full_simp_tac
paulson@7347
    81
    (simpset() addsimps [client_spec_def, client_increasing_def,
paulson@7347
    82
			 guarantees_Int_right]) 1);
paulson@7347
    83
qed "Client_Increasing_ask";
paulson@6828
    84
paulson@7347
    85
Goal "Client : UNIV guar Increasing rel";
paulson@7347
    86
by (cut_facts_tac [Client] 1);
paulson@7347
    87
by (asm_full_simp_tac
paulson@7347
    88
    (simpset() addsimps [client_spec_def, client_increasing_def,
paulson@7347
    89
			 guarantees_Int_right]) 1);
paulson@7347
    90
qed "Client_Increasing_rel";
paulson@7347
    91
paulson@7347
    92
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
paulson@7347
    93
paulson@7347
    94
Goal "Client : UNIV guar Always {s. ALL elt : set (ask s). elt <= NbT}";
paulson@7347
    95
by (cut_facts_tac [Client] 1);
paulson@7347
    96
by (asm_full_simp_tac
paulson@7347
    97
    (simpset() addsimps [client_spec_def, client_bounded_def]) 1);
paulson@7347
    98
qed "Client_Bounded";
paulson@7347
    99
paulson@7347
   100
(*Client_Progress we omit for now, since it's cumbersome to state*)
paulson@6837
   101
paulson@6837
   102
paulson@6837
   103
paulson@7347
   104
Goal "lift_prog i Client : UNIV guar Increasing (rel o sub i)";
paulson@7347
   105
by (rtac (Client_Increasing_rel RS lift_prog_guar_Increasing) 1);
paulson@7347
   106
qed "lift_prog_Client_Increasing_rel";
paulson@6837
   107
paulson@6837
   108
paulson@6837
   109
paulson@7347
   110
(*Comp.ML??????????*)
paulson@7347
   111
paulson@7347
   112
paulson@7347
   113
paulson@7347
   114
val project_guarantees' =
paulson@7347
   115
  [inj_sysOfClient, surj_sysOfClient] MRS export project_guarantees;
paulson@7347
   116
paulson@7347
   117
val extend_guar_Increasing' =
paulson@7347
   118
  [inj_sysOfClient, surj_sysOfClient] MRS export extend_guar_Increasing;
paulson@7347
   119
paulson@7347
   120
paulson@7347
   121
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7347
   122
Goal "!!s. inv sysOfClient s = \
paulson@7347
   123
\            (client s, \
paulson@7347
   124
\             (| allocGiv = allocGiv s, \
paulson@7347
   125
\                allocAsk = allocAsk s, \
paulson@7347
   126
\                allocRel = allocRel s|) )";
paulson@7347
   127
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
paulson@7347
   128
by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
paulson@7347
   129
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@7347
   130
qed "inv_sysOfClient";
paulson@7347
   131
paulson@7347
   132
paulson@6837
   133
paulson@6837
   134
paulson@7347
   135
val prems =
paulson@7347
   136
Goalw [PLam_def]
paulson@7347
   137
     "[| !!i. i:I ==> F i : X i guar Y i;  \
paulson@7347
   138
\        !!i H. [| i:I; H : XX i |] ==> drop_prog i H : X i;  \
paulson@7347
   139
\        !!i G. [| i:I; F i Join drop_prog i G : Y i |] \
paulson@7347
   140
\               ==> lift_prog i (F i) Join G : YY i |] \
paulson@7347
   141
\        ==> (PLam I F) : (INTER I XX) guar (INTER I YY)";
paulson@7347
   142
by (rtac (drop_prog_guarantees RS guarantees_JN_INT) 1);
paulson@7347
   143
by (REPEAT (ares_tac prems 1));
paulson@7347
   144
qed "drop_prog_guarantees_PLam";
paulson@6828
   145
paulson@6828
   146
paulson@7347
   147
(*for proof of property (1) *)
paulson@7347
   148
Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
paulson@7347
   149
by (full_simp_tac (simpset() addsimps [System_def]) 1);
paulson@7347
   150
by (rtac ([asm_rl, UNIV_I] MRS guaranteesD) 1);
paulson@7347
   151
by (rtac (disjI2 RS guarantees_Join_I) 1);
paulson@7347
   152
by (rtac project_guarantees' 1);
paulson@7347
   153
by (rtac subset_refl 2);
paulson@7347
   154
by (Clarify_tac 2);
paulson@7347
   155
by (rtac ([extend_guar_Increasing',subset_refl] MRS 
paulson@7347
   156
    guarantees_weaken RS guaranteesD) 2);
paulson@7347
   157
by (rtac UNIV_I 4);
paulson@7347
   158
by (force_tac (claset(),
paulson@7347
   159
	       simpset() addsimps [inv_sysOfClient]) 3);
paulson@7347
   160
by (asm_simp_tac (simpset() addsimps [guarantees_PLam_I, 
paulson@7347
   161
		      Client_Increasing_rel RS lift_prog_guar_Increasing]) 2);
paulson@7347
   162
paulson@7347
   163
by (rtac (Client_Increasing_rel RS drop_prog_guarantees_PLam RS guarantees_weaken) 1);
paulson@7347
   164
by (force_tac (claset() addIs [lift_prog_Join_Stable],
paulson@7347
   165
	       simpset() addsimps [Increasing_def]) 2);
paulson@6828
   166
by Auto_tac;
paulson@7347
   167
qed "System_Increasing_rel";
paulson@6828
   168
paulson@6828
   169
paulson@7347
   170
yyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyyy;
paulson@6828
   171
paulson@6828
   172
paulson@6828
   173
paulson@6828
   174
(*partial system...*)
paulson@6828
   175
Goal "[| Alloc : alloc_spec;  Network : network_spec |] \
paulson@6828
   176
\     ==> (extend sysOfAlloc Alloc) Join Network : system_spec";
paulson@6828
   177
paulson@6828
   178
(*partial system...*)
paulson@6828
   179
Goal "[| Client : client_spec;  Network : network_spec |] \
paulson@6840
   180
\     ==> (extend sysOfClient (plam x: lessThan Nclients. Client)) \
paulson@6828
   181
\         Join Network : system_spec";
paulson@6828
   182
paulson@6828
   183
paulson@6828
   184
paulson@6828
   185
Goal "[| Alloc : alloc_spec;  Client : client_spec;  \
paulson@6828
   186
\        Network : network_spec |] \
paulson@6828
   187
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
   188
\         Join (extend sysOfClient (plam x: lessThan Nclients. Client)) \
paulson@6828
   189
\         Join Network : system_spec";
paulson@6828
   190
by (full_simp_tac
paulson@6828
   191
    (simpset() addsimps [system_spec_def, system_safety_def]) 1);
paulson@6828
   192
by Auto_tac;
paulson@6828
   193
by (full_simp_tac
paulson@6828
   194
    (simpset() addsimps [client_spec_def, client_increasing_def,
paulson@6828
   195
			 guarantees_Int_right]) 1);
paulson@6828
   196
by Auto_tac;
paulson@6828
   197
by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
paulson@6828
   198
back();
paulson@6828
   199
by (full_simp_tac
paulson@6828
   200
    (simpset() addsimps [network_spec_def, network_rel_def]) 1);
paulson@6828
   201
paulson@7347
   202
paulson@6828
   203
by (full_simp_tac
paulson@6828
   204
    (simpset() addsimps [alloc_spec_def, alloc_safety_def]) 1);
paulson@6828
   205
by Auto_tac;
paulson@6828
   206
paulson@6828
   207
by (Simp_tac 1);