src/HOL/UNITY/Union.thy
changeset 56248 67dc9549fa15
parent 46577 e5438c5797ae
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/UNITY/Union.thy	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -404,16 +404,16 @@
     1.4  by (simp add: stable_def)
     1.5  
     1.6  lemma safety_prop_Int [simp]:
     1.7 -     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
     1.8 -by (simp add: safety_prop_def, blast)
     1.9 +  "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
    1.10 +  by (simp add: safety_prop_def) blast
    1.11 +
    1.12 +lemma safety_prop_INTER [simp]:
    1.13 +  "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
    1.14 +  by (simp add: safety_prop_def) blast
    1.15  
    1.16  lemma safety_prop_INTER1 [simp]:
    1.17 -     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
    1.18 -by (auto simp add: safety_prop_def, blast)
    1.19 -
    1.20 -lemma safety_prop_INTER [simp]:
    1.21 -     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
    1.22 -by (auto simp add: safety_prop_def, blast)
    1.23 +  "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
    1.24 +  by (rule safety_prop_INTER) simp
    1.25  
    1.26  lemma def_prg_Allowed:
    1.27       "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]