src/HOL/UNITY/Union.ML

Union primitives and examples

(*  Title:      HOL/UNITY/Union.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Unions of programs

From Misra's Chapter 5: Asynchronous Compositions of Programs

NOT CLEAR WHETHER ALL THESE FORMS ARE NEEDED: 
    Maybe Join instead of Un, and JOIN for UNION
*)

(*** Safety: constrains, stable, FP ***)

Goalw [constrains_def]
    "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
by (Blast_tac 1);
qed "constrains_UN";

Goalw [constrains_def]
    "constrains (actsF Un actsG) A B =  \
\    (constrains actsF A B & constrains actsG A B)";
by (simp_tac (simpset() addsimps [ball_Un]) 1);
qed "constrains_Un";

(*Provable by constrains_Un and constrains_weaken, but why bother?*)
Goalw [constrains_def]
     "[| constrains actsF A A';  constrains actsG B B' |] \
\     ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
by (Blast_tac 1);
qed "constrains_Un_weaken";

Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
by (simp_tac (simpset() addsimps [constrains_UN]) 1);
qed "stable_UN";

Goalw [stable_def]
    "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
by (simp_tac (simpset() addsimps [constrains_Un]) 1);
qed "stable_Un";

Goal "stable (Acts (Join prgF prgG)) A = \
\     (stable (Acts prgF) A & stable (Acts prgG) A)";
by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
qed "stable_Join";

Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
qed "FP_UN";


(*** Progress: transient, ensures ***)

Goalw [transient_def]
    "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
by (Simp_tac 1);
qed "transient_UN";

Goalw [ensures_def,transient_def]
    "ensures (UN i:I. acts i) A B = \
\    ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
\     (EX i:I. ensures (acts i) A B))";
by (simp_tac (simpset() addsimps [constrains_UN]) 1);
by Auto_tac;
qed "ensures_UN";

(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
Goal "ensures (actsF Un actsG) A B =     \
\     (constrains actsF (A-B) (A Un B) & \
\      constrains actsG (A-B) (A Un B) & \
\      (ensures actsF A B | ensures actsG A B))";
by (simp_tac (simpset() addcongs [conj_cong]
			addsimps [ensures_UN, Un_eq_UN,
				  all_bool_eq, ex_bool_eq]) 1);
qed "ensures_Un";

(*Or a longer proof via constrains_imp_subset*)
Goalw [stable_def, constrains_def]
     "[| stable actsF A;  constrains actsG A A';  id: actsG |] \
\     ==> constrains (actsF Un actsG) A A'";
by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
qed "stable_constrains_Un";

Goalw [Join_def]
      "[| stable (Acts prgF) A;  invariant prgG A |]     \
\      ==> invariant (Join prgF prgG) A";
by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
by (Blast_tac 1);
qed "stable_Join_invariant";

Goal "[| stable actsF A;  ensures actsG A B |]     \
\     ==> ensures (actsF Un actsG) A B";
by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
by (etac constrains_weaken 1);
by Auto_tac;
qed "ensures_stable_Un1";

Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
\     ==> ensures (Acts (Join prgF prgG)) A B";
by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
qed "ensures_stable_Join1";

(*As above, but exchanging the roles of F and G*)
Goal "[| ensures actsF A B;  stable actsG A |]     \
\     ==> ensures (actsF Un actsG) A B";
by (stac Un_commute 1);
by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
qed "ensures_stable_Un2";

Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
\     ==> ensures (Acts (Join prgF prgG)) A B";
by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
qed "ensures_stable_Join2";