# HG changeset patch
# User haftmann
# Date 1330025615 -3600
# Node ID 2c5c003cee35fd6165caf5653e295d3f261333a6
# Parent  3abc964cdc4589f0ae5442d5da13373d450e000c
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax

diff -r 3abc964cdc45 -r 2c5c003cee35 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Feb 23 20:15:59 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Feb 23 20:33:35 2012 +0100
@@ -536,7 +536,7 @@
 end
 
 
-subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
+subsection {* Complete lattice on @{typ bool} *}
 
 instantiation bool :: complete_lattice
 begin
@@ -573,6 +573,9 @@
 instance bool :: complete_boolean_algebra proof
 qed (auto intro: bool_induct)
 
+
+subsection {* Complete lattice on @{typ "_ \<Rightarrow> _"} *}
+
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
 
@@ -608,6 +611,54 @@
 
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
+
+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)
+
+lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
+  by (simp add: INF_apply)
+
+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)
+
+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)
+
+lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
+  by (auto simp add: INF_apply)
+
+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)
+
+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)
+
+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)
+
+lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
+  by (simp add: SUP_apply)
+
+lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
+  by (simp add: SUP_apply)
+
+lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
+  by (auto simp add: SUP_apply)
+
+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)
+
+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)
+
+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)
+
+
+subsection {* Complete lattice on @{typ "_ set"} *}
+
 instantiation "set" :: (type) complete_lattice
 begin
 
@@ -627,7 +678,7 @@
 qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
   
 
-subsection {* Inter *}
+subsubsection {* Inter *}
 
 abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
   "Inter S \<equiv> \<Sqinter>S"
@@ -699,7 +750,7 @@
   by (fact Inf_superset_mono)
 
 
-subsection {* Intersections of families *}
+subsubsection {* Intersections of families *}
 
 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "INTER \<equiv> INFI"
@@ -810,7 +861,7 @@
   by blast
 
 
-subsection {* Union *}
+subsubsection {* Union *}
 
 abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   "Union S \<equiv> \<Squnion>S"
@@ -879,7 +930,7 @@
   by (fact Sup_subset_mono)
 
 
-subsection {* Unions of families *}
+subsubsection {* Unions of families *}
 
 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   "UNION \<equiv> SUPR"
@@ -1042,7 +1093,7 @@
   by blast
 
 
-subsection {* Distributive laws *}
+subsubsection {* Distributive laws *}
 
 lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   by (fact inf_Sup)
@@ -1084,7 +1135,7 @@
   by (fact Sup_inf_eq_bot_iff)
 
 
-subsection {* Complement *}
+subsubsection {* Complement *}
 
 lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   by (fact uminus_INF)
@@ -1093,7 +1144,7 @@
   by (fact uminus_SUP)
 
 
-subsection {* Miniscoping and maxiscoping *}
+subsubsection {* Miniscoping and maxiscoping *}
 
 text {* \medskip Miniscoping: pushing in quantifiers and big Unions
            and Intersections. *}
diff -r 3abc964cdc45 -r 2c5c003cee35 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Feb 23 20:15:59 2012 +0100
+++ b/src/HOL/Lattices.thy	Thu Feb 23 20:33:35 2012 +0100
@@ -606,7 +606,7 @@
   min_max.sup.left_commute
 
 
-subsection {* Bool as lattice *}
+subsection {* Lattice on @{typ bool} *}
 
 instantiation bool :: boolean_algebra
 begin
@@ -641,7 +641,7 @@
   by auto
 
 
-subsection {* Fun as lattice *}
+subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
 
 instantiation "fun" :: (type, lattice) lattice
 begin
@@ -701,6 +701,63 @@
 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)+
 
+
+subsection {* Lattice on unary and binary predicates *}
+
+lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
+  by (simp add: inf_fun_def)
+
+lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
+  by (simp add: inf_fun_def)
+
+lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: inf_fun_def)
+
+lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: inf_fun_def)
+
+lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
+  by (simp add: inf_fun_def)
+
+lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
+  by (simp add: inf_fun_def)
+
+lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
+  by (simp add: inf_fun_def)
+
+lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
+  by (simp add: inf_fun_def)
+
+lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
+  by (simp add: sup_fun_def)
+
+lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+  by (simp add: sup_fun_def)
+
+lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
+  by (simp add: sup_fun_def)
+
+lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+  by (simp add: sup_fun_def)
+
+lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: sup_fun_def) iprover
+
+lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: sup_fun_def) iprover
+
+text {*
+  \medskip Classical introduction rule: no commitment to @{text A} vs
+  @{text B}.
+*}
+
+lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
+  by (auto simp add: sup_fun_def)
+
+lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
+  by (auto simp add: sup_fun_def)
+
+
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
@@ -710,3 +767,4 @@
   bot ("\<bottom>")
 
 end
+
diff -r 3abc964cdc45 -r 2c5c003cee35 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Feb 23 20:15:59 2012 +0100
+++ b/src/HOL/Orderings.thy	Thu Feb 23 20:33:35 2012 +0100
@@ -1111,10 +1111,6 @@
 
 end
 
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>")
-
 
 subsection {* Dense orders *}
 
@@ -1227,7 +1223,7 @@
 end
 
 
-subsection {* Order on bool *}
+subsection {* Order on @{typ bool} *}
 
 instantiation bool :: "{bot, top, linorder}"
 begin
@@ -1239,10 +1235,10 @@
   [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
 
 definition
-  [simp]: "bot \<longleftrightarrow> False"
+  [simp]: "\<bottom> \<longleftrightarrow> False"
 
 definition
-  [simp]: "top \<longleftrightarrow> True"
+  [simp]: "\<top> \<longleftrightarrow> True"
 
 instance proof
 qed auto
@@ -1261,10 +1257,10 @@
 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   by simp
 
-lemma bot_boolE: "bot \<Longrightarrow> P"
+lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
   by simp
 
-lemma top_boolI: top
+lemma top_boolI: \<top>
   by simp
 
 lemma [code]:
@@ -1275,7 +1271,7 @@
   by simp_all
 
 
-subsection {* Order on functions *}
+subsection {* Order on @{typ "_ \<Rightarrow> _"} *}
 
 instantiation "fun" :: (type, ord) ord
 begin
@@ -1301,10 +1297,10 @@
 begin
 
 definition
-  "bot = (\<lambda>x. bot)"
+  "\<bottom> = (\<lambda>x. \<bottom>)"
 
 lemma bot_apply:
-  "bot x = bot"
+  "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
 instance proof
@@ -1316,11 +1312,11 @@
 begin
 
 definition
-  [no_atp]: "top = (\<lambda>x. top)"
+  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 declare top_fun_def_raw [no_atp]
 
 lemma top_apply:
-  "top x = top"
+  "\<top> x = \<top>"
   by (simp add: top_fun_def)
 
 instance proof
@@ -1338,6 +1334,61 @@
   unfolding le_fun_def by simp
 
 
+subsection {* Order on unary and binary predicates *}
+
+lemma predicate1I:
+  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+  shows "P \<le> Q"
+  apply (rule le_funI)
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate1D:
+  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+  apply (erule le_funE)
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate1D:
+  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
+  by (rule predicate1D)
+
+lemma predicate2I:
+  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+  shows "P \<le> Q"
+  apply (rule le_funI)+
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate2D:
+  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  apply (erule le_funE)+
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate2D:
+  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
+  by (rule predicate2D)
+
+lemma bot1E [no_atp]: "\<bottom> x \<Longrightarrow> P"
+  by (simp add: bot_fun_def)
+
+lemma bot2E: "\<bottom> x y \<Longrightarrow> P"
+  by (simp add: bot_fun_def)
+
+lemma top1I: "\<top> x"
+  by (simp add: top_fun_def)
+
+lemma top2I: "\<top> x y"
+  by (simp add: top_fun_def)
+
+
 subsection {* Name duplicates *}
 
 lemmas order_eq_refl = preorder_class.eq_refl
@@ -1375,4 +1426,8 @@
 lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
 lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
+no_notation
+  top ("\<top>") and
+  bot ("\<bottom>")
+
 end
diff -r 3abc964cdc45 -r 2c5c003cee35 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Feb 23 20:15:59 2012 +0100
+++ b/src/HOL/Predicate.thy	Thu Feb 23 20:33:35 2012 +0100
@@ -23,53 +23,40 @@
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 
-subsection {* Predicates as (complete) lattices *}
-
-text {*
-  Handy introduction and elimination rules for @{text "\<le>"}
-  on unary and binary predicates
-*}
-
-lemma predicate1I:
-  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "P \<le> Q"
-  apply (rule le_funI)
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate1D [Pure.dest?, dest?]:
-  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
-  apply (erule le_funE)
-  apply (erule le_boolE)
-  apply assumption+
-  done
+subsection {* Classical rules for reasoning on predicates *}
 
-lemma rev_predicate1D:
-  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
-  by (rule predicate1D)
+declare predicate1D [Pure.dest?, dest?]
+declare predicate2I [Pure.intro!, intro!]
+declare predicate2D [Pure.dest, dest]
+declare bot1E [elim!]
+declare bot2E [elim!]
+declare top1I [intro!]
+declare top2I [intro!]
+declare inf1I [intro!]
+declare inf2I [intro!]
+declare inf1E [elim!]
+declare inf2E [elim!]
+declare sup1I1 [intro?]
+declare sup2I1 [intro?]
+declare sup1I2 [intro?]
+declare sup2I2 [intro?]
+declare sup1E [elim!]
+declare sup2E [elim!]
+declare sup1CI [intro!]
+declare sup2CI [intro!]
+declare INF1_I [intro!]
+declare INF2_I [intro!]
+declare INF1_D [elim]
+declare INF2_D [elim]
+declare INF1_E [elim]
+declare INF2_E [elim]
+declare SUP1_I [intro]
+declare SUP2_I [intro]
+declare SUP1_E [elim!]
+declare SUP2_E [elim!]
 
-lemma predicate2I [Pure.intro!, intro!]:
-  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
-  shows "P \<le> Q"
-  apply (rule le_funI)+
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
 
-lemma predicate2D [Pure.dest, dest]:
-  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
-  apply (erule le_funE)+
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma rev_predicate2D:
-  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
-  by (rule predicate2D)
-
+subsection {* Conversion between set and predicate relations *}
 
 subsubsection {* Equality *}
 
@@ -91,51 +78,15 @@
 
 subsubsection {* Top and bottom elements *}
 
-lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
-  by (simp add: bot_fun_def)
-
-lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
-  by (simp add: bot_fun_def)
-
 lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
 
 lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma top1I [intro!]: "\<top> x"
-  by (simp add: top_fun_def)
-
-lemma top2I [intro!]: "\<top> x y"
-  by (simp add: top_fun_def)
-
 
 subsubsection {* Binary intersection *}
 
-lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
-  by (simp add: inf_fun_def)
-
-lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
-  by (simp add: inf_fun_def)
-
-lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
-  by (simp add: inf_fun_def)
-
-lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
-  by (simp add: inf_fun_def)
-
-lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
-  by (simp add: inf_fun_def)
-
-lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
-  by (simp add: inf_fun_def)
-
-lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
-  by (simp add: inf_fun_def)
-
-lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
-  by (simp add: inf_fun_def)
-
 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf_fun_def)
 
@@ -145,35 +96,6 @@
 
 subsubsection {* Binary union *}
 
-lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
-  by (simp add: sup_fun_def)
-
-lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
-  by (simp add: sup_fun_def)
-
-lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
-  by (simp add: sup_fun_def)
-
-lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
-  by (simp add: sup_fun_def)
-
-lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
-  by (simp add: sup_fun_def) iprover
-
-lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
-  by (simp add: sup_fun_def) iprover
-
-text {*
-  \medskip Classical introduction rule: no commitment to @{text A} vs
-  @{text B}.
-*}
-
-lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
-  by (auto simp add: sup_fun_def)
-
-lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
-  by (auto simp add: sup_fun_def)
-
 lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   by (simp add: sup_fun_def)
 
@@ -183,57 +105,15 @@
 
 subsubsection {* Intersections of families *}
 
-lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
-  by (simp add: INF_apply)
-
-lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-  by (simp add: INF_apply)
-
-lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
-  by (auto simp add: INF_apply)
-
-lemma INF2_I [intro!]: "(\<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)
-
-lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
-  by (auto simp add: INF_apply)
-
-lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
-  by (auto simp add: INF_apply)
-
-lemma INF1_E [elim]: "(\<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)
-
-lemma INF2_E [elim]: "(\<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)
-
-lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
+lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   by (simp add: INF_apply fun_eq_iff)
 
-lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
+lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   by (simp add: INF_apply fun_eq_iff)
 
 
 subsubsection {* Unions of families *}
 
-lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-  by (simp add: SUP_apply)
-
-lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-  by (simp add: SUP_apply)
-
-lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
-  by (auto simp add: SUP_apply)
-
-lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
-  by (auto simp add: SUP_apply)
-
-lemma SUP1_E [elim!]: "(\<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)
-
-lemma SUP2_E [elim!]: "(\<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)
-
 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)