# HG changeset patch
# User haftmann
# Date 1291816343 -3600
# Node ID 294956ff285b5556755512b1e3a9a845ccbc1f1f
# Parent  a0d9258e2091c9ca331ac113a7a52d9b7eed1427
nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules

diff -r a0d9258e2091 -r 294956ff285b src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -44,14 +44,22 @@
 lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Inf_empty:
+lemma Inf_empty [simp]:
   "\<Sqinter>{} = \<top>"
   by (auto intro: antisym Inf_greatest)
 
-lemma Sup_empty:
+lemma Sup_empty [simp]:
   "\<Squnion>{} = \<bottom>"
   by (auto intro: antisym Sup_least)
 
+lemma Inf_UNIV [simp]:
+  "\<Sqinter>UNIV = \<bottom>"
+  by (simp add: Sup_Inf Sup_empty [symmetric])
+
+lemma Sup_UNIV [simp]:
+  "\<Squnion>UNIV = \<top>"
+  by (simp add: Inf_Sup Inf_empty [symmetric])
+
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
@@ -74,14 +82,6 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_empty Sup_insert)
 
-lemma Inf_UNIV:
-  "\<Sqinter>UNIV = bot"
-  by (simp add: Sup_Inf Sup_empty [symmetric])
-
-lemma Sup_UNIV:
-  "\<Squnion>UNIV = top"
-  by (simp add: Inf_Sup Inf_empty [symmetric])
-
 lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   by (auto intro: Sup_least dest: Sup_upper)
 
@@ -117,10 +117,16 @@
 end
 
 syntax
-  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
-  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
   "SUP x y. B"   == "SUP x. SUP y. B"
@@ -212,25 +218,17 @@
 begin
 
 definition
-  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+  "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
 
 definition
-  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+  "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
 
 instance proof
 qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
 
 end
 
-lemma Inf_empty_bool [simp]:
-  "\<Sqinter>{}"
-  unfolding Inf_bool_def by auto
-
-lemma not_Sup_empty_bool [simp]:
-  "\<not> \<Squnion>{}"
-  unfolding Sup_bool_def by auto
-
-lemma INFI_bool_eq:
+lemma INFI_bool_eq [simp]:
   "INFI = Ball"
 proof (rule ext)+
   fix A :: "'a set"
@@ -239,7 +237,7 @@
     by (auto simp add: Ball_def INFI_def Inf_bool_def)
 qed
 
-lemma SUPR_bool_eq:
+lemma SUPR_bool_eq [simp]:
   "SUPR = Bex"
 proof (rule ext)+
   fix A :: "'a set"
@@ -252,36 +250,32 @@
 begin
 
 definition
-  Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+  "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+
+lemma Inf_apply:
+  "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
+  by (simp add: Inf_fun_def)
 
 definition
-  Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+  "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+
+lemma Sup_apply:
+  "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
+  by (simp add: Sup_fun_def)
 
 instance proof
-qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
+qed (auto simp add: le_fun_def Inf_apply Sup_apply
   intro: Inf_lower Sup_upper Inf_greatest Sup_least)
 
 end
 
-lemma SUPR_fun_expand:
-  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
-  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
-  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
-           simp: SUPR_def Sup_fun_def)
+lemma INFI_apply:
+  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
+  by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
 
-lemma INFI_fun_expand:
-  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
-  shows "(INF y:A. f y) x = (INF y:A. f y x)"
-  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
-           simp: INFI_def Inf_fun_def)
-
-lemma Inf_empty_fun:
-  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
-  by (simp add: Inf_fun_def)
-
-lemma Sup_empty_fun:
-  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
-  by (simp add: Sup_fun_def)
+lemma SUPR_apply:
+  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
+  by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
 
 
 subsection {* Union *}
@@ -572,7 +566,7 @@
   by blast
 
 lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
-  by blast
+  by (fact Inf_empty)
 
 lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
   by blast
@@ -871,6 +865,12 @@
   top ("\<top>") and
   bot ("\<bottom>")
 
+no_syntax (xsymbols)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+
 lemmas mem_simps =
   insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
diff -r a0d9258e2091 -r 294956ff285b src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -587,34 +587,33 @@
 begin
 
 definition
-  bool_Compl_def: "uminus = Not"
+  bool_Compl_def [simp]: "uminus = Not"
 
 definition
-  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
+  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
 
 definition
-  inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
+  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
 
 definition
-  sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
+  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
 
 instance proof
-qed (simp_all add: inf_bool_def sup_bool_def le_bool_def
-  bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto)
+qed auto
 
 end
 
 lemma sup_boolI1:
   "P \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_def)
+  by simp
 
 lemma sup_boolI2:
   "Q \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_def)
+  by simp
 
 lemma sup_boolE:
   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: sup_bool_def)
+  by auto
 
 
 subsection {* Fun as lattice *}
@@ -623,19 +622,26 @@
 begin
 
 definition
-  inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+
+lemma inf_apply:
+  "(f \<sqinter> g) x = f x \<sqinter> g x"
+  by (simp add: inf_fun_def)
 
 definition
-  sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+
+lemma sup_apply:
+  "(f \<squnion> g) x = f x \<squnion> g x"
+  by (simp add: sup_fun_def)
 
 instance proof
-qed (simp_all add: le_fun_def inf_fun_def sup_fun_def)
+qed (simp_all add: le_fun_def inf_apply sup_apply)
 
 end
 
-instance "fun" :: (type, distrib_lattice) distrib_lattice
-proof
-qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1)
+instance "fun" :: (type, distrib_lattice) distrib_lattice proof
+qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
 
 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
 
@@ -645,6 +651,10 @@
 definition
   fun_Compl_def: "- A = (\<lambda>x. - A x)"
 
+lemma uminus_apply:
+  "(- A) x = - (A x)"
+  by (simp add: fun_Compl_def)
+
 instance ..
 
 end
@@ -655,15 +665,16 @@
 definition
   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
 
+lemma minus_apply:
+  "(A - B) x = A x - B x"
+  by (simp add: fun_diff_def)
+
 instance ..
 
 end
 
-instance "fun" :: (type, boolean_algebra) boolean_algebra
-proof
-qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def
-  inf_compl_bot sup_compl_top diff_eq)
-
+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)+
 
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
diff -r a0d9258e2091 -r 294956ff285b src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -14,4 +14,10 @@
   Inf  ("\<Sqinter>_" [900] 900) and
   Sup  ("\<Squnion>_" [900] 900)
 
+syntax (xsymbols)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+
 end
diff -r a0d9258e2091 -r 294956ff285b src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -1208,46 +1208,46 @@
 begin
 
 definition
-  le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+  le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
 
 definition
-  less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
+  [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
 
 definition
-  top_bool_def: "top = True"
+  [simp]: "top \<longleftrightarrow> True"
 
 definition
-  bot_bool_def: "bot = False"
+  [simp]: "bot \<longleftrightarrow> False"
 
 instance proof
-qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
+qed auto
 
 end
 
 lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
-  by (simp add: le_bool_def)
+  by simp
 
 lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
-  by (simp add: le_bool_def)
+  by simp
 
 lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-  by (simp add: le_bool_def)
+  by simp
 
 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
-  by (simp add: le_bool_def)
+  by simp
 
 lemma bot_boolE: "bot \<Longrightarrow> P"
-  by (simp add: bot_bool_def)
+  by simp
 
 lemma top_boolI: top
-  by (simp add: top_bool_def)
+  by simp
 
 lemma [code]:
   "False \<le> b \<longleftrightarrow> True"
   "True \<le> b \<longleftrightarrow> b"
   "False < b \<longleftrightarrow> b"
   "True < b \<longleftrightarrow> False"
-  unfolding le_bool_def less_bool_def by simp_all
+  by simp_all
 
 
 subsection {* Order on functions *}
@@ -1259,7 +1259,7 @@
   le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
 
 definition
-  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
+  "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
 
 instance ..
 
@@ -1276,11 +1276,15 @@
 begin
 
 definition
-  top_fun_def [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"
+  by (simp add: top_fun_def)
+
 instance proof
-qed (simp add: top_fun_def le_fun_def)
+qed (simp add: le_fun_def top_apply)
 
 end
 
@@ -1288,10 +1292,14 @@
 begin
 
 definition
-  bot_fun_def: "bot = (\<lambda>x. bot)"
+  "bot = (\<lambda>x. bot)"
+
+lemma bot_apply:
+  "bot x = bot"
+  by (simp add: bot_fun_def)
 
 instance proof
-qed (simp add: bot_fun_def le_fun_def)
+qed (simp add: le_fun_def bot_apply)
 
 end
 
diff -r a0d9258e2091 -r 294956ff285b src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Predicate.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -16,6 +16,12 @@
   top ("\<top>") and
   bot ("\<bottom>")
 
+syntax (xsymbols)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+
 
 subsection {* Predicates as (complete) lattices *}
 
@@ -179,61 +185,61 @@
 subsubsection {* Unions of families *}
 
 lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
-  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
+  by (simp add: SUPR_apply)
 
 lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
-  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
+  by (simp add: SUPR_apply)
 
 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
-  by (auto simp add: SUP1_iff)
+  by (auto simp add: SUPR_apply)
 
 lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
-  by (auto simp add: SUP2_iff)
+  by (auto simp add: SUPR_apply)
 
 lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
-  by (auto simp add: SUP1_iff)
+  by (auto simp add: SUPR_apply)
 
 lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
-  by (auto simp add: SUP2_iff)
+  by (auto simp add: SUPR_apply)
 
 lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
-  by (simp add: SUP1_iff fun_eq_iff)
+  by (simp add: SUPR_apply fun_eq_iff)
 
 lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
-  by (simp add: SUP2_iff fun_eq_iff)
+  by (simp add: SUPR_apply fun_eq_iff)
 
 
 subsubsection {* Intersections of families *}
 
 lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
-  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
+  by (simp add: INFI_apply)
 
 lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
-  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
+  by (simp add: INFI_apply)
 
 lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
-  by (auto simp add: INF1_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
-  by (auto simp add: INF2_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
-  by (auto simp add: INF1_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
-  by (auto simp add: INF2_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
-  by (auto simp add: INF1_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
-  by (auto simp add: INF2_iff)
+  by (auto simp add: INFI_apply)
 
 lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
-  by (simp add: INF1_iff fun_eq_iff)
+  by (simp add: INFI_apply fun_eq_iff)
 
 lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
-  by (simp add: INF2_iff fun_eq_iff)
+  by (simp add: INFI_apply fun_eq_iff)
 
 
 subsection {* Predicates as relations *}
@@ -493,8 +499,7 @@
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def
-  fun_Compl_def fun_diff_def bool_Compl_def bool_diff_def)
+qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply)
 
 end
 
@@ -514,10 +519,10 @@
   by (simp add: single_def)
 
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
-  "P \<guillemotright>= f = (SUPR {x. Predicate.eval P x} f)"
+  "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
 
 lemma eval_bind [simp]:
-  "eval (P \<guillemotright>= f) = Predicate.eval (SUPR {x. Predicate.eval P x} f)"
+  "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind:
@@ -822,7 +827,7 @@
   "single x = Seq (\<lambda>u. Insert x \<bottom>)"
   unfolding Seq_def by simp
 
-primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
+primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
     "apply f Empty = Empty"
   | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
@@ -972,7 +977,7 @@
   "the A = (THE x. eval A x)"
 
 lemma the_eqI:
-  "(THE x. Predicate.eval P x) = x \<Longrightarrow> Predicate.the P = x"
+  "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   by (simp add: the_def)
 
 lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
@@ -1030,6 +1035,12 @@
   bot ("\<bottom>") and
   bind (infixl "\<guillemotright>=" 70)
 
+no_syntax (xsymbols)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
diff -r a0d9258e2091 -r 294956ff285b src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
@@ -1391,7 +1391,7 @@
 proof safe
   fix a
   have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
-    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_fun_expand[where 'c=pextreal])
+    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_apply[where 'c=pextreal])
   then show "{x\<in>space M. a < ?sup x} \<in> sets M"
     using assms by auto
 qed
@@ -1404,7 +1404,7 @@
 proof safe
   fix a
   have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
-    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_fun_expand)
+    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_apply)
   then show "{x\<in>space M. ?inf x < a} \<in> sets M"
     using assms by auto
 qed
@@ -1427,7 +1427,7 @@
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
   using assms unfolding psuminf_def
-  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
+  by (auto intro!: borel_measurable_SUP[unfolded SUPR_apply])
 
 section "LIMSEQ is borel measurable"
 
@@ -1456,7 +1456,7 @@
   with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
   have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
        "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
-    unfolding SUPR_fun_expand INFI_fun_expand by auto
+    unfolding SUPR_apply INFI_apply by auto
   note this[THEN borel_measurable_real]
   from borel_measurable_diff[OF this]
   show ?thesis unfolding * .