author haftmann Sat, 26 Apr 2014 13:25:46 +0200 changeset 56741 2b3710a4fa94 parent 56740 5ebaa364d8ab child 56742 678a52e676b6
subsumed by existing default simp rules for functions and booleans
```--- a/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:45 2014 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:46 2014 +0200
@@ -758,12 +758,6 @@

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
-
-lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-  by simp
-
lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
by auto

@@ -782,12 +776,6 @@
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

-lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-  by simp
-
-lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-  by simp
-
lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
by auto
```