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