equal
deleted
inserted
replaced
368 |
368 |
369 Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)"; |
369 Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)"; |
370 by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def, |
370 by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def, |
371 Join_left_absorb]) 1); |
371 Join_left_absorb]) 1); |
372 qed "self_Join_LocalTo"; |
372 qed "self_Join_LocalTo"; |
373 |
|
374 Goalw [LOCALTO_def] |
|
375 "[| G : v localTo[C] F; F<=F' |] ==> G : v localTo[C] F'"; |
|
376 by (Force_tac 1); |
|
377 qed "localTo_imp_o_localTo"; |
|
378 |
|
379 |
373 |
380 |
374 |
381 (*** Higher-level rules involving localTo and Join ***) |
375 (*** Higher-level rules involving localTo and Join ***) |
382 |
376 |
383 Goal "[| F : {s. P (v s)} co B; G : v localTo[C] F |] \ |
377 Goal "[| F : {s. P (v s)} co B; G : v localTo[C] F |] \ |