--- a/src/HOL/UNITY/Alloc.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Mon Oct 04 13:47:28 1999 +0200
@@ -6,19 +6,11 @@
Specification of Chandy and Charpentier's Allocator
STOP USING o (COMPOSITION), since function application is naturally associative
+
+guarantees_PLam_I looks wrong: refers to lift_prog
*)
-Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
-
-(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *)
-Goal "[| b:A; a=b |] ==> a:A";
-by (etac ssubst 1);
-by (assume_tac 1);
-qed "subst_elem";
-
-
-
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
by (induct_tac "n" 1);
by Auto_tac;
@@ -65,6 +57,7 @@
Goalw [good_map_def] "good_map sysOfAlloc";
by Auto_tac;
qed "good_map_sysOfAlloc";
+Addsimps [good_map_sysOfAlloc];
(*MUST BE AUTOMATED: even the statement of such results*)
Goal "!!s. inv sysOfAlloc s = \
@@ -76,7 +69,6 @@
by (auto_tac (claset() addSWrapper record_split_wrapper,
simpset() addsimps [sysOfAlloc_def]));
qed "inv_sysOfAlloc_eq";
-
Addsimps [inv_sysOfAlloc_eq];
(**SHOULD NOT BE NECESSARY: The various injections into the system
@@ -99,6 +91,7 @@
Goalw [good_map_def] "good_map sysOfClient";
by Auto_tac;
qed "good_map_sysOfClient";
+Addsimps [good_map_sysOfClient];
(*MUST BE AUTOMATED: even the statement of such results*)
Goal "!!s. inv sysOfClient s = \
@@ -110,6 +103,7 @@
by (auto_tac (claset() addSWrapper record_split_wrapper,
simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
qed "inv_sysOfClient_eq";
+Addsimps [inv_sysOfClient_eq];
Open_locale "System";
@@ -154,7 +148,7 @@
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
exporting it from the locale*)
-val Network_Ask = Network_Spec RS IntD1 RS IntD1;
+val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D;
val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D;
val Network_Rel = Network_Spec RS IntD2 RS INT_D;
@@ -189,14 +183,16 @@
AddIffs [Network_component_System, Alloc_component_System];
+fun alloc_export th = good_map_sysOfAlloc RS export th;
+
+fun client_export th = good_map_sysOfClient RS export th;
+
(* F : UNIV guarantees Increasing func
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
val extend_Client_guar_Increasing =
- good_map_sysOfClient RS export extend_guar_Increasing
+ client_export extend_guar_Increasing
|> simplify (simpset() addsimps [inv_sysOfClient_eq]);
-fun alloc_export th = good_map_sysOfAlloc RS export th;
-
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
Goal "i < Nclients \
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
@@ -205,31 +201,27 @@
qed "extend_Alloc_Increasing_allocGiv";
-(** Proof of property (1) **)
+(*** Proof of the safety property (1) ***)
-(*step 1*)
+(*safety (1), step 1*)
Goalw [System_def]
"i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I]
- MRS guaranteesD) 1);
-by (asm_simp_tac
- (simpset() addsimps [guarantees_PLam_I,
- extend_Client_guar_Increasing RS guaranteesD,
- lift_prog_guar_Increasing]) 1);
+by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2
+ RS guaranteesD) 1);
+by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
+(*gets Client_Increasing_rel from simpset*)
+by Auto_tac;
qed "System_Increasing_rel";
-(*Note: the first step above performs simple quantifier reasoning. It could
- be replaced by a proof mentioning no guarantees primitives*)
-
-(*step 2*)
+(*safety (1), step 2*)
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
by (rtac Follows_Increasing1 1);
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
System_Increasing_rel]) 1);
qed "System_Increasing_allocRel";
-(*step 2*)
+(*safety (1), step 3*)
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
by (res_inst_tac
@@ -250,7 +242,7 @@
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
qed "System_sum_bounded";
-(*step 3*)
+(*safety (1), step 4*)
Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o giv o sub i o client) s \
\ <= (tokens o sub i o allocGiv) s})";
@@ -266,6 +258,7 @@
qed "System_Always_giv_le_allocGiv";
+(*safety (1), step 5*)
Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (tokens o sub i o allocRel) s \
\ <= (tokens o rel o sub i o client) s})";
@@ -281,6 +274,7 @@
qed "System_Always_allocRel_le_rel";
+(*safety (1), step 6*)
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
\ <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv,
@@ -293,3 +287,40 @@
by Auto_tac;
qed "System_safety";
+
+
+(*** Proof of the progress property (2) ***)
+
+(*we begin with proofs identical to System_Increasing_rel and
+ System_Increasing_allocRel: tactics needed!*)
+
+(*progress (2), step 1*)
+Goalw [System_def]
+ "i < Nclients ==> System : Increasing (ask o sub i o client)";
+by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2
+ RS guaranteesD) 1);
+by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
+by Auto_tac;
+qed "System_Increasing_ask";
+
+(*progress (2), step 2*)
+Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
+by (rtac Follows_Increasing1 1);
+by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
+ System_Increasing_ask]) 1);
+qed "System_Increasing_allocAsk";
+
+(*progress (2), step 3*)
+(*All this trouble just to lift "Client_Bounded" through two extemd ops*)
+Goalw [System_def]
+ "i < Nclients \
+\ ==> System : Always \
+\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+by (rtac (lift_prog_guar_Always RS
+ guarantees_PLam_I RS client_export extend_guar_Always RS
+ guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
+by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1);
+by (auto_tac(claset(),
+ simpset() addsimps [Collect_eq_lift_set RS sym,
+ client_export Collect_eq_extend_set RS sym]));
+qed "System_Bounded";
--- a/src/HOL/UNITY/Constrains.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML Mon Oct 04 13:47:28 1999 +0200
@@ -282,6 +282,11 @@
Always_eq_invariant_reachable]));
qed "Always_eq_includes_reachable";
+Goal "Always UNIV = UNIV";
+by (auto_tac (claset(),
+ simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_UNIV_eq";
+Addsimps [Always_UNIV_eq];
Goal "Always A = (UN I: Pow A. invariant I)";
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
--- a/src/HOL/UNITY/Extend.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Mon Oct 04 13:47:28 1999 +0200
@@ -95,6 +95,13 @@
by (rtac extend_set_inverse 1);
qed "inj_extend_set";
+Goalw [extend_set_def] "extend_set h UNIV = UNIV";
+by Auto_tac;
+by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
+by Auto_tac;
+qed "extend_set_UNIV_eq";
+Addsimps [standard extend_set_UNIV_eq];
+
(*** project_set: basic properties ***)
(*project_set is simply image!*)
@@ -164,7 +171,7 @@
(*Premise is still undesirably strong, since Domain act can include
non-reachable states, but it seems necessary for this result.*)
-Goalw [extend_act_def,project_set_def, project_act_def]
+Goalw [extend_act_def, project_set_def, project_act_def]
"Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
by (Force_tac 1);
qed "extend_act_inverse";
@@ -206,8 +213,7 @@
qed "project_act_I";
Goalw [project_set_def, project_act_def]
- "UNIV <= project_set h C \
-\ ==> project_act C h Id = Id";
+ "UNIV <= project_set h C ==> project_act C h Id = Id";
by (Force_tac 1);
qed "project_act_Id";
@@ -290,6 +296,21 @@
qed "extend_JN";
Addsimps [extend_JN];
+
+(** These monotonicity results look natural but are UNUSED **)
+
+Goal "F <= G ==> extend h F <= extend h G";
+by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by Auto_tac;
+qed "extend_mono";
+
+Goal "F <= G ==> project C h F <= project C h G";
+by (full_simp_tac
+ (simpset() addsimps [component_eq_subset, project_set_def]) 1);
+by Auto_tac;
+qed "project_mono";
+
+
(*** Safety: co, stable ***)
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
--- a/src/HOL/UNITY/Guar.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML Mon Oct 04 13:47:28 1999 +0200
@@ -219,6 +219,9 @@
by (Blast_tac 1);
qed "guarantees_Join_I";
+bind_thm ("guarantees_Join_I1", disjI1 RS guarantees_Join_I);
+bind_thm ("guarantees_Join_I2", disjI2 RS guarantees_Join_I);
+
Goalw [guar_def]
"[| i : I; F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
--- a/src/HOL/UNITY/PPROD.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Mon Oct 04 13:47:28 1999 +0200
@@ -271,21 +271,7 @@
(*** guarantees properties ***)
Goalw [PLam_def]
- "[| i : I; lift_prog i (F i): X guarantees Y |] \
+ "[| lift_prog i (F i): X guarantees Y; i : I |] \
\ ==> (PLam I F) : X guarantees Y";
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
qed "guarantees_PLam_I";
-
-Goalw [PLam_def]
- "[| ALL i:I. F i : X guarantees Y |] \
-\ ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
-\ guarantees (INT i: I. lift_prog i `` Y)";
-by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
-bind_thm ("guarantees_PLam_INT", ballI RS result());
-
-Goalw [PLam_def]
- "[| ALL i:I. F i : X guarantees Y |] \
-\ ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
-\ guarantees (UN i: I. lift_prog i `` Y)";
-by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
-bind_thm ("guarantees_PLam_UN", ballI RS result());
--- a/src/HOL/UNITY/Project.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Project.ML Mon Oct 04 13:47:28 1999 +0200
@@ -18,7 +18,7 @@
Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-bd project_act_mono 1;
+by (dtac project_act_mono 1);
by (Blast_tac 1);
qed "project_constrains_mono";
@@ -65,7 +65,7 @@
qed "project_stable";
Goal "F : stable (extend_set h A) ==> project C h F : stable A";
-bd (project_stable RS iffD2) 1;
+by (dtac (project_stable RS iffD2) 1);
by (blast_tac (claset() addIs [project_stable_mono]) 1);
qed "project_stable_I";
@@ -106,6 +106,16 @@
extend_stable RS iffD1]));
qed "Join_project_increasing";
+(*For using project_guarantees in particular cases*)
+Goal "extend h F Join G : extend_set h A co extend_set h B \
+\ ==> F Join project UNIV h G : A co B";
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [project_constrains, Join_constrains,
+ extend_constrains]) 1);
+by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
+qed "project_constrains_I";
+
(*** Diff, needed for localTo ***)
@@ -140,13 +150,20 @@
qed "Diff_project_stable";
(*Converse appears to fail*)
-Goal "[| UNIV <= project_set h C; (H : (func o f) localTo extend h G) |] \
-\ ==> (project C h H : func localTo G)";
+Goal "[| UNIV <= project_set h C; H : (func o f) localTo extend h G |] \
+\ ==> project C h H : func localTo G";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def,
project_extend_Join RS sym,
subset_UNIV RS subset_trans RS Diff_project_stable,
Collect_eq_extend_set RS sym]) 1);
+qed "project_localTo_lemma";
+
+Goal "extend h F Join G : (v o f) localTo extend h H \
+\ ==> F Join project UNIV h G : v localTo H";
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
+by (asm_simp_tac
+ (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
qed "project_localTo_I";
@@ -166,6 +183,8 @@
by (etac extend_act_D 1);
qed "reachable_imp_reachable_project";
+(*The extra generality in the first premise allows guarantees with STRONG
+ preconditions (localTo) and WEAK postconditions.*)
Goalw [Constrains_def]
"[| reachable (extend h F Join G) <= C; \
\ F Join project C h G : A Co B |] \
@@ -188,7 +207,7 @@
\ F Join project C h G : Always A |] \
\ ==> extend h F Join G : Always (extend_set h A)";
by (force_tac (claset() addIs [reachable.Init, project_set_I],
- simpset() addsimps [project_Stable_D]) 1);
+ simpset() addsimps [project_Stable_D]) 1);
qed "project_Always_D";
Goalw [Increasing_def]
@@ -250,6 +269,15 @@
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
qed "project_Stable_I";
+Goalw [Always_def]
+ "[| C <= reachable (extend h F Join G); \
+\ extend h F Join G : Always (extend_set h A) |] \
+\ ==> F Join project C h G : Always A";
+by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
+bws [project_set_def, extend_set_def];
+by (Blast_tac 1);
+qed "project_Always_I";
+
Goalw [Increasing_def]
"[| C <= reachable (extend h F Join G); \
\ extend h F Join G : Increasing (func o f) |] \
@@ -369,15 +397,15 @@
by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken,
leadsTo_Trans]) 2);
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
-qed "Join_project_leadsTo_I";
+qed "project_leadsTo_lemma";
(*Instance of the previous theorem for STRONG progress*)
Goal "[| ALL x. project UNIV h G ~: transient {x}; \
\ F Join project UNIV h G : A leadsTo B |] \
\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (dtac Join_project_leadsTo_I 1);
+by (dtac project_leadsTo_lemma 1);
by Auto_tac;
-qed "Join_project_UNIV_leadsTo_I";
+qed "project_UNIV_leadsTo_lemma";
(** Towards the analogous theorem for WEAK progress*)
@@ -397,7 +425,7 @@
\ extend h F Join G : stable C; \
\ F Join project C h G : (project_set h C Int A) leadsTo B |] \
\ ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
-br (lemma RS leadsTo_weaken) 1;
+by (rtac (lemma RS leadsTo_weaken) 1);
by (auto_tac (claset() addIs [project_set_I], simpset()));
val lemma2 = result();
@@ -475,31 +503,31 @@
by Auto_tac;
qed "extend_guar_Increasing";
-Goal "F : (func localTo G) guarantees increasing func \
-\ ==> extend h F : (func o f) localTo (extend h G) \
+Goal "F : (v localTo G) guarantees increasing func \
+\ ==> extend h F : (v o f) localTo (extend h G) \
\ guarantees increasing (func o f)";
by (etac project_guarantees 1);
(*the "increasing" guarantee*)
-by (asm_simp_tac
- (simpset() addsimps [Join_project_increasing RS sym]) 2);
-(*the "localTo" requirement*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_simp_tac
- (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
+by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
+by (etac project_localTo_I 1);
qed "extend_localTo_guar_increasing";
-Goal "F : (func localTo G) guarantees Increasing func \
-\ ==> extend h F : (func o f) localTo (extend h G) \
+Goal "F : (v localTo G) guarantees Increasing func \
+\ ==> extend h F : (v o f) localTo (extend h G) \
\ guarantees Increasing (func o f)";
by (etac project_guarantees 1);
(*the "Increasing" guarantee*)
by (etac (subset_UNIV RS project_Increasing_D) 2);
-(*the "localTo" requirement*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_simp_tac
- (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
+by (etac project_localTo_I 1);
qed "extend_localTo_guar_Increasing";
+Goal "F : Always A guarantees Always B \
+\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
+by (etac project_guarantees 1);
+by (etac (subset_refl RS project_Always_D) 2);
+by (etac (subset_refl RS project_Always_I) 1);
+qed "extend_guar_Always";
+
(** Guarantees with a leadsTo postcondition **)
@@ -510,13 +538,38 @@
extend_set_sing, project_stable_I]) 1);
qed "localTo_imp_project_stable";
-
Goal "F : stable{s} ==> F ~: transient {s}";
by (auto_tac (claset(),
simpset() addsimps [FP_def, transient_def,
stable_def, constrains_def]));
qed "stable_sing_imp_not_transient";
+Goal "[| F Join project UNIV h G : A leadsTo B; \
+\ extend h F Join G : f localTo extend h F; \
+\ Disjoint (extend h F) G |] \
+\ ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
+by (rtac project_UNIV_leadsTo_lemma 1);
+by Auto_tac;
+by (asm_full_simp_tac
+ (simpset() addsimps [Join_localTo, self_localTo,
+ localTo_imp_project_stable,
+ stable_sing_imp_not_transient]) 1);
+qed "project_leadsTo_D";
+
+
+Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
+\ extend h F Join G : f localTo extend h F; \
+\ Disjoint (extend h F) G |] \
+\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
+by (rtac Join_project_LeadsTo 1);
+by Auto_tac;
+by (asm_full_simp_tac
+ (simpset() addsimps [Join_localTo, self_localTo,
+ localTo_imp_project_stable,
+ stable_sing_imp_not_transient]) 1);
+qed "project_LeadsTo_D";
+
+
(*STRONG precondition and postcondition*)
Goal "F : (A co A') guarantees (B leadsTo B') \
\ ==> extend h F : ((extend_set h A) co (extend_set h A')) \
@@ -524,18 +577,9 @@
\ guarantees ((extend_set h B) leadsTo (extend_set h B'))";
by (etac project_guarantees 1);
(*the safety precondition*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [project_constrains, Join_constrains,
- extend_constrains]) 1);
-by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
+by (fast_tac (claset() addIs [project_constrains_I]) 1);
(*the liveness postcondition*)
-by (rtac Join_project_UNIV_leadsTo_I 1);
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [Join_localTo, self_localTo,
- localTo_imp_project_stable,
- stable_sing_imp_not_transient]) 1);
+by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
qed "extend_co_guar_leadsTo";
(*WEAK precondition and postcondition*)
@@ -547,13 +591,7 @@
(*the safety precondition*)
by (fast_tac (claset() addIs [project_Constrains_I]) 1);
(*the liveness postcondition*)
-by (rtac Join_project_LeadsTo 1);
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [Join_localTo, self_localTo,
- localTo_imp_project_stable,
- stable_sing_imp_not_transient]) 1);
+by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
qed "extend_Co_guar_LeadsTo";
-
Close_locale "Extend";
--- a/src/HOL/UNITY/Project.thy Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Project.thy Mon Oct 04 13:47:28 1999 +0200
@@ -8,15 +8,4 @@
Inheritance of GUARANTEES properties under extension
*)
-Project = Extend +
-
-
-constdefs
-
- restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
- "restr_act C h act == project_act C h (extend_act h act)"
-
- restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
- "restr C h F == project C h (extend h F)"
-
-end
+Project = Extend
--- a/src/HOL/UNITY/Union.ML Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Mon Oct 04 13:47:28 1999 +0200
@@ -329,6 +329,11 @@
by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
qed "localTo_imp_o_localTo";
+Goalw [localTo_def, stable_def, constrains_def]
+ "(%s. x) localTo F = UNIV";
+by (Blast_tac 1);
+qed "triv_localTo_eq_UNIV";
+
Goal "(F Join G : v localTo H) = (F : v localTo H & G : v localTo H)";
by (asm_full_simp_tac
(simpset() addsimps [localTo_def, Diff_Join_distrib,