1.1 --- a/src/HOL/Complete_Lattices.thy	Mon Feb 20 21:04:00 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Feb 21 08:15:42 2012 +0100
     1.3 @@ -536,7 +536,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection {* @{typ bool} as complete lattice *}
     1.8 +subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
     1.9  
    1.10  instantiation bool :: complete_lattice
    1.11  begin
    1.12 @@ -573,9 +573,6 @@
    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 @@ -611,54 +608,6 @@
    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 @@ -678,7 +627,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 -subsubsection {* Inter *}
    1.82 +subsection {* Inter *}
    1.83  
    1.84  abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
    1.85    "Inter S \<equiv> \<Sqinter>S"
    1.86 @@ -750,7 +699,7 @@
    1.87    by (fact Inf_superset_mono)
    1.88  
    1.89  
    1.90 -subsubsection {* Intersections of families *}
    1.91 +subsection {* 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 @@ -861,7 +810,7 @@
    1.96    by blast
    1.97  
    1.98  
    1.99 -subsubsection {* Union *}
   1.100 +subsection {* Union *}
   1.101  
   1.102  abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
   1.103    "Union S \<equiv> \<Squnion>S"
   1.104 @@ -930,7 +879,7 @@
   1.105    by (fact Sup_subset_mono)
   1.106  
   1.107  
   1.108 -subsubsection {* Unions of families *}
   1.109 +subsection {* 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 @@ -1093,7 +1042,7 @@
   1.114    by blast
   1.115  
   1.116  
   1.117 -subsubsection {* Distributive laws *}
   1.118 +subsection {* 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 @@ -1135,7 +1084,7 @@
   1.123    by (fact Sup_inf_eq_bot_iff)
   1.124  
   1.125  
   1.126 -subsubsection {* Complement *}
   1.127 +subsection {* 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 @@ -1144,7 +1093,7 @@
   1.132    by (fact uminus_SUP)
   1.133  
   1.134  
   1.135 -subsubsection {* Miniscoping and maxiscoping *}
   1.136 +subsection {* Miniscoping and maxiscoping *}
   1.137  
   1.138  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
   1.139             and Intersections. *}