--- a/src/ZF/UNITY/Comp.ML Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/UNITY/Comp.ML Tue May 27 11:39:03 2003 +0200
@@ -109,6 +109,15 @@
(*** preserves ***)
+Goalw [preserves_def, safety_prop_def]
+ "safety_prop(preserves(f))";
+by (auto_tac (claset() addDs [ActsD], simpset() addsimps [stable_def, constrains_def]));
+by (dres_inst_tac [("c", "act")] subsetD 1);
+by Auto_tac;
+qed "preserves_is_safety_prop";
+Addsimps [preserves_is_safety_prop];
+
+
val prems = Goalw [preserves_def]
"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)";
by Auto_tac;
@@ -142,6 +151,86 @@
AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
+Goalw [fun_pair_def] "fun_pair(f,g,x) = <f(x), g(x)>";
+by (Simp_tac 1);
+qed "fun_pair_apply";
+Addsimps [fun_pair_apply];
+
+Goal "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)";
+by (rtac equalityI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
+by (REPEAT(Blast_tac 1));
+qed "preserves_fun_pair";
+
+Goal "F:preserves(fun_pair(v, w)) <-> F:preserves(v) Int preserves(w)";
+by (simp_tac (simpset() addsimps [preserves_fun_pair]) 1);
+qed "preserves_fun_pair_iff";
+AddIffs [preserves_fun_pair_iff];
+
+Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
+by (simp_tac (simpset() addsimps [fun_pair_def, comp_def]) 1);
+qed "fun_pair_comp_distrib";
+
+Goal "(f comp g)(x) = f(g(x))";
+by (simp_tac (simpset() addsimps [comp_def]) 1);
+qed "comp_apply";
+Addsimps [comp_apply];
+
+Goalw [preserves_def]
+ "preserves(v)<=program";
+by Auto_tac;
+qed "preserves_type";
+
+Goal "F:preserves(f) ==> F:program";
+by (blast_tac (claset() addIs [preserves_type RS subsetD]) 1);
+qed "preserves_into_program";
+AddTCs [preserves_into_program];
+
+Goal "preserves(f) <= preserves(g comp f)";
+by (auto_tac (claset(), simpset()
+ addsimps [preserves_def, stable_def, constrains_def]));
+by (dres_inst_tac [("x", "f(xb)")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by Auto_tac;
+qed "subset_preserves_comp";
+
+Goal "F:preserves(f) ==> F:preserves(g comp f)";
+by (blast_tac (claset() addIs [subset_preserves_comp RS subsetD]) 1);
+qed "imp_preserves_comp";
+
+Goal "preserves(f) <= stable({s:state. P(f(s))})";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, stable_def, constrains_def]));
+by (rename_tac "s' s" 1);
+by (subgoal_tac "f(s) = f(s')" 1);
+by (ALLGOALS Force_tac);
+qed "preserves_subset_stable";
+
+Goal "F:preserves(f) ==> F:stable({s:state. P(f(s))})";
+by (blast_tac (claset() addIs [preserves_subset_stable RS subsetD]) 1);
+qed "preserves_imp_stable";
+
+Goalw [increasing_def]
+ "[| F:preserves(f); ALL x:state. f(x):A |] ==> F:Increasing.increasing(A, r, f)";
+by (auto_tac (claset() addIs [preserves_into_program],
+ simpset()));
+by (res_inst_tac [("P", "%x. <k, x>:r")] preserves_imp_stable 1);
+by Auto_tac;
+qed "preserves_imp_increasing";
+
+Goalw [preserves_def, stable_def, constrains_def]
+ "st_set(A) ==> preserves(%x. x) <= stable(A)";
+by Auto_tac;
+by (dres_inst_tac [("x", "xb")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by (auto_tac (claset() addDs [ActsD], simpset()));
+qed "preserves_id_subset_stable";
+
+Goal "[| F:preserves(%x. x); st_set(A) |] ==> F:stable(A)";
+by (blast_tac (claset() addIs [preserves_id_subset_stable RS subsetD]) 1);
+qed "preserves_id_imp_stable";
+
(** Added by Sidi **)
(** component_of **)
@@ -190,3 +279,70 @@
AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
+(** Theorems used in ClientImpl **)
+
+Goal
+ "[| F:stable({s:state. P(f(s), g(s))}); G:preserves(f); G:preserves(g) |] \
+\ ==> F Join G : stable({s:state. P(f(s), g(s))})";
+by (auto_tac (claset() addDs [ActsD, preserves_into_program],
+ simpset() addsimps [stable_def, constrains_def]));
+by (case_tac "act:Acts(F)" 1);
+by Auto_tac;
+by (dtac preserves_imp_eq 1);
+by (dtac preserves_imp_eq 3);
+by Auto_tac;
+qed "stable_localTo_stable2";
+
+Goal "[| F : stable({s:state. <f(s), g(s)>:r}); G:preserves(f); \
+\ F Join G : Increasing(A, r, g); \
+\ ALL x:state. f(x):A & g(x):A |] \
+\ ==> F Join G : Stable({s:state. <f(s), g(s)>:r})";
+by (auto_tac (claset(),
+ simpset() addsimps [stable_def, Stable_def, Increasing_def,
+ Constrains_def, all_conj_distrib]));
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [constrains_type RS subsetD, preserves_type RS subsetD])));
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+(*The G case remains*)
+by (auto_tac (claset() addDs [ActsD],
+ simpset() addsimps [preserves_def, stable_def, constrains_def,
+ ball_conj_distrib, all_conj_distrib]));
+(*We have a G-action, so delete assumptions about F-actions*)
+by (thin_tac "ALL act:Acts(F). ?P(act)" 1);
+by (thin_tac "\\<forall>k\\<in>A. ALL act:Acts(F). ?P(k,act)" 1);
+by (subgoal_tac "f(x) = f(xa)" 1);
+by (auto_tac (claset() addSDs [bspec], simpset()));
+qed "Increasing_preserves_Stable";
+
+
+(** Lemma used in AllocImpl **)
+
+Goalw [Constrains_def, constrains_def]
+"[| ALL x:I. F: A(x) Co B; F:program |] ==> F:(UN x:I. A(x)) Co B";
+by Auto_tac;
+qed "Constrains_UN_left";
+
+Goalw [stable_def, Stable_def, preserves_def]
+ "[| F:stable({s:state. P(f(s), g(s))}); \
+\ ALL k:A. F Join G: Stable({s:state. P(k, g(s))}); \
+\ G:preserves(f); ALL s:state. f(s):A|] ==> \
+\ F Join G : Stable({s:state. P(f(s), g(s))})";
+by (res_inst_tac [("A", "(UN k:A. {s:state. f(s)=k} Int {s:state. P(f(s), g(s))})")]
+ Constrains_weaken_L 1);
+by (Blast_tac 2);
+by (rtac Constrains_UN_left 1);
+by Auto_tac;
+by (res_inst_tac [("A", "{s:state. f(s)=k} Int {s:state. P(f(s), g(s))} Int \
+\ {s:state. P(k, g(s))}"),
+ ("A'", "({s:state. f(s)=k} Un {s:state. P(f(s), g(s))}) \
+\ Int {s:state. P(k, g(s))}")] Constrains_weaken 1);
+by (REPEAT(Blast_tac 2));
+by (rtac Constrains_Int 1);
+by (rtac constrains_imp_Constrains 1);
+by (auto_tac (claset(), simpset() addsimps [constrains_type RS subsetD]));
+by (ALLGOALS(rtac constrains_weaken));
+by (rotate_tac ~1 4);
+by (dres_inst_tac [("x", "k")] spec 4);
+by (REPEAT(Blast_tac 1));
+qed "stable_Join_Stable";
+