generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
authorhaftmann
Sat Mar 22 08:37:43 2014 +0100 (2014-03-22)
changeset 5624867dc9549fa15
parent 56247 1ad01f98dc3e
child 56258 fec233e7f67d
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
NEWS
src/HOL/Complete_Lattices.thy
src/HOL/Fun_Def.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/Union.thy
     1.1 --- a/NEWS	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/NEWS	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -138,6 +138,10 @@
     1.4  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Default congruence rules strong_INF_cong and strong_SUP_cong,
     1.8 +with simplifier implication in premises.  Generalized and replace
     1.9 +former INT_cong, SUP_cong.  INCOMPATIBILITY.
    1.10 +
    1.11  * Consolidated theorem names containing INFI and SUPR: have INF
    1.12  and SUP instead uniformly.  INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/Complete_Lattices.thy	Fri Mar 21 22:54:16 2014 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Sat Mar 22 08:37:43 2014 +0100
     2.3 @@ -40,6 +40,10 @@
     2.4    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
     2.5    by (simp add: INF_def image_def)
     2.6  
     2.7 +lemma strong_INF_cong [cong]:
     2.8 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
     2.9 +  unfolding simp_implies_def by (fact INF_cong)
    2.10 +
    2.11  end
    2.12  
    2.13  class Sup =
    2.14 @@ -69,6 +73,10 @@
    2.15    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    2.16    by (simp add: SUP_def image_def)
    2.17  
    2.18 +lemma strong_SUP_cong [cong]:
    2.19 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
    2.20 +  unfolding simp_implies_def by (fact SUP_cong)
    2.21 +
    2.22  end
    2.23  
    2.24  text {*
    2.25 @@ -447,21 +455,23 @@
    2.26  lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
    2.27    using Inf_le_Sup [of "f ` A"] by simp
    2.28  
    2.29 -lemma SUP_eq_const:
    2.30 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
    2.31 -  by (auto intro: SUP_eqI)
    2.32 -
    2.33  lemma INF_eq_const:
    2.34    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
    2.35    by (auto intro: INF_eqI)
    2.36  
    2.37 -lemma SUP_eq_iff:
    2.38 -  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    2.39 -  using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
    2.40 +lemma SUP_eq_const:
    2.41 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
    2.42 +  by (auto intro: SUP_eqI)
    2.43  
    2.44  lemma INF_eq_iff:
    2.45    "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    2.46 -  using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
    2.47 +  using INF_eq_const [of I f c] INF_lower [of _ I f]
    2.48 +  by (auto intro: antisym cong del: strong_INF_cong)
    2.49 +
    2.50 +lemma SUP_eq_iff:
    2.51 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    2.52 +  using SUP_eq_const [of I f c] SUP_upper [of _ I f]
    2.53 +  by (auto intro: antisym cong del: strong_SUP_cong)
    2.54  
    2.55  end
    2.56  
    2.57 @@ -937,10 +947,6 @@
    2.58    -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
    2.59    by (auto simp add: INF_def image_def)
    2.60  
    2.61 -lemma INT_cong [cong]:
    2.62 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
    2.63 -  by (fact INF_cong)
    2.64 -
    2.65  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
    2.66    by blast
    2.67  
    2.68 @@ -1132,14 +1138,6 @@
    2.69  lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
    2.70    by (auto simp add: SUP_def image_def)
    2.71  
    2.72 -lemma UN_cong [cong]:
    2.73 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
    2.74 -  by (fact SUP_cong)
    2.75 -
    2.76 -lemma strong_UN_cong:
    2.77 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
    2.78 -  by (unfold simp_implies_def) (fact UN_cong)
    2.79 -
    2.80  lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
    2.81    by blast
    2.82  
     3.1 --- a/src/HOL/Fun_Def.thy	Fri Mar 21 22:54:16 2014 +0100
     3.2 +++ b/src/HOL/Fun_Def.thy	Sat Mar 22 08:37:43 2014 +0100
     3.3 @@ -144,7 +144,7 @@
     3.4    unfolding Let_def by blast
     3.5  
     3.6  lemmas [fundef_cong] =
     3.7 -  if_cong image_cong INT_cong UN_cong
     3.8 +  if_cong image_cong INF_cong SUP_cong
     3.9    bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
    3.10  
    3.11  lemma split_cong [fundef_cong]:
     4.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Fri Mar 21 22:54:16 2014 +0100
     4.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sat Mar 22 08:37:43 2014 +0100
     4.3 @@ -117,11 +117,11 @@
     4.4      apply simp
     4.5     apply clarify
     4.6     apply simp
     4.7 -   apply(subgoal_tac "j=0")
     4.8 -    apply (simp)
     4.9 +   apply(subgoal_tac "xa=0")
    4.10 +    apply simp
    4.11     apply arith
    4.12    apply clarify
    4.13 -  apply(case_tac i,simp,simp)
    4.14 +  apply(case_tac xaa, simp, simp)
    4.15   apply clarify
    4.16   apply simp
    4.17   apply(erule_tac x=0 in all_dupE)
    4.18 @@ -319,11 +319,10 @@
    4.19        \<lbrace>True\<rbrace>,
    4.20        \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and> 
    4.21          (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
    4.22 -apply(rule Parallel)
    4.23 ---{* 5 subgoals left *}
    4.24 -apply auto
    4.25 -apply force+
    4.26 -apply(rule While)
    4.27 +apply (rule Parallel)
    4.28 +apply (auto cong del: strong_INF_cong strong_SUP_cong) 
    4.29 +apply force
    4.30 +apply (rule While)
    4.31      apply force
    4.32     apply force
    4.33    apply force
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Mar 21 22:54:16 2014 +0100
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Sat Mar 22 08:37:43 2014 +0100
     5.3 @@ -1613,7 +1613,8 @@
     5.4      using `0 \<le> c` by (rule ereal_mult_left_mono)
     5.5  next
     5.6    fix y
     5.7 -  assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
     5.8 +  assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
     5.9 +  then have *: "\<And>i. c * f i \<le> y" by simp
    5.10    show "c * SUPREMUM UNIV f \<le> y"
    5.11    proof (cases "0 < c \<and> c \<noteq> \<infinity>")
    5.12      case True
    5.13 @@ -1631,7 +1632,7 @@
    5.14          then have "range f = {0}"
    5.15            by auto
    5.16          with True show "c * SUPREMUM UNIV f \<le> y"
    5.17 -          using * by (auto simp: SUP_def max.absorb1)
    5.18 +          using * by auto
    5.19        next
    5.20          case False
    5.21          then obtain i where "f i \<noteq> 0"
     6.1 --- a/src/HOL/Library/Old_Recdef.thy	Fri Mar 21 22:54:16 2014 +0100
     6.2 +++ b/src/HOL/Library/Old_Recdef.thy	Sat Mar 22 08:37:43 2014 +0100
     6.3 @@ -77,7 +77,7 @@
     6.4    less_Suc_eq [THEN iffD2]
     6.5  
     6.6  lemmas [recdef_cong] =
     6.7 -  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
     6.8 +  if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
     6.9    map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
    6.10  
    6.11  lemmas [recdef_wf] =
     7.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 21 22:54:16 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Mar 22 08:37:43 2014 +0100
     7.3 @@ -204,9 +204,9 @@
     7.4              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
     7.5            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
     7.6              (fn (i, (set_map0, coalg_set)) =>
     7.7 -              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
     7.8 +              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm SUP_cong})),
     7.9                  etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
    7.10 -                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
    7.11 +                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm SUP_cong}),
    7.12                  ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
    7.13                  REPEAT_DETERM o etac allE, atac, atac])
    7.14              (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
    7.15 @@ -866,14 +866,14 @@
    7.16            (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    7.17          rtac Un_cong, rtac refl,
    7.18          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
    7.19 -          (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
    7.20 +          (fn i => EVERY' [rtac @{thm SUP_cong[OF refl]},
    7.21              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
    7.22        (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
    7.23    end;
    7.24  
    7.25  fun mk_set_map0_tac col_natural =
    7.26    EVERY' (map rtac [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans,
    7.27 -    refl RS @{thm UN_cong}, col_natural]) 1;
    7.28 +    refl RS @{thm SUP_cong}, col_natural]) 1;
    7.29  
    7.30  fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
    7.31    let
    7.32 @@ -964,7 +964,7 @@
    7.33              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
    7.34              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
    7.35                (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
    7.36 -                rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
    7.37 +                rtac @{thm SUP_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
    7.38                  rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
    7.39                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
    7.40                  dtac @{thm ssubst_mem[OF pair_collapse]},
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 21 22:54:16 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sat Mar 22 08:37:43 2014 +0100
     8.3 @@ -196,7 +196,7 @@
     8.4  
     8.5  fun mk_min_algs_tac worel in_congs =
     8.6    let
     8.7 -    val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
     8.8 +    val minG_tac = EVERY' [rtac @{thm SUP_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
     8.9      fun minH_tac thm =
    8.10        EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
    8.11          REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
    8.12 @@ -530,8 +530,8 @@
    8.13    let
    8.14      val n = length ctor_maps;
    8.15  
    8.16 -    fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
    8.17 -      rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
    8.18 +    fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm SUP_cong},
    8.19 +      rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm SUP_cong},
    8.20        rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
    8.21  
    8.22      fun mk_set_nat cset ctor_map ctor_set set_nats =
    8.23 @@ -672,7 +672,7 @@
    8.24              rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac,
    8.25              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
    8.26                (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans,
    8.27 -                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
    8.28 +                rtac @{thm SUP_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
    8.29                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
    8.30                  dtac @{thm ssubst_mem[OF pair_collapse]},
    8.31                  REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
     9.1 --- a/src/HOL/UNITY/Follows.thy	Fri Mar 21 22:54:16 2014 +0100
     9.2 +++ b/src/HOL/UNITY/Follows.thy	Sat Mar 22 08:37:43 2014 +0100
     9.3 @@ -94,7 +94,7 @@
     9.4  
     9.5  apply (simp add: Follows_def Increasing_def Stable_def, auto)
     9.6  apply (erule_tac [3] Always_LeadsTo_weaken)
     9.7 -apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}" 
     9.8 +apply (erule_tac A = "{s. x \<le> f s}" and A' = "{s. x \<le> f s}" 
     9.9         in Always_Constrains_weaken, auto)
    9.10  apply (drule Always_Int_I, assumption)
    9.11  apply (force intro: Always_weaken)
    9.12 @@ -104,7 +104,7 @@
    9.13       "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
    9.14  apply (simp add: Follows_def Increasing_def Stable_def, auto)
    9.15  apply (erule_tac [3] Always_LeadsTo_weaken)
    9.16 -apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
    9.17 +apply (erule_tac A = "{s. x \<le> g s}" and A' = "{s. x \<le> g s}"
    9.18         in Always_Constrains_weaken, auto)
    9.19  apply (drule Always_Int_I, assumption)
    9.20  apply (force intro: Always_weaken)
    9.21 @@ -114,12 +114,13 @@
    9.22  subsection{*Union properties (with the subset ordering)*}
    9.23  
    9.24  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
    9.25 +
    9.26  lemma increasing_Un: 
    9.27      "[| F \<in> increasing f;  F \<in> increasing g |]  
    9.28       ==> F \<in> increasing (%s. (f s) \<union> (g s))"
    9.29  apply (simp add: increasing_def stable_def constrains_def, auto)
    9.30 -apply (drule_tac x = "f xa" in spec)
    9.31 -apply (drule_tac x = "g xa" in spec)
    9.32 +apply (drule_tac x = "f xb" in spec)
    9.33 +apply (drule_tac x = "g xb" in spec)
    9.34  apply (blast dest!: bspec)
    9.35  done
    9.36  
    9.37 @@ -128,8 +129,8 @@
    9.38       ==> F \<in> Increasing (%s. (f s) \<union> (g s))"
    9.39  apply (auto simp add: Increasing_def Stable_def Constrains_def
    9.40                        stable_def constrains_def)
    9.41 -apply (drule_tac x = "f xa" in spec)
    9.42 -apply (drule_tac x = "g xa" in spec)
    9.43 +apply (drule_tac x = "f xb" in spec)
    9.44 +apply (drule_tac x = "g xb" in spec)
    9.45  apply (blast dest!: bspec)
    9.46  done
    9.47  
    9.48 @@ -172,8 +173,8 @@
    9.49      "[| F \<in> increasing f;  F \<in> increasing g |]  
    9.50       ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
    9.51  apply (simp add: increasing_def stable_def constrains_def, auto)
    9.52 -apply (drule_tac x = "f xa" in spec)
    9.53 -apply (drule_tac x = "g xa" in spec)
    9.54 +apply (drule_tac x = "f xb" in spec)
    9.55 +apply (drule_tac x = "g xb" in spec)
    9.56  apply (drule bspec, assumption) 
    9.57  apply (blast intro: add_mono order_trans)
    9.58  done
    9.59 @@ -183,8 +184,8 @@
    9.60       ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
    9.61  apply (auto simp add: Increasing_def Stable_def Constrains_def
    9.62                        stable_def constrains_def)
    9.63 -apply (drule_tac x = "f xa" in spec)
    9.64 -apply (drule_tac x = "g xa" in spec)
    9.65 +apply (drule_tac x = "f xb" in spec)
    9.66 +apply (drule_tac x = "g xb" in spec)
    9.67  apply (drule bspec, assumption) 
    9.68  apply (blast intro: add_mono order_trans)
    9.69  done
    10.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Mar 21 22:54:16 2014 +0100
    10.2 +++ b/src/HOL/UNITY/Transformers.thy	Sat Mar 22 08:37:43 2014 +0100
    10.3 @@ -346,7 +346,7 @@
    10.4  apply (rule equalityI)
    10.5   apply (simp_all add: Un_upper1) 
    10.6  apply (simp add: wens_single_def wp_UN_eq, clarify) 
    10.7 -apply (rule_tac a="Suc(i)" in UN_I, auto) 
    10.8 +apply (rule_tac a="Suc xa" in UN_I, auto) 
    10.9  done
   10.10  
   10.11  lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
    11.1 --- a/src/HOL/UNITY/Union.thy	Fri Mar 21 22:54:16 2014 +0100
    11.2 +++ b/src/HOL/UNITY/Union.thy	Sat Mar 22 08:37:43 2014 +0100
    11.3 @@ -404,16 +404,16 @@
    11.4  by (simp add: stable_def)
    11.5  
    11.6  lemma safety_prop_Int [simp]:
    11.7 -     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
    11.8 -by (simp add: safety_prop_def, blast)
    11.9 +  "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
   11.10 +  by (simp add: safety_prop_def) blast
   11.11 +
   11.12 +lemma safety_prop_INTER [simp]:
   11.13 +  "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
   11.14 +  by (simp add: safety_prop_def) blast
   11.15  
   11.16  lemma safety_prop_INTER1 [simp]:
   11.17 -     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
   11.18 -by (auto simp add: safety_prop_def, blast)
   11.19 -
   11.20 -lemma safety_prop_INTER [simp]:
   11.21 -     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
   11.22 -by (auto simp add: safety_prop_def, blast)
   11.23 +  "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
   11.24 +  by (rule safety_prop_INTER) simp
   11.25  
   11.26  lemma def_prg_Allowed:
   11.27       "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]