--- a/src/HOL/Algebra/Ideal.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/Algebra/Ideal.thy Tue Aug 09 20:24:48 2011 +0200
@@ -227,26 +227,14 @@
and notempty: "S \<noteq> {}"
shows "ideal (Inter S) R"
apply (unfold_locales)
-apply (simp_all add: Inter_def INTER_def)
- apply (rule, simp) defer 1
+apply (simp_all add: Inter_eq)
+ apply rule unfolding mem_Collect_eq defer 1
apply rule defer 1
apply rule defer 1
apply (fold a_inv_def, rule) defer 1
apply rule defer 1
apply rule defer 1
proof -
- fix x
- assume "\<forall>I\<in>S. x \<in> I"
- hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
-
- from notempty have "\<exists>I0. I0 \<in> S" by blast
- from this obtain I0 where I0S: "I0 \<in> S" by auto
-
- interpret ideal I0 R by (rule Sideals[OF I0S])
-
- from xI[OF I0S] have "x \<in> I0" .
- from this and a_subset show "x \<in> carrier R" by fast
-next
fix x y
assume "\<forall>I\<in>S. x \<in> I"
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
@@ -298,6 +286,20 @@
from xI[OF JS] and ycarr
show "x \<otimes> y \<in> J" by (rule I_r_closed)
+next
+ fix x
+ assume "\<forall>I\<in>S. x \<in> I"
+ hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
+
+ from notempty have "\<exists>I0. I0 \<in> S" by blast
+ from this obtain I0 where I0S: "I0 \<in> S" by auto
+
+ interpret ideal I0 R by (rule Sideals[OF I0S])
+
+ from xI[OF I0S] have "x \<in> I0" .
+ from this and a_subset show "x \<in> carrier R" by fast
+next
+
qed
--- a/src/HOL/Import/HOLLight/hollight.imp Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Tue Aug 09 20:24:48 2011 +0200
@@ -590,7 +590,6 @@
"UNIONS_INSERT" > "Complete_Lattice.Union_insert"
"UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
"UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
- "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
"UNIONS_0" > "Complete_Lattice.Union_empty"
"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1596,7 +1595,6 @@
"INTERS_INSERT" > "Complete_Lattice.Inter_insert"
"INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
"INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
- "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
"INTERS_0" > "Complete_Lattice.Inter_empty"
"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
"INSERT_UNION_EQ" > "Set.Un_insert_left"
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Tue Aug 09 20:24:48 2011 +0200
@@ -8,7 +8,7 @@
imports
"~~/src/HOL/Algebra/Ring"
"~~/src/HOL/Algebra/FiniteProduct"
-begin;
+begin
(* finiteness stuff *)
@@ -34,7 +34,7 @@
definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
"units_of G == (| carrier = Units G,
Group.monoid.mult = Group.monoid.mult G,
- one = one G |)";
+ one = one G |)"
(*
@@ -264,7 +264,7 @@
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
==> finprod G f (Union C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, auto)
+ apply (auto simp add: SUP_def)
done
lemma (in comm_monoid) finprod_one [rule_format]:
--- a/src/HOL/Probability/Caratheodory.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Tue Aug 09 20:24:48 2011 +0200
@@ -6,7 +6,7 @@
header {*Caratheodory Extension Theorem*}
theory Caratheodory
- imports Sigma_Algebra Extended_Real_Limits
+imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
begin
lemma sums_def2:
@@ -433,8 +433,7 @@
hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
by (simp add: lambda_system_eq UNION_in)
have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
- by (blast intro: increasingD [OF inc] UNION_eq_Union_image
- UNION_in U_in)
+ by (blast intro: increasingD [OF inc] UNION_in U_in)
thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
next
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Aug 09 20:24:48 2011 +0200
@@ -315,10 +315,10 @@
by (auto simp add: binary_def)
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
- by (simp add: UNION_eq_Union_image range_binary_eq)
+ by (simp add: SUP_def range_binary_eq)
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
- by (simp add: INTER_eq_Inter_image range_binary_eq)
+ by (simp add: INF_def range_binary_eq)
lemma sigma_algebra_iff2:
"sigma_algebra M \<longleftrightarrow>
@@ -1109,7 +1109,7 @@
done
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
- by (simp add: UNION_eq_Union_image range_binaryset_eq)
+ by (simp add: SUP_def range_binaryset_eq)
section {* Closed CDI *}
--- a/src/HOL/UNITY/ELT.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/ELT.thy Tue Aug 09 20:24:48 2011 +0200
@@ -186,9 +186,7 @@
lemma leadsETo_Un:
"[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |]
==> F : (A Un B) leadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsETo_Union)
-done
+ using leadsETo_Union [of "{A, B}" F CC C] by auto
lemma single_leadsETo_I:
"(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
@@ -407,9 +405,7 @@
lemma LeadsETo_Un:
"[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]
==> F : (A Un B) LeadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsETo_Union)
-done
+ using LeadsETo_Union [of "{A, B}" F CC C] by auto
(*Lets us look at the starting state*)
lemma single_LeadsETo_I:
--- a/src/HOL/UNITY/ProgressSets.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Tue Aug 09 20:24:48 2011 +0200
@@ -42,25 +42,21 @@
lemma UN_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
-apply (simp add: UN_eq)
+apply (unfold SUP_def)
apply (blast intro: Union_in_lattice)
done
lemma INT_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i) \<in> L"
-apply (simp add: INT_eq)
+apply (unfold INF_def)
apply (blast intro: Inter_in_lattice)
done
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
-apply (simp only: Un_eq_Union)
-apply (blast intro: Union_in_lattice)
-done
+ using Union_in_lattice [of "{x, y}" L] by simp
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
-apply (simp only: Int_eq_Inter)
-apply (blast intro: Inter_in_lattice)
-done
+ using Inter_in_lattice [of "{x, y}" L] by simp
lemma lattice_stable: "lattice {X. F \<in> stable X}"
by (simp add: lattice_def stable_def constrains_def, blast)
--- a/src/HOL/UNITY/SubstAx.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Tue Aug 09 20:24:48 2011 +0200
@@ -85,16 +85,14 @@
lemma LeadsTo_UN:
"(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
-apply (simp only: Union_image_eq [symmetric])
+apply (unfold SUP_def)
apply (blast intro: LeadsTo_Union)
done
text{*Binary union introduction rule*}
lemma LeadsTo_Un:
"[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsTo_Union)
-done
+ using LeadsTo_UN [of "{A, B}" F id C] by auto
text{*Lets us look at the starting state*}
lemma single_LeadsTo_I:
--- a/src/HOL/UNITY/Transformers.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/Transformers.thy Tue Aug 09 20:24:48 2011 +0200
@@ -467,7 +467,7 @@
"single_valued act
==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq>
wens_set (mk_program (init, {act}, allowed)) B"
-apply (simp add: wens_single_eq_Union UN_eq)
+apply (simp add: SUP_def image_def wens_single_eq_Union)
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
done
--- a/src/HOL/UNITY/WFair.thy Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/WFair.thy Tue Aug 09 20:24:48 2011 +0200
@@ -211,9 +211,7 @@
text{*Binary union introduction rule*}
lemma leadsTo_Un:
"[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsTo_Union)
-done
+ using leadsTo_Union [of "{A, B}" F C] by auto
lemma single_leadsTo_I:
"(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"