distributed lattice properties of predicates to places of instantiation
authorhaftmann
Sun Feb 19 15:30:35 2012 +0100 (2012-02-19)
changeset 4655350a7e97fe653
parent 46552 5d33a3269029
child 46554 87d4e4958476
distributed lattice properties of predicates to places of instantiation
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	Mon Feb 20 15:17:03 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Feb 19 15:30: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 {* @{typ bool} as complete lattice *}
     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 {* @{typ "_ \<Rightarrow> _"} as complete lattice *}
    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 {* Unary and binary predicates as complete lattice *}
    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 [intro!]: "(\<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 [intro!]: "(\<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 [elim]: "(\<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 [elim]: "(\<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 [elim]: "(\<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 [elim]: "(\<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 [intro]: "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 [intro]: "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 [elim!]: "(\<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 [elim!]: "(\<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 {* @{typ "_ set"} as complete lattice *}
    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	Mon Feb 20 15:17:03 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Sun Feb 19 15:30:35 2012 +0100
     2.3 @@ -701,6 +701,63 @@
     2.4  instance "fun" :: (type, boolean_algebra) boolean_algebra proof
     2.5  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.6  
     2.7 +
     2.8 +subsection {* Unary and binary predicates as lattice *}
     2.9 +
    2.10 +lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    2.11 +  by (simp add: inf_fun_def)
    2.12 +
    2.13 +lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    2.14 +  by (simp add: inf_fun_def)
    2.15 +
    2.16 +lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    2.17 +  by (simp add: inf_fun_def)
    2.18 +
    2.19 +lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    2.20 +  by (simp add: inf_fun_def)
    2.21 +
    2.22 +lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    2.23 +  by (simp add: inf_fun_def)
    2.24 +
    2.25 +lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    2.26 +  by (simp add: inf_fun_def)
    2.27 +
    2.28 +lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    2.29 +  by (simp add: inf_fun_def)
    2.30 +
    2.31 +lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    2.32 +  by (simp add: inf_fun_def)
    2.33 +
    2.34 +lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
    2.35 +  by (simp add: sup_fun_def)
    2.36 +
    2.37 +lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    2.38 +  by (simp add: sup_fun_def)
    2.39 +
    2.40 +lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
    2.41 +  by (simp add: sup_fun_def)
    2.42 +
    2.43 +lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    2.44 +  by (simp add: sup_fun_def)
    2.45 +
    2.46 +lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
    2.47 +  by (simp add: sup_fun_def) iprover
    2.48 +
    2.49 +lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
    2.50 +  by (simp add: sup_fun_def) iprover
    2.51 +
    2.52 +text {*
    2.53 +  \medskip Classical introduction rule: no commitment to @{text A} vs
    2.54 +  @{text B}.
    2.55 +*}
    2.56 +
    2.57 +lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
    2.58 +  by (auto simp add: sup_fun_def)
    2.59 +
    2.60 +lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
    2.61 +  by (auto simp add: sup_fun_def)
    2.62 +
    2.63 +
    2.64  no_notation
    2.65    less_eq  (infix "\<sqsubseteq>" 50) and
    2.66    less (infix "\<sqsubset>" 50) and
    2.67 @@ -710,3 +767,4 @@
    2.68    bot ("\<bottom>")
    2.69  
    2.70  end
    2.71 +
     3.1 --- a/src/HOL/Orderings.thy	Mon Feb 20 15:17:03 2012 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Sun Feb 19 15:30: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 @@ -1239,10 +1235,10 @@
    3.15    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    3.16  
    3.17  definition
    3.18 -  [simp]: "bot \<longleftrightarrow> False"
    3.19 +  [simp]: "\<bottom> \<longleftrightarrow> False"
    3.20  
    3.21  definition
    3.22 -  [simp]: "top \<longleftrightarrow> True"
    3.23 +  [simp]: "\<top> \<longleftrightarrow> True"
    3.24  
    3.25  instance proof
    3.26  qed auto
    3.27 @@ -1261,10 +1257,10 @@
    3.28  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    3.29    by simp
    3.30  
    3.31 -lemma bot_boolE: "bot \<Longrightarrow> P"
    3.32 +lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
    3.33    by simp
    3.34  
    3.35 -lemma top_boolI: top
    3.36 +lemma top_boolI: \<top>
    3.37    by simp
    3.38  
    3.39  lemma [code]:
    3.40 @@ -1301,10 +1297,10 @@
    3.41  begin
    3.42  
    3.43  definition
    3.44 -  "bot = (\<lambda>x. bot)"
    3.45 +  "\<bottom> = (\<lambda>x. \<bottom>)"
    3.46  
    3.47  lemma bot_apply:
    3.48 -  "bot x = bot"
    3.49 +  "\<bottom> x = \<bottom>"
    3.50    by (simp add: bot_fun_def)
    3.51  
    3.52  instance proof
    3.53 @@ -1316,11 +1312,11 @@
    3.54  begin
    3.55  
    3.56  definition
    3.57 -  [no_atp]: "top = (\<lambda>x. top)"
    3.58 +  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    3.59  declare top_fun_def_raw [no_atp]
    3.60  
    3.61  lemma top_apply:
    3.62 -  "top x = top"
    3.63 +  "\<top> x = \<top>"
    3.64    by (simp add: top_fun_def)
    3.65  
    3.66  instance proof
    3.67 @@ -1338,6 +1334,61 @@
    3.68    unfolding le_fun_def by simp
    3.69  
    3.70  
    3.71 +subsection {* Order on unary and binary predicates *}
    3.72 +
    3.73 +lemma predicate1I:
    3.74 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    3.75 +  shows "P \<le> Q"
    3.76 +  apply (rule le_funI)
    3.77 +  apply (rule le_boolI)
    3.78 +  apply (rule PQ)
    3.79 +  apply assumption
    3.80 +  done
    3.81 +
    3.82 +lemma predicate1D [Pure.dest?, dest?]:
    3.83 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    3.84 +  apply (erule le_funE)
    3.85 +  apply (erule le_boolE)
    3.86 +  apply assumption+
    3.87 +  done
    3.88 +
    3.89 +lemma rev_predicate1D:
    3.90 +  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    3.91 +  by (rule predicate1D)
    3.92 +
    3.93 +lemma predicate2I [Pure.intro!, intro!]:
    3.94 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    3.95 +  shows "P \<le> Q"
    3.96 +  apply (rule le_funI)+
    3.97 +  apply (rule le_boolI)
    3.98 +  apply (rule PQ)
    3.99 +  apply assumption
   3.100 +  done
   3.101 +
   3.102 +lemma predicate2D [Pure.dest, dest]:
   3.103 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   3.104 +  apply (erule le_funE)+
   3.105 +  apply (erule le_boolE)
   3.106 +  apply assumption+
   3.107 +  done
   3.108 +
   3.109 +lemma rev_predicate2D:
   3.110 +  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   3.111 +  by (rule predicate2D)
   3.112 +
   3.113 +lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
   3.114 +  by (simp add: bot_fun_def)
   3.115 +
   3.116 +lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
   3.117 +  by (simp add: bot_fun_def)
   3.118 +
   3.119 +lemma top1I [intro!]: "\<top> x"
   3.120 +  by (simp add: top_fun_def)
   3.121 +
   3.122 +lemma top2I [intro!]: "\<top> x y"
   3.123 +  by (simp add: top_fun_def)
   3.124 +
   3.125 +
   3.126  subsection {* Name duplicates *}
   3.127  
   3.128  lemmas order_eq_refl = preorder_class.eq_refl
   3.129 @@ -1375,4 +1426,8 @@
   3.130  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   3.131  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   3.132  
   3.133 +no_notation
   3.134 +  top ("\<top>") and
   3.135 +  bot ("\<bottom>")
   3.136 +
   3.137  end
     4.1 --- a/src/HOL/Predicate.thy	Mon Feb 20 15:17:03 2012 +0100
     4.2 +++ b/src/HOL/Predicate.thy	Sun Feb 19 15:30:35 2012 +0100
     4.3 @@ -25,52 +25,6 @@
     4.4  
     4.5  subsection {* Predicates as (complete) lattices *}
     4.6  
     4.7 -text {*
     4.8 -  Handy introduction and elimination rules for @{text "\<le>"}
     4.9 -  on unary and binary predicates
    4.10 -*}
    4.11 -
    4.12 -lemma predicate1I:
    4.13 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    4.14 -  shows "P \<le> Q"
    4.15 -  apply (rule le_funI)
    4.16 -  apply (rule le_boolI)
    4.17 -  apply (rule PQ)
    4.18 -  apply assumption
    4.19 -  done
    4.20 -
    4.21 -lemma predicate1D [Pure.dest?, dest?]:
    4.22 -  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    4.23 -  apply (erule le_funE)
    4.24 -  apply (erule le_boolE)
    4.25 -  apply assumption+
    4.26 -  done
    4.27 -
    4.28 -lemma rev_predicate1D:
    4.29 -  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    4.30 -  by (rule predicate1D)
    4.31 -
    4.32 -lemma predicate2I [Pure.intro!, intro!]:
    4.33 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    4.34 -  shows "P \<le> Q"
    4.35 -  apply (rule le_funI)+
    4.36 -  apply (rule le_boolI)
    4.37 -  apply (rule PQ)
    4.38 -  apply assumption
    4.39 -  done
    4.40 -
    4.41 -lemma predicate2D [Pure.dest, dest]:
    4.42 -  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    4.43 -  apply (erule le_funE)+
    4.44 -  apply (erule le_boolE)
    4.45 -  apply assumption+
    4.46 -  done
    4.47 -
    4.48 -lemma rev_predicate2D:
    4.49 -  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
    4.50 -  by (rule predicate2D)
    4.51 -
    4.52 -
    4.53  subsubsection {* Equality *}
    4.54  
    4.55  lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    4.56 @@ -91,51 +45,15 @@
    4.57  
    4.58  subsubsection {* Top and bottom elements *}
    4.59  
    4.60 -lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
    4.61 -  by (simp add: bot_fun_def)
    4.62 -
    4.63 -lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
    4.64 -  by (simp add: bot_fun_def)
    4.65 -
    4.66  lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    4.67    by (auto simp add: fun_eq_iff)
    4.68  
    4.69  lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    4.70    by (auto simp add: fun_eq_iff)
    4.71  
    4.72 -lemma top1I [intro!]: "\<top> x"
    4.73 -  by (simp add: top_fun_def)
    4.74 -
    4.75 -lemma top2I [intro!]: "\<top> x y"
    4.76 -  by (simp add: top_fun_def)
    4.77 -
    4.78  
    4.79  subsubsection {* Binary intersection *}
    4.80  
    4.81 -lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    4.82 -  by (simp add: inf_fun_def)
    4.83 -
    4.84 -lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    4.85 -  by (simp add: inf_fun_def)
    4.86 -
    4.87 -lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    4.88 -  by (simp add: inf_fun_def)
    4.89 -
    4.90 -lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    4.91 -  by (simp add: inf_fun_def)
    4.92 -
    4.93 -lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    4.94 -  by (simp add: inf_fun_def)
    4.95 -
    4.96 -lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    4.97 -  by (simp add: inf_fun_def)
    4.98 -
    4.99 -lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   4.100 -  by (simp add: inf_fun_def)
   4.101 -
   4.102 -lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   4.103 -  by (simp add: inf_fun_def)
   4.104 -
   4.105  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.106    by (simp add: inf_fun_def)
   4.107  
   4.108 @@ -145,35 +63,6 @@
   4.109  
   4.110  subsubsection {* Binary union *}
   4.111  
   4.112 -lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   4.113 -  by (simp add: sup_fun_def)
   4.114 -
   4.115 -lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   4.116 -  by (simp add: sup_fun_def)
   4.117 -
   4.118 -lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   4.119 -  by (simp add: sup_fun_def)
   4.120 -
   4.121 -lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   4.122 -  by (simp add: sup_fun_def)
   4.123 -
   4.124 -lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   4.125 -  by (simp add: sup_fun_def) iprover
   4.126 -
   4.127 -lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   4.128 -  by (simp add: sup_fun_def) iprover
   4.129 -
   4.130 -text {*
   4.131 -  \medskip Classical introduction rule: no commitment to @{text A} vs
   4.132 -  @{text B}.
   4.133 -*}
   4.134 -
   4.135 -lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   4.136 -  by (auto simp add: sup_fun_def)
   4.137 -
   4.138 -lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   4.139 -  by (auto simp add: sup_fun_def)
   4.140 -
   4.141  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.142    by (simp add: sup_fun_def)
   4.143  
   4.144 @@ -183,57 +72,15 @@
   4.145  
   4.146  subsubsection {* Intersections of families *}
   4.147  
   4.148 -lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
   4.149 -  by (simp add: INF_apply)
   4.150 -
   4.151 -lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   4.152 -  by (simp add: INF_apply)
   4.153 -
   4.154 -lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   4.155 -  by (auto simp add: INF_apply)
   4.156 -
   4.157 -lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   4.158 -  by (auto simp add: INF_apply)
   4.159 -
   4.160 -lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   4.161 -  by (auto simp add: INF_apply)
   4.162 -
   4.163 -lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   4.164 -  by (auto simp add: INF_apply)
   4.165 -
   4.166 -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.167 -  by (auto simp add: INF_apply)
   4.168 -
   4.169 -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.170 -  by (auto simp add: INF_apply)
   4.171 -
   4.172 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   4.173 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   4.174    by (simp add: INF_apply fun_eq_iff)
   4.175  
   4.176 -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.177 +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.178    by (simp add: INF_apply fun_eq_iff)
   4.179  
   4.180  
   4.181  subsubsection {* Unions of families *}
   4.182  
   4.183 -lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   4.184 -  by (simp add: SUP_apply)
   4.185 -
   4.186 -lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   4.187 -  by (simp add: SUP_apply)
   4.188 -
   4.189 -lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   4.190 -  by (auto simp add: SUP_apply)
   4.191 -
   4.192 -lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   4.193 -  by (auto simp add: SUP_apply)
   4.194 -
   4.195 -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.196 -  by (auto simp add: SUP_apply)
   4.197 -
   4.198 -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.199 -  by (auto simp add: SUP_apply)
   4.200 -
   4.201  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   4.202    by (simp add: SUP_apply fun_eq_iff)
   4.203