nice syntax for lattice INFI, SUPR;
authorhaftmann
Wed Dec 08 14:52:23 2010 +0100 (2010-12-08)
changeset 41080294956ff285b
parent 41079 a0d9258e2091
child 41081 fb1e5377143d
nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules
src/HOL/Complete_Lattice.thy
src/HOL/Lattices.thy
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Probability/Borel_Space.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Dec 08 14:52:23 2010 +0100
     1.3 @@ -44,14 +44,22 @@
     1.4  lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
     1.5    by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
     1.6  
     1.7 -lemma Inf_empty:
     1.8 +lemma Inf_empty [simp]:
     1.9    "\<Sqinter>{} = \<top>"
    1.10    by (auto intro: antisym Inf_greatest)
    1.11  
    1.12 -lemma Sup_empty:
    1.13 +lemma Sup_empty [simp]:
    1.14    "\<Squnion>{} = \<bottom>"
    1.15    by (auto intro: antisym Sup_least)
    1.16  
    1.17 +lemma Inf_UNIV [simp]:
    1.18 +  "\<Sqinter>UNIV = \<bottom>"
    1.19 +  by (simp add: Sup_Inf Sup_empty [symmetric])
    1.20 +
    1.21 +lemma Sup_UNIV [simp]:
    1.22 +  "\<Squnion>UNIV = \<top>"
    1.23 +  by (simp add: Inf_Sup Inf_empty [symmetric])
    1.24 +
    1.25  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    1.26    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    1.27  
    1.28 @@ -74,14 +82,6 @@
    1.29    "\<Squnion>{a, b} = a \<squnion> b"
    1.30    by (simp add: Sup_empty Sup_insert)
    1.31  
    1.32 -lemma Inf_UNIV:
    1.33 -  "\<Sqinter>UNIV = bot"
    1.34 -  by (simp add: Sup_Inf Sup_empty [symmetric])
    1.35 -
    1.36 -lemma Sup_UNIV:
    1.37 -  "\<Squnion>UNIV = top"
    1.38 -  by (simp add: Inf_Sup Inf_empty [symmetric])
    1.39 -
    1.40  lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    1.41    by (auto intro: Sup_least dest: Sup_upper)
    1.42  
    1.43 @@ -117,10 +117,16 @@
    1.44  end
    1.45  
    1.46  syntax
    1.47 -  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.48 -  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.49 -  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.50 -  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.51 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    1.52 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    1.53 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    1.54 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    1.55 +
    1.56 +syntax (xsymbols)
    1.57 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.58 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.59 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.60 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.61  
    1.62  translations
    1.63    "SUP x y. B"   == "SUP x. SUP y. B"
    1.64 @@ -212,25 +218,17 @@
    1.65  begin
    1.66  
    1.67  definition
    1.68 -  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.69 +  "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.70  
    1.71  definition
    1.72 -  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.73 +  "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.74  
    1.75  instance proof
    1.76  qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    1.77  
    1.78  end
    1.79  
    1.80 -lemma Inf_empty_bool [simp]:
    1.81 -  "\<Sqinter>{}"
    1.82 -  unfolding Inf_bool_def by auto
    1.83 -
    1.84 -lemma not_Sup_empty_bool [simp]:
    1.85 -  "\<not> \<Squnion>{}"
    1.86 -  unfolding Sup_bool_def by auto
    1.87 -
    1.88 -lemma INFI_bool_eq:
    1.89 +lemma INFI_bool_eq [simp]:
    1.90    "INFI = Ball"
    1.91  proof (rule ext)+
    1.92    fix A :: "'a set"
    1.93 @@ -239,7 +237,7 @@
    1.94      by (auto simp add: Ball_def INFI_def Inf_bool_def)
    1.95  qed
    1.96  
    1.97 -lemma SUPR_bool_eq:
    1.98 +lemma SUPR_bool_eq [simp]:
    1.99    "SUPR = Bex"
   1.100  proof (rule ext)+
   1.101    fix A :: "'a set"
   1.102 @@ -252,36 +250,32 @@
   1.103  begin
   1.104  
   1.105  definition
   1.106 -  Inf_fun_def: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.107 +  "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   1.108 +
   1.109 +lemma Inf_apply:
   1.110 +  "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
   1.111 +  by (simp add: Inf_fun_def)
   1.112  
   1.113  definition
   1.114 -  Sup_fun_def: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.115 +  "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   1.116 +
   1.117 +lemma Sup_apply:
   1.118 +  "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
   1.119 +  by (simp add: Sup_fun_def)
   1.120  
   1.121  instance proof
   1.122 -qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   1.123 +qed (auto simp add: le_fun_def Inf_apply Sup_apply
   1.124    intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   1.125  
   1.126  end
   1.127  
   1.128 -lemma SUPR_fun_expand:
   1.129 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
   1.130 -  shows "(SUP y:A. f y) = (\<lambda>x. SUP y:A. f y x)"
   1.131 -  by (auto intro!: arg_cong[where f=Sup] ext[where 'a='b]
   1.132 -           simp: SUPR_def Sup_fun_def)
   1.133 +lemma INFI_apply:
   1.134 +  "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   1.135 +  by (auto intro: arg_cong [of _ _ Inf] simp add: INFI_def Inf_apply)
   1.136  
   1.137 -lemma INFI_fun_expand:
   1.138 -  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c\<Colon>{complete_lattice}"
   1.139 -  shows "(INF y:A. f y) x = (INF y:A. f y x)"
   1.140 -  by (auto intro!: arg_cong[where f=Inf] ext[where 'a='b]
   1.141 -           simp: INFI_def Inf_fun_def)
   1.142 -
   1.143 -lemma Inf_empty_fun:
   1.144 -  "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
   1.145 -  by (simp add: Inf_fun_def)
   1.146 -
   1.147 -lemma Sup_empty_fun:
   1.148 -  "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   1.149 -  by (simp add: Sup_fun_def)
   1.150 +lemma SUPR_apply:
   1.151 +  "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   1.152 +  by (auto intro: arg_cong [of _ _ Sup] simp add: SUPR_def Sup_apply)
   1.153  
   1.154  
   1.155  subsection {* Union *}
   1.156 @@ -572,7 +566,7 @@
   1.157    by blast
   1.158  
   1.159  lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
   1.160 -  by blast
   1.161 +  by (fact Inf_empty)
   1.162  
   1.163  lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
   1.164    by blast
   1.165 @@ -871,6 +865,12 @@
   1.166    top ("\<top>") and
   1.167    bot ("\<bottom>")
   1.168  
   1.169 +no_syntax (xsymbols)
   1.170 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   1.171 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   1.172 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   1.173 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   1.174 +
   1.175  lemmas mem_simps =
   1.176    insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
   1.177    mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
     2.1 --- a/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
     2.3 @@ -587,34 +587,33 @@
     2.4  begin
     2.5  
     2.6  definition
     2.7 -  bool_Compl_def: "uminus = Not"
     2.8 +  bool_Compl_def [simp]: "uminus = Not"
     2.9  
    2.10  definition
    2.11 -  bool_diff_def: "A - B \<longleftrightarrow> A \<and> \<not> B"
    2.12 +  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
    2.13  
    2.14  definition
    2.15 -  inf_bool_def: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    2.16 +  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    2.17  
    2.18  definition
    2.19 -  sup_bool_def: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    2.20 +  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    2.21  
    2.22  instance proof
    2.23 -qed (simp_all add: inf_bool_def sup_bool_def le_bool_def
    2.24 -  bot_bool_def top_bool_def bool_Compl_def bool_diff_def, auto)
    2.25 +qed auto
    2.26  
    2.27  end
    2.28  
    2.29  lemma sup_boolI1:
    2.30    "P \<Longrightarrow> P \<squnion> Q"
    2.31 -  by (simp add: sup_bool_def)
    2.32 +  by simp
    2.33  
    2.34  lemma sup_boolI2:
    2.35    "Q \<Longrightarrow> P \<squnion> Q"
    2.36 -  by (simp add: sup_bool_def)
    2.37 +  by simp
    2.38  
    2.39  lemma sup_boolE:
    2.40    "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    2.41 -  by (auto simp add: sup_bool_def)
    2.42 +  by auto
    2.43  
    2.44  
    2.45  subsection {* Fun as lattice *}
    2.46 @@ -623,19 +622,26 @@
    2.47  begin
    2.48  
    2.49  definition
    2.50 -  inf_fun_def: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    2.51 +  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
    2.52 +
    2.53 +lemma inf_apply:
    2.54 +  "(f \<sqinter> g) x = f x \<sqinter> g x"
    2.55 +  by (simp add: inf_fun_def)
    2.56  
    2.57  definition
    2.58 -  sup_fun_def: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    2.59 +  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    2.60 +
    2.61 +lemma sup_apply:
    2.62 +  "(f \<squnion> g) x = f x \<squnion> g x"
    2.63 +  by (simp add: sup_fun_def)
    2.64  
    2.65  instance proof
    2.66 -qed (simp_all add: le_fun_def inf_fun_def sup_fun_def)
    2.67 +qed (simp_all add: le_fun_def inf_apply sup_apply)
    2.68  
    2.69  end
    2.70  
    2.71 -instance "fun" :: (type, distrib_lattice) distrib_lattice
    2.72 -proof
    2.73 -qed (simp_all add: inf_fun_def sup_fun_def sup_inf_distrib1)
    2.74 +instance "fun" :: (type, distrib_lattice) distrib_lattice proof
    2.75 +qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
    2.76  
    2.77  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
    2.78  
    2.79 @@ -645,6 +651,10 @@
    2.80  definition
    2.81    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    2.82  
    2.83 +lemma uminus_apply:
    2.84 +  "(- A) x = - (A x)"
    2.85 +  by (simp add: fun_Compl_def)
    2.86 +
    2.87  instance ..
    2.88  
    2.89  end
    2.90 @@ -655,15 +665,16 @@
    2.91  definition
    2.92    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    2.93  
    2.94 +lemma minus_apply:
    2.95 +  "(A - B) x = A x - B x"
    2.96 +  by (simp add: fun_diff_def)
    2.97 +
    2.98  instance ..
    2.99  
   2.100  end
   2.101  
   2.102 -instance "fun" :: (type, boolean_algebra) boolean_algebra
   2.103 -proof
   2.104 -qed (simp_all add: inf_fun_def sup_fun_def bot_fun_def top_fun_def fun_Compl_def fun_diff_def
   2.105 -  inf_compl_bot sup_compl_top diff_eq)
   2.106 -
   2.107 +instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   2.108 +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.109  
   2.110  no_notation
   2.111    less_eq  (infix "\<sqsubseteq>" 50) and
     3.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Wed Dec 08 14:52:23 2010 +0100
     3.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Wed Dec 08 14:52:23 2010 +0100
     3.3 @@ -14,4 +14,10 @@
     3.4    Inf  ("\<Sqinter>_" [900] 900) and
     3.5    Sup  ("\<Squnion>_" [900] 900)
     3.6  
     3.7 +syntax (xsymbols)
     3.8 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
     3.9 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    3.10 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    3.11 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    3.12 +
    3.13  end
     4.1 --- a/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
     4.3 @@ -1208,46 +1208,46 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     4.8 +  le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
     4.9  
    4.10  definition
    4.11 -  less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    4.12 +  [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    4.13  
    4.14  definition
    4.15 -  top_bool_def: "top = True"
    4.16 +  [simp]: "top \<longleftrightarrow> True"
    4.17  
    4.18  definition
    4.19 -  bot_bool_def: "bot = False"
    4.20 +  [simp]: "bot \<longleftrightarrow> False"
    4.21  
    4.22  instance proof
    4.23 -qed (auto simp add: bot_bool_def top_bool_def less_bool_def, auto simp add: le_bool_def)
    4.24 +qed auto
    4.25  
    4.26  end
    4.27  
    4.28  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    4.29 -  by (simp add: le_bool_def)
    4.30 +  by simp
    4.31  
    4.32  lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    4.33 -  by (simp add: le_bool_def)
    4.34 +  by simp
    4.35  
    4.36  lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    4.37 -  by (simp add: le_bool_def)
    4.38 +  by simp
    4.39  
    4.40  lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    4.41 -  by (simp add: le_bool_def)
    4.42 +  by simp
    4.43  
    4.44  lemma bot_boolE: "bot \<Longrightarrow> P"
    4.45 -  by (simp add: bot_bool_def)
    4.46 +  by simp
    4.47  
    4.48  lemma top_boolI: top
    4.49 -  by (simp add: top_bool_def)
    4.50 +  by simp
    4.51  
    4.52  lemma [code]:
    4.53    "False \<le> b \<longleftrightarrow> True"
    4.54    "True \<le> b \<longleftrightarrow> b"
    4.55    "False < b \<longleftrightarrow> b"
    4.56    "True < b \<longleftrightarrow> False"
    4.57 -  unfolding le_bool_def less_bool_def by simp_all
    4.58 +  by simp_all
    4.59  
    4.60  
    4.61  subsection {* Order on functions *}
    4.62 @@ -1259,7 +1259,7 @@
    4.63    le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    4.64  
    4.65  definition
    4.66 -  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    4.67 +  "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
    4.68  
    4.69  instance ..
    4.70  
    4.71 @@ -1276,11 +1276,15 @@
    4.72  begin
    4.73  
    4.74  definition
    4.75 -  top_fun_def [no_atp]: "top = (\<lambda>x. top)"
    4.76 +  [no_atp]: "top = (\<lambda>x. top)"
    4.77  declare top_fun_def_raw [no_atp]
    4.78  
    4.79 +lemma top_apply:
    4.80 +  "top x = top"
    4.81 +  by (simp add: top_fun_def)
    4.82 +
    4.83  instance proof
    4.84 -qed (simp add: top_fun_def le_fun_def)
    4.85 +qed (simp add: le_fun_def top_apply)
    4.86  
    4.87  end
    4.88  
    4.89 @@ -1288,10 +1292,14 @@
    4.90  begin
    4.91  
    4.92  definition
    4.93 -  bot_fun_def: "bot = (\<lambda>x. bot)"
    4.94 +  "bot = (\<lambda>x. bot)"
    4.95 +
    4.96 +lemma bot_apply:
    4.97 +  "bot x = bot"
    4.98 +  by (simp add: bot_fun_def)
    4.99  
   4.100  instance proof
   4.101 -qed (simp add: bot_fun_def le_fun_def)
   4.102 +qed (simp add: le_fun_def bot_apply)
   4.103  
   4.104  end
   4.105  
     5.1 --- a/src/HOL/Predicate.thy	Wed Dec 08 14:52:23 2010 +0100
     5.2 +++ b/src/HOL/Predicate.thy	Wed Dec 08 14:52:23 2010 +0100
     5.3 @@ -16,6 +16,12 @@
     5.4    top ("\<top>") and
     5.5    bot ("\<bottom>")
     5.6  
     5.7 +syntax (xsymbols)
     5.8 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
     5.9 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    5.10 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    5.11 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    5.12 +
    5.13  
    5.14  subsection {* Predicates as (complete) lattices *}
    5.15  
    5.16 @@ -179,61 +185,61 @@
    5.17  subsubsection {* Unions of families *}
    5.18  
    5.19  lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
    5.20 -  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
    5.21 +  by (simp add: SUPR_apply)
    5.22  
    5.23  lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
    5.24 -  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
    5.25 +  by (simp add: SUPR_apply)
    5.26  
    5.27  lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
    5.28 -  by (auto simp add: SUP1_iff)
    5.29 +  by (auto simp add: SUPR_apply)
    5.30  
    5.31  lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
    5.32 -  by (auto simp add: SUP2_iff)
    5.33 +  by (auto simp add: SUPR_apply)
    5.34  
    5.35  lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
    5.36 -  by (auto simp add: SUP1_iff)
    5.37 +  by (auto simp add: SUPR_apply)
    5.38  
    5.39  lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
    5.40 -  by (auto simp add: SUP2_iff)
    5.41 +  by (auto simp add: SUPR_apply)
    5.42  
    5.43  lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
    5.44 -  by (simp add: SUP1_iff fun_eq_iff)
    5.45 +  by (simp add: SUPR_apply fun_eq_iff)
    5.46  
    5.47  lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
    5.48 -  by (simp add: SUP2_iff fun_eq_iff)
    5.49 +  by (simp add: SUPR_apply fun_eq_iff)
    5.50  
    5.51  
    5.52  subsubsection {* Intersections of families *}
    5.53  
    5.54  lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
    5.55 -  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    5.56 +  by (simp add: INFI_apply)
    5.57  
    5.58  lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
    5.59 -  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    5.60 +  by (simp add: INFI_apply)
    5.61  
    5.62  lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
    5.63 -  by (auto simp add: INF1_iff)
    5.64 +  by (auto simp add: INFI_apply)
    5.65  
    5.66  lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
    5.67 -  by (auto simp add: INF2_iff)
    5.68 +  by (auto simp add: INFI_apply)
    5.69  
    5.70  lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
    5.71 -  by (auto simp add: INF1_iff)
    5.72 +  by (auto simp add: INFI_apply)
    5.73  
    5.74  lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
    5.75 -  by (auto simp add: INF2_iff)
    5.76 +  by (auto simp add: INFI_apply)
    5.77  
    5.78  lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
    5.79 -  by (auto simp add: INF1_iff)
    5.80 +  by (auto simp add: INFI_apply)
    5.81  
    5.82  lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
    5.83 -  by (auto simp add: INF2_iff)
    5.84 +  by (auto simp add: INFI_apply)
    5.85  
    5.86  lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
    5.87 -  by (simp add: INF1_iff fun_eq_iff)
    5.88 +  by (simp add: INFI_apply fun_eq_iff)
    5.89  
    5.90  lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
    5.91 -  by (simp add: INF2_iff fun_eq_iff)
    5.92 +  by (simp add: INFI_apply fun_eq_iff)
    5.93  
    5.94  
    5.95  subsection {* Predicates as relations *}
    5.96 @@ -493,8 +499,7 @@
    5.97    by (simp add: minus_pred_def)
    5.98  
    5.99  instance proof
   5.100 -qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def
   5.101 -  fun_Compl_def fun_diff_def bool_Compl_def bool_diff_def)
   5.102 +qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply)
   5.103  
   5.104  end
   5.105  
   5.106 @@ -514,10 +519,10 @@
   5.107    by (simp add: single_def)
   5.108  
   5.109  definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
   5.110 -  "P \<guillemotright>= f = (SUPR {x. Predicate.eval P x} f)"
   5.111 +  "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
   5.112  
   5.113  lemma eval_bind [simp]:
   5.114 -  "eval (P \<guillemotright>= f) = Predicate.eval (SUPR {x. Predicate.eval P x} f)"
   5.115 +  "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
   5.116    by (simp add: bind_def)
   5.117  
   5.118  lemma bind_bind:
   5.119 @@ -822,7 +827,7 @@
   5.120    "single x = Seq (\<lambda>u. Insert x \<bottom>)"
   5.121    unfolding Seq_def by simp
   5.122  
   5.123 -primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   5.124 +primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   5.125      "apply f Empty = Empty"
   5.126    | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   5.127    | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
   5.128 @@ -972,7 +977,7 @@
   5.129    "the A = (THE x. eval A x)"
   5.130  
   5.131  lemma the_eqI:
   5.132 -  "(THE x. Predicate.eval P x) = x \<Longrightarrow> Predicate.the P = x"
   5.133 +  "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   5.134    by (simp add: the_def)
   5.135  
   5.136  lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
   5.137 @@ -1030,6 +1035,12 @@
   5.138    bot ("\<bottom>") and
   5.139    bind (infixl "\<guillemotright>=" 70)
   5.140  
   5.141 +no_syntax (xsymbols)
   5.142 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   5.143 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   5.144 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   5.145 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   5.146 +
   5.147  hide_type (open) pred seq
   5.148  hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   5.149    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
     6.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
     6.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 14:52:23 2010 +0100
     6.3 @@ -1391,7 +1391,7 @@
     6.4  proof safe
     6.5    fix a
     6.6    have "{x\<in>space M. a < ?sup x} = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
     6.7 -    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_fun_expand[where 'c=pextreal])
     6.8 +    by (auto simp: less_Sup_iff SUPR_def[where 'a=pextreal] SUPR_apply[where 'c=pextreal])
     6.9    then show "{x\<in>space M. a < ?sup x} \<in> sets M"
    6.10      using assms by auto
    6.11  qed
    6.12 @@ -1404,7 +1404,7 @@
    6.13  proof safe
    6.14    fix a
    6.15    have "{x\<in>space M. ?inf x < a} = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
    6.16 -    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_fun_expand)
    6.17 +    by (auto simp: Inf_less_iff INFI_def[where 'a=pextreal] INFI_apply)
    6.18    then show "{x\<in>space M. ?inf x < a} \<in> sets M"
    6.19      using assms by auto
    6.20  qed
    6.21 @@ -1427,7 +1427,7 @@
    6.22    assumes "\<And>i. f i \<in> borel_measurable M"
    6.23    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
    6.24    using assms unfolding psuminf_def
    6.25 -  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
    6.26 +  by (auto intro!: borel_measurable_SUP[unfolded SUPR_apply])
    6.27  
    6.28  section "LIMSEQ is borel measurable"
    6.29  
    6.30 @@ -1456,7 +1456,7 @@
    6.31    with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
    6.32    have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
    6.33         "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
    6.34 -    unfolding SUPR_fun_expand INFI_fun_expand by auto
    6.35 +    unfolding SUPR_apply INFI_apply by auto
    6.36    note this[THEN borel_measurable_real]
    6.37    from borel_measurable_diff[OF this]
    6.38    show ?thesis unfolding * .