src/HOL/UNITY/Lift_prog.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7688 d106cad8f515
child 7840 e1fd12b864a1
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
paulson@7186
     1
(*  Title:      HOL/UNITY/Lift_prog.ML
paulson@7186
     2
    ID:         $Id$
paulson@7186
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7186
     4
    Copyright   1998  University of Cambridge
paulson@7482
     5
paulson@7826
     6
Arrays of processes.  Many results are instances of those in Extend & Project.
paulson@7186
     7
*)
paulson@7186
     8
paulson@7186
     9
paulson@7186
    10
(*** Basic properties ***)
paulson@7186
    11
paulson@7186
    12
(** lift_set and drop_set **)
paulson@7186
    13
paulson@7186
    14
Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)";
paulson@7186
    15
by Auto_tac;
paulson@7186
    16
qed "lift_set_iff";
paulson@7186
    17
AddIffs [lift_set_iff];
paulson@7186
    18
paulson@7525
    19
Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)";
paulson@7525
    20
by Auto_tac;
paulson@7525
    21
qed "Int_lift_set";
paulson@7525
    22
paulson@7525
    23
Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)";
paulson@7186
    24
by Auto_tac;
paulson@7525
    25
qed "Un_lift_set";
paulson@7525
    26
paulson@7525
    27
Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)";
paulson@7525
    28
by Auto_tac;
paulson@7525
    29
qed "Diff_lift_set";
paulson@7525
    30
paulson@7525
    31
Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
paulson@7186
    32
paulson@7186
    33
(*Converse fails*)
paulson@7186
    34
Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
paulson@7186
    35
by Auto_tac;
paulson@7186
    36
qed "drop_set_I";
paulson@7186
    37
paulson@7186
    38
(** lift_act and drop_act **)
paulson@7186
    39
paulson@7186
    40
Goalw [lift_act_def] "lift_act i Id = Id";
paulson@7186
    41
by Auto_tac;
paulson@7186
    42
by (etac rev_mp 1);
paulson@7186
    43
by (dtac sym 1);
paulson@7186
    44
by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
paulson@7186
    45
qed "lift_act_Id";
paulson@7186
    46
Addsimps [lift_act_Id];
paulson@7186
    47
paulson@7688
    48
(*For compatibility with the original definition and perhaps simpler proofs*)
paulson@7688
    49
Goalw [lift_act_def]
paulson@7688
    50
    "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
paulson@7688
    51
by Auto_tac;
paulson@7688
    52
by (rtac exI 1);
paulson@7688
    53
by Auto_tac;
paulson@7688
    54
qed "lift_act_eq";
paulson@7688
    55
AddIffs [lift_act_eq];
paulson@7688
    56
paulson@7688
    57
Goalw [drop_act_def]
paulson@7688
    58
     "[| (s, s') : act;  s : C |] ==> (s i, s' i) : drop_act C i act";
paulson@7688
    59
by Auto_tac;
paulson@7186
    60
qed "drop_act_I";
paulson@7186
    61
paulson@7688
    62
Goalw [drop_set_def, drop_act_def]
paulson@7688
    63
     "UNIV <= drop_set i C ==> drop_act C i Id = Id";
paulson@7688
    64
by (Blast_tac 1);
paulson@7186
    65
qed "drop_act_Id";
paulson@7186
    66
Addsimps [drop_act_Id];
paulson@7186
    67
paulson@7186
    68
(** lift_prog and drop_prog **)
paulson@7186
    69
paulson@7186
    70
Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
paulson@7186
    71
by Auto_tac;
paulson@7186
    72
qed "Init_lift_prog";
paulson@7186
    73
Addsimps [Init_lift_prog];
paulson@7186
    74
paulson@7186
    75
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
paulson@7186
    76
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
paulson@7186
    77
qed "Acts_lift_prog";
paulson@7186
    78
Addsimps [Acts_lift_prog];
paulson@7186
    79
paulson@7688
    80
Goalw [drop_prog_def] "Init (drop_prog C i F) = drop_set i (Init F)";
paulson@7186
    81
by Auto_tac;
paulson@7186
    82
qed "Init_drop_prog";
paulson@7186
    83
Addsimps [Init_drop_prog];
paulson@7186
    84
paulson@7688
    85
Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
paulson@7688
    86
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
paulson@7688
    87
	      simpset() addsimps [drop_prog_def]));
paulson@7186
    88
qed "Acts_drop_prog";
paulson@7186
    89
Addsimps [Acts_drop_prog];
paulson@7186
    90
paulson@7688
    91
paulson@7688
    92
(*** sub ***)
paulson@7688
    93
paulson@7688
    94
Addsimps [sub_def];
paulson@7688
    95
paulson@7688
    96
Goal "lift_set i {s. P s} = {s. P (sub i s)}";
paulson@7688
    97
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@7688
    98
qed "lift_set_sub";
paulson@7343
    99
paulson@7688
   100
Goal "{s. P (s i)} = lift_set i {s. P s}";
paulson@7688
   101
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@7688
   102
qed "Collect_eq_lift_set";
paulson@7186
   103
paulson@7688
   104
Goal "sub i -`` A = lift_set i A";
paulson@7688
   105
by (Force_tac 1);
paulson@7688
   106
qed "sub_vimage";
paulson@7688
   107
Addsimps [sub_vimage];
paulson@7688
   108
paulson@7688
   109
paulson@7688
   110
paulson@7688
   111
(*** lift_prog and the lattice operations ***)
paulson@7186
   112
paulson@7186
   113
Goal "lift_prog i SKIP = SKIP";
paulson@7186
   114
by (auto_tac (claset() addSIs [program_equalityI],
paulson@7186
   115
	      simpset() addsimps [SKIP_def, lift_prog_def]));
paulson@7186
   116
qed "lift_prog_SKIP";
paulson@7186
   117
paulson@7186
   118
Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)";
paulson@7186
   119
by (rtac program_equalityI 1);
paulson@7537
   120
by Auto_tac;
paulson@7186
   121
qed "lift_prog_Join";
paulson@7186
   122
paulson@7525
   123
Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))";
paulson@7186
   124
by (rtac program_equalityI 1);
paulson@7537
   125
by Auto_tac;
paulson@7186
   126
qed "lift_prog_JN";
paulson@7186
   127
paulson@7186
   128
paulson@7525
   129
(*** Equivalence with "extend" version ***)
paulson@7525
   130
paulson@7525
   131
Goalw [lift_map_def] "good_map (lift_map i)";
paulson@7525
   132
by (rtac good_mapI 1);
paulson@7525
   133
by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1);
paulson@7525
   134
by Auto_tac;
paulson@7525
   135
by (dres_inst_tac [("f", "%f. f i")] arg_cong 1);
paulson@7525
   136
by Auto_tac;
paulson@7525
   137
qed "good_map_lift_map";
paulson@7525
   138
paulson@7525
   139
fun lift_export th = good_map_lift_map RS export th;
paulson@7525
   140
paulson@7525
   141
Goal "fst (inv (lift_map i) g) = g i";
paulson@7525
   142
by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1);
paulson@7525
   143
by (auto_tac (claset(), simpset() addsimps [lift_map_def]));
paulson@7525
   144
qed "fst_inv_lift_map";
paulson@7525
   145
Addsimps [fst_inv_lift_map];
paulson@7525
   146
paulson@7525
   147
paulson@7525
   148
Goal "lift_set i A = extend_set (lift_map i) A";
paulson@7525
   149
by (auto_tac (claset(), 
paulson@7525
   150
     simpset() addsimps [lift_export mem_extend_set_iff]));
paulson@7525
   151
qed "lift_set_correct";
paulson@7525
   152
paulson@7525
   153
Goalw [drop_set_def, project_set_def, lift_map_def]
paulson@7525
   154
     "drop_set i A = project_set (lift_map i) A";
paulson@7525
   155
by Auto_tac;
paulson@7525
   156
by (rtac image_eqI 2);
paulson@7525
   157
by (rtac exI 1);
paulson@7525
   158
by (stac (refl RS fun_upd_idem) 1);
paulson@7525
   159
by Auto_tac;
paulson@7525
   160
qed "drop_set_correct";
paulson@7525
   161
paulson@7525
   162
Goal "lift_act i = extend_act (lift_map i)";
paulson@7525
   163
by (rtac ext 1);
paulson@7525
   164
by Auto_tac;
paulson@7525
   165
by (forward_tac [lift_export extend_act_D] 2);
paulson@7688
   166
by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
paulson@7525
   167
by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
paulson@7525
   168
by (rtac bexI 1);
paulson@7525
   169
by (auto_tac (claset() addSIs [exI], simpset()));
paulson@7525
   170
qed "lift_act_correct";
paulson@7525
   171
paulson@7688
   172
Goal "drop_act C i = project_act C (lift_map i)";
paulson@7525
   173
by (rtac ext 1);
paulson@7525
   174
by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
paulson@7525
   175
by Auto_tac;
paulson@7688
   176
by (REPEAT_FIRST (ares_tac [exI, conjI]));
paulson@7525
   177
by Auto_tac;
paulson@7688
   178
by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem)));
paulson@7525
   179
qed "drop_act_correct";
paulson@7525
   180
paulson@7688
   181
Goal "lift_prog i = extend (lift_map i)";
paulson@7688
   182
by (rtac (program_equalityI RS ext) 1);
paulson@7525
   183
by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
paulson@7525
   184
by (simp_tac (simpset() 
paulson@7525
   185
	      addsimps [lift_export Acts_extend, 
paulson@7525
   186
			lift_act_correct]) 1);
paulson@7525
   187
qed "lift_prog_correct";
paulson@7525
   188
paulson@7688
   189
Goal "drop_prog C i = project C (lift_map i)";
paulson@7688
   190
by (rtac (program_equalityI RS ext) 1);
paulson@7525
   191
by (simp_tac (simpset() addsimps [drop_set_correct]) 1);
paulson@7525
   192
by (simp_tac (simpset() 
paulson@7547
   193
	      addsimps [Acts_project, drop_act_correct]) 1);
paulson@7525
   194
qed "drop_prog_correct";
paulson@7525
   195
paulson@7525
   196
paulson@7688
   197
(** Injectivity of lift_set, lift_act, lift_prog **)
paulson@7688
   198
paulson@7688
   199
Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F";
paulson@7688
   200
by Auto_tac;
paulson@7688
   201
qed "lift_set_inverse";
paulson@7688
   202
Addsimps [lift_set_inverse];
paulson@7688
   203
paulson@7688
   204
Goal "inj (lift_set i)";
paulson@7688
   205
by (rtac inj_on_inverseI 1);
paulson@7688
   206
by (rtac lift_set_inverse 1);
paulson@7688
   207
qed "inj_lift_set";
paulson@7688
   208
paulson@7688
   209
(*Because A and B could differ outside i, cannot generalize result to 
paulson@7688
   210
   drop_set i (A Int B) = drop_set i A Int drop_set i B
paulson@7688
   211
*)
paulson@7688
   212
Goalw [lift_set_def, drop_set_def]
paulson@7688
   213
     "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)";
paulson@7688
   214
by Auto_tac;
paulson@7688
   215
qed "drop_set_Int_lift_set";
paulson@7688
   216
paulson@7688
   217
Goalw [lift_set_def, drop_set_def]
paulson@7688
   218
     "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A";
paulson@7688
   219
by Auto_tac;
paulson@7688
   220
qed "drop_set_Int_lift_set2";
paulson@7688
   221
paulson@7688
   222
Goalw [drop_set_def]
paulson@7688
   223
     "i : I ==> drop_set i (INT j:I. lift_set j A) = A";
paulson@7688
   224
by Auto_tac;
paulson@7688
   225
qed "drop_set_INT";
paulson@7688
   226
paulson@7688
   227
Goal "lift_set i UNIV = UNIV";
paulson@7688
   228
by (simp_tac
paulson@7688
   229
    (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
paulson@7688
   230
qed "lift_set_UNIV_eq";
paulson@7688
   231
Addsimps [lift_set_UNIV_eq];
paulson@7688
   232
paulson@7688
   233
Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
paulson@7688
   234
by (asm_full_simp_tac
paulson@7688
   235
    (simpset() addsimps [drop_set_correct, drop_act_correct, 
paulson@7688
   236
			 lift_act_correct, lift_export extend_act_inverse]) 1);
paulson@7688
   237
qed "lift_act_inverse";
paulson@7688
   238
Addsimps [lift_act_inverse];
paulson@7688
   239
paulson@7688
   240
Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
paulson@7688
   241
by (asm_full_simp_tac
paulson@7688
   242
    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
paulson@7688
   243
			 lift_prog_correct, lift_export extend_inverse]) 1);
paulson@7688
   244
qed "lift_prog_inverse";
paulson@7688
   245
Addsimps [lift_prog_inverse];
paulson@7688
   246
paulson@7688
   247
Goal "inj (lift_prog i)";
paulson@7688
   248
by (simp_tac
paulson@7688
   249
    (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
paulson@7688
   250
qed "inj_lift_prog";
paulson@7688
   251
paulson@7688
   252
paulson@7525
   253
(*** More Lemmas ***)
paulson@7525
   254
paulson@7525
   255
Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
paulson@7525
   256
by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
paulson@7525
   257
				      lift_export extend_act_Image]) 1);
paulson@7525
   258
qed "lift_act_Image";
paulson@7525
   259
Addsimps [lift_act_Image];
paulson@7525
   260
paulson@7525
   261
paulson@7525
   262
paulson@7186
   263
(*** Safety: co, stable, invariant ***)
paulson@7186
   264
paulson@7186
   265
(** Safety and lift_prog **)
paulson@7186
   266
paulson@7186
   267
Goal "(lift_prog i F : (lift_set i A) co (lift_set i B))  =  \
paulson@7186
   268
\     (F : A co B)";
paulson@7186
   269
by (auto_tac (claset(), 
paulson@7186
   270
	      simpset() addsimps [constrains_def]));
paulson@7186
   271
by (Force_tac 1);
paulson@7343
   272
qed "lift_prog_constrains";
paulson@7186
   273
paulson@7186
   274
Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)";
paulson@7343
   275
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1);
paulson@7343
   276
qed "lift_prog_stable";
paulson@7186
   277
paulson@7186
   278
Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
paulson@7186
   279
by (auto_tac (claset(),
paulson@7343
   280
	      simpset() addsimps [invariant_def, lift_prog_stable]));
paulson@7343
   281
qed "lift_prog_invariant";
paulson@7186
   282
paulson@7826
   283
Goal "[| lift_prog i F : A co B |] \
paulson@7826
   284
\     ==> F : (drop_set i A) co (drop_set i B)";
paulson@7826
   285
by (asm_full_simp_tac
paulson@7826
   286
    (simpset() addsimps [drop_set_correct, lift_prog_correct, 
paulson@7826
   287
			 lift_export extend_constrains_project_set]) 1);
paulson@7826
   288
qed "lift_prog_constrains_drop_set";
paulson@7826
   289
paulson@7186
   290
(*This one looks strange!  Proof probably is by case analysis on i=j.
paulson@7186
   291
  If i~=j then lift_prog j (F j) does nothing to lift_set i, and the 
paulson@7186
   292
  premise ensures A<=B.*)
paulson@7186
   293
Goal "F i : A co B  \
paulson@7186
   294
\     ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)";
paulson@7186
   295
by (auto_tac (claset(), 
paulson@7186
   296
	      simpset() addsimps [constrains_def]));
paulson@7186
   297
by (REPEAT (Blast_tac 1));
paulson@7186
   298
qed "constrains_imp_lift_prog_constrains";
paulson@7186
   299
paulson@7186
   300
paulson@7186
   301
(** Safety and drop_prog **)
paulson@7186
   302
paulson@7688
   303
Goal "(drop_prog C i F : A co B)  =  \
paulson@7688
   304
\     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
paulson@7688
   305
by (simp_tac
paulson@7688
   306
    (simpset() addsimps [drop_prog_correct, 
paulson@7688
   307
			 lift_set_correct, lift_export project_constrains]) 1);
paulson@7343
   308
qed "drop_prog_constrains";
paulson@7186
   309
paulson@7688
   310
Goal "(drop_prog UNIV i F : stable A)  =  (F : stable (lift_set i A))";
paulson@7343
   311
by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1);
paulson@7343
   312
qed "drop_prog_stable";
paulson@7186
   313
paulson@7186
   314
paulson@7343
   315
(*** Diff, needed for localTo ***)
paulson@7186
   316
paulson@7688
   317
Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
paulson@7688
   318
\        Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |]  \
paulson@7688
   319
\     ==> Diff (drop_prog C i G) acts : A co B";
paulson@7688
   320
by (asm_full_simp_tac
paulson@7688
   321
    (simpset() addsimps [drop_set_correct, drop_prog_correct, 
paulson@7688
   322
			 lift_set_correct, lift_act_correct, 
paulson@7826
   323
			 lift_export Diff_project_constrains]) 1);
paulson@7826
   324
qed "Diff_drop_prog_constrains";
paulson@7186
   325
paulson@7186
   326
Goalw [stable_def]
paulson@7688
   327
     "[| (UN act:acts. Domain act) <= drop_set i C; \
paulson@7688
   328
\        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
paulson@7688
   329
\     ==> Diff (drop_prog C i G) acts : stable A";
paulson@7826
   330
by (etac Diff_drop_prog_constrains 1);
paulson@7688
   331
by (assume_tac 1);
paulson@7186
   332
qed "Diff_drop_prog_stable";
paulson@7186
   333
paulson@7343
   334
Goalw [constrains_def, Diff_def]
paulson@7688
   335
     "Diff G acts : A co B  \
paulson@7688
   336
\     ==> Diff (lift_prog i G) (lift_act i `` acts) \
paulson@7186
   337
\         : (lift_set i A) co (lift_set i B)";
paulson@7343
   338
by Auto_tac;
paulson@7343
   339
by (Blast_tac 1);
paulson@7186
   340
qed "Diff_lift_prog_co";
paulson@7186
   341
paulson@7186
   342
Goalw [stable_def]
paulson@7688
   343
     "Diff G acts : stable A  \
paulson@7688
   344
\     ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
paulson@7186
   345
by (etac Diff_lift_prog_co 1);
paulson@7186
   346
qed "Diff_lift_prog_stable";
paulson@7186
   347
paulson@7186
   348
paulson@7343
   349
(*** Weak safety primitives: Co, Stable ***)
paulson@7186
   350
paulson@7186
   351
(** Reachability **)
paulson@7186
   352
paulson@7186
   353
Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
paulson@7688
   354
by (simp_tac
paulson@7688
   355
    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
paulson@7688
   356
			 lift_export reachable_extend_eq]) 1);
paulson@7186
   357
qed "reachable_lift_prog";
paulson@7186
   358
paulson@7186
   359
Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
paulson@7186
   360
\     (F : A Co B)";
paulson@7186
   361
by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
paulson@7343
   362
				  lift_prog_constrains]) 1);
paulson@7343
   363
qed "lift_prog_Constrains";
paulson@7186
   364
paulson@7186
   365
Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
paulson@7343
   366
by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1);
paulson@7343
   367
qed "lift_prog_Stable";
paulson@7186
   368
paulson@7688
   369
Goal "[| reachable (lift_prog i F Join G) <= C;    \
paulson@7688
   370
\        F Join drop_prog C i G : A Co B |] \
paulson@7688
   371
\     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
paulson@7688
   372
by (asm_full_simp_tac
paulson@7688
   373
    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
paulson@7688
   374
		     lift_set_correct, lift_export project_Constrains_D]) 1);
paulson@7186
   375
qed "drop_prog_Constrains_D";
paulson@7186
   376
paulson@7186
   377
Goalw [Stable_def]
paulson@7688
   378
     "[| reachable (lift_prog i F Join G) <= C;    \
paulson@7688
   379
\        F Join drop_prog C i G : Stable A |]  \
paulson@7688
   380
\     ==> lift_prog i F Join G : Stable (lift_set i A)";
paulson@7186
   381
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1);
paulson@7186
   382
qed "drop_prog_Stable_D";
paulson@7186
   383
paulson@7688
   384
Goal "[| reachable (lift_prog i F Join G) <= C;  \
paulson@7688
   385
\        F Join drop_prog C i G : Always A |]   \
paulson@7688
   386
\     ==> lift_prog i F Join G : Always (lift_set i A)";
paulson@7688
   387
by (asm_full_simp_tac
paulson@7688
   388
    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
paulson@7688
   389
		     lift_set_correct, lift_export project_Always_D]) 1);
paulson@7688
   390
qed "drop_prog_Always_D";
paulson@7186
   391
paulson@7688
   392
Goalw [Increasing_def]
paulson@7688
   393
     "[| reachable (lift_prog i F Join G) <= C;  \
paulson@7688
   394
\        F Join drop_prog C i G : Increasing func |] \
paulson@7688
   395
\     ==> lift_prog i F Join G : Increasing (func o (sub i))";
paulson@7186
   396
by Auto_tac;
paulson@7688
   397
by (stac Collect_eq_lift_set 1);
paulson@7688
   398
by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); 
paulson@7688
   399
qed "project_Increasing_D";
paulson@7186
   400
paulson@7361
   401
paulson@7688
   402
(*UNUSED*)
paulson@7688
   403
Goal "UNIV <= drop_set i C \
paulson@7688
   404
\     ==> drop_prog C i ((lift_prog i F) Join G) = F Join (drop_prog C i G)";
paulson@7688
   405
by (asm_full_simp_tac
paulson@7688
   406
    (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
paulson@7688
   407
		     drop_set_correct, lift_export project_extend_Join]) 1);
paulson@7688
   408
qed "drop_prog_lift_prog_Join";
paulson@7186
   409
paulson@7186
   410
paulson@7525
   411
(*** Progress: transient, ensures ***)
paulson@7525
   412
paulson@7525
   413
Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
paulson@7525
   414
by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
paulson@7525
   415
			  lift_export extend_transient]) 1);
paulson@7525
   416
qed "lift_prog_transient";
paulson@7525
   417
paulson@7525
   418
Goal "(lift_prog i F : transient (lift_set j A)) = \
paulson@7525
   419
\     (i=j & F : transient A | A={})";
paulson@7525
   420
by (case_tac "i=j" 1);
paulson@7525
   421
by (auto_tac (claset(), simpset() addsimps [lift_prog_transient]));
paulson@7525
   422
by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def]));
paulson@7525
   423
by (Force_tac 1);
paulson@7525
   424
qed "lift_prog_transient_eq_disj";
paulson@7525
   425
paulson@7525
   426
paulson@7186
   427
(*** guarantees properties ***)
paulson@7186
   428
paulson@7688
   429
val [xguary,project,lift_prog] =
paulson@7361
   430
Goal "[| F : X guarantees Y;  \
paulson@7688
   431
\        !!G. lift_prog i F Join G : X' ==> F Join proj G : X;  \
paulson@7688
   432
\        !!G. [| F Join proj G : Y; lift_prog i F Join G : X'; \
paulson@7688
   433
\                Disjoint (lift_prog i F) G |] \
paulson@7688
   434
\             ==> lift_prog i F Join G : Y' |] \
paulson@7688
   435
\     ==> lift_prog i F : X' guarantees Y'";
paulson@7343
   436
by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
paulson@7688
   437
by (etac project 1);
paulson@7688
   438
by (assume_tac 1);
paulson@7688
   439
by (assume_tac 1);
paulson@7186
   440
qed "drop_prog_guarantees";
paulson@7186
   441
paulson@7186
   442
paulson@7186
   443
(** Are these two useful?? **)
paulson@7186
   444
paulson@7186
   445
(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not
paulson@7186
   446
  ensure that F has the form lift_prog i F for some F.*)
paulson@7186
   447
Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}";
paulson@7186
   448
by Auto_tac;
paulson@7186
   449
by (stac Collect_eq_lift_set 1); 
paulson@7343
   450
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1);
paulson@7186
   451
qed "image_lift_prog_Stable";
paulson@7186
   452
paulson@7186
   453
Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
paulson@7186
   454
by (simp_tac (simpset() addsimps [Increasing_def,
paulson@7186
   455
				  inj_lift_prog RS image_INT]) 1);
paulson@7186
   456
by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1);
paulson@7186
   457
qed "image_lift_prog_Increasing";
paulson@7186
   458
paulson@7186
   459
paulson@7186
   460
(*** guarantees corollaries ***)
paulson@7186
   461
paulson@7688
   462
Goal "F : UNIV guarantees increasing f \
paulson@7361
   463
\     ==> lift_prog i F : UNIV guarantees increasing (f o sub i)";
paulson@7688
   464
by (dtac (lift_export extend_guar_increasing) 1);
paulson@7688
   465
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
paulson@7186
   466
qed "lift_prog_guar_increasing";
paulson@7186
   467
paulson@7688
   468
Goal "F : UNIV guarantees Increasing f \
paulson@7361
   469
\     ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)";
paulson@7688
   470
by (dtac (lift_export extend_guar_Increasing) 1);
paulson@7688
   471
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
paulson@7186
   472
qed "lift_prog_guar_Increasing";
paulson@7186
   473
paulson@7688
   474
Goal "F : (v localTo G) guarantees increasing func  \
paulson@7688
   475
\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
paulson@7688
   476
\                         guarantees increasing (func o sub i)";
paulson@7688
   477
by (dtac (lift_export extend_localTo_guar_increasing) 1);
paulson@7688
   478
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
paulson@7343
   479
qed "lift_prog_localTo_guar_increasing";
paulson@7186
   480
paulson@7688
   481
Goal "F : (v localTo G) guarantees Increasing func  \
paulson@7688
   482
\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
paulson@7688
   483
\                         guarantees Increasing (func o sub i)";
paulson@7688
   484
by (dtac (lift_export extend_localTo_guar_Increasing) 1);
paulson@7688
   485
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
paulson@7343
   486
qed "lift_prog_localTo_guar_Increasing";
paulson@7186
   487
paulson@7688
   488
Goal "F : Always A guarantees Always B \
paulson@7688
   489
\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
paulson@7688
   490
by (asm_simp_tac
paulson@7688
   491
    (simpset() addsimps [lift_set_correct, lift_prog_correct, 
paulson@7688
   492
			 lift_export extend_guar_Always]) 1);
paulson@7688
   493
qed "lift_prog_guar_Always";