(* Title: HOL/UNITY/Comp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Composition
From Chandy and Sanders, "Reasoning About Program Composition"
*)
(*** component ***)
Goalw [component_def]
"H <= F | H <= G ==> H <= (F Join G)";
by Auto_tac;
by (res_inst_tac [("x", "G Join Ga")] 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]
"(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
by (force_tac (claset() addSIs [exI, program_equalityI],
simpset()) 1);
qed "component_eq_subset";
Goalw [component_def] "SKIP <= F";
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
qed "component_SKIP";
Goalw [component_def] "F <= (F :: 'a program)";
by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
qed "component_refl";
AddIffs [component_SKIP, component_refl];
Goal "F <= SKIP ==> F = SKIP";
by (auto_tac (claset() addSIs [program_equalityI],
simpset() addsimps [component_eq_subset]));
qed "SKIP_minimal";
Goalw [component_def] "F <= (F Join G)";
by (Blast_tac 1);
qed "component_Join1";
Goalw [component_def] "G <= (F Join G)";
by (simp_tac (simpset() addsimps [Join_commute]) 1);
by (Blast_tac 1);
qed "component_Join2";
Goal "F<=G ==> F Join G = G";
by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb]));
qed "Join_absorb1";
Goal "G<=F ==> F Join G = F";
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
qed "Join_absorb2";
Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (Blast_tac 1);
qed "JN_component_iff";
Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
by (blast_tac (claset() addIs [JN_absorb]) 1);
qed "component_JN";
Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)";
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
qed "component_trans";
Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)";
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (blast_tac (claset() addSIs [program_equalityI]) 1);
qed "component_antisym";
Goal "((F Join G) <= H) = (F <= H & G <= H)";
by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (Blast_tac 1);
qed "Join_component_iff";
Goal "[| F <= G; G : A co B |] ==> F : A co B";
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] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
by (blast_tac (claset() addIs prems) 1);
qed "preservesI";
Goalw [preserves_def, stable_def, constrains_def]
"[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'";
by (Force_tac 1);
qed "preserves_imp_eq";
Goalw [preserves_def]
"(F Join G : preserves v) = (F : preserves v & G : preserves v)";
by Auto_tac;
qed "Join_preserves";
Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1);
by (Blast_tac 1);
qed "JN_preserves";
AddIffs [Join_preserves, JN_preserves];
Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
by (Simp_tac 1);
qed "funPair_apply";
Addsimps [funPair_apply];
Goal "preserves (funPair v w) = preserves v Int preserves w";
by (auto_tac (claset(),
simpset() addsimps [preserves_def, stable_def, constrains_def]));
by (Blast_tac 1);
qed "preserves_funPair";
(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
AddIffs [preserves_funPair RS eqset_imp_iff];
Goal "(funPair f g) o h = funPair (f o h) (g o h)";
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "funPair_o_distrib";
Goal "fst o (funPair f g) = f";
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "fst_o_funPair";
Goal "snd o (funPair f g) = g";
by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
qed "snd_o_funPair";
Addsimps [fst_o_funPair, snd_o_funPair];
Goal "preserves v <= preserves (w o v)";
by (force_tac (claset(),
simpset() addsimps [preserves_def,
stable_def, constrains_def]) 1);
qed "subset_preserves_o";
Goal "preserves v <= stable {s. P (v s)}";
by (auto_tac (claset(),
simpset() addsimps [preserves_def, stable_def, constrains_def]));
by (rename_tac "s' s" 1);
by (subgoal_tac "v s = v s'" 1);
by (ALLGOALS Force_tac);
qed "preserves_subset_stable";
Goal "preserves v <= increasing v";
by (auto_tac (claset(),
simpset() addsimps [impOfSubs preserves_subset_stable,
increasing_def]));
qed "preserves_subset_increasing";
Goal "preserves id <= stable A";
by (force_tac (claset(),
simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
qed "preserves_id_subset_stable";
(** Some lemmas used only in Client.ML **)
Goal "[| F : stable {s. P (v s) (w s)}; \
\ G : preserves v; G : preserves w |] \
\ ==> F Join G : stable {s. P (v s) (w s)}";
by (Asm_simp_tac 1);
by (subgoal_tac "G: preserves (funPair v w)" 1);
by (Asm_simp_tac 2);
by (dres_inst_tac [("P1", "split ?Q")]
(impOfSubs preserves_subset_stable) 1);
by Auto_tac;
qed "stable_localTo_stable2";
Goal "[| F : stable {s. v s <= w s}; G : preserves v; \
\ F Join G : Increasing w |] \
\ ==> F Join G : Stable {s. v s <= w s}";
by (auto_tac (claset(),
simpset() addsimps [stable_def, Stable_def, Increasing_def,
Constrains_def, all_conj_distrib]));
by (blast_tac (claset() addIs [constrains_weaken]) 1);
(*The G case remains*)
by (auto_tac (claset(),
simpset() addsimps [preserves_def, stable_def, constrains_def]));
by (case_tac "act: Acts F" 1);
by (Blast_tac 1);
(*We have a G-action, so delete assumptions about F-actions*)
by (thin_tac "ALL act:Acts F. ?P act" 1);
by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
by (subgoal_tac "v x = v xa" 1);
by (Blast_tac 2);
by Auto_tac;
by (etac order_trans 1);
by (Blast_tac 1);
qed "Increasing_preserves_Stable";