--- a/src/HOL/Complete_Lattices.thy Tue Sep 13 16:21:48 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy Tue Sep 13 16:22:01 2011 +0200
@@ -164,13 +164,13 @@
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
- by (simp add: INF_def Inf_insert)
+ by (simp add: INF_def)
lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
- by (simp add: SUP_def Sup_insert)
+ by (simp add: SUP_def)
lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
by (simp add: INF_def image_image)
@@ -293,7 +293,7 @@
proof
assume "\<forall>x\<in>A. x = \<top>"
then have "A = {} \<or> A = {\<top>}" by auto
- then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
+ then show "\<Sqinter>A = \<top>" by auto
next
assume "\<Sqinter>A = \<top>"
show "\<forall>x\<in>A. x = \<top>"
@@ -301,7 +301,7 @@
assume "\<not> (\<forall>x\<in>A. x = \<top>)"
then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
then obtain B where "A = insert x B" by blast
- with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
+ with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by simp
qed
qed
then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
@@ -310,7 +310,7 @@
lemma INF_top_conv [simp]:
"(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
"\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
- by (auto simp add: INF_def Inf_top_conv)
+ by (auto simp add: INF_def)
lemma Sup_bot_conv [simp, no_atp]:
"\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
@@ -324,7 +324,7 @@
lemma SUP_bot_conv [simp]:
"(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
"\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
- by (auto simp add: SUP_def Sup_bot_conv)
+ by (auto simp add: SUP_def)
lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
by (auto intro: antisym INF_lower INF_greatest)
@@ -420,7 +420,7 @@
subclass distrib_lattice proof
fix a b c
from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
- then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
+ then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def)
qed
lemma Inf_sup:
@@ -535,7 +535,7 @@
lemma SUP_eq_top_iff [simp]:
"(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
- unfolding SUP_def Sup_eq_top_iff by auto
+ unfolding SUP_def by auto
lemma Inf_eq_bot_iff [simp]:
"\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
@@ -547,7 +547,7 @@
lemma INF_eq_bot_iff [simp]:
"(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
- unfolding INF_def Inf_eq_bot_iff by auto
+ unfolding INF_def by auto
end
@@ -1152,19 +1152,19 @@
lemma (in complete_lattice) Inf_singleton [simp]:
"\<Sqinter>{a} = a"
- by (simp add: Inf_insert)
+ by simp
lemma (in complete_lattice) Sup_singleton [simp]:
"\<Squnion>{a} = a"
- by (simp add: Sup_insert)
+ by simp
lemma (in complete_lattice) Inf_binary:
"\<Sqinter>{a, b} = a \<sqinter> b"
- by (simp add: Inf_insert)
+ by simp
lemma (in complete_lattice) Sup_binary:
"\<Squnion>{a, b} = a \<squnion> b"
- by (simp add: Sup_insert)
+ by simp
lemmas (in complete_lattice) INFI_def = INF_def
lemmas (in complete_lattice) SUPR_def = SUP_def
@@ -1202,7 +1202,7 @@
by (fact SUP_def)
lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by (simp add: Inf_insert)
+ by simp
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
--- a/src/HOL/Finite_Set.thy Tue Sep 13 16:21:48 2011 +0200
+++ b/src/HOL/Finite_Set.thy Tue Sep 13 16:22:01 2011 +0200
@@ -754,7 +754,7 @@
proof -
interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: Inf_insert inf_commute fold_fun_comm)
+ (simp_all add: inf_commute fold_fun_comm)
qed
lemma sup_Sup_fold_sup:
@@ -763,7 +763,7 @@
proof -
interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
from `finite A` show ?thesis by (induct A arbitrary: B)
- (simp_all add: Sup_insert sup_commute fold_fun_comm)
+ (simp_all add: sup_commute fold_fun_comm)
qed
lemma Inf_fold_inf:
@@ -784,7 +784,7 @@
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?inf"
by (induct A arbitrary: B)
- (simp_all add: INFI_def Inf_insert inf_left_commute)
+ (simp_all add: INFI_def inf_left_commute)
qed
lemma sup_SUPR_fold_sup:
@@ -795,7 +795,7 @@
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?sup"
by (induct A arbitrary: B)
- (simp_all add: SUPR_def Sup_insert sup_left_commute)
+ (simp_all add: SUPR_def sup_left_commute)
qed
lemma INFI_fold_inf:
--- a/src/HOL/Lattices.thy Tue Sep 13 16:21:48 2011 +0200
+++ b/src/HOL/Lattices.thy Tue Sep 13 16:22:01 2011 +0200
@@ -271,7 +271,7 @@
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
- by(simp add:inf_sup_absorb inf_commute)
+ by(simp add: inf_commute)
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
finally show ?thesis .
qed
@@ -284,7 +284,7 @@
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
- by(simp add:sup_inf_absorb sup_commute)
+ by(simp add: sup_commute)
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
finally show ?thesis .
qed
@@ -547,7 +547,7 @@
lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
"- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
- by (auto simp add: less_le compl_le_compl_iff)
+ by (auto simp add: less_le)
lemma compl_less_swap1:
assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"