--- a/src/HOL/UNITY/Alloc.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Mon Oct 18 15:18:24 1999 +0200
@@ -388,35 +388,37 @@
(*A LOT of work just to lift "Client_Progress" to the array*)
Goal "lift_prog i Client \
-\ : Increasing (giv o sub i) Int ((%z. z i) localTo (lift_prog i Client)) \
+\ : Increasing (giv o sub i) Int ((%z. z i) localTo[UNIV] (lift_prog i Client)) \
\ guarantees \
\ (INT h. {s. h <= (giv o sub i) s & \
\ h pfixGe (ask o sub i) s} \
\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
-br (Client_Progress RS drop_prog_guarantees) 1;
-br (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
-br subset_refl 4;
+by (rtac (Client_Progress RS drop_prog_guarantees) 1);
+by (rtac (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2);
by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
by (auto_tac (claset(), simpset() addsimps [o_def]));
qed "Client_i_Progress";
+xxxxxxxxxxxxxxxx;
+
Goalw [System_def]
"i < Nclients \
\ ==> System : (INT h. {s. h <= (giv o sub i o client) s & \
\ h pfixGe (ask o sub i o client) s} \
\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
-br (guarantees_PLam_I RS project_guarantees) 1;
-br Client_i_Progress 1;
+by (rtac (guarantees_PLam_I RS project_guarantees) 1);
+by (rtac Client_i_Progress 1);
by (Force_tac 1);
-br (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
-br subset_refl 4;
+by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
-br projecting_Int 1;
-br (client_export projecting_Increasing) 1;
-br (client_export projecting_localTo) 1;
+by (rtac projecting_Int 1);
+by (rtac (client_export projecting_Increasing) 1);
+by (rtac (client_export projecting_localTo) 1);
by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
--- a/src/HOL/UNITY/Client.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Mon Oct 18 15:18:24 1999 +0200
@@ -73,7 +73,7 @@
program_defs_ref := [];
(*Safety property 2: clients return the right number of tokens*)
-Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \
+Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg)) \
\ guarantees Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
by (rtac AlwaysI 1);
@@ -101,7 +101,7 @@
val Increasing_length = mono_length RS mono_Increasing_o;
Goal "Cli_prg : \
-\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
+\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \
\ guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
\ {s. size (rel s) <= size (giv s)})";
by (rtac guaranteesI 1);
@@ -122,7 +122,7 @@
Goal "Cli_prg : \
-\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\ (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \
\ Int Always giv_meets_ask) \
\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
by (rtac guaranteesI 1);
--- a/src/HOL/UNITY/Comp.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Mon Oct 18 15:18:24 1999 +0200
@@ -62,7 +62,7 @@
qed "component_antisym";
Goalw [component_def]
- "F <= H = (EX G. F Join G = H & Disjoint F G)";
+ "F <= H = (EX G. F Join G = H & Disjoint UNIV F G)";
by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
qed "component_eq";
@@ -77,8 +77,3 @@
qed "component_constrains";
bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
-
-Goal "Diff F (Acts G) <= F";
-by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Diff_def, component_eq_subset]));
-qed "Diff_component";
--- a/src/HOL/UNITY/Extend.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Mon Oct 18 15:18:24 1999 +0200
@@ -8,6 +8,17 @@
function g (forgotten) maps the extended state to the "extending part"
*)
+
+
+ Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
+ by (Blast_tac 1);
+ qed "disjoint_iff_not_equal";
+
+ Goal "ff -`` (ff `` A) = {y. EX x:A. ff x = ff y}";
+ by (blast_tac (claset() addIs [sym]) 1);
+ qed "vimage_image_eq";
+
+
(** These we prove OUTSIDE the locale. **)
(*Possibly easier than reasoning about "inv h"*)
@@ -57,13 +68,41 @@
(*FIXME: If locales worked properly we could put just "f" above*)
by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
qed "h_inject1";
-AddSDs [h_inject1];
+AddDs [h_inject1];
Goal "h(f z, g z) = z";
by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym,
surj_h RS surj_f_inv_f]) 1);
qed "h_f_g_eq";
+
+(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
+
+val cT = TFree ("'c", ["term"]);
+
+(* "PROP P x == PROP P (h (f x, g x))" *)
+val lemma1 = Thm.combination
+ (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT))))
+ (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection));
+
+val prems = Goalw [lemma1] "(!!u y. PROP P (h (u, y))) ==> PROP P x";
+by (resolve_tac prems 1);
+val lemma2 = result();
+
+val prems = Goal "(!!u y. PROP P (h (u, y))) ==> (!!z. PROP P z)";
+by (rtac lemma2 1);
+by (resolve_tac prems 1);
+val lemma3 = result();
+
+val prems = Goal "(!!z. PROP P z) ==> (!!u y. PROP P (h (u, y)))";
+(*not needed for proof, but prevents generalization over h, 'c, etc.*)
+by (cut_facts_tac [surj_h] 1);
+by (resolve_tac prems 1);
+val lemma4 = result();
+
+val split_extended_all = Thm.equal_intr lemma4 lemma3;
+
+
(*** extend_set: basic properties ***)
Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
@@ -101,9 +140,8 @@
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;
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
qed "extend_set_UNIV_eq";
Addsimps [standard extend_set_UNIV_eq];
@@ -111,14 +149,14 @@
(*project_set is simply image!*)
Goalw [project_set_def] "project_set h C = f `` C";
-by (auto_tac (claset() addIs [f_h_eq RS sym, h_f_g_eq RS ssubst],
- simpset()));
+by (auto_tac (claset() addIs [f_h_eq RS sym],
+ simpset() addsimps [split_extended_all]));
qed "project_set_eq";
(*Converse appears to fail*)
-Goalw [project_set_def] "z : C ==> f z : project_set h C";
-by (auto_tac (claset() addIs [h_f_g_eq RS ssubst],
- simpset()));
+Goalw [project_set_def] "!!z. z : C ==> f z : project_set h C";
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
qed "project_set_I";
@@ -160,31 +198,41 @@
(*** extend_act ***)
-(*Actions could affect the g-part, so result Cannot be strengthened to
- ((z, z') : extend_act h act) = ((f z, f z') : act)
-*)
Goalw [extend_act_def]
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
by Auto_tac;
qed "mem_extend_act_iff";
AddIffs [mem_extend_act_iff];
+(*Converse fails: (z,z') would include actions that changed the g-part*)
Goalw [extend_act_def]
"(z, z') : extend_act h act ==> (f z, f z') : act";
by Auto_tac;
qed "extend_act_D";
+Goalw [extend_act_def, project_act_def, project_set_def]
+ "project_act h (Restrict C (extend_act h act)) = \
+\ Restrict (project_set h C) act";
+by (Blast_tac 1);
+qed "project_act_extend_act_restrict";
+Addsimps [project_act_extend_act_restrict];
+
+Goalw [extend_act_def, project_act_def, project_set_def]
+ "(Restrict C (extend_act h act) = Restrict C (extend_act h act')) \
+\ = (Restrict (project_set h C) act = Restrict (project_set h C) act')";
+by Auto_tac;
+by (ALLGOALS (blast_tac (claset() addSEs [equalityE])));
+qed "Restrict_extend_act_eq_Restrict_project_act";
+
(*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]
- "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
-by (Force_tac 1);
+Goal "Domain act <= project_set h C \
+\ ==> project_act h (Restrict C (extend_act h act)) = act";
+by (asm_simp_tac (simpset() addsimps [Restrict_triv]) 1);
qed "extend_act_inverse";
-Addsimps [extend_act_inverse];
-(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
Goalw [extend_act_def, project_act_def]
- "act' <= extend_act h act ==> project_act C h act' <= act";
+ "act' <= extend_act h act ==> project_act h act' <= act";
by (Force_tac 1);
qed "subset_extend_act_D";
@@ -218,22 +266,20 @@
qed "extend_act_Id";
Goalw [project_act_def]
- "[| (z, z') : act; z: C |] \
-\ ==> (f z, f z') : project_act C h act";
-by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst],
- simpset()));
+ "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act";
+by (force_tac (claset(),
+ simpset() addsimps [split_extended_all]) 1);
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 h (Restrict C Id) = Id";
by (Force_tac 1);
qed "project_act_Id";
Goalw [project_set_def, project_act_def]
- "Domain (project_act C h act) = project_set h (Domain act Int C)";
-by Auto_tac;
-by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
-by Auto_tac;
+ "Domain (project_act h (Restrict C act)) = project_set h (Domain act Int C)";
+by (force_tac (claset(),
+ simpset() addsimps [split_extended_all]) 1);
qed "Domain_project_act";
Addsimps [extend_act_Id, project_act_Id];
@@ -267,7 +313,7 @@
simpset() addsimps [extend_def, image_iff]));
qed "Acts_extend";
-Goal "Acts (project C h F) = insert Id (project_act C h `` Acts F)";
+Goal "Acts (project C h F) = insert Id (project_act h `` Restrict C `` Acts F)";
by (auto_tac (claset(),
simpset() addsimps [project_def, image_iff]));
qed "Acts_project";
@@ -279,17 +325,18 @@
by Auto_tac;
qed "extend_SKIP";
-Goalw [project_set_def] "UNIV <= project_set h UNIV";
+Goalw [project_set_def] "project_set h UNIV = UNIV";
by Auto_tac;
qed "project_set_UNIV";
+Addsimps [project_set_UNIV];
(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
Goal "UNIV <= project_set h C \
\ ==> project C h (extend h F) = F";
by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_image_eq_UN,
- subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
+by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN,
+ subset_UNIV RS subset_trans RS Restrict_triv]) 2);
by (Simp_tac 1);
qed "extend_inverse";
Addsimps [extend_inverse];
@@ -354,43 +401,84 @@
(*** Diff, needed for localTo ***)
-Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
+Goal "Restrict (extend_set h C) (extend_act h act) = \
+\ extend_act h (Restrict C act)";
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
+by (auto_tac (claset(),
+ simpset() addsimps [extend_act_def]));
+qed "Restrict_extend_set";
+
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
+\ extend h (Diff C G acts)";
by (auto_tac (claset() addSIs [program_equalityI],
- simpset() addsimps [Diff_def,
+ simpset() addsimps [Diff_def, image_image_eq_UN,
+ Restrict_extend_set,
inj_extend_act RS image_set_diff]));
qed "Diff_extend_eq";
-Goal "(Diff (extend h G) (extend_act h `` acts) \
+(*Opposite inclusion fails; this inclusion's more general than that of
+ Diff_extend_eq*)
+Goal "Diff (project_set h C) G acts \
+\ <= project C h (Diff C (extend h G) (extend_act h `` acts))";
+by (simp_tac
+ (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
+ image_image, image_Diff_image_eq,
+ Restrict_extend_act_eq_Restrict_project_act,
+ vimage_image_eq]) 1);
+by (blast_tac (claset() addSEs [equalityE])1);
+qed "Diff_project_set_component";
+
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
\ : (extend_set h A) co (extend_set h B)) \
-\ = (Diff G acts : A co B)";
+\ = (Diff C G acts : A co B)";
by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
qed "Diff_extend_constrains";
-Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
-\ = (Diff G acts : stable A)";
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
+\ : stable (extend_set h A)) \
+\ = (Diff C G acts : stable A)";
by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
qed "Diff_extend_stable";
-Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
-\ ==> Diff G acts : (project_set h A) co (project_set h B)";
+(*UNUSED!!*)
+Goal "Diff (extend_set h C) (extend h G) (extend_act h `` acts) : A co B \
+\ ==> Diff C G acts : (project_set h A) co (project_set h B)";
by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq,
extend_constrains_project_set]) 1);
qed "Diff_extend_constrains_project_set";
-Goalw [localTo_def]
- "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
-by (simp_tac (simpset() addsimps []) 1);
+Goalw [LOCALTO_def]
+ "(extend h F : (v o f) localTo[extend_set h C] extend h H) = \
+\ (F : v localTo[C] H)";
+by (Simp_tac 1);
(*A trick to strip both quantifiers*)
by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
by (stac Collect_eq_extend_set 1);
by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
qed "extend_localTo_extend_eq";
-Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
-by (simp_tac (simpset() addsimps [Disjoint_def,
- inj_extend_act RS image_Int RS sym]) 1);
-by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+(*USED?? opposite inclusion fails*)
+Goal "Restrict C (extend_act h act) <= \
+\ extend_act h (Restrict (project_set h C) act)";
+by (auto_tac (claset(),
+ simpset() addsimps [split_extended_all]));
+by (auto_tac (claset(),
+ simpset() addsimps [extend_act_def, project_set_def]));
+qed "Restrict_extend_set_subset";
+
+
+Goal "(extend_act h `` Acts F) - {Id} = extend_act h `` (Acts F - {Id})";
+by (stac (extend_act_Id RS sym) 1);
+by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
+qed "extend_act_image_Id_eq";
+
+Goal "Disjoint C (extend h F) (extend h G) = Disjoint (project_set h C) F G";
+by (simp_tac
+ (simpset() addsimps [Disjoint_def, disjoint_iff_not_equal,
+ image_Diff_image_eq,
+ Restrict_extend_act_eq_Restrict_project_act,
+ extend_act_Id_iff, vimage_def]) 1);
qed "Disjoint_extend_eq";
Addsimps [Disjoint_extend_eq];
--- a/src/HOL/UNITY/Extend.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Mon Oct 18 15:18:24 1999 +0200
@@ -25,18 +25,17 @@
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
"extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
- (*Argument C allows weak safety laws to be projected*)
- project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
- "project_act C h act ==
- {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
+ project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
+ "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
extend_act h `` Acts F)"
+ (*Argument C allows weak safety laws to be projected*)
project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
"project C h F == mk_program (project_set h (Init F),
- project_act C h `` Acts F)"
+ project_act h `` Restrict C `` Acts F)"
locale Extend =
fixes
--- a/src/HOL/UNITY/Guar.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML Mon Oct 18 15:18:24 1999 +0200
@@ -65,7 +65,7 @@
(*** guarantees ***)
val prems = Goal
- "(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \
+ "(!!G. [| F Join G : X; Disjoint UNIV F G |] ==> F Join G : Y) \
\ ==> F : X guarantees Y";
by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
by (blast_tac (claset() addIs prems) 1);
@@ -84,7 +84,7 @@
(*This equation is more intuitive than the official definition*)
Goal "(F : X guarantees Y) = \
-\ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
+\ (ALL G. F Join G : X & Disjoint UNIV F G --> F Join G : Y)";
by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
by (Blast_tac 1);
qed "guarantees_eq";
--- a/src/HOL/UNITY/LessThan.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML Mon Oct 18 15:18:24 1999 +0200
@@ -7,6 +7,61 @@
*)
+(*** Restrict [MOVE TO RELATION.THY??] ***)
+
+Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
+by (Blast_tac 1);
+qed "Restrict_iff";
+AddIffs [Restrict_iff];
+
+Goal "Restrict UNIV = id";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_UNIV";
+Addsimps [Restrict_UNIV];
+
+Goal "Restrict {} r = {}";
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_empty";
+Addsimps [Restrict_empty];
+
+Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
+by (Blast_tac 1);
+qed "Restrict_Int";
+Addsimps [Restrict_Int];
+
+Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
+by Auto_tac;
+qed "Restrict_triv";
+
+Goalw [Restrict_def] "Restrict A r <= r";
+by Auto_tac;
+qed "Restrict_subset";
+
+Goalw [Restrict_def]
+ "[| A <= B; Restrict B r = Restrict B s |] \
+\ ==> Restrict A r = Restrict A s";
+by (blast_tac (claset() addSEs [equalityE]) 1);
+qed "Restrict_eq_mono";
+
+Goalw [Restrict_def, image_def]
+ "[| s : RR; Restrict A r = Restrict A s |] \
+\ ==> Restrict A r : Restrict A `` RR";
+by Auto_tac;
+qed "Restrict_imageI";
+
+Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
+by Auto_tac;
+by (rewrite_goals_tac [image_def, Restrict_def]);
+by (Blast_tac 1);
+qed "Restrict_image_Diff";
+
+(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
+Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
+by (Blast_tac 1);
+qed "image_Diff_image_eq";
+
+
(*** lessThan ***)
Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
--- a/src/HOL/UNITY/LessThan.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/LessThan.thy Mon Oct 18 15:18:24 1999 +0200
@@ -12,6 +12,10 @@
constdefs
+ (*MOVE TO RELATION.THY??*)
+ Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
+ "Restrict A r == r Int (A Times UNIV)"
+
lessThan :: "nat => nat set"
"lessThan n == {i. i<n}"
--- a/src/HOL/UNITY/Lift_prog.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Mon Oct 18 15:18:24 1999 +0200
@@ -54,13 +54,8 @@
qed "lift_act_eq";
AddIffs [lift_act_eq];
-Goalw [drop_act_def]
- "[| (s, s') : act; s : C |] ==> (s i, s' i) : drop_act C i act";
-by Auto_tac;
-qed "drop_act_I";
-
Goalw [drop_set_def, drop_act_def]
- "UNIV <= drop_set i C ==> drop_act C i Id = Id";
+ "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
by (Blast_tac 1);
qed "drop_act_Id";
Addsimps [drop_act_Id];
@@ -82,7 +77,7 @@
qed "Init_drop_prog";
Addsimps [Init_drop_prog];
-Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
+Goal "Acts (drop_prog C i F) = insert Id (drop_act i `` Restrict C `` Acts F)";
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)],
simpset() addsimps [drop_prog_def]));
qed "Acts_drop_prog";
@@ -169,7 +164,7 @@
by (auto_tac (claset() addSIs [exI], simpset()));
qed "lift_act_correct";
-Goal "drop_act C i = project_act C (lift_map i)";
+Goal "drop_act i = project_act (lift_map i)";
by (rtac ext 1);
by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
by Auto_tac;
@@ -230,12 +225,14 @@
qed "lift_set_UNIV_eq";
Addsimps [lift_set_UNIV_eq];
-Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
+(*
+Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, drop_act_correct,
lift_act_correct, lift_export extend_act_inverse]) 1);
qed "lift_act_inverse";
Addsimps [lift_act_inverse];
+*)
Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
by (asm_full_simp_tac
@@ -314,9 +311,8 @@
(*** Diff, needed for localTo ***)
-Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
-\ Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
-\ ==> Diff (drop_prog C i G) acts : A co B";
+Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
+\ ==> Diff (drop_set i C) (drop_prog C i G) acts : A co B";
by (asm_full_simp_tac
(simpset() addsimps [drop_set_correct, drop_prog_correct,
lift_set_correct, lift_act_correct,
@@ -324,27 +320,11 @@
qed "Diff_drop_prog_constrains";
Goalw [stable_def]
- "[| (UN act:acts. Domain act) <= drop_set i C; \
-\ Diff G (lift_act i `` acts) : stable (lift_set i A) |] \
-\ ==> Diff (drop_prog C i G) acts : stable A";
-by (etac Diff_drop_prog_constrains 1);
-by (assume_tac 1);
+ "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |] \
+\ ==> Diff (drop_set i C) (drop_prog C i G) acts : stable A";
+by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
qed "Diff_drop_prog_stable";
-Goalw [constrains_def, Diff_def]
- "Diff G acts : A co B \
-\ ==> Diff (lift_prog i G) (lift_act i `` acts) \
-\ : (lift_set i A) co (lift_set i B)";
-by Auto_tac;
-by (Blast_tac 1);
-qed "Diff_lift_prog_co";
-
-Goalw [stable_def]
- "Diff G acts : stable A \
-\ ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
-by (etac Diff_lift_prog_co 1);
-qed "Diff_lift_prog_stable";
-
(*** Weak safety primitives: Co, Stable ***)
@@ -466,19 +446,19 @@
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_guar_Increasing";
-Goal "F : (v localTo G) guarantees increasing func \
-\ ==> lift_prog i F : (v o sub i) localTo (lift_prog i G) \
+Goal "F : (v localTo[UNIV] G) guarantees increasing func \
+\ ==> lift_prog i F : (v o sub i) localTo[UNIV] (lift_prog i G) \
\ guarantees increasing (func o sub i)";
by (dtac (lift_export extend_localTo_guar_increasing) 1);
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
qed "lift_prog_localTo_guar_increasing";
-Goal "F : (v localTo G) guarantees Increasing func \
-\ ==> lift_prog i F : (v o sub i) localTo (lift_prog i G) \
+Goal "F : (v LocalTo G) guarantees Increasing func \
+\ ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G) \
\ guarantees Increasing (func o sub i)";
-by (dtac (lift_export extend_localTo_guar_Increasing) 1);
+by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_localTo_guar_Increasing";
+qed "lift_prog_LocalTo_guar_Increasing";
Goal "F : Always A guarantees Always B \
\ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
--- a/src/HOL/UNITY/Lift_prog.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Mon Oct 18 15:18:24 1999 +0200
@@ -22,19 +22,19 @@
lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
"lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
- (*Argument C allows weak safety laws to be projected*)
- drop_act :: "[('a=>'b) set, 'a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
- "drop_act C i act == {(f i, f' i) | f f'. (f,f'): act & f: C}"
+ drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
+ "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
lift_prog :: "['a, 'b program] => ('a => 'b) program"
"lift_prog i F ==
mk_program (lift_set i (Init F),
lift_act i `` Acts F)"
+ (*Argument C allows weak safety laws to be projected*)
drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
"drop_prog C i F ==
mk_program (drop_set i (Init F),
- drop_act C i `` (Acts F))"
+ drop_act i `` Restrict C `` (Acts F))"
(*simplifies the expression of specifications*)
constdefs
--- a/src/HOL/UNITY/Project.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Project.ML Mon Oct 18 15:18:24 1999 +0200
@@ -12,7 +12,7 @@
(** projection: monotonicity for safety **)
-Goal "D <= C ==> project_act D h act <= project_act C h act";
+Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
by (auto_tac (claset(), simpset() addsimps [project_act_def]));
qed "project_act_mono";
@@ -35,8 +35,8 @@
Goal "UNIV <= project_set h C \
\ ==> project C h ((extend h F) Join G) = F Join (project C h G)";
by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_Un, image_image,
- subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
+by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
+ subset_UNIV RS subset_trans RS Restrict_triv]) 2);
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
qed "project_extend_Join";
@@ -231,61 +231,106 @@
(*Opposite direction fails because Diff in the extended state may remove
fewer actions, i.e. those that affect other state variables.*)
-Goal "Diff (project C h G) (project_act C h `` acts) <= \
-\ project C h (Diff G acts)";
-by (auto_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def,
- UN_subset_iff]));
+Goalw [project_set_def, project_act_def]
+ "Restrict (project_set h C) (project_act h (Restrict C act)) = \
+\ project_act h (Restrict C act)";
+by (Blast_tac 1);
+qed "Restrict_project_act";
+
+Goalw [project_set_def, project_act_def]
+ "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
+by (Blast_tac 1);
+qed "project_act_Restrict_Id";
+
+Goal
+ "Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \
+\ <= project C h (Diff C G acts)";
+by (simp_tac
+ (simpset() addsimps [component_eq_subset, Diff_def,
+ Restrict_project_act, project_act_Restrict_Id,
+ image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
+by (Force_tac 1);
qed "Diff_project_project_component_project_Diff";
-Goal "(UN act:acts. Domain act) <= project_set h C \
-\ ==> Diff (project C h G) acts <= \
-\ project C h (Diff G (extend_act h `` acts))";
-by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
- UN_subset_iff]) 1);
-by (force_tac (claset() addSIs [image_diff_subset RS subsetD],
- simpset() addsimps [image_image_eq_UN]) 1);
+Goal "Diff (project_set h C) (project C h G) acts <= \
+\ project C h (Diff C G (extend_act h `` acts))";
+by (rtac component_trans 1);
+by (rtac Diff_project_project_component_project_Diff 2);
+by (simp_tac
+ (simpset() addsimps [component_eq_subset, Diff_def,
+ Restrict_project_act, project_act_Restrict_Id,
+ image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
+by (Blast_tac 1);
qed "Diff_project_component_project_Diff";
-Goal
- "[| (UN act:acts. Domain act) <= project_set h C; \
-\ Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
-\ ==> Diff (project C h G) acts : A co B";
-by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
+Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
+\ ==> Diff (project_set h C) (project C h G) acts : A co B";
+by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
by (rtac (project_constrains RS iffD2) 1);
by (ftac constrains_imp_subset 1);
-by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Diff_project_constrains";
Goalw [stable_def]
- "[| (UN act:acts. Domain act) <= project_set h C; \
-\ Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
-\ ==> Diff (project C h G) acts : stable A";
+ "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
+\ ==> Diff (project_set h C) (project C h G) acts : stable A";
by (etac Diff_project_constrains 1);
-by (assume_tac 1);
qed "Diff_project_stable";
+(** Some results for Diff, extend and project_set **)
+
+Goal "Diff C (extend h G) (extend_act h `` acts) \
+\ : (extend_set h A) co (extend_set h B) \
+\ ==> Diff (project_set h C) G acts : A co B";
+br (Diff_project_set_component RS component_constrains) 1;
+by (forward_tac [constrains_imp_subset] 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "Diff_project_set_constrains_I";
+
+Goalw [stable_def]
+ "Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \
+\ ==> Diff (project_set h C) G acts : stable A";
+by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1);
+qed "Diff_project_set_stable_I";
+
+Goalw [LOCALTO_def]
+ "extend h F : (v o f) localTo[C] extend h H \
+\ ==> F : v localTo[project_set h C] H";
+by Auto_tac;
+br Diff_project_set_stable_I 1;
+by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
+qed "localTo_project_set_I";
+
(*Converse fails: even if the conclusion holds, H could modify (v o f)
simultaneously with other variables, and this action would not be
superseded by anything in (extend h G) *)
-Goal "[| UNIV <= project_set h C; H : (func o f) localTo extend h G |] \
-\ ==> project C h H : func localTo G";
+Goal "H : (v o f) localTo[C] extend h G \
+\ ==> project C h H : v localTo[project_set h C] G";
by (asm_full_simp_tac
- (simpset() addsimps [localTo_def,
+ (simpset() addsimps [LOCALTO_def,
project_extend_Join RS sym,
- subset_UNIV RS subset_trans RS Diff_project_stable,
+ 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);
+Goal "extend h F Join G : (v o f) localTo[C] extend h H \
+\ ==> F Join project C h G : v localTo[project_set h C] H";
+by (asm_full_simp_tac
+ (simpset() addsimps [Join_localTo, localTo_project_set_I,
+ project_localTo_lemma]) 1);
+qed "gen_project_localTo_I";
+
+Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
+\ ==> F Join project UNIV h G : v localTo[UNIV] H";
+bd gen_project_localTo_I 1;
+by (Asm_full_simp_tac 1);
qed "project_localTo_I";
Goalw [projecting_def]
- "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
+ "projecting (%G. UNIV) h F \
+\ ((v o f) localTo[UNIV] extend h H) (v localTo[UNIV] H)";
by (blast_tac (claset() addIs [project_localTo_I]) 1);
qed "projecting_localTo";
@@ -428,6 +473,13 @@
Collect_eq_extend_set RS sym]) 1);
qed "project_Increasing";
+Goal "extend h F Join G : (v o f) LocalTo extend h H \
+\ ==> F Join project (reachable (extend h F Join G)) h G : v LocalTo H";
+by (asm_full_simp_tac
+ (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
+ gen_project_localTo_I]) 1);
+qed "project_LocalTo_I";
+
(** A lot of redundant theorems: all are proved to facilitate reasoning
about guarantees. **)
@@ -455,6 +507,12 @@
by (blast_tac (claset() addIs [project_Increasing_I]) 1);
qed "projecting_Increasing";
+Goalw [projecting_def]
+ "projecting (%G. reachable (extend h F Join G)) h F \
+\ ((v o f) LocalTo extend h H) (v LocalTo H)";
+by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
+qed "projecting_LocalTo";
+
Goalw [extending_def]
"extending (%G. reachable (extend h F Join G)) h F X' \
\ (extend_set h A Co extend_set h B) (A Co B)";
@@ -510,7 +568,7 @@
being enabled for all possible values of the new variables.*)
Goalw [transient_def]
"[| project C h F : transient A; \
-\ ALL act: Acts F. project_act C h act ^^ A <= - A --> \
+\ ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
\ Domain act <= C \
\ & extend_set h (project_set h (Domain act)) <= Domain act |] \
\ ==> F : transient (extend_set h A)";
@@ -622,7 +680,8 @@
\ extend h F : (extend h `` X) guarantees (extend h `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
-by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D,
+by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS
+ extend_Join_eq_extend_D,
guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
@@ -650,7 +709,7 @@
Goal "[| F : X guarantees Y; \
\ !!G. extend h F Join G : X' ==> F Join proj G h G : X; \
\ !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
-\ Disjoint (extend h F) G |] \
+\ Disjoint UNIV (extend h F) G |] \
\ ==> extend h F Join G : Y' |] \
\ ==> extend h F : X' guarantees Y'";
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
@@ -689,22 +748,22 @@
by Auto_tac;
qed "extend_guar_Increasing";
-Goal "F : (v localTo G) guarantees increasing func \
-\ ==> extend h F : (v o f) localTo (extend h G) \
+Goal "F : (v localTo[UNIV] G) guarantees increasing func \
+\ ==> extend h F : (v o f) localTo[UNIV] (extend h G) \
\ guarantees increasing (func o f)";
by (etac project_guarantees 1);
by (rtac extending_increasing 2);
by (rtac projecting_localTo 1);
qed "extend_localTo_guar_increasing";
-Goal "F : (v localTo G) guarantees Increasing func \
-\ ==> extend h F : (v 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);
by (rtac extending_Increasing 2);
-by (rtac projecting_localTo 1);
+by (rtac projecting_LocalTo 1);
by Auto_tac;
-qed "extend_localTo_guar_Increasing";
+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)";
@@ -729,8 +788,15 @@
but it can fail if C removes some parts of an action of G.*)
-Goal "[| G : f localTo extend h F; \
-\ Disjoint (extend h F) G |] ==> project C h G : stable {x}";
+Goal "[| G : v localTo[UNIV] F; Disjoint UNIV F G |] ==> G : stable {s. v s = z}";
+by (asm_full_simp_tac
+ (simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def,
+ stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_stable";
+
+Goal "[| G : f localTo[UNIV] extend h F; \
+\ Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}";
by (asm_full_simp_tac
(simpset() addsimps [localTo_imp_stable,
extend_set_sing, project_stable_I]) 1);
@@ -742,14 +808,9 @@
stable_def, constrains_def]));
qed "stable_sing_imp_not_transient";
-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; \
-\ G : f localTo extend h F; \
-\ Disjoint (extend h F) G |] \
+\ G : f localTo[UNIV] extend h F; \
+\ Disjoint UNIV (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 (Clarify_tac 1);
@@ -760,8 +821,8 @@
qed "project_leadsTo_D";
Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
-\ G : f localTo extend h F; \
-\ Disjoint (extend h F) G |] \
+\ G : f localTo[UNIV] extend h F; \
+\ Disjoint UNIV (extend h F) G |] \
\ ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
by (rtac (refl RS Join_project_LeadsTo) 1);
by (Clarify_tac 1);
@@ -773,7 +834,7 @@
Goalw [extending_def]
"extending (%G. UNIV) h F \
-\ (f localTo extend h F) \
+\ (f localTo[UNIV] extend h F) \
\ (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
addIs [project_leadsTo_D]) 1);
@@ -781,7 +842,7 @@
Goalw [extending_def]
"extending (%G. reachable (extend h F Join G)) h F \
-\ (f localTo extend h F) \
+\ (f localTo[UNIV] extend h F) \
\ (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
addIs [project_LeadsTo_D]) 1);
@@ -790,7 +851,7 @@
(*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')) \
-\ Int (f localTo (extend h F)) \
+\ Int (f localTo[UNIV] (extend h F)) \
\ guarantees ((extend_set h B) leadsTo (extend_set h B'))";
by (etac project_guarantees 1);
by (rtac (extending_leadsTo RS extending_weaken) 2);
@@ -801,7 +862,7 @@
(*WEAK precondition and postcondition*)
Goal "F : (A Co A') guarantees (B LeadsTo B') \
\ ==> extend h F : ((extend_set h A) Co (extend_set h A')) \
-\ Int (f localTo (extend h F)) \
+\ Int (f localTo[UNIV] (extend h F)) \
\ guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
by (etac project_guarantees 1);
by (rtac (extending_LeadsTo RS extending_weaken) 2);
--- a/src/HOL/UNITY/Project.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Project.thy Mon Oct 18 15:18:24 1999 +0200
@@ -20,7 +20,7 @@
'c program set, 'c program set, 'a program set] => bool"
"extending C h F X' Y' Y ==
ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
- Disjoint (extend h F) G
+ Disjoint UNIV (extend h F) G
--> extend h F Join G : Y'"
end
--- a/src/HOL/UNITY/Union.ML Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Mon Oct 18 15:18:24 1999 +0200
@@ -288,98 +288,122 @@
(** Diff and localTo **)
-Goalw [Diff_def] "F Join (Diff G (Acts F)) = F Join G";
+Goalw [Diff_def] "F Join (Diff UNIV G (Acts F)) = F Join G";
by (rtac program_equalityI 1);
by Auto_tac;
qed "Join_Diff2";
Goalw [Diff_def]
- "Diff (F Join G) (Acts H) = (Diff F (Acts H)) Join (Diff G (Acts H))";
+ "Diff C (F Join G) (Acts H) = (Diff C F (Acts H)) Join (Diff C G (Acts H))";
by (rtac program_equalityI 1);
by Auto_tac;
qed "Diff_Join_distrib";
-Goalw [Diff_def, constrains_def] "(Diff F (Acts F) : A co B) = (A <= B)";
+Goalw [Diff_def] "Diff C F (Acts F) = mk_program(Init F, {})";
by Auto_tac;
-qed "Diff_self_constrains";
+qed "Diff_self_eq";
-Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
-by Auto_tac;
+Goalw [Diff_def, Disjoint_def] "Disjoint C F (Diff C G (Acts F))";
+by (force_tac (claset(),
+ simpset() addsimps [Restrict_imageI,
+ sym RSN (2,Restrict_imageI)]) 1);
qed "Diff_Disjoint";
-Goal "[| G : v localTo F; Disjoint F G |] ==> G : stable {s. v s = z}";
-by (asm_full_simp_tac
- (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
- stable_def, constrains_def]) 1);
-by (Blast_tac 1);
-qed "localTo_imp_stable";
+Goalw [Disjoint_def]
+ "[| A <= B; Disjoint A F G |] ==> Disjoint B F G";
+by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
+qed "Disjoint_mono";
+
+(*** localTo ***)
-Goalw [localTo_def, stable_def, constrains_def]
- "v localTo F <= (f o v) localTo F";
+Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
+ "A <= B ==> v localTo[B] F <= v localTo[A] F";
+by Auto_tac;
+by (dres_inst_tac [("x", "v xc")] spec 1);
+by (dres_inst_tac [("x", "Restrict B xa")] bspec 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
+qed "localTo_anti_mono";
+
+Goalw [LocalTo_def]
+ "G : v localTo[UNIV] F ==> G : v LocalTo F";
+by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
+qed "localTo_imp_LocalTo";
+
+Goalw [LOCALTO_def, stable_def, constrains_def]
+ "v localTo[C] F <= (f o v) localTo[C] F";
by (Clarify_tac 1);
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";
+Goalw [LOCALTO_def, stable_def, constrains_def]
+ "(%s. x) localTo[C] 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)";
+Goal "(F Join G : v localTo[C] H) = (F : v localTo[C] H & G : v localTo[C] H)";
by (asm_full_simp_tac
- (simpset() addsimps [localTo_def, Diff_Join_distrib,
+ (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
stable_def, Join_constrains]) 1);
by (Blast_tac 1);
qed "Join_localTo";
-Goal "F : v localTo F";
+Goal "F : v localTo[C] F";
by (simp_tac
- (simpset() addsimps [localTo_def, stable_def, Diff_self_constrains]) 1);
+ (simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
+ Diff_self_eq]) 1);
qed "self_localTo";
(*** Higher-level rules involving localTo and Join ***)
-Goal "[| F : {s. P (v s)} co {s. P' (v s)}; G : v localTo F |] \
-\ ==> F Join G : {s. P (v s)} co {s. P' (v s)}";
-by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
+Goal "[| F : {s. P (v s)} co {s. P' (v s)}; G : v localTo[C] F |] \
+\ ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
+by (ftac constrains_imp_subset 1);
by (auto_tac (claset(),
- simpset() addsimps [localTo_def, stable_def, constrains_def,
+ simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
Diff_def]));
-by (case_tac "act: Acts F" 1);
-by (Blast_tac 1);
-by (dtac bspec 1 THEN rtac Id_in_Acts 1);
+by (case_tac "Restrict C act: Restrict C `` Acts F" 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
by (subgoal_tac "v x = v xa" 1);
+by (Force_tac 1);
+by (thin_tac "ALL act: ?A. ?P act" 1);
+by (dtac spec 1);
+by (dres_inst_tac [("x", "Restrict C act")] bspec 1);
by Auto_tac;
qed "constrains_localTo_constrains";
-Goalw [localTo_def, stable_def, constrains_def, Diff_def]
- "[| G : v localTo F; G : w localTo F |] \
-\ ==> G : (%s. (v s, w s)) localTo F";
+Goalw [LOCALTO_def, stable_def, constrains_def, Diff_def]
+ "[| G : v localTo[C] F; G : w localTo[C] F |] \
+\ ==> G : (%s. (v s, w s)) localTo[C] F";
by (Blast_tac 1);
qed "localTo_pairfun";
Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)}; \
-\ G : v localTo F; \
-\ G : w localTo F |] \
-\ ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (res_inst_tac [("A", "{s. (%(x,y). P x y) (v s, w s)}"),
+\ G : v localTo[C] F; \
+\ G : w localTo[C] F |] \
+\ ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
+by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
("A'", "{s. (%(x,y). P' x y) (v s, w s)}")]
constrains_weaken 1);
by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
by Auto_tac;
qed "constrains_localTo_constrains2";
+(*Used just once, in Client.ML. Having F in the conclusion is silly.*)
Goalw [stable_def]
"[| F : stable {s. P (v s) (w s)}; \
-\ G : v localTo F; G : w localTo F |] \
+\ G : v localTo[UNIV] F; G : w localTo[UNIV] F |] \
\ ==> F Join G : stable {s. P (v s) (w s)}";
-by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
+by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_localTo_constrains2 RS
+ constrains_weaken]) 1);
qed "stable_localTo_stable2";
+(*Used just in Client.ML. Generalize to arbitrary C?*)
Goal "[| F : stable {s. v s <= w s}; \
-\ G : v localTo F; \
+\ G : v localTo[UNIV] F; \
\ F Join G : Increasing w |] \
\ ==> F Join G : Stable {s. v s <= w s}";
by (auto_tac (claset(),
@@ -388,8 +412,8 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
(*The G case remains; proved like constrains_localTo_constrains*)
by (auto_tac (claset(),
- simpset() addsimps [localTo_def, stable_def, constrains_def,
- Diff_def]));
+ simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
+ Diff_def]));
by (case_tac "act: Acts F" 1);
by (Blast_tac 1);
by (thin_tac "ALL act:Acts F. ?P act" 1);
--- a/src/HOL/UNITY/Union.thy Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Union.thy Mon Oct 18 15:18:24 1999 +0200
@@ -22,17 +22,25 @@
SKIP :: 'a program
"SKIP == mk_program (UNIV, {})"
- Diff :: "['a program, ('a * 'a)set set] => 'a program"
- "Diff F acts == mk_program (Init F, Acts F - acts)"
+ Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
+ "Diff C G acts ==
+ mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
(*The set of systems that regard "v" as local to F*)
- localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
- "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
+ LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
+ ("(_/ localTo[_]/ _)" [80,0,80] 80)
+ "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
+
+ (*The weak version of localTo, considering only G's reachable states*)
+ LocalTo :: ['a => 'b, 'a program] => 'a program set (infixl 80)
+ "v LocalTo F == {G. G : v localTo[reachable G] F}"
(*Two programs with disjoint actions, except for identity actions.
It's a weak property but still useful.*)
- Disjoint :: ['a program, 'a program] => bool
- "Disjoint F G == Acts F Int Acts G <= {Id}"
+ Disjoint :: ['a set, 'a program, 'a program] => bool
+ "Disjoint C F G ==
+ (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
+ <= {}"
syntax
"@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10)