author haftmann Sun Feb 19 15:30:35 2012 +0100 (2012-02-19) changeset 46553 50a7e97fe653 parent 46552 5d33a3269029 child 46554 87d4e4958476
distributed lattice properties of predicates to places of instantiation
 src/HOL/Complete_Lattices.thy file | annotate | diff | revisions src/HOL/Lattices.thy file | annotate | diff | revisions src/HOL/Orderings.thy file | annotate | diff | revisions src/HOL/Predicate.thy file | annotate | diff | revisions
```     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.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.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.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.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
```