--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Comp.ML Wed Aug 08 14:33:10 2001 +0200
@@ -0,0 +1,214 @@
+(* Title: ZF/UNITY/Comp.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 1998 University of Cambridge
+Composition
+From Chandy and Sanders, "Reasoning About Program Composition"
+
+Revised by Sidi Ehmety on January 2001
+
+*)
+
+(*** component and strict_component relations ***)
+
+Goalw [component_def]
+ "H component F | H component G ==> H component (F Join G)";
+by Auto_tac;
+by (res_inst_tac [("x", "Ga Join G")] exI 1);
+by (res_inst_tac [("x", "G Join F")] exI 2);
+by (auto_tac (claset(), simpset() addsimps Join_ac));
+qed "componentI";
+
+Goalw [component_def]
+ "G:program ==> (F component G) <-> \
+\ (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))";
+by Auto_tac;
+by (rtac exI 1);
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "component_eq_subset";
+
+
+Goalw [component_def]
+ "F:program ==> SKIP component F";
+by (res_inst_tac [("x", "F")] exI 1);
+by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
+qed "component_SKIP";
+
+
+Goalw [component_def]
+"F:program ==> F component F";
+by (res_inst_tac [("x", "F")] exI 1);
+by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
+qed "component_refl";
+
+Addsimps [component_SKIP, component_refl];
+
+Goal "F component SKIP ==> programify(F) = SKIP";
+by (rtac program_equalityI 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset])));
+by (Blast_tac 1);
+qed "SKIP_minimal";
+
+
+Goalw [component_def] "F component (F Join G)";
+by (Blast_tac 1);
+qed "component_Join1";
+
+
+Goalw [component_def] "G component (F Join G)";
+by (simp_tac (simpset() addsimps [Join_commute]) 1);
+by (Blast_tac 1);
+qed "component_Join2";
+
+Goal "F component G ==> F Join G = G";
+by (auto_tac (claset(), simpset()
+ addsimps [component_def, Join_left_absorb]));
+qed "Join_absorb1";
+
+Goal "G component F ==> F Join G = F";
+by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
+qed "Join_absorb2";
+
+
+
+Goal "H:program ==> \
+\ (JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)";
+by (case_tac "I=0" 1);
+by (Force_tac 1);
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by Auto_tac;
+by (dres_inst_tac [("c", "xb"), ("A", "AllowedActs(H)")] subsetD 2);
+by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
+qed "JN_component_iff";
+
+
+Goalw [component_def] "i : I ==> F(i) component (JN i:I. (F(i)))";
+by (blast_tac (claset() addIs [JN_absorb]) 1);
+qed "component_JN";
+
+
+Goalw [component_def] "[| F component G; G component H |] ==> F component H";
+by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
+qed "component_trans";
+
+Goal "[| F:program; G:program |] ==> \
+\ (F component G & G component F) --> F = G";
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Clarify_tac 1);
+by (rtac program_equalityI 1);
+by Auto_tac;
+qed "component_antisym";
+
+Goal "H:program ==> ((F Join G) component H) <-> (F component H & G component H)";
+by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Blast_tac 1);
+qed "Join_component_iff";
+
+
+Goal "[| F component G; G:A co B; F:program |] ==> F : A co B";
+by (forward_tac [constrainsD2] 1);
+by (rotate_tac ~1 1);
+by (auto_tac (claset(),
+ simpset() addsimps [constrains_def, component_eq_subset]));
+qed "component_constrains";
+
+(*Used in Guar.thy to show that programs are partially ordered*)
+(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
+
+
+(*** preserves ***)
+
+val prems =
+Goalw [preserves_def]
+"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)";
+by Auto_tac;
+by (blast_tac (claset() addDs [stableD2]) 1);
+bind_thm("preservesI", allI RS result());
+
+Goalw [preserves_def, stable_def, constrains_def]
+ "[| F:preserves(f); act : Acts(F); <s,t> : act |] ==> f(s) = f(t)";
+by (subgoal_tac "s:state & t:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by Auto_tac;
+by (dres_inst_tac [("x", "f(s)")] spec 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by Auto_tac;
+qed "preserves_imp_eq";
+
+Goalw [preserves_def]
+"(F Join G : preserves(v)) <-> \
+\ (programify(F) : preserves(v) & programify(G) : preserves(v))";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+qed "Join_preserves";
+
+
+Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))";
+by (auto_tac (claset(), simpset() addsimps
+ [JN_stable, preserves_def, INT_iff]@state_simps));
+qed "JN_preserves";
+
+Goal "SKIP : preserves(v)";
+by (auto_tac (claset(), simpset()
+ addsimps [preserves_def, INT_iff]@state_simps));
+qed "SKIP_preserves";
+
+AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
+
+
+
+
+(** component_of **)
+
+(* component_of is stronger than component *)
+Goalw [component_def, component_of_def]
+"F component_of H ==> F component H";
+by (Blast_tac 1);
+qed "component_of_imp_component";
+
+
+
+(* component_of satisfies many of the <='s properties *)
+Goalw [component_of_def]
+"F:program ==> F component_of F";
+by (res_inst_tac [("x", "SKIP")] exI 1);
+by Auto_tac;
+qed "component_of_refl";
+
+
+
+Goalw [component_of_def]
+"F:program ==>SKIP component_of F";
+by Auto_tac;
+by (res_inst_tac [("x", "F")] exI 1);
+by Auto_tac;
+qed "component_of_SKIP";
+
+Addsimps [component_of_refl, component_of_SKIP];
+
+
+
+Goalw [component_of_def]
+"[| F component_of G; G component_of H |] ==> F component_of H";
+by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
+qed "component_of_trans";
+
+
+(** localize **)
+Goalw [localize_def]
+ "Init(localize(v,F)) = Init(F)";
+by (Simp_tac 1);
+qed "localize_Init_eq";
+
+
+Goalw [localize_def]
+ "Acts(localize(v,F)) = Acts(F)";
+by (Simp_tac 1);
+qed "localize_Acts_eq";
+
+Goalw [localize_def]
+ "AllowedActs(localize(v,F)) = AllowedActs(F Int (UN G:preserves(v). Acts(G)))";
+by Auto_tac;
+qed "localize_AllowedActs_eq";
+
+Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];