src/HOL/UNITY/Alloc.ML
author paulson
Thu Jun 17 10:43:05 1999 +0200 (1999-06-17)
changeset 6837 1bd850260747
parent 6828 ea6832d74353
child 6840 0e5c82abfc71
permissions -rw-r--r--
another snapshot, still not working
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@6837
     9
paulson@6815
    10
Addsimps [sub_def];
paulson@6828
    11
paulson@6828
    12
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    13
by (rtac injI 1);
paulson@6828
    14
by Auto_tac;
paulson@6828
    15
qed "inj_sysOfAlloc";
paulson@6828
    16
paulson@6828
    17
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    18
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    19
\                                allocAsk = allocAsk s,    \
paulson@6828
    20
\                                allocRel = allocRel s |), \
paulson@6828
    21
\                             client s)")] surjI 1);
paulson@6828
    22
by Auto_tac;
paulson@6828
    23
qed "surj_sysOfAlloc";
paulson@6828
    24
paulson@6828
    25
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    26
paulson@6828
    27
paulson@6828
    28
Open_locale "System";
paulson@6828
    29
paulson@6828
    30
val Alloc = thm "Alloc";
paulson@6828
    31
val Client = thm "Client";
paulson@6828
    32
val Network = thm "Network";
paulson@6828
    33
val System_def = thm "System_def";
paulson@6828
    34
paulson@6828
    35
AddIffs [finite_lessThan];
paulson@6828
    36
paulson@6828
    37
(*could move to PPROD.ML, but function "sub" is needed there*)
paulson@6837
    38
Goal "lift_set i {s. P s} = {s. P (sub i s)}";
paulson@6828
    39
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@6828
    40
qed "lift_set_sub";
paulson@6828
    41
paulson@6828
    42
(*ONE OF THESE IS REDUNDANT!*)
paulson@6837
    43
Goal "lift_set i {s. P s} = {s. P (s i)}";
paulson@6828
    44
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@6828
    45
qed "lift_set_sub2";
paulson@6828
    46
paulson@6828
    47
Goalw [Increasing_def]
paulson@6828
    48
     "[| i: I;  finite I |]  \
paulson@6828
    49
\     ==> ((PPI x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
paulson@6828
    50
by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
paulson@6828
    51
by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
paulson@6828
    52
by (asm_full_simp_tac (simpset() addsimps [PFUN_Stable]) 1);
paulson@6828
    53
qed "PFUN_Increasing";
paulson@6828
    54
paulson@6837
    55
paulson@6837
    56
(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
paulson@6837
    57
  ensure that F has the form lift_prog i F for some F.*)
paulson@6837
    58
Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
paulson@6837
    59
by Auto_tac;
paulson@6837
    60
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
    61
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
paulson@6837
    62
qed "image_lift_prog_Stable";
paulson@6837
    63
paulson@6837
    64
Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
paulson@6837
    65
by (simp_tac (simpset() addsimps [Increasing_def,
paulson@6837
    66
				  inj_lift_prog RS image_INT]) 1);
paulson@6837
    67
by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
paulson@6837
    68
qed "image_lift_prog_Increasing";
paulson@6837
    69
paulson@6837
    70
paulson@6837
    71
(*****************PPROD.ML******************)
paulson@6837
    72
paulson@6837
    73
(*????????????????????????????????????????????????????????????????????????*)
paulson@6837
    74
Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  modular i Y |] \
paulson@6837
    75
\     ==> lift_prog i F : X guar Y";
paulson@6837
    76
by (rtac guaranteesI 1);
paulson@6837
    77
by (dtac guaranteesD 1);
paulson@6837
    78
by (rtac image_eqI 1);
paulson@6837
    79
by (rtac (drop_prog_lift_prog_Join RS sym) 1);
paulson@6837
    80
by (assume_tac 1);
paulson@6837
    81
by Auto_tac;
paulson@6837
    82
by (full_simp_tac (simpset() addsimps [modular_def,
paulson@6837
    83
				       drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
    84
by (dtac sym 1);
paulson@6837
    85
by (Blast_tac 1);
paulson@6837
    86
qed "drop_prog_guarantees";
paulson@6837
    87
paulson@6837
    88
Goalw [constrains_def]
paulson@6837
    89
     "(drop_prog i F : A co B)  =  \
paulson@6837
    90
\     (F : (lift_set i A) co (lift_set i B))";
paulson@6837
    91
by Auto_tac;
paulson@6837
    92
by (force_tac (claset(), 
paulson@6837
    93
	       simpset() addsimps [drop_act_def]) 2);
paulson@6837
    94
by (blast_tac (claset() addIs [drop_act_I]) 1);
paulson@6837
    95
qed "drop_prog_constrains_eq";
paulson@6837
    96
paulson@6837
    97
Goal "(drop_prog i F : stable A)  =  (F : stable (lift_set i A))";
paulson@6837
    98
by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains_eq]) 1);
paulson@6837
    99
qed "drop_prog_stable_eq";
paulson@6837
   100
paulson@6837
   101
Goal "modular i (stable {s. P(s i)})";
paulson@6837
   102
by (simp_tac (simpset() addsimps [modular_def, lift_set_sub2 RS sym,
paulson@6837
   103
				  drop_prog_stable_eq RS sym]) 1);
paulson@6837
   104
by Auto_tac;
paulson@6837
   105
qed "modular_stable_i";
paulson@6837
   106
paulson@6837
   107
paulson@6837
   108
(** Weak Constrains and Stable **)
paulson@6837
   109
paulson@6837
   110
Goal "f : reachable F ==> f i : reachable (drop_prog i F)";
paulson@6837
   111
by (etac reachable.induct 1);
paulson@6837
   112
by (force_tac (claset() addIs [reachable.Acts, drop_act_I],
paulson@6837
   113
	       simpset()) 2);
paulson@6837
   114
by (force_tac (claset() addIs [reachable.Init, drop_set_I],
paulson@6837
   115
	       simpset()) 1);
paulson@6837
   116
qed "reachable_imp_reachable_drop_prog";
paulson@6837
   117
paulson@6837
   118
Goalw [Constrains_def]
paulson@6837
   119
     "drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)";
paulson@6837
   120
by (full_simp_tac (simpset() addsimps [drop_prog_constrains_eq]) 1);
paulson@6837
   121
by (etac constrains_weaken_L 1);
paulson@6837
   122
by Auto_tac;
paulson@6837
   123
by (etac reachable_imp_reachable_drop_prog 1);
paulson@6837
   124
qed "drop_prog_Constrains_D";
paulson@6837
   125
paulson@6837
   126
Goalw [Stable_def]
paulson@6837
   127
     "drop_prog i F : Stable A ==> F : Stable (lift_set i A)";
paulson@6837
   128
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
paulson@6837
   129
qed "drop_prog_Stable_D";
paulson@6837
   130
paulson@6837
   131
(***????????????????
paulson@6837
   132
Goal "i ~= j ==> lift_prog i `` UNIV <= stable {s. P (f (s j))}";
paulson@6837
   133
by Auto_tac;
paulson@6837
   134
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
   135
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
paulson@6837
   136
qed "image_lift_prog_Stable";
paulson@6837
   137
????????????????*)
paulson@6837
   138
paulson@6837
   139
paulson@6837
   140
paulson@6837
   141
(****UNITY.ML?****)
paulson@6837
   142
Goalw [constrains_def, Idle_def] "F : Idle ==> (F : A co B) = (A<=B)";
paulson@6837
   143
by (Blast_tac 1);
paulson@6837
   144
qed "constrains_Idle_iff";
paulson@6837
   145
paulson@6837
   146
Goalw [stable_def,constrains_def,Idle_def] "F : Idle ==> F : stable A";
paulson@6837
   147
by (Blast_tac 1);
paulson@6837
   148
qed "stable_Idle";
paulson@6837
   149
paulson@6837
   150
Goalw [drop_act_def, lift_act_def]
paulson@6837
   151
     "i~=j ==> drop_act i (lift_act j act) <= Id";
paulson@6837
   152
by Auto_tac;
paulson@6837
   153
qed "neq_drop_act_lift_act";
paulson@6837
   154
paulson@6837
   155
paulson@6837
   156
Goal "drop_prog i (JN j:I - {i}. lift_prog j F) : Idle";
paulson@6837
   157
by (simp_tac (simpset() addsimps [Acts_JN,Idle_def]) 1);
paulson@6837
   158
by Auto_tac;
paulson@6837
   159
by (rtac ccontr 1);  
paulson@6837
   160
  (*otherwise PROOF FAILED because tactics don't get negated conclusion*)
paulson@6837
   161
by (blast_tac (claset() addSDs [impOfSubs neq_drop_act_lift_act]) 1);
paulson@6837
   162
qed "drop_prog_JN_other_Idle";
paulson@6837
   163
paulson@6837
   164
Goal "[| F component G;  G : Idle |] ==> F : Idle";
paulson@6837
   165
by (full_simp_tac (simpset() addsimps [Idle_def, component_eq_subset]) 1);
paulson@6837
   166
by Auto_tac;
paulson@6837
   167
qed "component_Idle";
paulson@6837
   168
paulson@6837
   169
Goal "G component (JN j: I-{i}. JN H: UNIV. lift_prog j H) \
paulson@6837
   170
\     ==> drop_prog i G : Idle";
paulson@6837
   171
by (dtac drop_prog_mono 1);
paulson@6837
   172
be component_Idle 1;
paulson@6837
   173
by (simp_tac (simpset() addsimps [drop_prog_JN_other_Idle, 
paulson@6837
   174
				  lift_prog_JN RS sym]) 1);
paulson@6837
   175
qed "component_JN_neq_imp_Idle";
paulson@6837
   176
paulson@6837
   177
Goal "drop_prog i G : Idle ==> G : stable (lift_set i A)";
paulson@6837
   178
by (simp_tac (simpset() addsimps [drop_prog_stable_eq RS sym]) 1);
paulson@6837
   179
by (blast_tac (claset() addIs [stable_Idle]) 1);
paulson@6837
   180
qed "Idle_imp_stable_lift_set";
paulson@6837
   181
paulson@6837
   182
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
paulson@6837
   183
paulson@6837
   184
Goalw [guarantees_def]
paulson@6837
   185
    "[| F : (X Int A) guar (Y Int A);  \
paulson@6837
   186
\       F : (X Int B) guar (Y Int B);  \
paulson@6837
   187
\       UNIV <= A Un B |] \
paulson@6837
   188
\    ==> F : X guar Y";
paulson@6828
   189
by (Blast_tac 1);
paulson@6837
   190
qed "guarantees_Un_partition_I";
paulson@6837
   191
paulson@6837
   192
Goalw [guarantees_def]
paulson@6837
   193
    "[| ALL i:I. F : (X Int A i) guar (Y Int A i);  UNIV <= UNION I A |] \
paulson@6837
   194
\    ==> F : X guar Y";
paulson@6837
   195
by (Blast_tac 1);
paulson@6837
   196
qed "guarantees_UN_partition_I";
paulson@6837
   197
paulson@6837
   198
Goal "{G. G component (JN j: I-{i}. JN H: UNIV. lift_prog j H)} \
paulson@6837
   199
\     <= stable (lift_set i A)";
paulson@6837
   200
by (Clarify_tac 1);
paulson@6837
   201
by (etac (component_JN_neq_imp_Idle RS Idle_imp_stable_lift_set) 1);
paulson@6837
   202
result();
paulson@6837
   203
paulson@6837
   204
Goal "i~=j ==> (lift_prog j `` UNIV) <= Increasing (f o sub i)";
paulson@6837
   205
by (rewtac Increasing_def);
paulson@6837
   206
by Auto_tac;
paulson@6837
   207
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
   208
by (blast_tac (claset() addIs [neq_imp_lift_prog_Stable]) 1);
paulson@6837
   209
result();
paulson@6837
   210
paulson@6837
   211
Goal "Cl : UNIV guar Increasing f   ==> \
paulson@6837
   212
\ lift_prog i Cl : {G. G component (JN j: I. JN H: UNIV. lift_prog j H)} \
paulson@6837
   213
\                  guar Increasing (f o sub i)";
paulson@6837
   214
by (rtac guarantees_partition_I 1);
paulson@6837
   215
by (simp_tac (simpset() addsimps []) 1);
paulson@6837
   216
paulson@6837
   217
by (dtac lift_prog_guarantees 1);
paulson@6837
   218
by (etac guarantees_weaken 1);
paulson@6837
   219
by Auto_tac;
paulson@6837
   220
by (rtac (impOfSubs image_lift_prog_Increasing) 1);
paulson@6837
   221
by Auto_tac;
paulson@6837
   222
result();
paulson@6837
   223
paulson@6837
   224
paulson@6837
   225
paulson@6837
   226
paulson@6837
   227
paulson@6837
   228
paulson@6837
   229
????????????????????????????????????????????????????????????????;
paulson@6837
   230
paulson@6837
   231
paulson@6837
   232
paulson@6837
   233
paulson@6837
   234
Goal "drop_prog i `` UNIV = UNIV";
paulson@6837
   235
by Auto_tac;
paulson@6837
   236
fr image_eqI;
paulson@6837
   237
by (rtac (lift_prog_inverse RS sym) 1);
paulson@6837
   238
by Auto_tac;
paulson@6837
   239
result();
paulson@6837
   240
paulson@6837
   241
paulson@6837
   242
Goal "[| F : (drop_prog i `` XX) guar Y;    \
paulson@6837
   243
\        ALL Z:XX. Z component (JN i:UNIV. JN G:UNIV. lift_prog i G) |] \
paulson@6837
   244
\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
paulson@6837
   245
by (rtac guaranteesI 1);
paulson@6837
   246
by (dtac guaranteesD 1);
paulson@6837
   247
by (ball_tac 1);
paulson@6837
   248
by (full_simp_tac (simpset() addsimps [Join_component_iff]) 1);
paulson@6837
   249
by (full_simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
paulson@6837
   250
paulson@6837
   251
by (rtac image_eqI 2);
paulson@6837
   252
by (assume_tac 3);
paulson@6837
   253
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 2);
paulson@6837
   254
paulson@6837
   255
by (rtac (drop_prog_lift_prog_Join RS sym) 1);
paulson@6837
   256
by (assume_tac 1);
paulson@6837
   257
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   258
by (rtac image_eqI 1);
paulson@6837
   259
by (assume_tac 2);
paulson@6837
   260
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   261
paulson@6837
   262
by (rtac guaranteesI 1);
paulson@6837
   263
by (dtac guaranteesD 1);
paulson@6837
   264
by (rtac image_eqI 1);
paulson@6837
   265
by (rtac (drop_prog_lift_prog_Join RS sym) 1);
paulson@6837
   266
by (assume_tac 1);
paulson@6837
   267
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   268
by (rtac image_eqI 1);
paulson@6837
   269
by (assume_tac 2);
paulson@6837
   270
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   271
paulson@6837
   272
paulson@6837
   273
by (dtac sym 1);
paulson@6837
   274
by (Blast_tac 1);
paulson@6837
   275
paulson@6837
   276
paulson@6837
   277
by (rtac guaranteesI 1);
paulson@6837
   278
by (dtac guaranteesD 1);
paulson@6837
   279
by (rtac image_eqI 2);
paulson@6837
   280
by (assume_tac 3);
paulson@6837
   281
paulson@6837
   282
paulson@6837
   283
Goal "F : X guar Y \
paulson@6837
   284
\     ==> lift_prog i F : XX guar (lift_prog i `` Y)";
paulson@6837
   285
by (rtac guaranteesI 1);
paulson@6837
   286
by (dtac guaranteesD 1);
paulson@6837
   287
by (rtac image_eqI 2);
paulson@6837
   288
by (assume_tac 3);
paulson@6837
   289
paulson@6837
   290
by Auto_tac;
paulson@6837
   291
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
paulson@6837
   292
qed "lift_prog_guarantees";
paulson@6837
   293
paulson@6837
   294
paulson@6837
   295
paulson@6837
   296
paulson@6837
   297
paulson@6837
   298
Goal "x : reachable (drop_prog i F) ==> x : drop_set i (reachable F)";
paulson@6837
   299
by (etac reachable.induct 1);
paulson@6837
   300
by Auto_tac;
paulson@6837
   301
by (rewtac drop_set_def);
paulson@6837
   302
by (force_tac (claset() addIs [reachable.Init, drop_set_I],
paulson@6837
   303
	       simpset()) 1);
paulson@6837
   304
by (rewtac drop_act_def);
paulson@6837
   305
by Auto_tac;
paulson@6837
   306
by (rtac imageI 1);
paulson@6837
   307
by (rtac reachable.Acts 1);
paulson@6837
   308
by (assume_tac 1);
paulson@6837
   309
by (assume_tac 1);
paulson@6837
   310
paulson@6837
   311
paulson@6837
   312
Goal "reachable (drop_prog i F) = drop_set i (reachable F)";
paulson@6837
   313
by (rewtac drop_set_def);
paulson@6837
   314
by Auto_tac;
paulson@6837
   315
by (etac reachable_imp_reachable_drop_prog 2);
paulson@6837
   316
paulson@6837
   317
paulson@6837
   318
(*FAILS, so the X condition is too strong*)
paulson@6837
   319
Goal "((f o sub i) localTo (lift_prog i F))  <= (UN F. {lift_prog i F})";
paulson@6837
   320
by (simp_tac (simpset() addsimps [localTo_def]) 1);
paulson@6837
   321
by Auto_tac;
paulson@6837
   322
paulson@6837
   323
paulson@6837
   324
Goal "lift_prog i `` drop_prog i `` ((f o sub i) localTo (lift_prog i F)) \
paulson@6837
   325
\     <= ((f o sub i) localTo (lift_prog i F))";
paulson@6837
   326
by (simp_tac (simpset() addsimps [localTo_def]) 1);
paulson@6837
   327
by Auto_tac;
paulson@6828
   328
paulson@6828
   329
paulson@6828
   330
paulson@6837
   331
Goalw [Constrains_def]
paulson@6837
   332
     "(F : (lift_set i A) Co (lift_set i B)) \
paulson@6837
   333
\     ==> (drop_prog i F : A Co B)";
paulson@6837
   334
by (full_simp_tac (simpset() addsimps [drop_prog_constrains_eq]) 1);
paulson@6837
   335
by (etac constrains_weaken_L 1);
paulson@6837
   336
paulson@6837
   337
by Auto_tac;
paulson@6837
   338
by (force_tac (claset(), 
paulson@6837
   339
	       simpset() addsimps [drop_act_def]) 2);
paulson@6837
   340
by (blast_tac (claset() addIs [drop_act_I]) 1);
paulson@6837
   341
qed "drop_prog_Constrains_eq";
paulson@6837
   342
paulson@6837
   343
paulson@6837
   344
(*Does NOT appear to be provable, so this notion of modular is too strong*)
paulson@6837
   345
Goal "lift_prog i `` drop_prog i `` Increasing (f o sub i) \
paulson@6837
   346
\        <= Increasing (f o sub i)";
paulson@6837
   347
by (simp_tac (simpset() addsimps [Increasing_def]) 1);
paulson@6837
   348
by Auto_tac;
paulson@6837
   349
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
   350
by (simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
paulson@6837
   351
paulson@6837
   352
paulson@6837
   353
paulson@6837
   354
paulson@6837
   355
paulson@6837
   356
Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
paulson@6837
   357
\        X <= (UN F. {lift_prog i F});  \
paulson@6837
   358
\        lift_prog i `` drop_prog i `` Y <= Y |] \
paulson@6837
   359
\     ==> lift_prog i F : X guar Y";
paulson@6837
   360
by (rtac guaranteesI 1);
paulson@6837
   361
by (set_mp_tac 1);
paulson@6837
   362
by (Clarify_tac 1);
paulson@6837
   363
by (dtac guaranteesD 1);
paulson@6837
   364
by (rtac image_eqI 1);
paulson@6837
   365
by (rtac (drop_prog_lift_prog_Join RS sym) 1);
paulson@6837
   366
by (assume_tac 1);
paulson@6837
   367
by Auto_tac;
paulson@6837
   368
by (asm_full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   369
by Auto_tac;
paulson@6837
   370
qed "drop_prog_guarantees";
paulson@6837
   371
paulson@6837
   372
paulson@6837
   373
paulson@6837
   374
NEW NOTION OF MODULAR
paulson@6837
   375
paulson@6837
   376
paulson@6837
   377
Goal "(ALL H:X. lift_prog i (drop_prog i H) : X) = \
paulson@6837
   378
\     (lift_prog i `` drop_prog i `` X <= X)";
paulson@6837
   379
by Auto_tac;
paulson@6837
   380
qed "modular_equiv";
paulson@6837
   381
paulson@6837
   382
Goal "lift_prog i `` drop_prog i `` (lift_prog i `` F) <= lift_prog i `` F";
paulson@6837
   383
by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 1);
paulson@6837
   384
result();
paulson@6837
   385
paulson@6837
   386
Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
paulson@6837
   387
\        lift_prog i `` drop_prog i `` X <= X;  \
paulson@6837
   388
\        lift_prog i `` drop_prog i `` Y <= Y|] \
paulson@6837
   389
\     ==> lift_prog i F : X guar Y";
paulson@6837
   390
by (full_simp_tac (simpset() addsimps [modular_equiv RS sym]) 1);
paulson@6837
   391
by (rtac guaranteesI 1);
paulson@6837
   392
by (ball_tac 1);
paulson@6837
   393
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   394
by (dtac guaranteesD 1);
paulson@6837
   395
by (rtac image_eqI 1);
paulson@6837
   396
by (assume_tac 2);back();
paulson@6837
   397
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   398
by (ALLGOALS Clarify_tac);
paulson@6837
   399
by (dres_inst_tac [("f", "lift_prog i")] arg_cong 1);
paulson@6837
   400
paulson@6837
   401
by (rtac guaranteesI 1);
paulson@6837
   402
by (dtac guaranteesD 1);
paulson@6837
   403
by (ALLGOALS Clarify_tac);
paulson@6837
   404
by (rtac image_eqI 1);
paulson@6837
   405
by (rtac (drop_prog_lift_prog_Join RS sym) 1);
paulson@6837
   406
by (assume_tac 1);
paulson@6837
   407
by (full_simp_tac (simpset() addsimps [modular_equiv RS sym]) 1);
paulson@6837
   408
by (REPEAT (ball_tac 1));
paulson@6837
   409
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   410
ren "H" 1;
paulson@6837
   411
by (dtac sym 1);
paulson@6837
   412
by (asm_full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   413
????????????????;
paulson@6837
   414
paulson@6837
   415
by Auto_tac;
paulson@6837
   416
paulson@6837
   417
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
paulson@6837
   418
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   419
by (assume_tac 1);
paulson@6837
   420
by (ALLGOALS Clarify_tac);
paulson@6837
   421
by (set_mp_tac 1);
paulson@6837
   422
by (ALLGOALS Clarify_tac);
paulson@6837
   423
by Auto_tac;
paulson@6837
   424
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
paulson@6837
   425
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   426
by Auto_tac;
paulson@6837
   427
qed "drop_prog_guarantees";
paulson@6837
   428
paulson@6837
   429
paulson@6837
   430
paulson@6837
   431
paulson@6837
   432
paulson@6837
   433
paulson@6837
   434
paulson@6837
   435
paulson@6837
   436
Goal "(lift_prog i `` F) <= lift_prog i `` drop_prog i `` (lift_prog i `` F)";
paulson@6837
   437
by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 1);
paulson@6837
   438
by Auto_tac;
paulson@6837
   439
result();
paulson@6837
   440
paulson@6837
   441
paulson@6837
   442
Goal "H : lift_prog i `` drop_prog i `` X";
paulson@6837
   443
paulson@6837
   444
paulson@6837
   445
Goal "[| F : (drop_prog i `` X) guar (drop_prog i `` Y);  \
paulson@6837
   446
\        X <= lift_prog i `` drop_prog i `` X;  \
paulson@6837
   447
\        Y <= lift_prog i `` drop_prog i `` Y |] \
paulson@6837
   448
\     ==> lift_prog i F : X guar Y";
paulson@6837
   449
by (rtac guaranteesI 1);
paulson@6837
   450
by (set_mp_tac 1);
paulson@6837
   451
by (ALLGOALS Clarify_tac);
paulson@6837
   452
by (dtac guaranteesD 1);
paulson@6837
   453
by (rtac image_eqI 1);
paulson@6837
   454
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
paulson@6837
   455
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   456
by (assume_tac 1);
paulson@6837
   457
by (ALLGOALS Clarify_tac);
paulson@6837
   458
by (set_mp_tac 1);
paulson@6837
   459
by (ALLGOALS Clarify_tac);
paulson@6837
   460
by Auto_tac;
paulson@6837
   461
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1);
paulson@6837
   462
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1);
paulson@6837
   463
by Auto_tac;
paulson@6837
   464
qed "drop_prog_guarantees";
paulson@6837
   465
paulson@6837
   466
paulson@6837
   467
paulson@6837
   468
(*FAILS*)
paulson@6837
   469
Goal "modular i (lift_prog i `` Y)";
paulson@6837
   470
paulson@6837
   471
paulson@6837
   472
paulson@6837
   473
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!;
paulson@6837
   474
(*Precondition is TOO STRONG*)
paulson@6837
   475
Goal "Cl : UNIV guar Increasing f \
paulson@6837
   476
\     ==>lift_prog i Cl : (lift_prog i `` UNIV) guar Increasing (f o sub i)";
paulson@6837
   477
by (rtac drop_prog_guarantees 1);
paulson@6837
   478
by (etac guarantees_weaken 1);
paulson@6837
   479
by Auto_tac;
paulson@6837
   480
by (rtac (impOfSubs image_lift_prog_Increasing) 2);
paulson@6837
   481
by (rtac image_eqI 1);
paulson@6837
   482
by (rtac (lift_prog_inverse RS sym) 1);
paulson@6837
   483
by (rtac (impOfSubs image_lift_prog_Increasing) 1);
paulson@6837
   484
by Auto_tac;
paulson@6837
   485
fr imageI;
paulson@6837
   486
paulson@6837
   487
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
   488
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
paulson@6837
   489
paulson@6837
   490
paulson@6837
   491
paulson@6837
   492
paulson@6837
   493
paulson@6837
   494
paulson@6837
   495
Goal "Cl : UNIV guar Increasing f \
paulson@6837
   496
\     ==>lift_prog i Cl : UNIV guar Increasing (f o sub i)";
paulson@6837
   497
by (rtac drop_prog_guarantees 1);
paulson@6837
   498
by (rewtac Increasing_def);
paulson@6837
   499
by (etac guarantees_weaken 1);
paulson@6837
   500
by Auto_tac;
paulson@6837
   501
by (rtac image_eqI 1);
paulson@6837
   502
by (rtac (lift_prog_inverse RS sym) 1);
paulson@6837
   503
by Auto_tac;
paulson@6837
   504
by (stac (lift_set_sub2 RS sym) 1); 
paulson@6837
   505
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable_eq]) 1);
paulson@6837
   506
paulson@6837
   507
paulson@6837
   508
paulson@6837
   509
(*could move to PPROD.ML, but function "sub" is needed there*)
paulson@6837
   510
Goalw [drop_set_def] "drop_set i {s. P (f (sub i s))} = {s. P (f s)}";
paulson@6837
   511
by Auto_tac;
paulson@6837
   512
qed "drop_set_sub";
paulson@6837
   513
paulson@6837
   514
Goal "lift_set i (reachable (drop_prog i F)) = reachable F";
paulson@6837
   515
paulson@6837
   516
(*False?*)
paulson@6837
   517
Goal "modular i ((f o sub i) localTo (lift_prog i F))";
paulson@6837
   518
by (simp_tac (simpset() addsimps [localTo_def, modular_def]) 1);
paulson@6837
   519
by Auto_tac;
paulson@6837
   520
paulson@6837
   521
paulson@6837
   522
paulson@6837
   523
(*FAILS*)
paulson@6837
   524
Goal "(drop_prog i F : A Co B)  =  \
paulson@6837
   525
\     (F : (lift_set i A) Co (lift_set i B))";
paulson@6837
   526
by (simp_tac (simpset() addsimps [Constrains_def, drop_prog_constrains_eq,
paulson@6837
   527
				  lift_set_Int]) 1);
paulson@6837
   528
paulson@6837
   529
??
paulson@6837
   530
by (simp_tac (simpset() addsimps [Constrains_def, reachable_drop_prog,
paulson@6837
   531
				  drop_set_Int RS sym,
paulson@6837
   532
				  drop_prog_constrains_eq]) 1);
paulson@6837
   533
qed "drop_prog_Constrains_eq";
paulson@6837
   534
paulson@6837
   535
(*FAILS*)
paulson@6837
   536
Goal "(drop_prog i F : Stable A)  =  (F : Stable (lift_set i A))";
paulson@6837
   537
by (simp_tac (simpset() addsimps [Stable_def, drop_prog_Constrains_eq]) 1);
paulson@6837
   538
qed "drop_prog_Stable_eq";
paulson@6837
   539
paulson@6837
   540
paulson@6837
   541
(*FAILS*)
paulson@6837
   542
Goal "modular i (Stable {s. P(s i)})";
paulson@6837
   543
by (full_simp_tac (simpset() addsimps [modular_def,
paulson@6837
   544
				       drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   545
by (full_simp_tac (simpset() addsimps [lift_set_sub2 RS sym,
paulson@6828
   546
				      lift_prog_Stable_eq]) 1);
paulson@6837
   547
by Auto_tac;
paulson@6837
   548
paulson@6837
   549
paulson@6837
   550
paulson@6837
   551
Goal "modular i (Increasing (rel o sub i))";
paulson@6837
   552
by (full_simp_tac (simpset() addsimps [modular_def, Increasing_def,
paulson@6837
   553
				       drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   554
paulson@6837
   555
paulson@6837
   556
Goal "modular i (lift_prog i `` X)";
paulson@6837
   557
by (full_simp_tac (simpset() addsimps [modular_def,
paulson@6837
   558
				       drop_prog_lift_prog_Join RS sym]) 1);
paulson@6837
   559
paulson@6828
   560
paulson@6828
   561
paulson@6828
   562
Goal "i < Nclients ==> \
paulson@6837
   563
\     lift_prog i Client : UNIV guar Increasing (rel o sub i)";
paulson@6837
   564
paulson@6837
   565
paulson@6837
   566
paulson@6837
   567
paulson@6837
   568
paulson@6837
   569
paulson@6837
   570
Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
paulson@6837
   571
paulson@6837
   572
paulson@6837
   573
paulson@6837
   574
paulson@6837
   575
paulson@6837
   576
paulson@6837
   577
Goal "(f o sub i) localTo (lift_prog i F) <= lift_prog i `` (f localTo F)";
paulson@6837
   578
by (simp_tac (simpset() addsimps [localTo_def]) 1);
paulson@6837
   579
by Auto_tac;
paulson@6837
   580
by (dres_inst_tac [("x","z")] spec 1);
paulson@6837
   581
by Auto_tac;
paulson@6837
   582
by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym,
paulson@6837
   583
				      lift_prog_stable_eq]) 1);
paulson@6837
   584
qed "image_lift_prog_?";
paulson@6837
   585
paulson@6837
   586
Goal "{GX. EX G: UNIV. lift_prog i G component GX} = UNIV";
paulson@6837
   587
by Auto_tac;
paulson@6837
   588
by (asm_full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
paulson@6837
   589
by (asm_full_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@6837
   590
ren "GX" 1;
paulson@6837
   591
by (res_inst_tac [("x", "mk_program((%f. f i)``(Init GX), drop_act i `` Acts GX)")] exI 1);
paulson@6837
   592
by Auto_tac;
paulson@6837
   593
paulson@6837
   594
paulson@6837
   595
by (stac Acts_eq 1);
paulson@6837
   596
paulson@6837
   597
fr conjI;
paulson@6837
   598
by (Clarify_tac 1);
paulson@6837
   599
by (stac Init_eq 1);
paulson@6837
   600
paulson@6837
   601
paulson@6837
   602
{GX. EX G:X. lift_prog i G component GX}
paulson@6837
   603
{GY. EX G:Y. lift_prog i G component GY}
paulson@6837
   604
paulson@6837
   605
paulson@6837
   606
paulson@6837
   607
uuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuuu;
paulson@6837
   608
paulson@6828
   609
paulson@6828
   610
paulson@6828
   611
paulson@6828
   612
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@6828
   613
by (cut_facts_tac [Client] 1);
paulson@6828
   614
by (full_simp_tac
paulson@6828
   615
    (simpset() addsimps [System_def,
paulson@6828
   616
			 client_spec_def, client_increasing_def,
paulson@6828
   617
			 guarantees_Int_right]) 1);
paulson@6828
   618
by Auto_tac;
paulson@6828
   619
by (dtac lift_prog_guarantees 1);
paulson@6828
   620
by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
paulson@6828
   621
back();
paulson@6828
   622
by (dtac (lessThan_iff RS iffD2 RS PFUN_Increasing RS iffD2) 1);
paulson@6828
   623
by Auto_tac;
paulson@6828
   624
paulson@6828
   625
paulson@6828
   626
by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (PFUN_Increasing RS sym)]) 1);
paulson@6828
   627
paulson@6828
   628
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
paulson@6828
   629
paulson@6828
   630
paulson@6828
   631
Goal "System : system_spec";
paulson@6828
   632
paulson@6828
   633
by (full_simp_tac
paulson@6828
   634
    (simpset() addsimps [alloc_spec_def, alloc_safety_def, System_def]) 1);
paulson@6828
   635
paulson@6828
   636
paulson@6828
   637
paulson@6828
   638
paulson@6828
   639
paulson@6828
   640
paulson@6828
   641
(*partial system...*)
paulson@6828
   642
Goal "[| Alloc : alloc_spec;  Network : network_spec |] \
paulson@6828
   643
\     ==> (extend sysOfAlloc Alloc) Join Network : system_spec";
paulson@6828
   644
paulson@6828
   645
(*partial system...*)
paulson@6828
   646
Goal "[| Client : client_spec;  Network : network_spec |] \
paulson@6828
   647
\     ==> (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
paulson@6828
   648
\         Join Network : system_spec";
paulson@6828
   649
paulson@6828
   650
paulson@6828
   651
paulson@6828
   652
Goal "[| Alloc : alloc_spec;  Client : client_spec;  \
paulson@6828
   653
\        Network : network_spec |] \
paulson@6828
   654
\     ==> (extend sysOfAlloc Alloc) \
paulson@6828
   655
\         Join (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
paulson@6828
   656
\         Join Network : system_spec";
paulson@6828
   657
by (full_simp_tac
paulson@6828
   658
    (simpset() addsimps [system_spec_def, system_safety_def]) 1);
paulson@6828
   659
by Auto_tac;
paulson@6828
   660
by (full_simp_tac
paulson@6828
   661
    (simpset() addsimps [client_spec_def, client_increasing_def,
paulson@6828
   662
			 guarantees_Int_right]) 1);
paulson@6828
   663
by Auto_tac;
paulson@6828
   664
by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
paulson@6828
   665
back();
paulson@6828
   666
by (full_simp_tac
paulson@6828
   667
    (simpset() addsimps [network_spec_def, network_rel_def]) 1);
paulson@6828
   668
paulson@6828
   669
by (subgoal_tac "" 1);
paulson@6828
   670
by (full_simp_tac
paulson@6828
   671
    (simpset() addsimps [alloc_spec_def, alloc_safety_def]) 1);
paulson@6828
   672
by Auto_tac;
paulson@6828
   673
paulson@6828
   674
by (Simp_tac 1);
paulson@6828
   675
paulson@6828
   676
paulson@6828
   677
paulson@6828
   678
paulson@6828
   679
(*Generalized version allowing different clients*)
paulson@6828
   680
Goal "[| Alloc : alloc_spec;  \
paulson@6828
   681
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6828
   682
\        Network : network_spec |] \
paulson@6828
   683
\     ==> (extend sysOfAlloc Alloc) \
paulson@6828
   684
\         Join (extend sysOfClient (PPROD (lessThan Nclients) Client)) \
paulson@6828
   685
\         Join Network : system_spec";
paulson@6828
   686