tuned proofs
authorhaftmann
Tue Aug 09 20:24:48 2011 +0200 (2011-08-09)
changeset 441060e018cbcc0de
parent 44105 04e51b7a3422
child 44107 60edd70b72bd
tuned proofs
src/HOL/Algebra/Ideal.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Aug 09 18:52:18 2011 +0200
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Aug 09 20:24:48 2011 +0200
     1.3 @@ -227,26 +227,14 @@
     1.4      and notempty: "S \<noteq> {}"
     1.5    shows "ideal (Inter S) R"
     1.6  apply (unfold_locales)
     1.7 -apply (simp_all add: Inter_def INTER_def)
     1.8 -      apply (rule, simp) defer 1
     1.9 +apply (simp_all add: Inter_eq)
    1.10 +      apply rule unfolding mem_Collect_eq defer 1
    1.11        apply rule defer 1
    1.12        apply rule defer 1
    1.13        apply (fold a_inv_def, rule) defer 1
    1.14        apply rule defer 1
    1.15        apply rule defer 1
    1.16  proof -
    1.17 -  fix x
    1.18 -  assume "\<forall>I\<in>S. x \<in> I"
    1.19 -  hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
    1.20 -
    1.21 -  from notempty have "\<exists>I0. I0 \<in> S" by blast
    1.22 -  from this obtain I0 where I0S: "I0 \<in> S" by auto
    1.23 -
    1.24 -  interpret ideal I0 R by (rule Sideals[OF I0S])
    1.25 -
    1.26 -  from xI[OF I0S] have "x \<in> I0" .
    1.27 -  from this and a_subset show "x \<in> carrier R" by fast
    1.28 -next
    1.29    fix x y
    1.30    assume "\<forall>I\<in>S. x \<in> I"
    1.31    hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
    1.32 @@ -298,6 +286,20 @@
    1.33  
    1.34    from xI[OF JS] and ycarr
    1.35        show "x \<otimes> y \<in> J" by (rule I_r_closed)
    1.36 +next
    1.37 +  fix x
    1.38 +  assume "\<forall>I\<in>S. x \<in> I"
    1.39 +  hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
    1.40 +
    1.41 +  from notempty have "\<exists>I0. I0 \<in> S" by blast
    1.42 +  from this obtain I0 where I0S: "I0 \<in> S" by auto
    1.43 +
    1.44 +  interpret ideal I0 R by (rule Sideals[OF I0S])
    1.45 +
    1.46 +  from xI[OF I0S] have "x \<in> I0" .
    1.47 +  from this and a_subset show "x \<in> carrier R" by fast
    1.48 +next
    1.49 +
    1.50  qed
    1.51  
    1.52  
     2.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Tue Aug 09 18:52:18 2011 +0200
     2.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Aug 09 20:24:48 2011 +0200
     2.3 @@ -590,7 +590,6 @@
     2.4    "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
     2.5    "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
     2.6    "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
     2.7 -  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
     2.8    "UNIONS_0" > "Complete_Lattice.Union_empty"
     2.9    "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
    2.10    "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
    2.11 @@ -1596,7 +1595,6 @@
    2.12    "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
    2.13    "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
    2.14    "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
    2.15 -  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
    2.16    "INTERS_0" > "Complete_Lattice.Inter_empty"
    2.17    "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
    2.18    "INSERT_UNION_EQ" > "Set.Un_insert_left"
     3.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Aug 09 18:52:18 2011 +0200
     3.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Aug 09 20:24:48 2011 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  imports
     3.5    "~~/src/HOL/Algebra/Ring"
     3.6    "~~/src/HOL/Algebra/FiniteProduct"
     3.7 -begin;
     3.8 +begin
     3.9  
    3.10  (* finiteness stuff *)
    3.11  
    3.12 @@ -34,7 +34,7 @@
    3.13  definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    3.14    "units_of G == (| carrier = Units G,
    3.15       Group.monoid.mult = Group.monoid.mult G,
    3.16 -     one  = one G |)";
    3.17 +     one  = one G |)"
    3.18  
    3.19  (*
    3.20  
    3.21 @@ -264,7 +264,7 @@
    3.22        (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
    3.23     ==> finprod G f (Union C) = finprod G (finprod G f) C" 
    3.24    apply (frule finprod_UN_disjoint [of C id f])
    3.25 -  apply (unfold Union_def id_def, auto)
    3.26 +  apply (auto simp add: SUP_def)
    3.27  done
    3.28  
    3.29  lemma (in comm_monoid) finprod_one [rule_format]: 
     4.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 18:52:18 2011 +0200
     4.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Aug 09 20:24:48 2011 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {*Caratheodory Extension Theorem*}
     4.5  
     4.6  theory Caratheodory
     4.7 -  imports Sigma_Algebra Extended_Real_Limits
     4.8 +imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
     4.9  begin
    4.10  
    4.11  lemma sums_def2:
    4.12 @@ -433,8 +433,7 @@
    4.13              hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
    4.14                by (simp add: lambda_system_eq UNION_in)
    4.15              have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
    4.16 -              by (blast intro: increasingD [OF inc] UNION_eq_Union_image
    4.17 -                               UNION_in U_in)
    4.18 +              by (blast intro: increasingD [OF inc] UNION_in U_in)
    4.19              thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
    4.20                by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
    4.21            next
     5.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Aug 09 18:52:18 2011 +0200
     5.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Aug 09 20:24:48 2011 +0200
     5.3 @@ -315,10 +315,10 @@
     5.4    by (auto simp add: binary_def)
     5.5  
     5.6  lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
     5.7 -  by (simp add: UNION_eq_Union_image range_binary_eq)
     5.8 +  by (simp add: SUP_def range_binary_eq)
     5.9  
    5.10  lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
    5.11 -  by (simp add: INTER_eq_Inter_image range_binary_eq)
    5.12 +  by (simp add: INF_def range_binary_eq)
    5.13  
    5.14  lemma sigma_algebra_iff2:
    5.15       "sigma_algebra M \<longleftrightarrow>
    5.16 @@ -1109,7 +1109,7 @@
    5.17    done
    5.18  
    5.19  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
    5.20 -  by (simp add: UNION_eq_Union_image range_binaryset_eq)
    5.21 +  by (simp add: SUP_def range_binaryset_eq)
    5.22  
    5.23  section {* Closed CDI *}
    5.24  
     6.1 --- a/src/HOL/UNITY/ELT.thy	Tue Aug 09 18:52:18 2011 +0200
     6.2 +++ b/src/HOL/UNITY/ELT.thy	Tue Aug 09 20:24:48 2011 +0200
     6.3 @@ -186,9 +186,7 @@
     6.4  lemma leadsETo_Un:
     6.5       "[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] 
     6.6        ==> F : (A Un B) leadsTo[CC] C"
     6.7 -apply (subst Un_eq_Union)
     6.8 -apply (blast intro: leadsETo_Union)
     6.9 -done
    6.10 +  using leadsETo_Union [of "{A, B}" F CC C] by auto
    6.11  
    6.12  lemma single_leadsETo_I:
    6.13       "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
    6.14 @@ -407,9 +405,7 @@
    6.15  lemma LeadsETo_Un:
    6.16       "[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]  
    6.17        ==> F : (A Un B) LeadsTo[CC] C"
    6.18 -apply (subst Un_eq_Union)
    6.19 -apply (blast intro: LeadsETo_Union)
    6.20 -done
    6.21 +  using LeadsETo_Union [of "{A, B}" F CC C] by auto
    6.22  
    6.23  (*Lets us look at the starting state*)
    6.24  lemma single_LeadsETo_I:
     7.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 18:52:18 2011 +0200
     7.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Aug 09 20:24:48 2011 +0200
     7.3 @@ -42,25 +42,21 @@
     7.4  
     7.5  lemma UN_in_lattice:
     7.6       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
     7.7 -apply (simp add: UN_eq) 
     7.8 +apply (unfold SUP_def)
     7.9  apply (blast intro: Union_in_lattice) 
    7.10  done
    7.11  
    7.12  lemma INT_in_lattice:
    7.13       "[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i)  \<in> L"
    7.14 -apply (simp add: INT_eq) 
    7.15 +apply (unfold INF_def)
    7.16  apply (blast intro: Inter_in_lattice) 
    7.17  done
    7.18  
    7.19  lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
    7.20 -apply (simp only: Un_eq_Union) 
    7.21 -apply (blast intro: Union_in_lattice) 
    7.22 -done
    7.23 +  using Union_in_lattice [of "{x, y}" L] by simp
    7.24  
    7.25  lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
    7.26 -apply (simp only: Int_eq_Inter) 
    7.27 -apply (blast intro: Inter_in_lattice) 
    7.28 -done
    7.29 +  using Inter_in_lattice [of "{x, y}" L] by simp
    7.30  
    7.31  lemma lattice_stable: "lattice {X. F \<in> stable X}"
    7.32  by (simp add: lattice_def stable_def constrains_def, blast)
     8.1 --- a/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 18:52:18 2011 +0200
     8.2 +++ b/src/HOL/UNITY/SubstAx.thy	Tue Aug 09 20:24:48 2011 +0200
     8.3 @@ -85,16 +85,14 @@
     8.4  
     8.5  lemma LeadsTo_UN: 
     8.6       "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
     8.7 -apply (simp only: Union_image_eq [symmetric])
     8.8 +apply (unfold SUP_def)
     8.9  apply (blast intro: LeadsTo_Union)
    8.10  done
    8.11  
    8.12  text{*Binary union introduction rule*}
    8.13  lemma LeadsTo_Un:
    8.14       "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
    8.15 -apply (subst Un_eq_Union)
    8.16 -apply (blast intro: LeadsTo_Union)
    8.17 -done
    8.18 +  using LeadsTo_UN [of "{A, B}" F id C] by auto
    8.19  
    8.20  text{*Lets us look at the starting state*}
    8.21  lemma single_LeadsTo_I:
     9.1 --- a/src/HOL/UNITY/Transformers.thy	Tue Aug 09 18:52:18 2011 +0200
     9.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 09 20:24:48 2011 +0200
     9.3 @@ -467,7 +467,7 @@
     9.4        "single_valued act
     9.5         ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
     9.6             wens_set (mk_program (init, {act}, allowed)) B"
     9.7 -apply (simp add: wens_single_eq_Union UN_eq) 
     9.8 +apply (simp add: SUP_def image_def wens_single_eq_Union) 
     9.9  apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
    9.10  done
    9.11  
    10.1 --- a/src/HOL/UNITY/WFair.thy	Tue Aug 09 18:52:18 2011 +0200
    10.2 +++ b/src/HOL/UNITY/WFair.thy	Tue Aug 09 20:24:48 2011 +0200
    10.3 @@ -211,9 +211,7 @@
    10.4  text{*Binary union introduction rule*}
    10.5  lemma leadsTo_Un:
    10.6       "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
    10.7 -apply (subst Un_eq_Union)
    10.8 -apply (blast intro: leadsTo_Union)
    10.9 -done
   10.10 +  using leadsTo_Union [of "{A, B}" F C] by auto
   10.11  
   10.12  lemma single_leadsTo_I: 
   10.13       "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"