src/HOL/UNITY/Transformers.thy
changeset 32693 6c6b1ba5e71e
parent 32587 caa5ada96a00
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:14 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:15 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/UNITY/Transformers
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   2003  University of Cambridge
     1.8  
     1.9 @@ -133,7 +132,7 @@
    1.10  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
    1.11  apply (simp add: Un_Int_distrib2 Compl_partition2) 
    1.12  apply (erule constrains_weaken, blast) 
    1.13 -apply (simp add: Un_subset_iff wens_weakening) 
    1.14 +apply (simp add: wens_weakening)
    1.15  done
    1.16  
    1.17  text{*Assertion 4.20 in the thesis.*}
    1.18 @@ -151,7 +150,7 @@
    1.19        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
    1.20         ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
    1.21  apply (rule equalityI)
    1.22 - apply (simp_all add: Int_lower1 Int_subset_iff) 
    1.23 + apply (simp_all add: Int_lower1) 
    1.24   apply (rule wens_Int_eq_lemma, assumption+) 
    1.25  apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
    1.26  done
    1.27 @@ -176,7 +175,7 @@
    1.28   apply (drule_tac act1=act and A1=X 
    1.29          in constrains_Un [OF Diff_wens_constrains]) 
    1.30   apply (erule constrains_weaken, blast) 
    1.31 - apply (simp add: Un_subset_iff wens_weakening) 
    1.32 + apply (simp add: wens_weakening) 
    1.33  apply (rule constrains_weaken) 
    1.34  apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
    1.35  done
    1.36 @@ -229,7 +228,7 @@
    1.37  apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
    1.38                      wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
    1.39   apply (rule subset_wens) 
    1.40 - apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
    1.41 + apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
    1.42   apply (simp add: awp_def wp_def, blast) 
    1.43  apply (insert wens_subset [of F act B], blast) 
    1.44  done
    1.45 @@ -253,7 +252,7 @@
    1.46   apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
    1.47  apply (rule equalityI) 
    1.48   prefer 2 apply blast
    1.49 -apply (simp add: Int_lower1 Int_subset_iff) 
    1.50 +apply (simp add: Int_lower1) 
    1.51  apply (frule wens_set_imp_subset) 
    1.52  apply (subgoal_tac "T-X \<subseteq> awp F T")  
    1.53   prefer 2 apply (blast intro: awpF [THEN subsetD]) 
    1.54 @@ -347,7 +346,7 @@
    1.55        "single_valued act
    1.56         ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
    1.57  apply (rule equalityI)
    1.58 - apply (simp_all add: Un_upper1 Un_subset_iff) 
    1.59 + apply (simp_all add: Un_upper1) 
    1.60  apply (simp add: wens_single_def wp_UN_eq, clarify) 
    1.61  apply (rule_tac a="Suc(i)" in UN_I, auto) 
    1.62  done