reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
authorhaftmann
Tue Feb 21 08:15:42 2012 +0100 (2012-02-21)
changeset 46557ae926869a311
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
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Product_Type.thy
src/HOL/ZF/Games.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Mon Feb 20 21:04:00 2012 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Feb 21 08:15:42 2012 +0100
     1.3 @@ -786,13 +786,15 @@
     1.4    by (simp only: card_def setsum_def)
     1.5  
     1.6  lemma card_UN_disjoint:
     1.7 -  assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     1.8 -    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
     1.9 -  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
    1.10 -proof -
    1.11 -  have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
    1.12 -  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
    1.13 -qed
    1.14 +  "finite I ==> (ALL i:I. finite (A i)) ==>
    1.15 +   (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {})
    1.16 +   ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
    1.17 +apply (simp add: card_eq_setsum del: setsum_constant)
    1.18 +apply (subgoal_tac
    1.19 +         "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
    1.20 +apply (simp add: setsum_UN_disjoint del: setsum_constant)
    1.21 +apply simp
    1.22 +done
    1.23  
    1.24  lemma card_Union_disjoint:
    1.25    "finite C ==> (ALL A:C. finite A) ==>
     2.1 --- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
     2.3 @@ -536,7 +536,7 @@
     2.4  end
     2.5  
     2.6  
     2.7 -subsection {* @{typ bool} as complete lattice *}
     2.8 +subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
     2.9  
    2.10  instantiation bool :: complete_lattice
    2.11  begin
    2.12 @@ -573,9 +573,6 @@
    2.13  instance bool :: complete_boolean_algebra proof
    2.14  qed (auto intro: bool_induct)
    2.15  
    2.16 -
    2.17 -subsection {* @{typ "_ \<Rightarrow> _"} as complete lattice *}
    2.18 -
    2.19  instantiation "fun" :: (type, complete_lattice) complete_lattice
    2.20  begin
    2.21  
    2.22 @@ -611,54 +608,6 @@
    2.23  
    2.24  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
    2.25  
    2.26 -
    2.27 -subsection {* Unary and binary predicates as complete lattice *}
    2.28 -
    2.29 -lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
    2.30 -  by (simp add: INF_apply)
    2.31 -
    2.32 -lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
    2.33 -  by (simp add: INF_apply)
    2.34 -
    2.35 -lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
    2.36 -  by (auto simp add: INF_apply)
    2.37 -
    2.38 -lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
    2.39 -  by (auto simp add: INF_apply)
    2.40 -
    2.41 -lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
    2.42 -  by (auto simp add: INF_apply)
    2.43 -
    2.44 -lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
    2.45 -  by (auto simp add: INF_apply)
    2.46 -
    2.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"
    2.48 -  by (auto simp add: INF_apply)
    2.49 -
    2.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"
    2.51 -  by (auto simp add: INF_apply)
    2.52 -
    2.53 -lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
    2.54 -  by (simp add: SUP_apply)
    2.55 -
    2.56 -lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
    2.57 -  by (simp add: SUP_apply)
    2.58 -
    2.59 -lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
    2.60 -  by (auto simp add: SUP_apply)
    2.61 -
    2.62 -lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
    2.63 -  by (auto simp add: SUP_apply)
    2.64 -
    2.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"
    2.66 -  by (auto simp add: SUP_apply)
    2.67 -
    2.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"
    2.69 -  by (auto simp add: SUP_apply)
    2.70 -
    2.71 -
    2.72 -subsection {* @{typ "_ set"} as complete lattice *}
    2.73 -
    2.74  instantiation "set" :: (type) complete_lattice
    2.75  begin
    2.76  
    2.77 @@ -678,7 +627,7 @@
    2.78  qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
    2.79    
    2.80  
    2.81 -subsubsection {* Inter *}
    2.82 +subsection {* Inter *}
    2.83  
    2.84  abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
    2.85    "Inter S \<equiv> \<Sqinter>S"
    2.86 @@ -750,7 +699,7 @@
    2.87    by (fact Inf_superset_mono)
    2.88  
    2.89  
    2.90 -subsubsection {* Intersections of families *}
    2.91 +subsection {* Intersections of families *}
    2.92  
    2.93  abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    2.94    "INTER \<equiv> INFI"
    2.95 @@ -861,7 +810,7 @@
    2.96    by blast
    2.97  
    2.98  
    2.99 -subsubsection {* Union *}
   2.100 +subsection {* Union *}
   2.101  
   2.102  abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   2.103    "Union S \<equiv> \<Squnion>S"
   2.104 @@ -930,7 +879,7 @@
   2.105    by (fact Sup_subset_mono)
   2.106  
   2.107  
   2.108 -subsubsection {* Unions of families *}
   2.109 +subsection {* Unions of families *}
   2.110  
   2.111  abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
   2.112    "UNION \<equiv> SUPR"
   2.113 @@ -1093,7 +1042,7 @@
   2.114    by blast
   2.115  
   2.116  
   2.117 -subsubsection {* Distributive laws *}
   2.118 +subsection {* Distributive laws *}
   2.119  
   2.120  lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
   2.121    by (fact inf_Sup)
   2.122 @@ -1135,7 +1084,7 @@
   2.123    by (fact Sup_inf_eq_bot_iff)
   2.124  
   2.125  
   2.126 -subsubsection {* Complement *}
   2.127 +subsection {* Complement *}
   2.128  
   2.129  lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   2.130    by (fact uminus_INF)
   2.131 @@ -1144,7 +1093,7 @@
   2.132    by (fact uminus_SUP)
   2.133  
   2.134  
   2.135 -subsubsection {* Miniscoping and maxiscoping *}
   2.136 +subsection {* Miniscoping and maxiscoping *}
   2.137  
   2.138  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
   2.139             and Intersections. *}
     3.1 --- a/src/HOL/Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
     3.3 @@ -701,63 +701,6 @@
     3.4  instance "fun" :: (type, boolean_algebra) boolean_algebra proof
     3.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)+
     3.6  
     3.7 -
     3.8 -subsection {* Unary and binary predicates as lattice *}
     3.9 -
    3.10 -lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    3.11 -  by (simp add: inf_fun_def)
    3.12 -
    3.13 -lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    3.14 -  by (simp add: inf_fun_def)
    3.15 -
    3.16 -lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    3.17 -  by (simp add: inf_fun_def)
    3.18 -
    3.19 -lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    3.20 -  by (simp add: inf_fun_def)
    3.21 -
    3.22 -lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    3.23 -  by (simp add: inf_fun_def)
    3.24 -
    3.25 -lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    3.26 -  by (simp add: inf_fun_def)
    3.27 -
    3.28 -lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    3.29 -  by (simp add: inf_fun_def)
    3.30 -
    3.31 -lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    3.32 -  by (simp add: inf_fun_def)
    3.33 -
    3.34 -lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
    3.35 -  by (simp add: sup_fun_def)
    3.36 -
    3.37 -lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    3.38 -  by (simp add: sup_fun_def)
    3.39 -
    3.40 -lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
    3.41 -  by (simp add: sup_fun_def)
    3.42 -
    3.43 -lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    3.44 -  by (simp add: sup_fun_def)
    3.45 -
    3.46 -lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
    3.47 -  by (simp add: sup_fun_def) iprover
    3.48 -
    3.49 -lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
    3.50 -  by (simp add: sup_fun_def) iprover
    3.51 -
    3.52 -text {*
    3.53 -  \medskip Classical introduction rule: no commitment to @{text A} vs
    3.54 -  @{text B}.
    3.55 -*}
    3.56 -
    3.57 -lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
    3.58 -  by (auto simp add: sup_fun_def)
    3.59 -
    3.60 -lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
    3.61 -  by (auto simp add: sup_fun_def)
    3.62 -
    3.63 -
    3.64  no_notation
    3.65    less_eq  (infix "\<sqsubseteq>" 50) and
    3.66    less (infix "\<sqsubset>" 50) and
    3.67 @@ -767,4 +710,3 @@
    3.68    bot ("\<bottom>")
    3.69  
    3.70  end
    3.71 -
     4.1 --- a/src/HOL/Orderings.thy	Mon Feb 20 21:04:00 2012 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Tue Feb 21 08:15:42 2012 +0100
     4.3 @@ -1111,6 +1111,10 @@
     4.4  
     4.5  end
     4.6  
     4.7 +no_notation
     4.8 +  bot ("\<bottom>") and
     4.9 +  top ("\<top>")
    4.10 +
    4.11  
    4.12  subsection {* Dense orders *}
    4.13  
    4.14 @@ -1235,10 +1239,10 @@
    4.15    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    4.16  
    4.17  definition
    4.18 -  [simp]: "\<bottom> \<longleftrightarrow> False"
    4.19 +  [simp]: "bot \<longleftrightarrow> False"
    4.20  
    4.21  definition
    4.22 -  [simp]: "\<top> \<longleftrightarrow> True"
    4.23 +  [simp]: "top \<longleftrightarrow> True"
    4.24  
    4.25  instance proof
    4.26  qed auto
    4.27 @@ -1257,10 +1261,10 @@
    4.28  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    4.29    by simp
    4.30  
    4.31 -lemma bot_boolE: "\<bottom> \<Longrightarrow> P"
    4.32 +lemma bot_boolE: "bot \<Longrightarrow> P"
    4.33    by simp
    4.34  
    4.35 -lemma top_boolI: \<top>
    4.36 +lemma top_boolI: top
    4.37    by simp
    4.38  
    4.39  lemma [code]:
    4.40 @@ -1297,10 +1301,10 @@
    4.41  begin
    4.42  
    4.43  definition
    4.44 -  "\<bottom> = (\<lambda>x. \<bottom>)"
    4.45 +  "bot = (\<lambda>x. bot)"
    4.46  
    4.47  lemma bot_apply:
    4.48 -  "\<bottom> x = \<bottom>"
    4.49 +  "bot x = bot"
    4.50    by (simp add: bot_fun_def)
    4.51  
    4.52  instance proof
    4.53 @@ -1312,11 +1316,11 @@
    4.54  begin
    4.55  
    4.56  definition
    4.57 -  [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    4.58 +  [no_atp]: "top = (\<lambda>x. top)"
    4.59  declare top_fun_def_raw [no_atp]
    4.60  
    4.61  lemma top_apply:
    4.62 -  "\<top> x = \<top>"
    4.63 +  "top x = top"
    4.64    by (simp add: top_fun_def)
    4.65  
    4.66  instance proof
    4.67 @@ -1334,61 +1338,6 @@
    4.68    unfolding le_fun_def by simp
    4.69  
    4.70  
    4.71 -subsection {* Order on unary and binary predicates *}
    4.72 -
    4.73 -lemma predicate1I:
    4.74 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    4.75 -  shows "P \<le> Q"
    4.76 -  apply (rule le_funI)
    4.77 -  apply (rule le_boolI)
    4.78 -  apply (rule PQ)
    4.79 -  apply assumption
    4.80 -  done
    4.81 -
    4.82 -lemma predicate1D [Pure.dest?, dest?]:
    4.83 -  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    4.84 -  apply (erule le_funE)
    4.85 -  apply (erule le_boolE)
    4.86 -  apply assumption+
    4.87 -  done
    4.88 -
    4.89 -lemma rev_predicate1D:
    4.90 -  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    4.91 -  by (rule predicate1D)
    4.92 -
    4.93 -lemma predicate2I [Pure.intro!, intro!]:
    4.94 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    4.95 -  shows "P \<le> Q"
    4.96 -  apply (rule le_funI)+
    4.97 -  apply (rule le_boolI)
    4.98 -  apply (rule PQ)
    4.99 -  apply assumption
   4.100 -  done
   4.101 -
   4.102 -lemma predicate2D [Pure.dest, dest]:
   4.103 -  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   4.104 -  apply (erule le_funE)+
   4.105 -  apply (erule le_boolE)
   4.106 -  apply assumption+
   4.107 -  done
   4.108 -
   4.109 -lemma rev_predicate2D:
   4.110 -  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   4.111 -  by (rule predicate2D)
   4.112 -
   4.113 -lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
   4.114 -  by (simp add: bot_fun_def)
   4.115 -
   4.116 -lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
   4.117 -  by (simp add: bot_fun_def)
   4.118 -
   4.119 -lemma top1I [intro!]: "\<top> x"
   4.120 -  by (simp add: top_fun_def)
   4.121 -
   4.122 -lemma top2I [intro!]: "\<top> x y"
   4.123 -  by (simp add: top_fun_def)
   4.124 -
   4.125 -
   4.126  subsection {* Name duplicates *}
   4.127  
   4.128  lemmas order_eq_refl = preorder_class.eq_refl
   4.129 @@ -1426,8 +1375,4 @@
   4.130  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
   4.131  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   4.132  
   4.133 -no_notation
   4.134 -  top ("\<top>") and
   4.135 -  bot ("\<bottom>")
   4.136 -
   4.137  end
     5.1 --- a/src/HOL/Predicate.thy	Mon Feb 20 21:04:00 2012 +0100
     5.2 +++ b/src/HOL/Predicate.thy	Tue Feb 21 08:15:42 2012 +0100
     5.3 @@ -25,6 +25,52 @@
     5.4  
     5.5  subsection {* Predicates as (complete) lattices *}
     5.6  
     5.7 +text {*
     5.8 +  Handy introduction and elimination rules for @{text "\<le>"}
     5.9 +  on unary and binary predicates
    5.10 +*}
    5.11 +
    5.12 +lemma predicate1I:
    5.13 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    5.14 +  shows "P \<le> Q"
    5.15 +  apply (rule le_funI)
    5.16 +  apply (rule le_boolI)
    5.17 +  apply (rule PQ)
    5.18 +  apply assumption
    5.19 +  done
    5.20 +
    5.21 +lemma predicate1D [Pure.dest?, dest?]:
    5.22 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    5.23 +  apply (erule le_funE)
    5.24 +  apply (erule le_boolE)
    5.25 +  apply assumption+
    5.26 +  done
    5.27 +
    5.28 +lemma rev_predicate1D:
    5.29 +  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
    5.30 +  by (rule predicate1D)
    5.31 +
    5.32 +lemma predicate2I [Pure.intro!, intro!]:
    5.33 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    5.34 +  shows "P \<le> Q"
    5.35 +  apply (rule le_funI)+
    5.36 +  apply (rule le_boolI)
    5.37 +  apply (rule PQ)
    5.38 +  apply assumption
    5.39 +  done
    5.40 +
    5.41 +lemma predicate2D [Pure.dest, dest]:
    5.42 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    5.43 +  apply (erule le_funE)+
    5.44 +  apply (erule le_boolE)
    5.45 +  apply assumption+
    5.46 +  done
    5.47 +
    5.48 +lemma rev_predicate2D:
    5.49 +  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
    5.50 +  by (rule predicate2D)
    5.51 +
    5.52 +
    5.53  subsubsection {* Equality *}
    5.54  
    5.55  lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
    5.56 @@ -45,15 +91,51 @@
    5.57  
    5.58  subsubsection {* Top and bottom elements *}
    5.59  
    5.60 +lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
    5.61 +  by (simp add: bot_fun_def)
    5.62 +
    5.63 +lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
    5.64 +  by (simp add: bot_fun_def)
    5.65 +
    5.66  lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    5.67    by (auto simp add: fun_eq_iff)
    5.68  
    5.69  lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    5.70    by (auto simp add: fun_eq_iff)
    5.71  
    5.72 +lemma top1I [intro!]: "\<top> x"
    5.73 +  by (simp add: top_fun_def)
    5.74 +
    5.75 +lemma top2I [intro!]: "\<top> x y"
    5.76 +  by (simp add: top_fun_def)
    5.77 +
    5.78  
    5.79  subsubsection {* Binary intersection *}
    5.80  
    5.81 +lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    5.82 +  by (simp add: inf_fun_def)
    5.83 +
    5.84 +lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    5.85 +  by (simp add: inf_fun_def)
    5.86 +
    5.87 +lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    5.88 +  by (simp add: inf_fun_def)
    5.89 +
    5.90 +lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    5.91 +  by (simp add: inf_fun_def)
    5.92 +
    5.93 +lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    5.94 +  by (simp add: inf_fun_def)
    5.95 +
    5.96 +lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    5.97 +  by (simp add: inf_fun_def)
    5.98 +
    5.99 +lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   5.100 +  by (simp add: inf_fun_def)
   5.101 +
   5.102 +lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   5.103 +  by (simp add: inf_fun_def)
   5.104 +
   5.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)"
   5.106    by (simp add: inf_fun_def)
   5.107  
   5.108 @@ -63,6 +145,35 @@
   5.109  
   5.110  subsubsection {* Binary union *}
   5.111  
   5.112 +lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   5.113 +  by (simp add: sup_fun_def)
   5.114 +
   5.115 +lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   5.116 +  by (simp add: sup_fun_def)
   5.117 +
   5.118 +lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   5.119 +  by (simp add: sup_fun_def)
   5.120 +
   5.121 +lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   5.122 +  by (simp add: sup_fun_def)
   5.123 +
   5.124 +lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   5.125 +  by (simp add: sup_fun_def) iprover
   5.126 +
   5.127 +lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   5.128 +  by (simp add: sup_fun_def) iprover
   5.129 +
   5.130 +text {*
   5.131 +  \medskip Classical introduction rule: no commitment to @{text A} vs
   5.132 +  @{text B}.
   5.133 +*}
   5.134 +
   5.135 +lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   5.136 +  by (auto simp add: sup_fun_def)
   5.137 +
   5.138 +lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   5.139 +  by (auto simp add: sup_fun_def)
   5.140 +
   5.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)"
   5.142    by (simp add: sup_fun_def)
   5.143  
   5.144 @@ -72,15 +183,57 @@
   5.145  
   5.146  subsubsection {* Intersections of families *}
   5.147  
   5.148 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   5.149 +lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
   5.150 +  by (simp add: INF_apply)
   5.151 +
   5.152 +lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   5.153 +  by (simp add: INF_apply)
   5.154 +
   5.155 +lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   5.156 +  by (auto simp add: INF_apply)
   5.157 +
   5.158 +lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   5.159 +  by (auto simp add: INF_apply)
   5.160 +
   5.161 +lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   5.162 +  by (auto simp add: INF_apply)
   5.163 +
   5.164 +lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   5.165 +  by (auto simp add: INF_apply)
   5.166 +
   5.167 +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"
   5.168 +  by (auto simp add: INF_apply)
   5.169 +
   5.170 +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"
   5.171 +  by (auto simp add: INF_apply)
   5.172 +
   5.173 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   5.174    by (simp add: INF_apply fun_eq_iff)
   5.175  
   5.176 -lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   5.177 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
   5.178    by (simp add: INF_apply fun_eq_iff)
   5.179  
   5.180  
   5.181  subsubsection {* Unions of families *}
   5.182  
   5.183 +lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   5.184 +  by (simp add: SUP_apply)
   5.185 +
   5.186 +lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   5.187 +  by (simp add: SUP_apply)
   5.188 +
   5.189 +lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   5.190 +  by (auto simp add: SUP_apply)
   5.191 +
   5.192 +lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   5.193 +  by (auto simp add: SUP_apply)
   5.194 +
   5.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"
   5.196 +  by (auto simp add: SUP_apply)
   5.197 +
   5.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"
   5.199 +  by (auto simp add: SUP_apply)
   5.200 +
   5.201  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   5.202    by (simp add: SUP_apply fun_eq_iff)
   5.203  
     6.1 --- a/src/HOL/Product_Type.thy	Mon Feb 20 21:04:00 2012 +0100
     6.2 +++ b/src/HOL/Product_Type.thy	Tue Feb 21 08:15:42 2012 +0100
     6.3 @@ -22,7 +22,7 @@
     6.4  lemma
     6.5    shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
     6.6      and [code]: "HOL.equal True P \<longleftrightarrow> P" 
     6.7 -    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
     6.8 +    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 
     6.9      and [code]: "HOL.equal P True \<longleftrightarrow> P"
    6.10      and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    6.11    by (simp_all add: equal)
     7.1 --- a/src/HOL/ZF/Games.thy	Mon Feb 20 21:04:00 2012 +0100
     7.2 +++ b/src/HOL/ZF/Games.thy	Tue Feb 21 08:15:42 2012 +0100
     7.3 @@ -19,7 +19,11 @@
     7.4    "games_gfp \<equiv> gfp fixgames"
     7.5  
     7.6  lemma mono_fixgames: "mono (fixgames)"
     7.7 -  by (auto simp add: mono_def fixgames_def)
     7.8 +  apply (auto simp add: mono_def fixgames_def)
     7.9 +  apply (rule_tac x=l in exI)
    7.10 +  apply (rule_tac x=r in exI)
    7.11 +  apply auto
    7.12 +  done
    7.13  
    7.14  lemma games_lfp_unfold: "games_lfp = fixgames games_lfp"
    7.15    by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames)
    7.16 @@ -970,4 +974,3 @@
    7.17  qed
    7.18  
    7.19  end
    7.20 -