src/ZF/UNITY/Union.ML

added HOL-Library;

(*  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";
AddIffs [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";

AddIffs [ok_programify_left, ok_programify_right, 
          Join_programify_left, Join_programify_right];

(** SKIP and safety properties **)

Goalw [constrains_def, st_set_def] 
"(SKIP: A co B) <-> (A<=B & st_set(A))";
by Auto_tac;
qed "SKIP_in_constrains_iff";
AddIffs [SKIP_in_constrains_iff];

Goalw [Constrains_def]"(SKIP : A Co B)<-> (state Int A<=B)";
by Auto_tac;
qed "SKIP_in_Constrains_iff";
AddIffs [SKIP_in_Constrains_iff];

Goal "SKIP:stable(A) <-> st_set(A)";
by (auto_tac (claset(), 
    simpset() addsimps [stable_def]));
qed "SKIP_in_stable";
AddIffs [SKIP_in_stable];

Goalw [Stable_def] "SKIP:Stable(A)";
by Auto_tac;
qed "SKIP_in_Stable";
AddIffs [SKIP_in_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_distrib2, 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_distrib2, 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_distrib2]) 1);
qed "Join_assoc";

(* Needed below *)
Goal "cons(id(state), Pow(state * state)) = Pow(state*state)";
by Auto_tac;
qed "cons_id";
AddIffs [cons_id];

Goalw [Join_def, SKIP_def] 
    "SKIP Join F = programify(F)";
by (auto_tac (claset(), simpset() addsimps [Int_absorb,cons_eq]));
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";

AddIffs [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 form 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";

AddIffs [OK_programify, JN_programify];

(* JN *)

Goalw [JOIN_def] "JOIN(0, F) = SKIP";
by Auto_tac;
qed "JN_empty";
AddIffs [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 (simp_tac (simpset() addsimps [JOIN_def]) 1);
by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib]));
qed "Init_JN";

Goalw [JOIN_def]
     "Acts(JOIN(I,F)) = cons(id(state), UN i:I.  Acts(F(i)))";
by (auto_tac (claset(), simpset() delsimps (INT_simps@UN_simps)));
by (rtac equalityI 1);
by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
qed "Acts_JN";

Goalw [JOIN_def]
"AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))";
by Auto_tac;
by (rtac equalityI 1);
by (auto_tac (claset() addDs [AllowedActs_type RS subsetD], simpset()));
qed "AllowedActs_JN";
AddIffs [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";
AddIffs[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";

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 (simpset() addsimps [UN_Un,INT_Un])));
by (ALLGOALS(asm_full_simp_tac (simpset() delsimps INT_simps
		                          addsimps INT_extend_simps)));
by (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,st_set_def]
 "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)";
by Auto_tac;
by (cut_inst_tac [("F","F(xa)")] Acts_type 1);
by (Blast_tac 2);
by (dres_inst_tac [("x", "xb")] bspec 1);
by Auto_tac;
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";

AddIffs [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 "st_set(A) & st_set(B) & 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 : state co 0, which is false.*)
val [major, minor] = Goal 
"[| (!!i. 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 (cut_facts_tac [minor] 1);
by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
by (Clarify_tac 1);
by (forw_inst_tac [("i", "x")] major 1);
by (forward_tac [constrainsD2] 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "JN_constrains_weaken";

Goal "(JN i:I. F(i)): stable(A) <-> ((ALL i:I. programify(F(i)):stable(A)) & st_set(A))";
by (asm_simp_tac 
    (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
by Auto_tac;
by (cut_inst_tac [("F", "F(xa)")] Acts_type 1);
by (dres_inst_tac [("x","xb")] bspec 1);
by Auto_tac;
qed "JN_stable";

val [major, minor] = Goalw [initially_def]
 "[| (!!i. i:I ==>F(i):initially(A)); i:I |] ==> (JN i:I. F(i)):initially(A)";
by (cut_facts_tac [minor] 1);
by (Asm_full_simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [Inter_iff]) 1);
by (forw_inst_tac [("i", "x")] major 1);
by Auto_tac;
qed "initially_JN_I";

val [major, minor] = Goal 
"[|(!!i. i:I ==> F(i) : invariant(A)); i:I|]==> (JN i:I. F(i)):invariant(A)";
by (cut_facts_tac [minor] 1);
by (auto_tac (claset() addSIs [initially_JN_I] addDs [major], 
              simpset() addsimps [invariant_def, JN_stable]));
by (thin_tac "i:I" 1);
by (forward_tac [major] 1);
by (dtac major 2);
by (auto_tac (claset(), simpset() addsimps [invariant_def]));
by (ALLGOALS(forward_tac [stableD2]));
by Auto_tac;
qed "invariant_JN_I";

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";
AddIffs [Join_stable];

Goalw [initially_def] "[| F:initially(A); G:initially(A) |] ==> F Join G: initially(A)";
by Auto_tac;
qed "initially_JoinI";
AddSIs [initially_JoinI];

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 "st_set({x})"));
by (rotate_tac ~1 3);
by (rotate_tac ~1 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable])));
by (rewrite_goals_tac [st_set_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 (rewrite_goals_tac [st_set_def]);
by (dres_inst_tac [("x", "xb")] bspec 2);
by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
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_distrib2]));
qed "Join_transient";

AddIffs [Join_transient];


Goal "F : transient(A) ==> F Join G : transient(A)";
by (asm_full_simp_tac (simpset() 
           addsimps [Join_transient, transientD2]) 1);
qed "Join_transient_I1";


Goal "G : transient(A) ==> F Join G : transient(A)";
by (asm_full_simp_tac (simpset() 
           addsimps [Join_transient, transientD2]) 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, st_set_def]
    "[| F : stable(A);  G : A co A' |] \
\    ==> F Join G : A co A'";
by (cut_inst_tac [("F", "F")] Acts_type 1);
by (cut_inst_tac [("F", "G")] Acts_type 1);
by Auto_tac;
by (REPEAT(Blast_tac 1));
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 "F:program & G:program & st_set(A)" 1);
by (blast_tac (claset() addDs [invariantD2, stableD2]) 2);
by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def,initially_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 & st_set(A)" 1);
by (blast_tac (claset() addDs [stableD2, ensures_type RS subsetD]) 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 [Acts_type RS subsetD], simpset() addsimps [ok_def]));
qed "ok_SKIP1";  

Goal "F ok SKIP";
by (auto_tac (claset() addDs [Acts_type RS subsetD],
      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_distrib2, 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 [Acts_type RS subsetD]) 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 [Acts_type RS subsetD]) 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 [Acts_type RS subsetD], 
               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]));
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(state), (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 "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]));  
by (rewrite_goals_tac [safety_prop_def]);
by Auto_tac;
qed "safety_prop_AllowedActs_iff_Allowed";


Goal "safety_prop(X) ==> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X";
by (subgoal_tac "cons(id(state), Union(RepFun(X, Acts)) Int Pow(state * state)) = \
\                   Union(RepFun(X, Acts))" 1);
by (rtac equalityI 2);
by (REPEAT(force_tac (claset() addDs [Acts_type RS subsetD],
               simpset() addsimps [safety_prop_def]) 2));
by (asm_full_simp_tac (simpset() delsimps UN_simps
                   addsimps [Allowed_def, safety_prop_Acts_iff]) 1);
by (rewrite_goals_tac [safety_prop_def]);
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 "safety_prop(A co B) <-> (A <= B & st_set(A))";
by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1);
by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
by (REPEAT(Blast_tac 1));
qed "safety_prop_constrains";
AddIffs [safety_prop_constrains];

(* To be used with resolution *)
Goal "[| A<=B; st_set(A) |] ==>safety_prop(A co B)";
by Auto_tac;
qed "safety_prop_constrainsI";

Goal "safety_prop(stable(A)) <-> st_set(A)";
by (asm_simp_tac (simpset() addsimps [stable_def]) 1);
qed "safety_prop_stable";
AddIffs [safety_prop_stable];

Goal "st_set(A) ==> safety_prop(stable(A))";
by Auto_tac;
qed "safety_prop_stableI";

Goal "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)";
by (asm_full_simp_tac (simpset() addsimps [safety_prop_def]) 1);
by Auto_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 *)
val [major, minor] = Goalw [safety_prop_def] 
"[| (!!i. i:I ==>safety_prop(X(i))); i:I |] ==> safety_prop(INT i:I. X(i))";
by (cut_facts_tac [minor] 1);
by Safe_tac;
by (full_simp_tac (simpset() addsimps [Inter_iff]) 1);
by (Clarify_tac 1);
by (forward_tac [major] 1);
by (dres_inst_tac [("i", "xa")] major 2);
by (forw_inst_tac [("i", "xa")] major 4);
by (ALLGOALS(Asm_full_simp_tac));
by Auto_tac;
by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"),
                   ("C", "Union(RepFun(X(xa), Acts))")] subset_trans 1);
by (REPEAT(Blast_tac 1));
qed "safety_prop_Inter";

Goalw [ok_def]
"[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X) |] \
\     ==> F ok G <-> (programify(G):X & acts Int Pow(state*state) <= AllowedActs(G))";
by (dres_inst_tac [("G", "G")] safety_prop_Acts_iff 1);
by Safe_tac;
by (ALLGOALS(cut_inst_tac [("F", "G")] AllowedActs_type));
by (ALLGOALS(cut_inst_tac [("F", "G")] Acts_type));
by Auto_tac;
qed "def_UNION_ok_iff";