(* Title: ZF/UNITY/Union.ML
ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
Unions of programs
From Misra's Chapter 5: Asynchronous Compositions of Programs
Proofs ported from HOL.
*)
(** SKIP **)
Goal "reachable(SKIP) = state";
by (force_tac (claset() addEs [reachable.induct]
addIs reachable.intrs, simpset()) 1);
qed "reachable_SKIP";
Addsimps [reachable_SKIP];
(* Elimination programify from ok and Join *)
Goal "programify(F) ok G <-> F ok G";
by (simp_tac (simpset() addsimps [ok_def]) 1);
qed "ok_programify_left";
Goal "F ok programify(G) <-> F ok G";
by (simp_tac (simpset() addsimps [ok_def]) 1);
qed "ok_programify_right";
Goal "programify(F) Join G = F Join G";
by (simp_tac (simpset() addsimps [Join_def]) 1);
qed "Join_programify_left";
Goal "F Join programify(G) = F Join G";
by (simp_tac (simpset() addsimps [Join_def]) 1);
qed "Join_programify_right";
Addsimps [ok_programify_left, ok_programify_right,
Join_programify_left, Join_programify_right];
(** SKIP and safety properties **)
Goalw [constrains_def]
"[| A:condition; B:condition |] ==> (SKIP: A co B) <-> (A<=B)";
by Auto_tac;
qed "SKIP_in_constrains_iff";
Addsimps [SKIP_in_constrains_iff];
Goalw [Constrains_def]
"[| A:condition; B:condition |] ==> (SKIP : A Co B)<-> (A<=B)";
by (Asm_simp_tac 1);
by (auto_tac (claset(),
simpset() addsimps [condition_def]));
qed "SKIP_in_Constrains_iff";
Addsimps [SKIP_in_Constrains_iff];
Goal "A:condition ==>SKIP : stable(A)";
by (auto_tac (claset(),
simpset() addsimps [stable_def]));
qed "SKIP_in_stable";
Addsimps [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable];
(** Join and JOIN types **)
Goalw [Join_def]
"F Join G : program";
by Auto_tac;
qed "Join_in_program";
AddIffs [Join_in_program];
AddTCs [Join_in_program];
Goalw [JOIN_def]
"JOIN(I,F):program";
by Auto_tac;
qed "JOIN_in_program";
AddIffs [JOIN_in_program];
AddTCs [JOIN_in_program];
(* Init, Acts, and AllowedActs of Join and JOIN *)
Goal "Init(F Join G) = Init(F) Int Init(G)";
by (simp_tac (simpset()
addsimps [Int_assoc, Join_def]) 1);
qed "Init_Join";
Goal "Acts(F Join G) = Acts(F) Un Acts(G)";
by (simp_tac (simpset()
addsimps [Int_Un_distrib,cons_absorb,Join_def]) 1);
qed "Acts_Join";
Goal "AllowedActs(F Join G) = \
\ AllowedActs(F) Int AllowedActs(G)";
by (simp_tac (simpset()
addsimps [Int_assoc,cons_absorb,Join_def]) 1);
qed "AllowedActs_Join";
Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
(** Join's algebraic laws **)
Goal "F Join G = G Join F";
by (simp_tac (simpset() addsimps
[Join_def, Un_commute, Int_commute]) 1);
qed "Join_commute";
Goal "A Join (B Join C) = B Join (A Join C)";
by (asm_simp_tac (simpset() addsimps
Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1);
qed "Join_left_commute";
Goal "(F Join G) Join H = F Join (G Join H)";
by (asm_simp_tac (simpset() addsimps
Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib]) 1);
qed "Join_assoc";
Goalw [Join_def, SKIP_def]
"SKIP Join F = programify(F)";
by (simp_tac (simpset() addsimps [Int_absorb, cons_absorb,cons_eq]) 1);
qed "Join_SKIP_left";
Goal "F Join SKIP = programify(F)";
by (stac Join_commute 1);
by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1);
qed "Join_SKIP_right";
Addsimps [Join_SKIP_left, Join_SKIP_right];
Goal "F Join F = programify(F)";
by (rtac program_equalityI 1);
by Auto_tac;
qed "Join_absorb";
Addsimps [Join_absorb];
Goal "F Join (F Join G) = F Join G";
by (asm_simp_tac (simpset() addsimps [Join_assoc RS sym]) 1);
qed "Join_left_absorb";
(*Join is an AC-operator*)
val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
(** Eliminating programify in JN and OK expressions **)
Goal "OK(I, %x. programify(F(x))) <-> OK(I, F)";
by (simp_tac (simpset() addsimps [OK_def]) 1);
qed "OK_programify";
Goal "JOIN(I, %x. programify(F(x))) = JOIN(I, F)";
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
qed "JN_programify";
Addsimps [OK_programify, JN_programify];
(* JN *)
Goalw [JOIN_def]
"JOIN(0, F) = SKIP";
by Auto_tac;
qed "JN_empty";
Addsimps [JN_empty];
AddSEs [not_emptyE];
Addsimps [Inter_0];
Goal
"Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (auto_tac (claset(), simpset()
addsimps [JOIN_def,INT_Int_distrib2]));
qed "Init_JN";
Goal
"Acts(JOIN(I,F)) = cons(Id, UN i:I. Acts(F(i)))";
by (auto_tac (claset(),
simpset() addsimps [JOIN_def, UN_Int_distrib]));
qed "Acts_JN";
Goal
"AllowedActs(JN i:I. F(i)) = (if I=0 then action else (INT i:I. AllowedActs(F(i))))";
by (auto_tac (claset(), simpset()
addsimps [JOIN_def, INT_cons RS sym, INT_Int_distrib2]));
qed "AllowedActs_JN";
Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))";
by (rtac program_equalityI 1);
by Auto_tac;
qed "JN_cons";
Addsimps[JN_cons];
val prems = Goalw [JOIN_def]
"[| I=J; !!i. i:J ==> F(i) = G(i) |] ==> \
\ (JN i:I. F(i)) = (JN i:J. G(i))";
by (asm_simp_tac (simpset() addsimps prems) 1);
qed "JN_cong";
Addcongs [JN_cong];
(*** JN laws ***)
Goal "k:I ==>F(k) Join (JN i:I. F(i)) = (JN i:I. F(i))";
by (stac (JN_cons RS sym) 1);
by (auto_tac (claset(),
simpset() addsimps [cons_absorb]));
qed "JN_absorb";
Goalw [Inter_def] "[| i:I; j:J |] ==> \
\ (INT i:I Un J. A(i)) = ((INT i:I. A(i)) Int (INT j:J. A(j)))";
by Auto_tac;
by (Blast_tac 1);
qed "INT_Un";
Goal "(JN i: I Un J. F(i)) = ((JN i: I. F(i)) Join (JN i:J. F(i)))";
by (rtac program_equalityI 1);
by (ALLGOALS(Asm_full_simp_tac));
by Safe_tac;
by (ALLGOALS(asm_full_simp_tac (simpset()
addsimps [Int_absorb, INT_Int_distrib2,
Int_INT_distrib, UN_cons, INT_cons])));
by (ALLGOALS(Clarify_tac));
by (REPEAT(Blast_tac 1));
qed "JN_Un";
Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))";
by (rtac program_equalityI 1);
by Auto_tac;
qed "JN_constant";
Goal
"(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))";
by (rtac program_equalityI 1);
by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb])));
by Safe_tac;
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps
[INT_Int_distrib, Int_absorb])));
by (Force_tac 1);
qed "JN_Join_distrib";
Goal
"(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
by (asm_simp_tac (simpset()
addsimps [JN_Join_distrib, JN_constant]) 1);
qed "JN_Join_miniscope";
(*Used to prove guarantees_JN_I*)
Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)";
by (rtac program_equalityI 1);
by Auto_tac;
qed "JN_Join_diff";
(*** Safety: co, stable, FP ***)
(*Fails if I=0 because it collapses to SKIP : A co B, i.e. to A<=B. So an
alternative precondition is A<=B, but most proofs using this rule require
I to be nonempty for other reasons anyway.*)
Goalw [constrains_def, JOIN_def]
"i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)";
by Auto_tac;
by (blast_tac (claset() addDs [ActsD]) 1);
qed "JN_constrains";
Goal "(F Join G : A co B) <-> \
\ (programify(F):A co B & programify(G):A co B)";
by (auto_tac
(claset(), simpset() addsimps [constrains_def]));
qed "Join_constrains";
Goal "(F Join G : A unless B) <-> \
\ (programify(F) : A unless B & programify(G):A unless B)";
by (asm_simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
qed "Join_unless";
Addsimps [Join_constrains, Join_unless];
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
reachable (F Join G) could be much bigger than reachable F, reachable G
*)
Goal "[| F : A co A'; G:B co B' |] \
\ ==> F Join G : (A Int B) co (A' Un B')";
by (subgoal_tac "A:condition&A':condition & B: condition& \
\ B': condition & F:program & G:program" 1);
by (blast_tac (claset() addDs [constrainsD2]) 2);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "Join_constrains_weaken";
(*If I=0, it degenerates to SKIP : UNIV co 0, which is false.*)
Goal "[| ALL i:I. F(i) : A(i) co A'(i); i: I |] \
\ ==> (JN i:I. F(i)) : (INT i:I. A(i)) co (UN i:I. A'(i))";
by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
by (Clarify_tac 1);
by (subgoal_tac "(ALL i:I. F(i):program & A(i):condition)&\
\ (Union(RepFun(I, A')):condition)&\
\ (Inter(RepFun(I, A)):condition)" 1);
by (blast_tac (claset() addDs [constrainsD2]) 2);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "JN_constrains_weaken";
Goal "A:condition ==> (JN i:I. F(i)) : stable(A) <-> \
\ (ALL i:I. programify(F(i)):stable(A))";
by (asm_simp_tac
(simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
by Auto_tac;
by (blast_tac (claset() addDs [ActsD]) 1);
qed "JN_stable";
Goal "[| ALL i:I. F(i) : invariant(A); i : I |] \
\ ==> (JN i:I. F(i)) : invariant(A)";
by (subgoal_tac "A:condition" 1);
by (blast_tac (claset() addDs [invariantD2]) 2);
by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1);
by (Blast_tac 1);
bind_thm ("invariant_JN_I", ballI RS result());
Goal " (F Join G : stable(A)) <-> \
\ (programify(F) : stable(A) & programify(G): stable(A))";
by (asm_simp_tac (simpset() addsimps [stable_def]) 1);
qed "Join_stable";
(* TO BE DONE: stable_increasing *)
Addsimps [Join_stable];
Goal "[| F : invariant(A); G : invariant(A) |] \
\ ==> F Join G : invariant(A)";
by (subgoal_tac "F:program&G:program" 1);
by (blast_tac (claset() addDs [invariantD2]) 2);
by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
by (auto_tac (claset() addIs [Join_in_program], simpset()));
qed "invariant_JoinI";
(* Fails if I=0 because INT i:0. A(i) = 0 *)
Goal "i:I ==> FP(JN i:I. F(i)) = (INT i:I. FP (programify(F(i))))";
by (asm_simp_tac (simpset() addsimps [FP_def, Inter_def]) 1);
by (rtac equalityI 1);
by Safe_tac;
by (ALLGOALS(subgoal_tac "{x}:condition"));
by (rotate_tac ~1 3);
by (rotate_tac ~1 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable])));
by (rewrite_goals_tac [condition_def]);
by (REPEAT(Blast_tac 1));
qed "FP_JN";
(*** Progress: transient, ensures ***)
Goal "i:I==>(JN i:I. F(i)) : transient(A) <-> \
\ (EX i:I. programify(F(i)) : transient(A))";
by (auto_tac (claset(),
simpset() addsimps [transient_def, JOIN_def]));
by (auto_tac (claset(), simpset() addsimps
[condition_def,UN_Int_distrib, INT_Int_distrib]));
qed "JN_transient";
Goal "F Join G : transient(A) <-> \
\ (programify(F) : transient(A) | programify(G):transient(A))";
by (auto_tac (claset(),
simpset() addsimps [transient_def,
Join_def, Int_Un_distrib]));
qed "Join_transient";
Addsimps [Join_transient];
Goal "F : transient(A) ==> F Join G : transient(A)";
by (asm_full_simp_tac (simpset()
addsimps [Join_transient, transientD]) 1);
qed "Join_transient_I1";
Goal "G : transient(A) ==> F Join G : transient(A)";
by (asm_full_simp_tac (simpset()
addsimps [Join_transient, transientD]) 1);
qed "Join_transient_I2";
(*If I=0 it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
Goal "i : I ==> \
\ (JN i:I. F(i)) : A ensures B <-> \
\ ((ALL i:I. programify(F(i)) : (A-B) co (A Un B)) & \
\ (EX i:I. programify(F(i)) : A ensures B))";
by (auto_tac (claset(),
simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
qed "JN_ensures";
Goalw [ensures_def]
"F Join G : A ensures B <-> \
\ (programify(F) : (A-B) co (A Un B) & programify(G) : (A-B) co (A Un B) & \
\ (programify(F): transient (A-B) | programify(G) : transient (A-B)))";
by (auto_tac (claset(), simpset() addsimps [Join_transient]));
qed "Join_ensures";
Goalw [stable_def, constrains_def, Join_def]
"[| F : stable(A); G : A co A' |] \
\ ==> F Join G : A co A'";
by Auto_tac;
by (rewrite_goals_tac [condition_def]);
by Auto_tac;
by (blast_tac (claset() addDs [ActsD]) 3);
by (dres_inst_tac [("x", "Id")] bspec 1);
by (dres_inst_tac [("x", "Id")] bspec 2);
by (dres_inst_tac [("x", "x")] bspec 4);
by (dres_inst_tac [("x", "Id")] bspec 5);
by Auto_tac;
qed "stable_Join_constrains";
(*Premise for G cannot use Always because F: Stable A is
weaker than G : stable A *)
Goal "[| F : stable(A); G : invariant(A) |] ==> F Join G : Always(A)";
by (subgoal_tac "A:condition & F:program" 1);
by (blast_tac (claset() addDs [stableD2]) 2);
by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def,
Stable_eq_stable]) 1);
by (force_tac(claset() addIs [stable_Int], simpset()) 1);
qed "stable_Join_Always1";
(*As above, but exchanging the roles of F and G*)
Goal "[| F : invariant(A); G : stable(A) |] ==> F Join G : Always(A)";
by (stac Join_commute 1);
by (blast_tac (claset() addIs [stable_Join_Always1]) 1);
qed "stable_Join_Always2";
Goal "[| F : stable(A); G : A ensures B |] ==> F Join G : A ensures B";
by (subgoal_tac "F:program&G:program&A:condition&B:condition" 1);
by (blast_tac (claset() addDs [stableD2, ensuresD2]) 2);
by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
by (etac constrains_weaken 1);
by Auto_tac;
qed "stable_Join_ensures1";
(*As above, but exchanging the roles of F and G*)
Goal "[| F : A ensures B; G : stable(A) |] ==> F Join G : A ensures B";
by (stac Join_commute 1);
by (blast_tac (claset() addIs [stable_Join_ensures1]) 1);
qed "stable_Join_ensures2";
(*** the ok and OK relations ***)
Goal "SKIP ok F";
by (auto_tac (claset() addDs [ActsD],
simpset() addsimps [ok_def]));
qed "ok_SKIP1";
Goal "F ok SKIP";
by (auto_tac (claset() addDs [ActsD],
simpset() addsimps [ok_def]));
qed "ok_SKIP2";
AddIffs [ok_SKIP1, ok_SKIP2];
Goal "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_Join_commute";
Goal "(F ok G) <->(G ok F)";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_commute";
bind_thm ("ok_sym", ok_commute RS iffD1);
Goal "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)";
by (asm_full_simp_tac
(simpset() addsimps [ok_def, Join_def, OK_def,
Int_assoc, cons_absorb, Int_Un_distrib, Ball_def]) 1);
by (rtac iffI 1);
by Safe_tac;
by (REPEAT(Force_tac 1));
qed "ok_iff_OK";
Goal "F ok (G Join H) <-> (F ok G & F ok H)";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_Join_iff1";
Goal "(G Join H) ok F <-> (G ok F & H ok F)";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_Join_iff2";
AddIffs [ok_Join_iff1, ok_Join_iff2];
(*useful? Not with the previous two around*)
Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_Join_commute_I";
Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
by (blast_tac (claset() addDs [ActsD]) 1);
by (REPEAT(Force_tac 1));
qed "ok_JN_iff1";
Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)";
by (auto_tac (claset(), simpset() addsimps [ok_def]));
by (blast_tac (claset() addDs [ActsD]) 1);
qed "ok_JN_iff2";
AddIffs [ok_JN_iff1, ok_JN_iff2];
Goal "OK(I,F) <-> (ALL i: I. ALL j: I-{i}. F(i) ok (F(j)))";
by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));
qed "OK_iff_ok";
Goal "[| OK(I,F); i: I; j: I; i~=j|] ==> F(i) ok F(j)";
by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));
qed "OK_imp_ok";
(*** Allowed ***)
Goal "Allowed(SKIP) = program";
by (auto_tac (claset() addDs [ActsD],
simpset() addsimps [Allowed_def]));
qed "Allowed_SKIP";
Goal "Allowed(F Join G) = \
\ Allowed(programify(F)) Int Allowed(programify(G))";
by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
qed "Allowed_Join";
Goal "i:I ==> \
\ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))";
by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
br equalityI 1;
by Auto_tac;
qed "Allowed_JN";
Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
Goal
"F ok G <-> (programify(F):Allowed(programify(G)) & \
\ programify(G):Allowed(programify(F)))";
by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
qed "ok_iff_Allowed";
Goal "OK(I,F) <-> \
\ (ALL i: I. ALL j: I-{i}. programify(F(i)) : Allowed(programify(F(j))))";
by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));
qed "OK_iff_Allowed";
(*** safety_prop, for reasoning about given instances of "ok" ***)
Goal "safety_prop(X) ==> (Acts(G) <= cons(Id, (UN F:X. Acts(F)))) <-> (programify(G):X)";
by (full_simp_tac( simpset() addsimps [safety_prop_def]) 1);
by (Clarify_tac 1);
by (case_tac "G:program" 1);
by (ALLGOALS(Asm_full_simp_tac));
by (Blast_tac 1);
by Safe_tac;
by (Force_tac 2);
by (force_tac (claset(), simpset()
addsimps [programify_def]) 1);
qed "safety_prop_Acts_iff";
Goal "X:property ==> \
\ (safety_prop(X) --> \
\ ((UN G:X. Acts(G)) <= AllowedActs(F)) <-> (X <= Allowed(programify(F))))";
by (auto_tac (claset(),
simpset() addsimps [Allowed_def,
safety_prop_Acts_iff RS iff_sym, property_def]));
qed "safety_prop_AllowedActs_iff_Allowed";
Goal "X:property ==> \
\ safety_prop(X) --> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X";
by (asm_full_simp_tac (simpset() addsimps [Allowed_def,
UN_Int_distrib,safety_prop_Acts_iff, property_def]) 1);
by Auto_tac;
qed "Allowed_eq";
Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); X:property; safety_prop(X) |] \
\ ==> Allowed(F) = X";
by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1);
qed "def_prg_Allowed";
(*For safety_prop to hold, the property must be satisfiable!*)
Goal "B:condition ==> safety_prop(A co B) <-> (A <= B)";
by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
by Auto_tac;
by (Blast_tac 2);
by (force_tac (claset(), simpset() addsimps [condition_def]) 1);
qed "safety_prop_constrains";
Addsimps [safety_prop_constrains];
Goal "A:condition ==>safety_prop(stable(A))";
by (asm_simp_tac (simpset() addsimps [stable_def]) 1);
qed "safety_prop_stable";
Addsimps [safety_prop_stable];
Goal "[| X:property; Y:property |] ==> \
\ safety_prop(X) --> safety_prop(Y) --> safety_prop(X Int Y)";
by (asm_full_simp_tac (simpset()
addsimps [safety_prop_def, property_def]) 1);
by Safe_tac;
by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
("C", "Union(RepFun(Y, Acts))")] subset_trans 2);
by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"),
("C", "Union(RepFun(X, Acts))")] subset_trans 1);
by (REPEAT(Blast_tac 1));
qed "safety_prop_Int";
Addsimps [safety_prop_Int];
(* If I=0 the conclusion becomes safety_prop(0) which is false *)
Goal "[| ALL i:I. X(i):property; i:I |] ==> \
\ (ALL i:I. safety_prop(X(i))) --> safety_prop(INT i:I. X(i))";
by (asm_full_simp_tac (simpset() addsimps [safety_prop_def, property_def]) 1);
by Safe_tac;
by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"),
("C", "Union(RepFun(X(xb), Acts))")] subset_trans 3);
by (REPEAT(Blast_tac 1));
bind_thm ("safety_prop_Inter", ballI RS result());
Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X); X:property |] \
\ ==> F ok G <-> (programify(G):X & acts Int action <= AllowedActs(G))";
by (auto_tac (claset(),
simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib, property_def]));
qed "def_UNION_ok_iff";