author haftmann Tue, 21 Feb 2012 08:15:42 +0100 changeset 46557 ae926869a311 parent 46556 2848e36e0348 child 46558 fdb84c40e074
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
 src/HOL/Big_Operators.thy file | annotate | diff | comparison | revisions src/HOL/Complete_Lattices.thy file | annotate | diff | comparison | revisions src/HOL/Lattices.thy file | annotate | diff | comparison | revisions src/HOL/Orderings.thy file | annotate | diff | comparison | revisions src/HOL/Predicate.thy file | annotate | diff | comparison | revisions src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions src/HOL/ZF/Games.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Big_Operators.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -786,13 +786,15 @@
by (simp only: card_def setsum_def)

lemma card_UN_disjoint:
-  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
-    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
-  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
-proof -
-  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
-  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
-qed
+  "finite I ==> (ALL i:I. finite (A i)) ==>
+   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
+   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
+apply (simp add: card_eq_setsum del: setsum_constant)
+apply (subgoal_tac
+         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
+apply (simp add: setsum_UN_disjoint del: setsum_constant)
+apply simp
+done

lemma card_Union_disjoint:
"finite C ==> (ALL A:C. finite A) ==>```
```--- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -536,7 +536,7 @@
end

-subsection {* @{typ bool} as complete lattice *}
+subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}

instantiation bool :: complete_lattice
begin
@@ -573,9 +573,6 @@
instance bool :: complete_boolean_algebra proof
qed (auto intro: bool_induct)

-
-subsection {* @{typ "_ \<Rightarrow> _"} as complete lattice *}
-
instantiation "fun" :: (type, complete_lattice) complete_lattice
begin

@@ -611,54 +608,6 @@

instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..

-
-subsection {* Unary and binary predicates as complete lattice *}
-
-lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
-
-lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-
-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 SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-
-lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-
-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)
-
-
-subsection {* @{typ "_ set"} as complete lattice *}
-
instantiation "set" :: (type) complete_lattice
begin

@@ -678,7 +627,7 @@
qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)

-subsubsection {* Inter *}
+subsection {* Inter *}

abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
"Inter S \<equiv> \<Sqinter>S"
@@ -750,7 +699,7 @@
by (fact Inf_superset_mono)

-subsubsection {* Intersections of families *}
+subsection {* Intersections of families *}

abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"INTER \<equiv> INFI"
@@ -861,7 +810,7 @@
by blast

-subsubsection {* Union *}
+subsection {* Union *}

abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
"Union S \<equiv> \<Squnion>S"
@@ -930,7 +879,7 @@
by (fact Sup_subset_mono)

-subsubsection {* Unions of families *}
+subsection {* Unions of families *}

abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
"UNION \<equiv> SUPR"
@@ -1093,7 +1042,7 @@
by blast

-subsubsection {* Distributive laws *}
+subsection {* Distributive laws *}

lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
by (fact inf_Sup)
@@ -1135,7 +1084,7 @@
by (fact Sup_inf_eq_bot_iff)

-subsubsection {* Complement *}
+subsection {* Complement *}

lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
by (fact uminus_INF)
@@ -1144,7 +1093,7 @@
by (fact uminus_SUP)

-subsubsection {* Miniscoping and maxiscoping *}
+subsection {* Miniscoping and maxiscoping *}

text {* \medskip Miniscoping: pushing in quantifiers and big Unions
and Intersections. *}```
```--- a/src/HOL/Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -701,63 +701,6 @@
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 {* Unary and binary predicates as lattice *}
-
-lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
-
-lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
-
-lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
-
-lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
-
-lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
-
-lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
-
-lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
-
-lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
-
-lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
-
-lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
-
-lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
-
-lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
-
-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)
-
-
no_notation
less_eq  (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50) and
@@ -767,4 +710,3 @@
bot ("\<bottom>")

end
-```
```--- a/src/HOL/Orderings.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Orderings.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -1111,6 +1111,10 @@

end

+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>")
+

subsection {* Dense orders *}

@@ -1235,10 +1239,10 @@
[simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"

definition
-  [simp]: "\<bottom> \<longleftrightarrow> False"
+  [simp]: "bot \<longleftrightarrow> False"

definition
-  [simp]: "\<top> \<longleftrightarrow> True"
+  [simp]: "top \<longleftrightarrow> True"

instance proof
qed auto
@@ -1257,10 +1261,10 @@
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
by simp

-lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
+lemma bot_boolE: "bot \<Longrightarrow> P"
by simp

-lemma top_boolI: \<top>
+lemma top_boolI: top
by simp

lemma [code]:
@@ -1297,10 +1301,10 @@
begin

definition
-  "\<bottom> = (\<lambda>x. \<bottom>)"
+  "bot = (\<lambda>x. bot)"

lemma bot_apply:
-  "\<bottom> x = \<bottom>"
+  "bot x = bot"

instance proof
@@ -1312,11 +1316,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"

instance proof
@@ -1334,61 +1338,6 @@
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 [Pure.dest?, dest?]:
-  "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 [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)
-
-lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
-
-lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
-
-lemma top1I [intro!]: "\<top> x"
-
-lemma top2I [intro!]: "\<top> x y"
-
-
subsection {* Name duplicates *}

lemmas order_eq_refl = preorder_class.eq_refl
@@ -1426,8 +1375,4 @@
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3

-no_notation
-  top ("\<top>") and
-  bot ("\<bottom>")
-
end```
```--- a/src/HOL/Predicate.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Predicate.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -25,6 +25,52 @@

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
+
+lemma rev_predicate1D:
+  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
+  by (rule predicate1D)
+
+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)
+
+
subsubsection {* Equality *}

lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
@@ -45,15 +91,51 @@

subsubsection {* Top and bottom elements *}

+lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
+
+lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
+
lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"

lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"

+lemma top1I [intro!]: "\<top> x"
+
+lemma top2I [intro!]: "\<top> x y"
+

subsubsection {* Binary intersection *}

+lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
+
+lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
+
+lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
+
+lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
+
+lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
+
+lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
+
+lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
+
+lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
+
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)"

@@ -63,6 +145,35 @@

subsubsection {* Binary union *}

+lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
+
+lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+
+lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
+
+lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+
+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)"

@@ -72,15 +183,57 @@

subsubsection {* Intersections of families *}

-lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
+lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
+
+lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
+
+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_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
+lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"

subsubsection {* Unions of families *}

+lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
+
+lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
+
+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))"
```
```--- a/src/HOL/Product_Type.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/Product_Type.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -22,7 +22,7 @@
lemma
shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
and [code]: "HOL.equal True P \<longleftrightarrow> P"
-    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
+    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
and [code]: "HOL.equal P True \<longleftrightarrow> P"
and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
```--- a/src/HOL/ZF/Games.thy	Mon Feb 20 21:04:00 2012 +0100
+++ b/src/HOL/ZF/Games.thy	Tue Feb 21 08:15:42 2012 +0100
@@ -19,7 +19,11 @@
"games_gfp \<equiv> gfp fixgames"

lemma mono_fixgames: "mono (fixgames)"
-  by (auto simp add: mono_def fixgames_def)
+  apply (auto simp add: mono_def fixgames_def)
+  apply (rule_tac x=l in exI)
+  apply (rule_tac x=r in exI)
+  apply auto
+  done

lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
@@ -970,4 +974,3 @@
qed

end
-```