src/HOL/UNITY/Extend.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7878 43b03d412b82
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
paulson@6297
     1
(*  Title:      HOL/UNITY/Extend.ML
paulson@6297
     2
    ID:         $Id$
paulson@6297
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6297
     4
    Copyright   1999  University of Cambridge
paulson@6297
     5
paulson@6297
     6
Extending of state sets
paulson@6297
     7
  function f (forget)    maps the extended state to the original state
paulson@6297
     8
  function g (forgotten) maps the extended state to the "extending part"
paulson@7482
     9
*)
paulson@7362
    10
paulson@7482
    11
(** These we prove OUTSIDE the locale. **)
paulson@7482
    12
paulson@7482
    13
(*Possibly easier than reasoning about "inv h"*)
paulson@7482
    14
val [surj_h,prem] = 
paulson@7482
    15
Goalw [good_map_def]
paulson@7482
    16
     "[| surj h; !! x x' y y'. h(x,y) = h(x',y') ==> x=x' |] ==> good_map h";
paulson@7482
    17
by (safe_tac (claset() addSIs [surj_h]));
paulson@7482
    18
by (rtac prem 1);
paulson@7482
    19
by (stac (surjective_pairing RS sym) 1);
paulson@7482
    20
by (stac (surj_h RS surj_f_inv_f) 1);
paulson@7482
    21
by (rtac refl 1);
paulson@7482
    22
qed "good_mapI";
paulson@7482
    23
paulson@7482
    24
Goalw [good_map_def] "good_map h ==> surj h";
paulson@7482
    25
by Auto_tac;
paulson@7482
    26
qed "good_map_is_surj";
paulson@7482
    27
paulson@7482
    28
(*A convenient way of finding a closed form for inv h*)
paulson@7482
    29
val [surj,prem] = Goalw [inv_def]
paulson@7482
    30
     "[| surj h;  !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z";
paulson@7482
    31
by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1);
wenzelm@7499
    32
by (rtac selectI2 1);
paulson@7482
    33
by (dres_inst_tac [("f", "g")] arg_cong 2);
paulson@7482
    34
by (auto_tac (claset(), simpset() addsimps [prem]));
paulson@7482
    35
qed "fst_inv_equalityI";
paulson@7482
    36
paulson@6297
    37
paulson@6297
    38
Open_locale "Extend";
paulson@6297
    39
paulson@6297
    40
val slice_def = thm "slice_def";
paulson@6297
    41
paulson@6297
    42
(*** Trivial properties of f, g, h ***)
paulson@6297
    43
paulson@7482
    44
val good_h = rewrite_rule [good_map_def] (thm "good_h");
paulson@7482
    45
val surj_h = good_h RS conjunct1;
paulson@6297
    46
paulson@6297
    47
val f_def = thm "f_def";
paulson@6297
    48
val g_def = thm "g_def";
paulson@6297
    49
paulson@6297
    50
Goal "f(h(x,y)) = x";
paulson@7482
    51
by (simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
paulson@6297
    52
qed "f_h_eq";
paulson@6297
    53
Addsimps [f_h_eq];
paulson@6297
    54
paulson@7482
    55
Goal "h(x,y) = h(x',y') ==> x=x'";
paulson@7482
    56
by (dres_inst_tac [("f", "fst o inv h")] arg_cong 1);
paulson@7482
    57
(*FIXME: If locales worked properly we could put just "f" above*)
paulson@7482
    58
by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
paulson@7482
    59
qed "h_inject1";
paulson@7482
    60
AddSDs [h_inject1];
paulson@6297
    61
paulson@6297
    62
Goal "h(f z, g z) = z";
paulson@7482
    63
by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym,
paulson@7482
    64
				  surj_h RS surj_f_inv_f]) 1);
paulson@6297
    65
qed "h_f_g_eq";
paulson@6297
    66
paulson@6297
    67
(*** extend_set: basic properties ***)
paulson@6297
    68
paulson@7594
    69
Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
paulson@7594
    70
by (Blast_tac 1);
paulson@7594
    71
qed "extend_set_mono";
paulson@7594
    72
paulson@7826
    73
Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
paulson@7341
    74
by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
paulson@6297
    75
qed "mem_extend_set_iff";
paulson@6297
    76
AddIffs [mem_extend_set_iff]; 
paulson@6297
    77
paulson@7826
    78
Goalw [extend_set_def]
paulson@7826
    79
    "(extend_set h A <= extend_set h B) = (A <= B)";
paulson@7826
    80
by (Force_tac 1);
paulson@7826
    81
qed "extend_set_strict_mono";
paulson@7826
    82
AddIffs [extend_set_strict_mono];
paulson@7826
    83
paulson@7378
    84
Goal "{s. P (f s)} = extend_set h {s. P s}";
paulson@7378
    85
by Auto_tac;
paulson@7378
    86
qed "Collect_eq_extend_set";
paulson@7378
    87
paulson@7594
    88
Goal "extend_set h {x} = {s. f s = x}";
paulson@7594
    89
by Auto_tac;
paulson@7594
    90
qed "extend_set_sing";
paulson@7594
    91
paulson@7537
    92
Goalw [extend_set_def, project_set_def]
paulson@7660
    93
     "project_set h (extend_set h C) = C";
paulson@7341
    94
by Auto_tac;
paulson@7341
    95
qed "extend_set_inverse";
paulson@7341
    96
Addsimps [extend_set_inverse];
paulson@7341
    97
paulson@6297
    98
Goal "inj (extend_set h)";
paulson@7341
    99
by (rtac inj_on_inverseI 1);
paulson@7341
   100
by (rtac extend_set_inverse 1);
paulson@6297
   101
qed "inj_extend_set";
paulson@6297
   102
paulson@7689
   103
Goalw [extend_set_def] "extend_set h UNIV = UNIV";
paulson@7689
   104
by Auto_tac;
paulson@7689
   105
by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
paulson@7689
   106
by Auto_tac;
paulson@7689
   107
qed "extend_set_UNIV_eq";
paulson@7689
   108
Addsimps [standard extend_set_UNIV_eq];
paulson@7689
   109
paulson@7482
   110
(*** project_set: basic properties ***)
paulson@7482
   111
paulson@7482
   112
(*project_set is simply image!*)
paulson@7482
   113
Goalw [project_set_def] "project_set h C = f `` C";
paulson@7482
   114
by (auto_tac (claset() addIs [f_h_eq RS sym, h_f_g_eq RS ssubst], 
paulson@7482
   115
	      simpset()));
paulson@7482
   116
qed "project_set_eq";
paulson@7482
   117
paulson@7482
   118
(*Converse appears to fail*)
paulson@7482
   119
Goalw [project_set_def] "z : C ==> f z : project_set h C";
paulson@7482
   120
by (auto_tac (claset() addIs [h_f_g_eq RS ssubst], 
paulson@7482
   121
	      simpset()));
paulson@7482
   122
qed "project_set_I";
paulson@7482
   123
paulson@7482
   124
paulson@7482
   125
(*** More laws ***)
paulson@7482
   126
paulson@7341
   127
(*Because A and B could differ on the "other" part of the state, 
paulson@7341
   128
   cannot generalize result to 
paulson@7341
   129
      project_set h (A Int B) = project_set h A Int project_set h B
paulson@7341
   130
*)
paulson@7341
   131
Goalw [project_set_def]
paulson@7341
   132
     "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
paulson@7341
   133
by Auto_tac;
paulson@7341
   134
qed "project_set_extend_set_Int";
paulson@7341
   135
paulson@7341
   136
Goal "extend_set h (A Un B) = extend_set h A Un extend_set h B";
paulson@6297
   137
by Auto_tac;
paulson@6297
   138
qed "extend_set_Un_distrib";
paulson@6297
   139
paulson@7341
   140
Goal "extend_set h (A Int B) = extend_set h A Int extend_set h B";
paulson@6297
   141
by Auto_tac;
paulson@6297
   142
qed "extend_set_Int_distrib";
paulson@6297
   143
paulson@7341
   144
Goal "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))";
paulson@7341
   145
by Auto_tac;
paulson@6834
   146
qed "extend_set_INT_distrib";
paulson@6647
   147
paulson@7341
   148
Goal "extend_set h (A - B) = extend_set h A - extend_set h B";
paulson@6297
   149
by Auto_tac;
paulson@6297
   150
qed "extend_set_Diff_distrib";
paulson@6297
   151
paulson@7341
   152
Goal "extend_set h (Union A) = (UN X:A. extend_set h X)";
paulson@6297
   153
by (Blast_tac 1);
paulson@6297
   154
qed "extend_set_Union";
paulson@6297
   155
paulson@7341
   156
Goalw [extend_set_def] "(extend_set h A <= - extend_set h B) = (A <= - B)";
paulson@6297
   157
by Auto_tac;
paulson@6297
   158
qed "extend_set_subset_Compl_eq";
paulson@6297
   159
paulson@7341
   160
paulson@6297
   161
(*** extend_act ***)
paulson@6297
   162
paulson@7341
   163
(*Actions could affect the g-part, so result Cannot be strengthened to
paulson@7341
   164
   ((z, z') : extend_act h act) = ((f z, f z') : act)
paulson@7341
   165
*)
paulson@6297
   166
Goalw [extend_act_def]
paulson@6297
   167
     "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
paulson@6297
   168
by Auto_tac;
paulson@6297
   169
qed "mem_extend_act_iff";
paulson@6297
   170
AddIffs [mem_extend_act_iff]; 
paulson@6297
   171
paulson@7341
   172
Goalw [extend_act_def]
paulson@7341
   173
     "(z, z') : extend_act h act ==> (f z, f z') : act";
paulson@7341
   174
by Auto_tac;
paulson@7341
   175
qed "extend_act_D";
paulson@7341
   176
paulson@7537
   177
(*Premise is still undesirably strong, since Domain act can include
paulson@7537
   178
  non-reachable states, but it seems necessary for this result.*)
paulson@7689
   179
Goalw [extend_act_def, project_set_def, project_act_def]
paulson@7537
   180
 "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
paulson@7537
   181
by (Force_tac 1);
paulson@7341
   182
qed "extend_act_inverse";
paulson@7341
   183
Addsimps [extend_act_inverse];
paulson@7341
   184
paulson@7826
   185
(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
paulson@7826
   186
Goalw [extend_act_def, project_act_def]
paulson@7826
   187
     "act' <= extend_act h act ==> project_act C h act' <= act";
paulson@7826
   188
by (Force_tac 1);
paulson@7826
   189
qed "subset_extend_act_D";
paulson@7826
   190
paulson@6297
   191
Goal "inj (extend_act h)";
paulson@7341
   192
by (rtac inj_on_inverseI 1);
paulson@7341
   193
by (rtac extend_act_inverse 1);
paulson@7537
   194
by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
paulson@6297
   195
qed "inj_extend_act";
paulson@6297
   196
paulson@6297
   197
Goalw [extend_set_def, extend_act_def]
paulson@6297
   198
     "extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)";
paulson@6297
   199
by (Force_tac 1);
paulson@6297
   200
qed "extend_act_Image";
paulson@6297
   201
Addsimps [extend_act_Image];
paulson@6297
   202
paulson@7826
   203
Goalw [extend_act_def] "(extend_act h act' <= extend_act h act) = (act'<=act)";
paulson@7826
   204
by Auto_tac;
paulson@7826
   205
qed "extend_act_strict_mono";
paulson@7826
   206
paulson@7826
   207
AddIffs [extend_act_strict_mono, inj_extend_act RS inj_eq];
paulson@7826
   208
(*The latter theorem is  (extend_act h act' = extend_act h act) = (act'=act) *)
paulson@6297
   209
paulson@6297
   210
Goalw [extend_set_def, extend_act_def]
paulson@6297
   211
    "Domain (extend_act h act) = extend_set h (Domain act)";
paulson@6297
   212
by (Force_tac 1);
paulson@6297
   213
qed "Domain_extend_act"; 
paulson@6297
   214
paulson@7341
   215
Goalw [extend_act_def]
paulson@6297
   216
    "extend_act h Id = Id";
paulson@6297
   217
by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
paulson@6297
   218
qed "extend_act_Id";
paulson@7341
   219
paulson@7341
   220
Goalw [project_act_def]
paulson@7546
   221
     "[| (z, z') : act;  z: C |] \
paulson@7537
   222
\     ==> (f z, f z') : project_act C h act";
paulson@7341
   223
by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst], 
paulson@7341
   224
	      simpset()));
paulson@7341
   225
qed "project_act_I";
paulson@7341
   226
paulson@7341
   227
Goalw [project_set_def, project_act_def]
paulson@7689
   228
    "UNIV <= project_set h C ==> project_act C h Id = Id";
paulson@7341
   229
by (Force_tac 1);
paulson@7341
   230
qed "project_act_Id";
paulson@7341
   231
paulson@7482
   232
Goalw [project_set_def, project_act_def]
paulson@7594
   233
    "Domain (project_act C h act) = project_set h (Domain act Int C)";
wenzelm@7499
   234
by Auto_tac;
paulson@7482
   235
by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
wenzelm@7499
   236
by Auto_tac;
paulson@7482
   237
qed "Domain_project_act";
paulson@7482
   238
paulson@7341
   239
Addsimps [extend_act_Id, project_act_Id];
paulson@6297
   240
paulson@7826
   241
Goal "(extend_act h act = Id) = (act = Id)";
paulson@7826
   242
by Auto_tac;
paulson@7826
   243
by (rewtac extend_act_def);
paulson@7826
   244
by (ALLGOALS (blast_tac (claset() addEs [equalityE])));
paulson@7826
   245
qed "extend_act_Id_iff";
paulson@7826
   246
paulson@6297
   247
Goal "Id : extend_act h `` Acts F";
paulson@6297
   248
by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
paulson@6297
   249
	      simpset() addsimps [image_iff]));
paulson@6297
   250
qed "Id_mem_extend_act";
paulson@6297
   251
paulson@6297
   252
paulson@6297
   253
(**** extend ****)
paulson@6297
   254
paulson@6297
   255
(*** Basic properties ***)
paulson@6297
   256
paulson@7341
   257
Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)";
paulson@6297
   258
by Auto_tac;
paulson@6297
   259
qed "Init_extend";
paulson@6297
   260
paulson@7537
   261
Goalw [project_def] "Init (project C h F) = project_set h (Init F)";
paulson@7341
   262
by Auto_tac;
paulson@7341
   263
qed "Init_project";
paulson@7341
   264
paulson@6297
   265
Goal "Acts (extend h F) = (extend_act h `` Acts F)";
paulson@6297
   266
by (auto_tac (claset() addSIs [extend_act_Id RS sym], 
paulson@6297
   267
	      simpset() addsimps [extend_def, image_iff]));
paulson@6297
   268
qed "Acts_extend";
paulson@6297
   269
paulson@7546
   270
Goal "Acts (project C h F) = insert Id (project_act C h `` Acts F)";
paulson@7546
   271
by (auto_tac (claset(), 
paulson@7341
   272
	      simpset() addsimps [project_def, image_iff]));
paulson@7341
   273
qed "Acts_project";
paulson@7341
   274
paulson@7341
   275
Addsimps [Init_extend, Init_project, Acts_extend, Acts_project];
paulson@6297
   276
paulson@6297
   277
Goalw [SKIP_def] "extend h SKIP = SKIP";
paulson@6297
   278
by (rtac program_equalityI 1);
paulson@7341
   279
by Auto_tac;
paulson@7341
   280
qed "extend_SKIP";
paulson@7341
   281
paulson@7537
   282
Goalw [project_set_def] "UNIV <= project_set h UNIV";
paulson@7537
   283
by Auto_tac;
paulson@7537
   284
qed "project_set_UNIV";
paulson@7537
   285
paulson@7537
   286
(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
paulson@7537
   287
Goal "UNIV <= project_set h C \
paulson@7537
   288
\     ==> project C h (extend h F) = F";
paulson@7341
   289
by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
paulson@7341
   290
by (rtac program_equalityI 1);
paulson@7537
   291
by (asm_simp_tac (simpset() addsimps [image_image_eq_UN,
paulson@7537
   292
                   subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
paulson@7341
   293
by (Simp_tac 1);
paulson@7341
   294
qed "extend_inverse";
paulson@7341
   295
Addsimps [extend_inverse];
paulson@6297
   296
paulson@6297
   297
Goal "inj (extend h)";
paulson@7341
   298
by (rtac inj_on_inverseI 1);
paulson@7341
   299
by (rtac extend_inverse 1);
paulson@7537
   300
by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
paulson@6297
   301
qed "inj_extend";
paulson@6297
   302
paulson@6297
   303
Goal "extend h (F Join G) = extend h F Join extend h G";
paulson@6297
   304
by (rtac program_equalityI 1);
paulson@7537
   305
by (simp_tac (simpset() addsimps [image_Un]) 2);
paulson@6297
   306
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
paulson@6297
   307
qed "extend_Join";
paulson@6297
   308
Addsimps [extend_Join];
paulson@6297
   309
paulson@6647
   310
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";
paulson@6647
   311
by (rtac program_equalityI 1);
paulson@7537
   312
by (simp_tac (simpset() addsimps [image_UN]) 2);
paulson@6834
   313
by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
paulson@6647
   314
qed "extend_JN";
paulson@6647
   315
Addsimps [extend_JN];
paulson@6647
   316
paulson@7689
   317
paulson@7689
   318
(** These monotonicity results look natural but are UNUSED **)
paulson@7689
   319
paulson@7689
   320
Goal "F <= G ==> extend h F <= extend h G";
paulson@7689
   321
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
paulson@7689
   322
by Auto_tac;
paulson@7689
   323
qed "extend_mono";
paulson@7689
   324
paulson@7689
   325
Goal "F <= G ==> project C h F <= project C h G";
paulson@7689
   326
by (full_simp_tac
paulson@7689
   327
    (simpset() addsimps [component_eq_subset, project_set_def]) 1);
paulson@7689
   328
by Auto_tac;
paulson@7689
   329
qed "project_mono";
paulson@7689
   330
paulson@7689
   331
paulson@6536
   332
(*** Safety: co, stable ***)
paulson@6297
   333
paulson@6536
   334
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
paulson@6536
   335
\     (F : A co B)";
paulson@6297
   336
by (simp_tac (simpset() addsimps [constrains_def]) 1);
paulson@6297
   337
qed "extend_constrains";
paulson@6297
   338
paulson@6297
   339
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)";
paulson@6297
   340
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1);
paulson@6297
   341
qed "extend_stable";
paulson@6297
   342
paulson@6297
   343
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)";
paulson@6297
   344
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
paulson@6297
   345
qed "extend_invariant";
paulson@6297
   346
paulson@7826
   347
(*Converse fails: A and B may differ in their extra variables*)
paulson@7826
   348
Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
paulson@7826
   349
by (auto_tac (claset(), 
paulson@7826
   350
	      simpset() addsimps [constrains_def, project_set_def]));
paulson@7826
   351
by (Force_tac 1);
paulson@7826
   352
qed "extend_constrains_project_set";
paulson@7826
   353
paulson@7341
   354
paulson@7341
   355
(*** Diff, needed for localTo ***)
paulson@7341
   356
paulson@7387
   357
Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
paulson@7387
   358
by (auto_tac (claset() addSIs [program_equalityI],
paulson@7387
   359
	      simpset() addsimps [Diff_def,
paulson@7826
   360
				  inj_extend_act RS image_set_diff]));
paulson@7387
   361
qed "Diff_extend_eq";
paulson@7387
   362
paulson@7387
   363
Goal "(Diff (extend h G) (extend_act h `` acts) \
paulson@7387
   364
\         : (extend_set h A) co (extend_set h B)) \
paulson@7387
   365
\     = (Diff G acts : A co B)";
paulson@7387
   366
by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
paulson@7826
   367
qed "Diff_extend_constrains";
paulson@7341
   368
paulson@7387
   369
Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
paulson@7387
   370
\     = (Diff G acts : stable A)";
paulson@7826
   371
by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
paulson@7341
   372
qed "Diff_extend_stable";
paulson@7341
   373
paulson@7826
   374
Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
paulson@7826
   375
\     ==> Diff G acts : (project_set h A) co (project_set h B)";
paulson@7826
   376
by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
paulson@7826
   377
					   extend_constrains_project_set]) 1);
paulson@7826
   378
qed "Diff_extend_constrains_project_set";
paulson@7826
   379
paulson@7826
   380
Goalw [localTo_def]
paulson@7826
   381
     "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
paulson@7826
   382
by (simp_tac (simpset() addsimps []) 1);
paulson@7826
   383
(*A trick to strip both quantifiers*)
paulson@7826
   384
by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
paulson@7826
   385
by (stac Collect_eq_extend_set 1);
paulson@7826
   386
by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
paulson@7826
   387
qed "extend_localTo_extend_eq";
paulson@7826
   388
paulson@7826
   389
Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
paulson@7826
   390
by (simp_tac (simpset() addsimps [Disjoint_def,
paulson@7826
   391
				  inj_extend_act RS image_Int RS sym]) 1);
paulson@7826
   392
by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
paulson@7826
   393
by (blast_tac (claset() addEs [equalityE]) 1);
paulson@7826
   394
qed "Disjoint_extend_eq";
paulson@7826
   395
Addsimps [Disjoint_extend_eq];
paulson@7826
   396
paulson@7341
   397
(*** Weak safety primitives: Co, Stable ***)
paulson@6297
   398
paulson@6297
   399
Goal "p : reachable (extend h F) ==> f p : reachable F";
paulson@6297
   400
by (etac reachable.induct 1);
paulson@6297
   401
by (auto_tac
paulson@6297
   402
    (claset() addIs reachable.intrs,
paulson@7341
   403
     simpset() addsimps [extend_act_def, image_iff]));
paulson@6297
   404
qed "reachable_extend_f";
paulson@6297
   405
paulson@6297
   406
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F";
paulson@6297
   407
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1);
paulson@6297
   408
qed "h_reachable_extend";
paulson@6297
   409
paulson@6297
   410
Goalw [extend_set_def]
paulson@6297
   411
     "reachable (extend h F) = extend_set h (reachable F)";
paulson@6297
   412
by (rtac equalityI 1);
paulson@6297
   413
by (force_tac (claset() addIs  [h_f_g_eq RS sym]
paulson@6297
   414
			addSDs [reachable_extend_f], 
paulson@6297
   415
	       simpset()) 1);
paulson@6297
   416
by (Clarify_tac 1);
paulson@6297
   417
by (etac reachable.induct 1);
paulson@6297
   418
by (ALLGOALS (force_tac (claset() addIs reachable.intrs, 
paulson@6297
   419
			 simpset())));
paulson@6297
   420
qed "reachable_extend_eq";
paulson@6297
   421
paulson@6536
   422
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) =  \
paulson@6536
   423
\     (F : A Co B)";
paulson@6297
   424
by (simp_tac
paulson@6297
   425
    (simpset() addsimps [Constrains_def, reachable_extend_eq, 
paulson@6297
   426
			 extend_constrains, extend_set_Int_distrib RS sym]) 1);
paulson@6297
   427
qed "extend_Constrains";
paulson@6297
   428
paulson@6297
   429
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)";
paulson@6297
   430
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1);
paulson@6297
   431
qed "extend_Stable";
paulson@6297
   432
paulson@6647
   433
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)";
paulson@6647
   434
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1);
paulson@6647
   435
qed "extend_Always";
paulson@6647
   436
paulson@6297
   437
paulson@6297
   438
(*** Progress: transient, ensures ***)
paulson@6297
   439
paulson@6297
   440
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
paulson@6297
   441
by (auto_tac (claset(),
paulson@6297
   442
	      simpset() addsimps [transient_def, extend_set_subset_Compl_eq,
paulson@6297
   443
				  Domain_extend_act]));
paulson@6297
   444
qed "extend_transient";
paulson@6297
   445
paulson@6536
   446
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \
paulson@6536
   447
\     (F : A ensures B)";
paulson@6297
   448
by (simp_tac
paulson@6297
   449
    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
paulson@6297
   450
			 extend_set_Un_distrib RS sym, 
paulson@6297
   451
			 extend_set_Diff_distrib RS sym]) 1);
paulson@6297
   452
qed "extend_ensures";
paulson@6297
   453
paulson@6536
   454
Goal "F : A leadsTo B \
paulson@6536
   455
\     ==> extend h F : (extend_set h A) leadsTo (extend_set h B)";
paulson@6297
   456
by (etac leadsTo_induct 1);
paulson@6297
   457
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
paulson@6297
   458
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
paulson@6297
   459
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1);
paulson@6297
   460
qed "leadsTo_imp_extend_leadsTo";
paulson@6297
   461
paulson@6297
   462
(*** Proving the converse takes some doing! ***)
paulson@6297
   463
paulson@6297
   464
Goalw [slice_def] "slice (Union S) y = (UN x:S. slice x y)";
paulson@6297
   465
by Auto_tac;
paulson@6297
   466
qed "slice_Union";
paulson@6297
   467
paulson@6297
   468
Goalw [slice_def] "slice (extend_set h A) y = A";
paulson@6297
   469
by Auto_tac;
paulson@6297
   470
qed "slice_extend_set";
paulson@6297
   471
paulson@7482
   472
Goalw [slice_def, project_set_def] "project_set h A = (UN y. slice A y)";
paulson@6297
   473
by Auto_tac;
paulson@7482
   474
qed "project_set_is_UN_slice";
paulson@6297
   475
paulson@6297
   476
Goalw [slice_def, transient_def]
paulson@6297
   477
    "extend h F : transient A ==> F : transient (slice A y)";
paulson@6297
   478
by Auto_tac;
paulson@6297
   479
by (rtac bexI 1);
paulson@6297
   480
by Auto_tac;
paulson@6297
   481
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1);
paulson@6297
   482
qed "extend_transient_slice";
paulson@6297
   483
paulson@7482
   484
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)";
paulson@6297
   485
by (full_simp_tac
paulson@6297
   486
    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
paulson@7482
   487
			 project_set_eq, image_Un RS sym,
paulson@6297
   488
			 extend_set_Un_distrib RS sym, 
paulson@6297
   489
			 extend_set_Diff_distrib RS sym]) 1);
paulson@6297
   490
by Safe_tac;
paulson@6297
   491
by (full_simp_tac (simpset() addsimps [constrains_def, extend_act_def, 
paulson@6297
   492
				       extend_set_def]) 1);
paulson@6297
   493
by (Clarify_tac 1);
paulson@6297
   494
by (ball_tac 1); 
paulson@6297
   495
by (full_simp_tac (simpset() addsimps [slice_def, image_iff, Image_iff]) 1);
paulson@6297
   496
by (force_tac (claset() addSIs [h_f_g_eq RS sym], simpset()) 1);
paulson@6297
   497
(*transient*)
paulson@6297
   498
by (dtac extend_transient_slice 1);
paulson@6297
   499
by (etac transient_strengthen 1);
paulson@6297
   500
by (force_tac (claset() addIs [f_h_eq RS sym], 
paulson@6297
   501
	       simpset() addsimps [slice_def]) 1);
paulson@6297
   502
qed "extend_ensures_slice";
paulson@6297
   503
paulson@7482
   504
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU";
paulson@7482
   505
by (simp_tac (simpset() addsimps [project_set_is_UN_slice]) 1);
paulson@6297
   506
by (blast_tac (claset() addIs [leadsTo_UN]) 1);
paulson@6297
   507
qed "leadsTo_slice_image";
paulson@6297
   508
paulson@6297
   509
paulson@6536
   510
Goal "extend h F : AU leadsTo BU \
paulson@7482
   511
\     ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)";
paulson@6297
   512
by (etac leadsTo_induct 1);
paulson@6297
   513
by (full_simp_tac (simpset() addsimps [slice_Union]) 3);
paulson@6297
   514
by (blast_tac (claset() addIs [leadsTo_UN]) 3);
paulson@6297
   515
by (blast_tac (claset() addIs [leadsTo_slice_image, leadsTo_Trans]) 2);
paulson@6297
   516
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1);
paulson@6297
   517
qed_spec_mp "extend_leadsTo_slice";
paulson@6297
   518
paulson@6536
   519
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \
paulson@6536
   520
\     (F : A leadsTo B)";
paulson@6297
   521
by Safe_tac;
paulson@6297
   522
by (etac leadsTo_imp_extend_leadsTo 2);
paulson@6297
   523
by (dtac extend_leadsTo_slice 1);
paulson@6297
   524
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
paulson@6647
   525
qed "extend_leadsto";
paulson@6297
   526
paulson@6536
   527
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =  \
paulson@6536
   528
\     (F : A LeadsTo B)";
paulson@6454
   529
by (simp_tac
paulson@6454
   530
    (simpset() addsimps [LeadsTo_def, reachable_extend_eq, 
paulson@6647
   531
			 extend_leadsto, extend_set_Int_distrib RS sym]) 1);
paulson@6454
   532
qed "extend_LeadsTo";
paulson@6454
   533
paulson@6297
   534
paulson@6297
   535
Close_locale "Extend";
paulson@7482
   536
paulson@7482
   537
(*Close_locale should do this!
paulson@7482
   538
Delsimps [f_h_eq, extend_set_inverse, f_image_extend_set, extend_act_inverse,
paulson@7482
   539
	  extend_act_Image];
paulson@7482
   540
Delrules [make_elim h_inject1];
paulson@7482
   541
*)