tuned proofs
authorhaftmann
Mon Sep 21 15:35:15 2009 +0200 (2009-09-21)
changeset 326936c6b1ba5e71e
parent 32692 90c8af39e215
child 32694 0264f360438d
tuned proofs
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:14 2009 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 21 15:35:15 2009 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4    apply (induct set: finite)
     1.5     apply simp
     1.6    apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb
     1.7 -    Int_mono2 Un_subset_iff)
     1.8 +    Int_mono2)
     1.9    done
    1.10  
    1.11  lemma (in LCD) foldD_nest_Un_disjoint:
    1.12 @@ -274,14 +274,14 @@
    1.13    apply (simp add: AC insert_absorb Int_insert_left
    1.14      LCD.foldD_insert [OF LCD.intro [of D]]
    1.15      LCD.foldD_closed [OF LCD.intro [of D]]
    1.16 -    Int_mono2 Un_subset_iff)
    1.17 +    Int_mono2)
    1.18    done
    1.19  
    1.20  lemma (in ACeD) foldD_Un_disjoint:
    1.21    "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
    1.22      foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
    1.23    by (simp add: foldD_Un_Int
    1.24 -    left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
    1.25 +    left_commute LCD.foldD_closed [OF LCD.intro [of D]])
    1.26  
    1.27  
    1.28  subsubsection {* Products over Finite Sets *}
    1.29 @@ -377,7 +377,7 @@
    1.30    from insert have A: "g \<in> A -> carrier G" by fast
    1.31    from insert A a show ?case
    1.32      by (simp add: m_ac Int_insert_left insert_absorb finprod_closed
    1.33 -          Int_mono2 Un_subset_iff) 
    1.34 +          Int_mono2) 
    1.35  qed
    1.36  
    1.37  lemma finprod_Un_disjoint:
     2.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 21 15:35:14 2009 +0200
     2.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Sep 21 15:35:15 2009 +0200
     2.3 @@ -1747,7 +1747,7 @@
     2.4        have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
     2.5  	by (simp add: need_second_arg_def)
     2.6        with s2
     2.7 -      show ?thesis using False by (simp add: Un_subset_iff)
     2.8 +      show ?thesis using False by simp
     2.9      qed
    2.10    next
    2.11      case Super thus ?case by simp
     3.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:14 2009 +0200
     3.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Sep 21 15:35:15 2009 +0200
     3.3 @@ -2953,7 +2953,7 @@
     3.4  	  by simp
     3.5  	from da_e1 s0_s1 True obtain E1' where
     3.6  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
     3.7 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
     3.8 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
     3.9  	with conf_s1 wt_e1
    3.10  	obtain 
    3.11  	  "s2\<Colon>\<preceq>(G, L)"
    3.12 @@ -2972,7 +2972,7 @@
    3.13  	  by simp
    3.14  	from da_e2 s0_s1 False obtain E2' where
    3.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    3.16 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    3.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
    3.18  	with conf_s1 wt_e2
    3.19  	obtain 
    3.20  	  "s2\<Colon>\<preceq>(G, L)"
     4.1 --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 21 15:35:14 2009 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Mon Sep 21 15:35:15 2009 +0200
     4.3 @@ -140,7 +140,7 @@
     4.4    apply fastsimp
     4.5    
     4.6    apply (erule disjE)
     4.7 -   apply (clarsimp simp add: Un_subset_iff)  
     4.8 +   apply clarsimp
     4.9     apply (drule method_wf_mdecl, assumption+)
    4.10     apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
    4.11     apply fastsimp
     5.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:14 2009 +0200
     5.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:15 2009 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/UNITY/ProgressSets
     5.5 -    ID:         $Id$
     5.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7      Copyright   2003  University of Cambridge
     5.8  
     5.9 @@ -245,7 +244,7 @@
    5.10    then have "cl C (T\<inter>?r) \<subseteq> ?r"
    5.11      by (blast intro!: subset_wens) 
    5.12    then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
    5.13 -    by (simp add: Int_subset_iff cl_ident TC
    5.14 +    by (simp add: cl_ident TC
    5.15                    subset_trans [OF cl_mono [OF Int_lower1]]) 
    5.16    show ?thesis
    5.17      by (rule cl_subset_in_lattice [OF cl_subset latt]) 
    5.18 @@ -486,7 +485,7 @@
    5.19    shows "closed F T B L"
    5.20  apply (simp add: closed_def, clarify)
    5.21  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
    5.22 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
    5.23 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
    5.24                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
    5.25  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
    5.26   prefer 2 
     6.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:14 2009 +0200
     6.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Sep 21 15:35:15 2009 +0200
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/UNITY/Transformers
     6.5 -    ID:         $Id$
     6.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7      Copyright   2003  University of Cambridge
     6.8  
     6.9 @@ -133,7 +132,7 @@
    6.10  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
    6.11  apply (simp add: Un_Int_distrib2 Compl_partition2) 
    6.12  apply (erule constrains_weaken, blast) 
    6.13 -apply (simp add: Un_subset_iff wens_weakening) 
    6.14 +apply (simp add: wens_weakening)
    6.15  done
    6.16  
    6.17  text{*Assertion 4.20 in the thesis.*}
    6.18 @@ -151,7 +150,7 @@
    6.19        "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
    6.20         ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
    6.21  apply (rule equalityI)
    6.22 - apply (simp_all add: Int_lower1 Int_subset_iff) 
    6.23 + apply (simp_all add: Int_lower1) 
    6.24   apply (rule wens_Int_eq_lemma, assumption+) 
    6.25  apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
    6.26  done
    6.27 @@ -176,7 +175,7 @@
    6.28   apply (drule_tac act1=act and A1=X 
    6.29          in constrains_Un [OF Diff_wens_constrains]) 
    6.30   apply (erule constrains_weaken, blast) 
    6.31 - apply (simp add: Un_subset_iff wens_weakening) 
    6.32 + apply (simp add: wens_weakening) 
    6.33  apply (rule constrains_weaken) 
    6.34  apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
    6.35  done
    6.36 @@ -229,7 +228,7 @@
    6.37  apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
    6.38                      wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
    6.39   apply (rule subset_wens) 
    6.40 - apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
    6.41 + apply (simp add: awp_Join_eq awp_Int_eq Un_commute)
    6.42   apply (simp add: awp_def wp_def, blast) 
    6.43  apply (insert wens_subset [of F act B], blast) 
    6.44  done
    6.45 @@ -253,7 +252,7 @@
    6.46   apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
    6.47  apply (rule equalityI) 
    6.48   prefer 2 apply blast
    6.49 -apply (simp add: Int_lower1 Int_subset_iff) 
    6.50 +apply (simp add: Int_lower1) 
    6.51  apply (frule wens_set_imp_subset) 
    6.52  apply (subgoal_tac "T-X \<subseteq> awp F T")  
    6.53   prefer 2 apply (blast intro: awpF [THEN subsetD]) 
    6.54 @@ -347,7 +346,7 @@
    6.55        "single_valued act
    6.56         ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
    6.57  apply (rule equalityI)
    6.58 - apply (simp_all add: Un_upper1 Un_subset_iff) 
    6.59 + apply (simp_all add: Un_upper1) 
    6.60  apply (simp add: wens_single_def wp_UN_eq, clarify) 
    6.61  apply (rule_tac a="Suc(i)" in UN_I, auto) 
    6.62  done
     7.1 --- a/src/HOL/UNITY/WFair.thy	Mon Sep 21 15:35:14 2009 +0200
     7.2 +++ b/src/HOL/UNITY/WFair.thy	Mon Sep 21 15:35:15 2009 +0200
     7.3 @@ -113,7 +113,7 @@
     7.4  lemma totalize_transient_iff:
     7.5     "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
     7.6  apply (simp add: totalize_def totalize_act_def transient_def 
     7.7 -                 Un_Image Un_subset_iff, safe)
     7.8 +                 Un_Image, safe)
     7.9  apply (blast intro!: rev_bexI)+
    7.10  done
    7.11