moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
authorhaftmann
Thu Feb 23 20:33:35 2012 +0100 (2012-02-23)
changeset 466312c5c003cee35
parent 46630 3abc964cdc45
child 46632 5949ad86dc9a
child 46634 c6d2fc7095ac
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Thu Feb 23 20:15:59 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Thu Feb 23 20:33:35 2012 +0100
     1.3 @@ -536,7 +536,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
     1.8 +subsection {* Complete lattice on @{typ bool} *}
     1.9  
    1.10  instantiation bool :: complete_lattice
    1.11  begin
    1.12 @@ -573,6 +573,9 @@
    1.13  instance bool :: complete_boolean_algebra proof
    1.14  qed (auto intro: bool_induct)
    1.15  
    1.16 +
    1.17 +subsection {* Complete lattice on @{typ "_ \<Rightarrow> _"} *}
    1.18 +
    1.19  instantiation "fun" :: (type, complete_lattice) complete_lattice
    1.20  begin
    1.21  
    1.22 @@ -608,6 +611,54 @@
    1.23  
    1.24  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
    1.25  
    1.26 +
    1.27 +subsection {* Complete lattice on unary and binary predicates *}
    1.28 +
    1.29 +lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
    1.30 +  by (simp add: INF_apply)
    1.31 +
    1.32 +lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
    1.33 +  by (simp add: INF_apply)
    1.34 +
    1.35 +lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
    1.36 +  by (auto simp add: INF_apply)
    1.37 +
    1.38 +lemma INF2_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
    1.39 +  by (auto simp add: INF_apply)
    1.40 +
    1.41 +lemma INF1_D: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
    1.42 +  by (auto simp add: INF_apply)
    1.43 +
    1.44 +lemma INF2_D: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
    1.45 +  by (auto simp add: INF_apply)
    1.46 +
    1.47 +lemma INF1_E: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
    1.48 +  by (auto simp add: INF_apply)
    1.49 +
    1.50 +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"
    1.51 +  by (auto simp add: INF_apply)
    1.52 +
    1.53 +lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
    1.54 +  by (simp add: SUP_apply)
    1.55 +
    1.56 +lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
    1.57 +  by (simp add: SUP_apply)
    1.58 +
    1.59 +lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
    1.60 +  by (auto simp add: SUP_apply)
    1.61 +
    1.62 +lemma SUP2_I: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
    1.63 +  by (auto simp add: SUP_apply)
    1.64 +
    1.65 +lemma SUP1_E: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
    1.66 +  by (auto simp add: SUP_apply)
    1.67 +
    1.68 +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"
    1.69 +  by (auto simp add: SUP_apply)
    1.70 +
    1.71 +
    1.72 +subsection {* Complete lattice on @{typ "_ set"} *}
    1.73 +
    1.74  instantiation "set" :: (type) complete_lattice
    1.75  begin
    1.76  
    1.77 @@ -627,7 +678,7 @@
    1.78  qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
    1.79    
    1.80  
    1.81 -subsection {* Inter *}
    1.82 +subsubsection {* Inter *}
    1.83  
    1.84  abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
    1.85    "Inter S \<equiv> \<Sqinter>S"
    1.86 @@ -699,7 +750,7 @@
    1.87    by (fact Inf_superset_mono)
    1.88  
    1.89  
    1.90 -subsection {* Intersections of families *}
    1.91 +subsubsection {* Intersections of families *}
    1.92  
    1.93  abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    1.94    "INTER \<equiv> INFI"
    1.95 @@ -810,7 +861,7 @@
    1.96    by blast
    1.97  
    1.98  
    1.99 -subsection {* Union *}
   1.100 +subsubsection {* Union *}
   1.101  
   1.102  abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   1.103    "Union S \<equiv> \<Squnion>S"
   1.104 @@ -879,7 +930,7 @@
   1.105    by (fact Sup_subset_mono)
   1.106  
   1.107  
   1.108 -subsection {* Unions of families *}
   1.109 +subsubsection {* Unions of families *}
   1.110  
   1.111  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   1.112    "UNION \<equiv> SUPR"
   1.113 @@ -1042,7 +1093,7 @@
   1.114    by blast
   1.115  
   1.116  
   1.117 -subsection {* Distributive laws *}
   1.118 +subsubsection {* Distributive laws *}
   1.119  
   1.120  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   1.121    by (fact inf_Sup)
   1.122 @@ -1084,7 +1135,7 @@
   1.123    by (fact Sup_inf_eq_bot_iff)
   1.124  
   1.125  
   1.126 -subsection {* Complement *}
   1.127 +subsubsection {* Complement *}
   1.128  
   1.129  lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   1.130    by (fact uminus_INF)
   1.131 @@ -1093,7 +1144,7 @@
   1.132    by (fact uminus_SUP)
   1.133  
   1.134  
   1.135 -subsection {* Miniscoping and maxiscoping *}
   1.136 +subsubsection {* Miniscoping and maxiscoping *}
   1.137  
   1.138  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
   1.139             and Intersections. *}
     2.1 --- a/src/HOL/Lattices.thy	Thu Feb 23 20:15:59 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Thu Feb 23 20:33:35 2012 +0100
     2.3 @@ -606,7 +606,7 @@
     2.4    min_max.sup.left_commute
     2.5  
     2.6  
     2.7 -subsection {* Bool as lattice *}
     2.8 +subsection {* Lattice on @{typ bool} *}
     2.9  
    2.10  instantiation bool :: boolean_algebra
    2.11  begin
    2.12 @@ -641,7 +641,7 @@
    2.13    by auto
    2.14  
    2.15  
    2.16 -subsection {* Fun as lattice *}
    2.17 +subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
    2.18  
    2.19  instantiation "fun" :: (type, lattice) lattice
    2.20  begin
    2.21 @@ -701,6 +701,63 @@
    2.22  instance "fun" :: (type, boolean_algebra) boolean_algebra proof
    2.23  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)+
    2.24  
    2.25 +
    2.26 +subsection {* Lattice on unary and binary predicates *}
    2.27 +
    2.28 +lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    2.29 +  by (simp add: inf_fun_def)
    2.30 +
    2.31 +lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    2.32 +  by (simp add: inf_fun_def)
    2.33 +
    2.34 +lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    2.35 +  by (simp add: inf_fun_def)
    2.36 +
    2.37 +lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    2.38 +  by (simp add: inf_fun_def)
    2.39 +
    2.40 +lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    2.41 +  by (simp add: inf_fun_def)
    2.42 +
    2.43 +lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    2.44 +  by (simp add: inf_fun_def)
    2.45 +
    2.46 +lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    2.47 +  by (simp add: inf_fun_def)
    2.48 +
    2.49 +lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    2.50 +  by (simp add: inf_fun_def)
    2.51 +
    2.52 +lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
    2.53 +  by (simp add: sup_fun_def)
    2.54 +
    2.55 +lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    2.56 +  by (simp add: sup_fun_def)
    2.57 +
    2.58 +lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
    2.59 +  by (simp add: sup_fun_def)
    2.60 +
    2.61 +lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    2.62 +  by (simp add: sup_fun_def)
    2.63 +
    2.64 +lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
    2.65 +  by (simp add: sup_fun_def) iprover
    2.66 +
    2.67 +lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
    2.68 +  by (simp add: sup_fun_def) iprover
    2.69 +
    2.70 +text {*
    2.71 +  \medskip Classical introduction rule: no commitment to @{text A} vs
    2.72 +  @{text B}.
    2.73 +*}
    2.74 +
    2.75 +lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
    2.76 +  by (auto simp add: sup_fun_def)
    2.77 +
    2.78 +lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
    2.79 +  by (auto simp add: sup_fun_def)
    2.80 +
    2.81 +
    2.82  no_notation
    2.83    less_eq  (infix "\<sqsubseteq>" 50) and
    2.84    less (infix "\<sqsubset>" 50) and
    2.85 @@ -710,3 +767,4 @@
    2.86    bot ("\<bottom>")
    2.87  
    2.88  end
    2.89 +
     3.1 --- a/src/HOL/Orderings.thy	Thu Feb 23 20:15:59 2012 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Thu Feb 23 20:33:35 2012 +0100
     3.3 @@ -1111,10 +1111,6 @@
     3.4  
     3.5  end
     3.6  
     3.7 -no_notation
     3.8 -  bot ("\<bottom>") and
     3.9 -  top ("\<top>")
    3.10 -
    3.11  
    3.12  subsection {* Dense orders *}
    3.13  
    3.14 @@ -1227,7 +1223,7 @@
    3.15  end
    3.16  
    3.17  
    3.18 -subsection {* Order on bool *}
    3.19 +subsection {* Order on @{typ bool} *}
    3.20  
    3.21  instantiation bool :: "{bot, top, linorder}"
    3.22  begin
    3.23 @@ -1239,10 +1235,10 @@
    3.24    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    3.25  
    3.26  definition
    3.27 -  [simp]: "bot \<longleftrightarrow> False"
    3.28 +  [simp]: "\<bottom> \<longleftrightarrow> False"
    3.29  
    3.30  definition
    3.31 -  [simp]: "top \<longleftrightarrow> True"
    3.32 +  [simp]: "\<top> \<longleftrightarrow> True"
    3.33  
    3.34  instance proof
    3.35  qed auto
    3.36 @@ -1261,10 +1257,10 @@
    3.37  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    3.38    by simp
    3.39  
    3.40 -lemma bot_boolE: "bot \<Longrightarrow> P"
    3.41 +lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
    3.42    by simp
    3.43  
    3.44 -lemma top_boolI: top
    3.45 +lemma top_boolI: \<top>
    3.46    by simp
    3.47  
    3.48  lemma [code]:
    3.49 @@ -1275,7 +1271,7 @@
    3.50    by simp_all
    3.51  
    3.52  
    3.53 -subsection {* Order on functions *}
    3.54 +subsection {* Order on @{typ "_ \<Rightarrow> _"} *}
    3.55  
    3.56  instantiation "fun" :: (type, ord) ord
    3.57  begin
    3.58 @@ -1301,10 +1297,10 @@
    3.59  begin
    3.60  
    3.61  definition
    3.62 -  "bot = (\<lambda>x. bot)"
    3.63 +  "\<bottom> = (\<lambda>x. \<bottom>)"
    3.64  
    3.65  lemma bot_apply:
    3.66 -  "bot x = bot"
    3.67 +  "\<bottom> x = \<bottom>"
    3.68    by (simp add: bot_fun_def)
    3.69  
    3.70  instance proof
    3.71 @@ -1316,11 +1312,11 @@
    3.72  begin
    3.73  
    3.74  definition
    3.75 -  [no_atp]: "top = (\<lambda>x. top)"
    3.76 +  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    3.77  declare top_fun_def_raw [no_atp]
    3.78  
    3.79  lemma top_apply:
    3.80 -  "top x = top"
    3.81 +  "\<top> x = \<top>"
    3.82    by (simp add: top_fun_def)
    3.83  
    3.84  instance proof
    3.85 @@ -1338,6 +1334,61 @@
    3.86    unfolding le_fun_def by simp
    3.87  
    3.88  
    3.89 +subsection {* Order on unary and binary predicates *}
    3.90 +
    3.91 +lemma predicate1I:
    3.92 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    3.93 +  shows "P \<le> Q"
    3.94 +  apply (rule le_funI)
    3.95 +  apply (rule le_boolI)
    3.96 +  apply (rule PQ)
    3.97 +  apply assumption
    3.98 +  done
    3.99 +
   3.100 +lemma predicate1D:
   3.101 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   3.102 +  apply (erule le_funE)
   3.103 +  apply (erule le_boolE)
   3.104 +  apply assumption+
   3.105 +  done
   3.106 +
   3.107 +lemma rev_predicate1D:
   3.108 +  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
   3.109 +  by (rule predicate1D)
   3.110 +
   3.111 +lemma predicate2I:
   3.112 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   3.113 +  shows "P \<le> Q"
   3.114 +  apply (rule le_funI)+
   3.115 +  apply (rule le_boolI)
   3.116 +  apply (rule PQ)
   3.117 +  apply assumption
   3.118 +  done
   3.119 +
   3.120 +lemma predicate2D:
   3.121 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   3.122 +  apply (erule le_funE)+
   3.123 +  apply (erule le_boolE)
   3.124 +  apply assumption+
   3.125 +  done
   3.126 +
   3.127 +lemma rev_predicate2D:
   3.128 +  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   3.129 +  by (rule predicate2D)
   3.130 +
   3.131 +lemma bot1E [no_atp]: "\<bottom> x \<Longrightarrow> P"
   3.132 +  by (simp add: bot_fun_def)
   3.133 +
   3.134 +lemma bot2E: "\<bottom> x y \<Longrightarrow> P"
   3.135 +  by (simp add: bot_fun_def)
   3.136 +
   3.137 +lemma top1I: "\<top> x"
   3.138 +  by (simp add: top_fun_def)
   3.139 +
   3.140 +lemma top2I: "\<top> x y"
   3.141 +  by (simp add: top_fun_def)
   3.142 +
   3.143 +
   3.144  subsection {* Name duplicates *}
   3.145  
   3.146  lemmas order_eq_refl = preorder_class.eq_refl
   3.147 @@ -1375,4 +1426,8 @@
   3.148  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   3.149  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   3.150  
   3.151 +no_notation
   3.152 +  top ("\<top>") and
   3.153 +  bot ("\<bottom>")
   3.154 +
   3.155  end
     4.1 --- a/src/HOL/Predicate.thy	Thu Feb 23 20:15:59 2012 +0100
     4.2 +++ b/src/HOL/Predicate.thy	Thu Feb 23 20:33:35 2012 +0100
     4.3 @@ -23,53 +23,40 @@
     4.4    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
     4.5  
     4.6  
     4.7 -subsection {* Predicates as (complete) lattices *}
     4.8 -
     4.9 -text {*
    4.10 -  Handy introduction and elimination rules for @{text "\<le>"}
    4.11 -  on unary and binary predicates
    4.12 -*}
    4.13 -
    4.14 -lemma predicate1I:
    4.15 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    4.16 -  shows "P \<le> Q"
    4.17 -  apply (rule le_funI)
    4.18 -  apply (rule le_boolI)
    4.19 -  apply (rule PQ)
    4.20 -  apply assumption
    4.21 -  done
    4.22 -
    4.23 -lemma predicate1D [Pure.dest?, dest?]:
    4.24 -  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    4.25 -  apply (erule le_funE)
    4.26 -  apply (erule le_boolE)
    4.27 -  apply assumption+
    4.28 -  done
    4.29 +subsection {* Classical rules for reasoning on predicates *}
    4.30  
    4.31 -lemma rev_predicate1D:
    4.32 -  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    4.33 -  by (rule predicate1D)
    4.34 +declare predicate1D [Pure.dest?, dest?]
    4.35 +declare predicate2I [Pure.intro!, intro!]
    4.36 +declare predicate2D [Pure.dest, dest]
    4.37 +declare bot1E [elim!]
    4.38 +declare bot2E [elim!]
    4.39 +declare top1I [intro!]
    4.40 +declare top2I [intro!]
    4.41 +declare inf1I [intro!]
    4.42 +declare inf2I [intro!]
    4.43 +declare inf1E [elim!]
    4.44 +declare inf2E [elim!]
    4.45 +declare sup1I1 [intro?]
    4.46 +declare sup2I1 [intro?]
    4.47 +declare sup1I2 [intro?]
    4.48 +declare sup2I2 [intro?]
    4.49 +declare sup1E [elim!]
    4.50 +declare sup2E [elim!]
    4.51 +declare sup1CI [intro!]
    4.52 +declare sup2CI [intro!]
    4.53 +declare INF1_I [intro!]
    4.54 +declare INF2_I [intro!]
    4.55 +declare INF1_D [elim]
    4.56 +declare INF2_D [elim]
    4.57 +declare INF1_E [elim]
    4.58 +declare INF2_E [elim]
    4.59 +declare SUP1_I [intro]
    4.60 +declare SUP2_I [intro]
    4.61 +declare SUP1_E [elim!]
    4.62 +declare SUP2_E [elim!]
    4.63  
    4.64 -lemma predicate2I [Pure.intro!, intro!]:
    4.65 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    4.66 -  shows "P \<le> Q"
    4.67 -  apply (rule le_funI)+
    4.68 -  apply (rule le_boolI)
    4.69 -  apply (rule PQ)
    4.70 -  apply assumption
    4.71 -  done
    4.72  
    4.73 -lemma predicate2D [Pure.dest, dest]:
    4.74 -  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    4.75 -  apply (erule le_funE)+
    4.76 -  apply (erule le_boolE)
    4.77 -  apply assumption+
    4.78 -  done
    4.79 -
    4.80 -lemma rev_predicate2D:
    4.81 -  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
    4.82 -  by (rule predicate2D)
    4.83 -
    4.84 +subsection {* Conversion between set and predicate relations *}
    4.85  
    4.86  subsubsection {* Equality *}
    4.87  
    4.88 @@ -91,51 +78,15 @@
    4.89  
    4.90  subsubsection {* Top and bottom elements *}
    4.91  
    4.92 -lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
    4.93 -  by (simp add: bot_fun_def)
    4.94 -
    4.95 -lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
    4.96 -  by (simp add: bot_fun_def)
    4.97 -
    4.98  lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    4.99    by (auto simp add: fun_eq_iff)
   4.100  
   4.101  lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   4.102    by (auto simp add: fun_eq_iff)
   4.103  
   4.104 -lemma top1I [intro!]: "\<top> x"
   4.105 -  by (simp add: top_fun_def)
   4.106 -
   4.107 -lemma top2I [intro!]: "\<top> x y"
   4.108 -  by (simp add: top_fun_def)
   4.109 -
   4.110  
   4.111  subsubsection {* Binary intersection *}
   4.112  
   4.113 -lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   4.114 -  by (simp add: inf_fun_def)
   4.115 -
   4.116 -lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
   4.117 -  by (simp add: inf_fun_def)
   4.118 -
   4.119 -lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
   4.120 -  by (simp add: inf_fun_def)
   4.121 -
   4.122 -lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
   4.123 -  by (simp add: inf_fun_def)
   4.124 -
   4.125 -lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
   4.126 -  by (simp add: inf_fun_def)
   4.127 -
   4.128 -lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
   4.129 -  by (simp add: inf_fun_def)
   4.130 -
   4.131 -lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   4.132 -  by (simp add: inf_fun_def)
   4.133 -
   4.134 -lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   4.135 -  by (simp add: inf_fun_def)
   4.136 -
   4.137  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)"
   4.138    by (simp add: inf_fun_def)
   4.139  
   4.140 @@ -145,35 +96,6 @@
   4.141  
   4.142  subsubsection {* Binary union *}
   4.143  
   4.144 -lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   4.145 -  by (simp add: sup_fun_def)
   4.146 -
   4.147 -lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   4.148 -  by (simp add: sup_fun_def)
   4.149 -
   4.150 -lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   4.151 -  by (simp add: sup_fun_def)
   4.152 -
   4.153 -lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   4.154 -  by (simp add: sup_fun_def)
   4.155 -
   4.156 -lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   4.157 -  by (simp add: sup_fun_def) iprover
   4.158 -
   4.159 -lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   4.160 -  by (simp add: sup_fun_def) iprover
   4.161 -
   4.162 -text {*
   4.163 -  \medskip Classical introduction rule: no commitment to @{text A} vs
   4.164 -  @{text B}.
   4.165 -*}
   4.166 -
   4.167 -lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   4.168 -  by (auto simp add: sup_fun_def)
   4.169 -
   4.170 -lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   4.171 -  by (auto simp add: sup_fun_def)
   4.172 -
   4.173  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)"
   4.174    by (simp add: sup_fun_def)
   4.175  
   4.176 @@ -183,57 +105,15 @@
   4.177  
   4.178  subsubsection {* Intersections of families *}
   4.179  
   4.180 -lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
   4.181 -  by (simp add: INF_apply)
   4.182 -
   4.183 -lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   4.184 -  by (simp add: INF_apply)
   4.185 -
   4.186 -lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   4.187 -  by (auto simp add: INF_apply)
   4.188 -
   4.189 -lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   4.190 -  by (auto simp add: INF_apply)
   4.191 -
   4.192 -lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   4.193 -  by (auto simp add: INF_apply)
   4.194 -
   4.195 -lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   4.196 -  by (auto simp add: INF_apply)
   4.197 -
   4.198 -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"
   4.199 -  by (auto simp add: INF_apply)
   4.200 -
   4.201 -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"
   4.202 -  by (auto simp add: INF_apply)
   4.203 -
   4.204 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   4.205 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   4.206    by (simp add: INF_apply fun_eq_iff)
   4.207  
   4.208 -lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
   4.209 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   4.210    by (simp add: INF_apply fun_eq_iff)
   4.211  
   4.212  
   4.213  subsubsection {* Unions of families *}
   4.214  
   4.215 -lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   4.216 -  by (simp add: SUP_apply)
   4.217 -
   4.218 -lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   4.219 -  by (simp add: SUP_apply)
   4.220 -
   4.221 -lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   4.222 -  by (auto simp add: SUP_apply)
   4.223 -
   4.224 -lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   4.225 -  by (auto simp add: SUP_apply)
   4.226 -
   4.227 -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"
   4.228 -  by (auto simp add: SUP_apply)
   4.229 -
   4.230 -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"
   4.231 -  by (auto simp add: SUP_apply)
   4.232 -
   4.233  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   4.234    by (simp add: SUP_apply fun_eq_iff)
   4.235