Theory Union

(*  Title:      ZF/UNITY/Union.thy
    Author:     Sidi O Ehmety, Computer Laboratory
    Copyright   2001  University of Cambridge

Unions of programs

Partly from Misra's Chapter 5 ∈ Asynchronous Compositions of Programs

Theory ported form HOL..

*)

theory Union imports SubstAx FP
begin

definition
  (*FIXME: conjoin Init(F) ∩ Init(G) ≠ 0 *)
  ok :: "[i, i] ⇒ o"     (infixl ‹ok› 65)  where
    "F ok G ≡ Acts(F) ⊆ AllowedActs(G) ∧
               Acts(G) ⊆ AllowedActs(F)"

definition
  (*FIXME: conjoin (⋂i ∈ I. Init(F(i))) ≠ 0 *)
  OK  :: "[i, i⇒i] ⇒ o"  where
    "OK(I,F) ≡ (∀i ∈ I. ∀j ∈ I-{i}. Acts(F(i)) ⊆ AllowedActs(F(j)))"

definition
  JOIN  :: "[i, i⇒i] ⇒ i"  where
  "JOIN(I,F) ≡ if I = 0 then SKIP else
                 mk_program(⋂i ∈ I. Init(F(i)), ⋃i ∈ I. Acts(F(i)),
                 ⋂i ∈ I. AllowedActs(F(i)))"

definition
  Join :: "[i, i] ⇒ i"  (infixl ‹⊔› 65)  where
  "F ⊔ G ≡ mk_program (Init(F) ∩ Init(G), Acts(F) ∪ Acts(G),
                                AllowedActs(F) ∩ AllowedActs(G))"
definition
  (*Characterizes safety properties.  Used with specifying AllowedActs*)
  safety_prop :: "i ⇒ o"  where
  "safety_prop(X) ≡ X⊆program ∧
      SKIP ∈ X ∧ (∀G ∈ program. Acts(G) ⊆ (⋃F ∈ X. Acts(F)) ⟶ G ∈ X)"

syntax
  "_JOIN1"  :: "[pttrns, i] ⇒ i"     (‹(‹indent=3 notation=‹binder ⨆››⨆_./ _)› 10)
  "_JOIN"   :: "[pttrn, i, i] ⇒ i"   (‹(‹indent=3 notation=‹binder ⨆∈››⨆_ ∈ _./ _)› 10)
syntax_consts
  "_JOIN1" "_JOIN" == JOIN
translations
  "⨆x ∈ A. B" == "CONST JOIN(A, (λx. B))"
  "⨆x y. B"   == "⨆x. ⨆y. B"
  "⨆x. B"     == "CONST JOIN(CONST state, (λx. B))"


subsection‹SKIP›

lemma reachable_SKIP [simp]: "reachable(SKIP) = state"
by (force elim: reachable.induct intro: reachable.intros)

text‹Elimination programify from ok and ⊔›

lemma ok_programify_left [iff]: "programify(F) ok G ⟷ F ok G"
by (simp add: ok_def)

lemma ok_programify_right [iff]: "F ok programify(G) ⟷ F ok G"
by (simp add: ok_def)

lemma Join_programify_left [simp]: "programify(F) ⊔ G = F ⊔ G"
by (simp add: Join_def)

lemma Join_programify_right [simp]: "F ⊔ programify(G) = F ⊔ G"
by (simp add: Join_def)

subsection‹SKIP and safety properties›

lemma SKIP_in_constrains_iff [iff]: "(SKIP ∈ A co B) ⟷ (A⊆B ∧ st_set(A))"
by (unfold constrains_def st_set_def, auto)

lemma SKIP_in_Constrains_iff [iff]: "(SKIP ∈ A Co B)⟷ (state ∩ A⊆B)"
by (unfold Constrains_def, auto)

lemma SKIP_in_stable [iff]: "SKIP ∈ stable(A) ⟷ st_set(A)"
by (auto simp add: stable_def)

lemma SKIP_in_Stable [iff]: "SKIP ∈ Stable(A)"
by (unfold Stable_def, auto)

subsection‹Join and JOIN types›

lemma Join_in_program [iff,TC]: "F ⊔ G ∈ program"
by (unfold Join_def, auto)

lemma JOIN_in_program [iff,TC]: "JOIN(I,F) ∈ program"
by (unfold JOIN_def, auto)

subsection‹Init, Acts, and AllowedActs of Join and JOIN›
lemma Init_Join [simp]: "Init(F ⊔ G) = Init(F) ∩ Init(G)"
by (simp add: Int_assoc Join_def)

lemma Acts_Join [simp]: "Acts(F ⊔ G) = Acts(F) ∪ Acts(G)"
by (simp add: Int_Un_distrib2 cons_absorb Join_def)

lemma AllowedActs_Join [simp]: "AllowedActs(F ⊔ G) =
  AllowedActs(F) ∩ AllowedActs(G)"
apply (simp add: Int_assoc cons_absorb Join_def)
done

subsection‹Join's algebraic laws›

lemma Join_commute: "F ⊔ G = G ⊔ F"
by (simp add: Join_def Un_commute Int_commute)

lemma Join_left_commute: "A ⊔ (B ⊔ C) = B ⊔ (A ⊔ C)"
apply (simp add: Join_def Int_Un_distrib2 cons_absorb)
apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb)
done

lemma Join_assoc: "(F ⊔ G) ⊔ H = F ⊔ (G ⊔ H)"
by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2)

subsection‹Needed below›
lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)"
by auto

lemma Join_SKIP_left [simp]: "SKIP ⊔ F = programify(F)"
  unfolding Join_def SKIP_def
apply (auto simp add: Int_absorb cons_eq)
done

lemma Join_SKIP_right [simp]: "F ⊔ SKIP =  programify(F)"
apply (subst Join_commute)
apply (simp add: Join_SKIP_left)
done

lemma Join_absorb [simp]: "F ⊔ F = programify(F)"
by (rule program_equalityI, auto)

lemma Join_left_absorb: "F ⊔ (F ⊔ G) = F ⊔ G"
by (simp add: Join_assoc [symmetric])

subsection‹Join is an AC-operator›
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute

subsection‹Eliminating programify form JOIN and OK expressions›

lemma OK_programify [iff]: "OK(I, λx. programify(F(x))) ⟷ OK(I, F)"
by (simp add: OK_def)

lemma JOIN_programify [iff]: "JOIN(I, λx. programify(F(x))) = JOIN(I, F)"
by (simp add: JOIN_def)


subsection‹JOIN›

lemma JOIN_empty [simp]: "JOIN(0, F) = SKIP"
by (unfold JOIN_def, auto)

lemma Init_JOIN [simp]:
     "Init(⨆i ∈ I. F(i)) = (if I=0 then state else (⋂i ∈ I. Init(F(i))))"
by (simp add: JOIN_def INT_extend_simps del: INT_simps)

lemma Acts_JOIN [simp]:
     "Acts(JOIN(I,F)) = cons(id(state), ⋃i ∈ I.  Acts(F(i)))"
  unfolding JOIN_def
apply (auto simp del: INT_simps UN_simps)
apply (rule equalityI)
apply (auto dest: Acts_type [THEN subsetD])
done

lemma AllowedActs_JOIN [simp]:
     "AllowedActs(⨆i ∈ I. F(i)) =
      (if I=0 then Pow(state*state) else (⋂i ∈ I. AllowedActs(F(i))))"
apply (unfold JOIN_def, auto)
apply (rule equalityI)
apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD])
done

lemma JOIN_cons [simp]: "(⨆i ∈ cons(a,I). F(i)) = F(a) ⊔ (⨆i ∈ I. F(i))"
by (rule program_equalityI, auto)

lemma JOIN_cong [cong]:
    "⟦I=J;  ⋀i. i ∈ J ⟹ F(i) = G(i)⟧ ⟹
     (⨆i ∈ I. F(i)) = (⨆i ∈ J. G(i))"
by (simp add: JOIN_def)



subsection‹JOIN laws›
lemma JOIN_absorb: "k ∈ I ⟹F(k) ⊔ (⨆i ∈ I. F(i)) = (⨆i ∈ I. F(i))"
apply (subst JOIN_cons [symmetric])
apply (auto simp add: cons_absorb)
done

lemma JOIN_Un: "(⨆i ∈ I ∪ J. F(i)) = ((⨆i ∈ I. F(i)) ⊔ (⨆i ∈ J. F(i)))"
apply (rule program_equalityI)
apply (simp_all add: UN_Un INT_Un)
apply (simp_all del: INT_simps add: INT_extend_simps, blast)
done

lemma JOIN_constant: "(⨆i ∈ I. c) = (if I=0 then SKIP else programify(c))"
by (rule program_equalityI, auto)

lemma JOIN_Join_distrib:
     "(⨆i ∈ I. F(i) ⊔ G(i)) = (⨆i ∈ I. F(i))  ⊔  (⨆i ∈ I. G(i))"
apply (rule program_equalityI)
apply (simp_all add: INT_Int_distrib, blast)
done

lemma JOIN_Join_miniscope: "(⨆i ∈ I. F(i) ⊔ G) = ((⨆i ∈ I. F(i) ⊔ G))"
by (simp add: JOIN_Join_distrib JOIN_constant)

text‹Used to prove guarantees_JOIN_I›
lemma JOIN_Join_diff: "i ∈ I⟹F(i) ⊔ JOIN(I - {i}, F) = JOIN(I, F)"
apply (rule program_equalityI)
apply (auto elim!: not_emptyE)
done

subsection‹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.*)

lemma JOIN_constrains:
 "i ∈ I⟹(⨆i ∈ I. F(i)) ∈ A co B ⟷ (∀i ∈ I. programify(F(i)) ∈ A co B)"

apply (unfold constrains_def JOIN_def st_set_def, auto)
prefer 2 apply blast
apply (rename_tac j act y z)
apply (cut_tac F = "F (j) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done

lemma Join_constrains [iff]:
     "(F ⊔ G ∈ A co B) ⟷ (programify(F) ∈ A co B ∧ programify(G) ∈ A co B)"
by (auto simp add: constrains_def)

lemma Join_unless [iff]:
     "(F ⊔ G ∈ A unless B) ⟷
    (programify(F) ∈ A unless B ∧ programify(G) ∈ A unless B)"
by (simp add: Join_constrains unless_def)


(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
  reachable (F ⊔ G) could be much bigger than reachable F, reachable G
*)

lemma Join_constrains_weaken:
     "⟦F ∈ A co A';  G ∈ B co B'⟧
      ⟹ F ⊔ G ∈ (A ∩ B) co (A' ∪ B')"
apply (subgoal_tac "st_set (A) ∧ st_set (B) ∧ F ∈ program ∧ G ∈ program")
prefer 2 apply (blast dest: constrainsD2, simp)
apply (blast intro: constrains_weaken)
done

(*If I=0, it degenerates to SKIP ∈ state co 0, which is false.*)
lemma JOIN_constrains_weaken:
  assumes major: "(⋀i. i ∈ I ⟹ F(i) ∈ A(i) co A'(i))"
      and minor: "i ∈ I"
  shows "(⨆i ∈ I. F(i)) ∈ (⋂i ∈ I. A(i)) co (⋃i ∈ I. A'(i))"
apply (cut_tac minor)
apply (simp (no_asm_simp) add: JOIN_constrains)
apply clarify
apply (rename_tac "j")
apply (frule_tac i = j in major)
apply (frule constrainsD2, simp)
apply (blast intro: constrains_weaken)
done

lemma JOIN_stable:
     "(⨆i ∈ I. F(i)) ∈  stable(A) ⟷ ((∀i ∈ I. programify(F(i)) ∈ stable(A)) ∧ st_set(A))"
apply (auto simp add: stable_def constrains_def JOIN_def)
apply (cut_tac F = "F (i) " in Acts_type)
apply (drule_tac x = act in bspec, auto)
done

lemma initially_JOIN_I:
  assumes major: "(⋀i. i ∈ I ⟹F(i) ∈ initially(A))"
      and minor: "i ∈ I"
  shows  "(⨆i ∈ I. F(i)) ∈ initially(A)"
apply (cut_tac minor)
apply (auto elim!: not_emptyE simp add: Inter_iff initially_def)
apply (frule_tac i = x in major)
apply (auto simp add: initially_def)
done

lemma invariant_JOIN_I:
  assumes major: "(⋀i. i ∈ I ⟹ F(i) ∈ invariant(A))"
      and minor: "i ∈ I"
  shows "(⨆i ∈ I. F(i)) ∈ invariant(A)"
apply (cut_tac minor)
apply (auto intro!: initially_JOIN_I dest: major simp add: invariant_def JOIN_stable)
apply (erule_tac V = "i ∈ I" in thin_rl)
apply (frule major)
apply (drule_tac [2] major)
apply (auto simp add: invariant_def)
apply (frule stableD2, force)+
done

lemma Join_stable [iff]:
     " (F ⊔ G ∈ stable(A)) ⟷
      (programify(F) ∈ stable(A) ∧ programify(G) ∈  stable(A))"
by (simp add: stable_def)

lemma initially_JoinI [intro!]:
     "⟦F ∈ initially(A); G ∈ initially(A)⟧ ⟹ F ⊔ G ∈ initially(A)"
by (unfold initially_def, auto)

lemma invariant_JoinI:
     "⟦F ∈ invariant(A); G ∈ invariant(A)⟧
      ⟹ F ⊔ G ∈ invariant(A)"
apply (subgoal_tac "F ∈ program∧G ∈ program")
prefer 2 apply (blast dest: invariantD2)
apply (simp add: invariant_def)
apply (auto intro: Join_in_program)
done


(* Fails if I=0 because ⋂i ∈ 0. A(i) = 0 *)
lemma FP_JOIN: "i ∈ I ⟹ FP(⨆i ∈ I. F(i)) = (⋂i ∈ I. FP (programify(F(i))))"
by (auto simp add: FP_def Inter_def st_set_def JOIN_stable)

subsection‹Progress: transient, ensures›

lemma JOIN_transient:
     "i ∈ I ⟹
      (⨆i ∈ I. F(i)) ∈ transient(A) ⟷ (∃i ∈ I. programify(F(i)) ∈ transient(A))"
apply (auto simp add: transient_def JOIN_def)
  unfolding st_set_def
apply (drule_tac [2] x = act in bspec)
apply (auto dest: Acts_type [THEN subsetD])
done

lemma Join_transient [iff]:
     "F ⊔ G ∈ transient(A) ⟷
      (programify(F) ∈ transient(A) | programify(G) ∈ transient(A))"
apply (auto simp add: transient_def Join_def Int_Un_distrib2)
done

lemma Join_transient_I1: "F ∈ transient(A) ⟹ F ⊔ G ∈ transient(A)"
by (simp add: Join_transient transientD2)


lemma Join_transient_I2: "G ∈ transient(A) ⟹ F ⊔ G ∈ transient(A)"
by (simp add: Join_transient transientD2)

(*If I=0 it degenerates to (SKIP ∈ A ensures B) = False, i.e. to ¬(A⊆B) *)
lemma JOIN_ensures:
     "i ∈ I ⟹
      (⨆i ∈ I. F(i)) ∈ A ensures B ⟷
      ((∀i ∈ I. programify(F(i)) ∈ (A-B) co (A ∪ B)) ∧
      (∃i ∈ I. programify(F(i)) ∈ A ensures B))"
by (auto simp add: ensures_def JOIN_constrains JOIN_transient)


lemma Join_ensures:
     "F ⊔ G ∈ A ensures B  ⟷
      (programify(F) ∈ (A-B) co (A ∪ B) ∧ programify(G) ∈ (A-B) co (A ∪ B) ∧
       (programify(F) ∈  transient (A-B) | programify(G) ∈ transient (A-B)))"

  unfolding ensures_def
apply (auto simp add: Join_transient)
done

lemma stable_Join_constrains:
    "⟦F ∈ stable(A);  G ∈ A co A'⟧
     ⟹ F ⊔ G ∈ A co A'"
  unfolding stable_def constrains_def Join_def st_set_def
apply (cut_tac F = F in Acts_type)
apply (cut_tac F = G in Acts_type, force)
done

(*Premise for G cannot use Always because  F ∈ Stable A  is
   weaker than G ∈ stable A *)
lemma stable_Join_Always1:
     "⟦F ∈ stable(A);  G ∈ invariant(A)⟧ ⟹ F ⊔ G ∈ Always(A)"
apply (subgoal_tac "F ∈ program ∧ G ∈ program ∧ st_set (A) ")
prefer 2 apply (blast dest: invariantD2 stableD2)
apply (simp add: Always_def invariant_def initially_def Stable_eq_stable)
apply (force intro: stable_Int)
done

(*As above, but exchanging the roles of F and G*)
lemma stable_Join_Always2:
     "⟦F ∈ invariant(A);  G ∈ stable(A)⟧ ⟹ F ⊔ G ∈ Always(A)"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done



lemma stable_Join_ensures1:
     "⟦F ∈ stable(A);  G ∈ A ensures B⟧ ⟹ F ⊔ G ∈ A ensures B"
apply (subgoal_tac "F ∈ program ∧ G ∈ program ∧ st_set (A) ")
prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD])
apply (simp (no_asm_simp) add: Join_ensures)
apply (simp add: stable_def ensures_def)
apply (erule constrains_weaken, auto)
done


(*As above, but exchanging the roles of F and G*)
lemma stable_Join_ensures2:
     "⟦F ∈ A ensures B;  G ∈ stable(A)⟧ ⟹ F ⊔ G ∈ A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done

subsection‹The ok and OK relations›

lemma ok_SKIP1 [iff]: "SKIP ok F"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)

lemma ok_SKIP2 [iff]: "F ok SKIP"
by (auto dest: Acts_type [THEN subsetD] simp add: ok_def)

lemma ok_Join_commute:
     "(F ok G ∧ (F ⊔ G) ok H) ⟷ (G ok H ∧ F ok (G ⊔ H))"
by (auto simp add: ok_def)

lemma ok_commute: "(F ok G) ⟷(G ok F)"
by (auto simp add: ok_def)

lemmas ok_sym = ok_commute [THEN iffD1]

lemma ok_iff_OK: "OK({⟨0,F⟩,⟨1,G⟩,⟨2,H⟩}, snd) ⟷ (F ok G ∧ (F ⊔ G) ok H)"
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
                 Int_Un_distrib2 Ball_def,  safe, force+)

lemma ok_Join_iff1 [iff]: "F ok (G ⊔ H) ⟷ (F ok G ∧ F ok H)"
by (auto simp add: ok_def)

lemma ok_Join_iff2 [iff]: "(G ⊔ H) ok F ⟷ (G ok F ∧ H ok F)"
by (auto simp add: ok_def)

(*useful?  Not with the previous two around*)
lemma ok_Join_commute_I: "⟦F ok G; (F ⊔ G) ok H⟧ ⟹ F ok (G ⊔ H)"
by (auto simp add: ok_def)

lemma ok_JOIN_iff1 [iff]: "F ok JOIN(I,G) ⟷ (∀i ∈ I. F ok G(i))"
by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def)

lemma ok_JOIN_iff2 [iff]: "JOIN(I,G) ok F   ⟷  (∀i ∈ I. G(i) ok F)"
apply (auto elim!: not_emptyE simp add: ok_def)
apply (blast dest: Acts_type [THEN subsetD])
done

lemma OK_iff_ok: "OK(I,F) ⟷ (∀i ∈ I. ∀j ∈ I-{i}. F(i) ok (F(j)))"
by (auto simp add: ok_def OK_def)

lemma OK_imp_ok: "⟦OK(I,F); i ∈ I; j ∈ I; i≠j⟧ ⟹ F(i) ok F(j)"
by (auto simp add: OK_iff_ok)


lemma OK_0 [iff]: "OK(0,F)"
by (simp add: OK_def)

lemma OK_cons_iff:
     "OK(cons(i, I), F) ⟷
      (i ∈ I ∧ OK(I, F)) | (i∉I ∧ OK(I, F) ∧ F(i) ok JOIN(I,F))"
apply (simp add: OK_iff_ok)
apply (blast intro: ok_sym)
done


subsection‹Allowed›

lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"
by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def)

lemma Allowed_Join [simp]:
     "Allowed(F ⊔ G) =
   Allowed(programify(F)) ∩ Allowed(programify(G))"
apply (auto simp add: Allowed_def)
done

lemma Allowed_JOIN [simp]:
     "i ∈ I ⟹
   Allowed(JOIN(I,F)) = (⋂i ∈ I. Allowed(programify(F(i))))"
apply (auto simp add: Allowed_def, blast)
done

lemma ok_iff_Allowed:
     "F ok G ⟷ (programify(F) ∈ Allowed(programify(G)) ∧
   programify(G) ∈ Allowed(programify(F)))"
by (simp add: ok_def Allowed_def)


lemma OK_iff_Allowed:
     "OK(I,F) ⟷
  (∀i ∈ I. ∀j ∈ I-{i}. programify(F(i)) ∈ Allowed(programify(F(j))))"
apply (auto simp add: OK_iff_ok ok_iff_Allowed)
done

subsection‹safety_prop, for reasoning about given instances of "ok"›

lemma safety_prop_Acts_iff:
     "safety_prop(X) ⟹ (Acts(G) ⊆ cons(id(state), (⋃F ∈ X. Acts(F)))) ⟷ (programify(G) ∈ X)"
apply (simp (no_asm_use) add: safety_prop_def)
apply clarify
apply (case_tac "G ∈ program", simp_all, blast, safe)
prefer 2 apply force
apply (force simp add: programify_def)
done

lemma safety_prop_AllowedActs_iff_Allowed:
     "safety_prop(X) ⟹
  (⋃G ∈ X. Acts(G)) ⊆ AllowedActs(F) ⟷ (X ⊆ Allowed(programify(F)))"
apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym]
                 safety_prop_def, blast)
done


lemma Allowed_eq:
     "safety_prop(X) ⟹ Allowed(mk_program(init, acts, ⋃F ∈ X. Acts(F))) = X"
apply (subgoal_tac "cons (id (state), ⋃(RepFun (X, Acts)) ∩ Pow (state * state)) = ⋃(RepFun (X, Acts))")
apply (rule_tac [2] equalityI)
  apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto)
apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+
done

lemma def_prg_Allowed:
     "⟦F ≡ mk_program (init, acts, ⋃F ∈ X. Acts(F)); safety_prop(X)⟧
      ⟹ Allowed(F) = X"
by (simp add: Allowed_eq)

(*For safety_prop to hold, the property must be satisfiable!*)
lemma safety_prop_constrains [iff]:
     "safety_prop(A co B) ⟷ (A ⊆ B ∧ st_set(A))"
by (simp add: safety_prop_def constrains_def st_set_def, blast)

(* To be used with resolution *)
lemma safety_prop_constrainsI [iff]:
     "⟦A⊆B; st_set(A)⟧ ⟹safety_prop(A co B)"
by auto

lemma safety_prop_stable [iff]: "safety_prop(stable(A)) ⟷ st_set(A)"
by (simp add: stable_def)

lemma safety_prop_stableI: "st_set(A) ⟹ safety_prop(stable(A))"
by auto

lemma safety_prop_Int [simp]:
     "⟦safety_prop(X) ; safety_prop(Y)⟧ ⟹ safety_prop(X ∩ Y)"
apply (simp add: safety_prop_def, safe, blast)
apply (drule_tac [2] B = "⋃(RepFun (X ∩ Y, Acts))" and C = "⋃(RepFun (Y, Acts))" in subset_trans)
apply (drule_tac B = "⋃(RepFun (X ∩ Y, Acts))" and C = "⋃(RepFun (X, Acts))" in subset_trans)
apply blast+
done

(* If I=0 the conclusion becomes safety_prop(0) which is false *)
lemma safety_prop_Inter:
  assumes major: "(⋀i. i ∈ I ⟹safety_prop(X(i)))"
      and minor: "i ∈ I"
  shows "safety_prop(⋂i ∈ I. X(i))"
apply (simp add: safety_prop_def)
apply (cut_tac minor, safe)
apply (simp (no_asm_use) add: Inter_iff)
apply clarify
apply (frule major)
apply (drule_tac [2] i = xa in major)
apply (frule_tac [4] i = xa in major)
apply (auto simp add: safety_prop_def)
apply (drule_tac B = "⋃(RepFun (⋂(RepFun (I, X)), Acts))" and C = "⋃(RepFun (X (xa), Acts))" in subset_trans)
apply blast+
done

lemma def_UNION_ok_iff:
"⟦F ≡ mk_program(init,acts, ⋃G ∈ X. Acts(G)); safety_prop(X)⟧
      ⟹ F ok G ⟷ (programify(G) ∈ X ∧ acts ∩ Pow(state*state) ⊆ AllowedActs(G))"
  unfolding ok_def
apply (drule_tac G = G in safety_prop_Acts_iff)
apply (cut_tac F = G in AllowedActs_type)
apply (cut_tac F = G in Acts_type, auto)
done

end