--- a/src/HOL/Complete_Lattices.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Mar 12 21:41:11 2012 +0100
@@ -591,20 +591,20 @@
by (simp add: Sup_fun_def)
instance proof
-qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
+qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)
end
lemma INF_apply [simp]:
"(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
- by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
+ by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def)
lemma SUP_apply [simp]:
"(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
- by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
+ by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def)
instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
-qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
+qed (auto simp add: INF_def SUP_def inf_Sup sup_Inf image_image)
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
@@ -612,46 +612,46 @@
subsection {* Complete lattice on unary and binary predicates *}
lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
- by (simp add: INF_apply)
+ by simp
lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
- by (simp add: INF_apply)
+ by simp
lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
- by (auto simp add: INF_apply)
+ by auto
lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
- by (auto simp add: INF_apply)
+ by auto
lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
- by (auto simp add: INF_apply)
+ by auto
lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
- by (auto simp add: INF_apply)
+ by auto
lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: INF_apply)
+ by auto
lemma INF2_E: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: INF_apply)
+ by auto
lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
- by (simp add: SUP_apply)
+ by simp
lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
- by (simp add: SUP_apply)
+ by simp
lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
- by (auto simp add: SUP_apply)
+ by auto
lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
- by (auto simp add: SUP_apply)
+ by auto
lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: SUP_apply)
+ by auto
lemma SUP2_E: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: SUP_apply)
+ by auto
subsection {* Complete lattice on @{typ "_ set"} *}
--- a/src/HOL/Lattices.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Lattices.thy Mon Mar 12 21:41:11 2012 +0100
@@ -662,12 +662,12 @@
by (simp add: sup_fun_def)
instance proof
-qed (simp_all add: le_fun_def inf_apply sup_apply)
+qed (simp_all add: le_fun_def)
end
instance "fun" :: (type, distrib_lattice) distrib_lattice proof
-qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
+qed (rule ext, simp add: sup_inf_distrib1)
instance "fun" :: (type, bounded_lattice) bounded_lattice ..
@@ -700,7 +700,7 @@
end
instance "fun" :: (type, boolean_algebra) boolean_algebra proof
-qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
+qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
subsection {* Lattice on unary and binary predicates *}
--- a/src/HOL/Library/Cset.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Library/Cset.thy Mon Mar 12 21:41:11 2012 +0100
@@ -175,10 +175,10 @@
subsection {* Simplified simprules *}
lemma empty_simp [simp]: "member Cset.empty = bot"
- by (simp add: fun_eq_iff bot_apply)
+ by (simp add: fun_eq_iff)
lemma UNIV_simp [simp]: "member Cset.UNIV = top"
- by (simp add: fun_eq_iff top_apply)
+ by (simp add: fun_eq_iff)
lemma is_empty_simp [simp]:
"is_empty A \<longleftrightarrow> set_of A = {}"
@@ -222,7 +222,7 @@
lemma member_SUP [simp]:
"member (SUPR A f) = SUPR A (member \<circ> f)"
- by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
+ by (auto simp add: fun_eq_iff member_def, unfold SUP_def, auto)
lemma member_bind [simp]:
"member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
@@ -247,14 +247,14 @@
lemma bind_single [simp]:
"A \<guillemotright>= single = A"
- by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
+ by (simp add: Cset.set_eq_iff fun_eq_iff single_def member_def)
lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
by (auto simp add: Cset.set_eq_iff fun_eq_iff)
lemma empty_bind [simp]:
"Cset.empty \<guillemotright>= f = Cset.empty"
- by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
+ by (simp add: Cset.set_eq_iff fun_eq_iff )
lemma member_of_pred [simp]:
"member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
@@ -360,7 +360,7 @@
Predicate.Empty \<Rightarrow> Cset.empty
| Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
| Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
- by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric])
+ by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff eval_member [symmetric] member_def [symmetric])
lemma of_seq_code [code]:
"of_seq Predicate.Empty = Cset.empty"
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Mar 12 21:41:11 2012 +0100
@@ -41,7 +41,7 @@
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \<and> \<not> B x)"
- by (simp add: fun_eq_iff minus_apply)
+ by (simp add: fun_eq_iff)
lemma subset_eq[code_pred_inline]:
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
@@ -232,4 +232,4 @@
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
unfolding less_nat[symmetric] by auto
-end
\ No newline at end of file
+end
--- a/src/HOL/List.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/List.thy Mon Mar 12 21:41:11 2012 +0100
@@ -4533,7 +4533,7 @@
"listsp A (x # xs)"
lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
-by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
+by (rule predicate1I, erule listsp.induct, blast+)
lemmas lists_mono = listsp_mono [to_set]
--- a/src/HOL/Orderings.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Orderings.thy Mon Mar 12 21:41:11 2012 +0100
@@ -1304,7 +1304,7 @@
by (simp add: bot_fun_def)
instance proof
-qed (simp add: le_fun_def bot_apply)
+qed (simp add: le_fun_def)
end
@@ -1320,7 +1320,7 @@
by (simp add: top_fun_def)
instance proof
-qed (simp add: le_fun_def top_apply)
+qed (simp add: le_fun_def)
end
--- a/src/HOL/Predicate.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Predicate.thy Mon Mar 12 21:41:11 2012 +0100
@@ -123,7 +123,7 @@
by (simp add: minus_pred_def)
instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
+qed (auto intro!: pred_eqI)
end
@@ -143,7 +143,7 @@
lemma bind_bind:
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
- by (rule pred_eqI) (auto simp add: SUP_apply)
+ by (rule pred_eqI) auto
lemma bind_single:
"P \<guillemotright>= single = P"
@@ -163,7 +163,7 @@
lemma Sup_bind:
"(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
- by (rule pred_eqI) (auto simp add: SUP_apply)
+ by (rule pred_eqI) auto
lemma pred_iffI:
assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
--- a/src/HOL/Probability/Borel_Space.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Mon Mar 12 21:41:11 2012 +0100
@@ -1417,7 +1417,7 @@
proof
fix a
have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_SUP_iff SUP_apply)
+ by (auto simp: less_SUP_iff)
then show "?sup -` {a<..} \<inter> space M \<in> sets M"
using assms by auto
qed
@@ -1430,7 +1430,7 @@
proof
fix a
have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
- by (auto simp: INF_less_iff INF_apply)
+ by (auto simp: INF_less_iff)
then show "?inf -` {..<a} \<inter> space M \<in> sets M"
using assms by auto
qed
--- a/src/HOL/Probability/Lebesgue_Integration.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon Mar 12 21:41:11 2012 +0100
@@ -1044,7 +1044,7 @@
with `a < 1` u_range[OF `x \<in> space M`]
have "a * u x < 1 * u x"
by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
- also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUP_apply)
+ also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def)
finally obtain i where "a * u x < f i x" unfolding SUP_def
by (auto simp add: less_Sup_iff)
hence "a * u x \<le> f i x" by auto
@@ -1115,7 +1115,7 @@
using f by (auto intro!: SUP_upper2)
ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
by (intro positive_integral_SUP_approx[OF f g _ g'])
- (auto simp: le_fun_def max_def SUP_apply)
+ (auto simp: le_fun_def max_def)
qed
qed
--- a/src/HOL/Relation.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Relation.thy Mon Mar 12 21:41:11 2012 +0100
@@ -96,40 +96,40 @@
by (simp add: sup_fun_def)
lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
- by (simp add: fun_eq_iff Inf_apply)
+ by (simp add: fun_eq_iff)
lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
- by (simp add: fun_eq_iff INF_apply)
+ by (simp add: fun_eq_iff)
lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
- by (simp add: fun_eq_iff Inf_apply INF_apply)
+ by (simp add: fun_eq_iff)
lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
- by (simp add: fun_eq_iff INF_apply)
+ by (simp add: fun_eq_iff)
lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
- by (simp add: fun_eq_iff Sup_apply)
+ by (simp add: fun_eq_iff)
lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
- by (simp add: fun_eq_iff SUP_apply)
+ by (simp add: fun_eq_iff)
lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
- by (simp add: fun_eq_iff Sup_apply SUP_apply)
+ by (simp add: fun_eq_iff)
lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
- by (simp add: fun_eq_iff SUP_apply)
+ by (simp add: fun_eq_iff)
lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
- by (simp add: INF_apply fun_eq_iff)
+ by (simp add: fun_eq_iff)
lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
- by (simp add: INF_apply fun_eq_iff)
+ by (simp add: fun_eq_iff)
lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
- by (simp add: SUP_apply fun_eq_iff)
+ by (simp add: fun_eq_iff)
lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
- by (simp add: SUP_apply fun_eq_iff)
+ by (simp add: fun_eq_iff)
@@ -818,7 +818,7 @@
by blast
lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
- by (auto simp add: Field_def Domain_insert Range_insert)
+ by (auto simp add: Field_def)
lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)"
by blast
@@ -884,10 +884,10 @@
by auto
lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
- by (induct set: finite) (auto simp add: Domain_insert)
+ by (induct set: finite) auto
lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
- by (induct set: finite) (auto simp add: Range_insert)
+ by (induct set: finite) auto
lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
by (simp add: Field_def finite_Domain finite_Range)