src/HOL/Predicate.thy
changeset 44414 fb25c131bd73
parent 44363 53f4f8287606
child 44415 ce6cd1b2344b
     1.1 --- a/src/HOL/Predicate.thy	Tue Aug 23 03:34:17 2011 +0900
     1.2 +++ b/src/HOL/Predicate.thy	Mon Aug 22 22:00:36 2011 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4    done
     1.5  
     1.6  lemma rev_predicate1D:
     1.7 -  "P x ==> P <= Q ==> Q x"
     1.8 +  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
     1.9    by (rule predicate1D)
    1.10  
    1.11  lemma predicate2I [Pure.intro!, intro!]:
    1.12 @@ -67,7 +67,7 @@
    1.13    done
    1.14  
    1.15  lemma rev_predicate2D:
    1.16 -  "P x y ==> P <= Q ==> Q x y"
    1.17 +  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
    1.18    by (rule predicate2D)
    1.19  
    1.20  
    1.21 @@ -82,85 +82,85 @@
    1.22  
    1.23  subsubsection {* Order relation *}
    1.24  
    1.25 -lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
    1.26 +lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) = (R \<subseteq> S)"
    1.27    by (simp add: mem_def)
    1.28  
    1.29 -lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
    1.30 +lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) = (R \<subseteq> S)"
    1.31    by fast
    1.32  
    1.33  
    1.34  subsubsection {* Top and bottom elements *}
    1.35  
    1.36 -lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
    1.37 +lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
    1.38    by (simp add: bot_fun_def)
    1.39  
    1.40 -lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    1.41 +lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
    1.42    by (simp add: bot_fun_def)
    1.43  
    1.44 -lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
    1.45 +lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    1.46    by (auto simp add: fun_eq_iff)
    1.47  
    1.48 -lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
    1.49 +lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.50    by (auto simp add: fun_eq_iff)
    1.51  
    1.52 -lemma top1I [intro!]: "top x"
    1.53 +lemma top1I [intro!]: "\<top> x"
    1.54    by (simp add: top_fun_def)
    1.55  
    1.56 -lemma top2I [intro!]: "top x y"
    1.57 +lemma top2I [intro!]: "\<top> x y"
    1.58    by (simp add: top_fun_def)
    1.59  
    1.60  
    1.61  subsubsection {* Binary intersection *}
    1.62  
    1.63 -lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
    1.64 +lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    1.65    by (simp add: inf_fun_def)
    1.66  
    1.67 -lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
    1.68 +lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    1.69    by (simp add: inf_fun_def)
    1.70  
    1.71 -lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
    1.72 +lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    1.73    by (simp add: inf_fun_def)
    1.74  
    1.75 -lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
    1.76 +lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    1.77    by (simp add: inf_fun_def)
    1.78  
    1.79 -lemma inf1D1: "inf A B x ==> A x"
    1.80 +lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    1.81    by (simp add: inf_fun_def)
    1.82  
    1.83 -lemma inf2D1: "inf A B x y ==> A x y"
    1.84 +lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    1.85    by (simp add: inf_fun_def)
    1.86  
    1.87 -lemma inf1D2: "inf A B x ==> B x"
    1.88 +lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    1.89    by (simp add: inf_fun_def)
    1.90  
    1.91 -lemma inf2D2: "inf A B x y ==> B x y"
    1.92 +lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    1.93    by (simp add: inf_fun_def)
    1.94  
    1.95 -lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.96 +lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.97    by (simp add: inf_fun_def mem_def)
    1.98  
    1.99 -lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   1.100 +lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   1.101    by (simp add: inf_fun_def mem_def)
   1.102  
   1.103  
   1.104  subsubsection {* Binary union *}
   1.105  
   1.106 -lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
   1.107 +lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   1.108    by (simp add: sup_fun_def)
   1.109  
   1.110 -lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
   1.111 +lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   1.112    by (simp add: sup_fun_def)
   1.113  
   1.114 -lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   1.115 +lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   1.116    by (simp add: sup_fun_def)
   1.117  
   1.118 -lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   1.119 +lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   1.120    by (simp add: sup_fun_def)
   1.121  
   1.122 -lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   1.123 +lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   1.124    by (simp add: sup_fun_def) iprover
   1.125  
   1.126 -lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   1.127 +lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   1.128    by (simp add: sup_fun_def) iprover
   1.129  
   1.130  text {*
   1.131 @@ -168,76 +168,76 @@
   1.132    @{text B}.
   1.133  *}
   1.134  
   1.135 -lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
   1.136 +lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   1.137    by (auto simp add: sup_fun_def)
   1.138  
   1.139 -lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
   1.140 +lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   1.141    by (auto simp add: sup_fun_def)
   1.142  
   1.143 -lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   1.144 +lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   1.145    by (simp add: sup_fun_def mem_def)
   1.146  
   1.147 -lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   1.148 +lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   1.149    by (simp add: sup_fun_def mem_def)
   1.150  
   1.151  
   1.152  subsubsection {* Intersections of families *}
   1.153  
   1.154 -lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
   1.155 +lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
   1.156    by (simp add: INFI_apply)
   1.157  
   1.158 -lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
   1.159 +lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   1.160    by (simp add: INFI_apply)
   1.161  
   1.162 -lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
   1.163 +lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   1.164    by (auto simp add: INFI_apply)
   1.165  
   1.166 -lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
   1.167 +lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   1.168    by (auto simp add: INFI_apply)
   1.169  
   1.170 -lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
   1.171 +lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   1.172    by (auto simp add: INFI_apply)
   1.173  
   1.174 -lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
   1.175 +lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   1.176    by (auto simp add: INFI_apply)
   1.177  
   1.178 -lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
   1.179 +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.180    by (auto simp add: INFI_apply)
   1.181  
   1.182 -lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
   1.183 +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.184    by (auto simp add: INFI_apply)
   1.185  
   1.186 -lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
   1.187 +lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   1.188    by (simp add: INFI_apply fun_eq_iff)
   1.189  
   1.190 -lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
   1.191 +lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
   1.192    by (simp add: INFI_apply fun_eq_iff)
   1.193  
   1.194  
   1.195  subsubsection {* Unions of families *}
   1.196  
   1.197 -lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
   1.198 +lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   1.199    by (simp add: SUPR_apply)
   1.200  
   1.201 -lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
   1.202 +lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   1.203    by (simp add: SUPR_apply)
   1.204  
   1.205 -lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
   1.206 +lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   1.207    by (auto simp add: SUPR_apply)
   1.208  
   1.209 -lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
   1.210 +lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   1.211    by (auto simp add: SUPR_apply)
   1.212  
   1.213 -lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
   1.214 +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.215    by (auto simp add: SUPR_apply)
   1.216  
   1.217 -lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
   1.218 +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.219    by (auto simp add: SUPR_apply)
   1.220  
   1.221 -lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
   1.222 +lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   1.223    by (simp add: SUPR_apply fun_eq_iff)
   1.224  
   1.225 -lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
   1.226 +lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
   1.227    by (simp add: SUPR_apply fun_eq_iff)
   1.228  
   1.229  
   1.230 @@ -245,12 +245,9 @@
   1.231  
   1.232  subsubsection {* Composition  *}
   1.233  
   1.234 -inductive
   1.235 -  pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
   1.236 -    (infixr "OO" 75)
   1.237 -  for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
   1.238 -where
   1.239 -  pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
   1.240 +inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
   1.241 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
   1.242 +  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
   1.243  
   1.244  inductive_cases pred_compE [elim!]: "(r OO s) a c"
   1.245  
   1.246 @@ -261,12 +258,9 @@
   1.247  
   1.248  subsubsection {* Converse *}
   1.249  
   1.250 -inductive
   1.251 -  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
   1.252 -    ("(_^--1)" [1000] 1000)
   1.253 -  for r :: "'a => 'b => bool"
   1.254 -where
   1.255 -  conversepI: "r a b ==> r^--1 b a"
   1.256 +inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
   1.257 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.258 +  conversepI: "r a b \<Longrightarrow> r^--1 b a"
   1.259  
   1.260  notation (xsymbols)
   1.261    conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   1.262 @@ -290,13 +284,13 @@
   1.263    by (iprover intro: order_antisym conversepI pred_compI
   1.264      elim: pred_compE dest: conversepD)
   1.265  
   1.266 -lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
   1.267 +lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   1.268    by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
   1.269  
   1.270 -lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
   1.271 +lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   1.272    by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
   1.273  
   1.274 -lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
   1.275 +lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   1.276    by (auto simp add: fun_eq_iff)
   1.277  
   1.278  lemma conversep_eq [simp]: "(op =)^--1 = op ="
   1.279 @@ -305,11 +299,9 @@
   1.280  
   1.281  subsubsection {* Domain *}
   1.282  
   1.283 -inductive
   1.284 -  DomainP :: "('a => 'b => bool) => 'a => bool"
   1.285 -  for r :: "'a => 'b => bool"
   1.286 -where
   1.287 -  DomainPI [intro]: "r a b ==> DomainP r a"
   1.288 +inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   1.289 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.290 +  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
   1.291  
   1.292  inductive_cases DomainPE [elim!]: "DomainP r a"
   1.293  
   1.294 @@ -319,11 +311,9 @@
   1.295  
   1.296  subsubsection {* Range *}
   1.297  
   1.298 -inductive
   1.299 -  RangeP :: "('a => 'b => bool) => 'b => bool"
   1.300 -  for r :: "'a => 'b => bool"
   1.301 -where
   1.302 -  RangePI [intro]: "r a b ==> RangeP r b"
   1.303 +inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
   1.304 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
   1.305 +  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
   1.306  
   1.307  inductive_cases RangePE [elim!]: "RangeP r b"
   1.308  
   1.309 @@ -333,9 +323,8 @@
   1.310  
   1.311  subsubsection {* Inverse image *}
   1.312  
   1.313 -definition
   1.314 -  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
   1.315 -  "inv_imagep r f == %x y. r (f x) (f y)"
   1.316 +definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
   1.317 +  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
   1.318  
   1.319  lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
   1.320    by (simp add: inv_image_def inv_imagep_def)
   1.321 @@ -347,7 +336,7 @@
   1.322  subsubsection {* Powerset *}
   1.323  
   1.324  definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.325 -  "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
   1.326 +  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
   1.327  
   1.328  lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   1.329    by (auto simp add: Powp_def fun_eq_iff)
   1.330 @@ -357,14 +346,14 @@
   1.331  
   1.332  subsubsection {* Properties of relations *}
   1.333  
   1.334 -abbreviation antisymP :: "('a => 'a => bool) => bool" where
   1.335 -  "antisymP r == antisym {(x, y). r x y}"
   1.336 +abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.337 +  "antisymP r \<equiv> antisym {(x, y). r x y}"
   1.338  
   1.339 -abbreviation transP :: "('a => 'a => bool) => bool" where
   1.340 -  "transP r == trans {(x, y). r x y}"
   1.341 +abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   1.342 +  "transP r \<equiv> trans {(x, y). r x y}"
   1.343  
   1.344 -abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   1.345 -  "single_valuedP r == single_valued {(x, y). r x y}"
   1.346 +abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.347 +  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
   1.348  
   1.349  (*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
   1.350  
   1.351 @@ -801,9 +790,9 @@
   1.352  datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
   1.353  
   1.354  primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
   1.355 -    "pred_of_seq Empty = \<bottom>"
   1.356 -  | "pred_of_seq (Insert x P) = single x \<squnion> P"
   1.357 -  | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
   1.358 +  "pred_of_seq Empty = \<bottom>"
   1.359 +| "pred_of_seq (Insert x P) = single x \<squnion> P"
   1.360 +| "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
   1.361  
   1.362  definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
   1.363    "Seq f = pred_of_seq (f ())"
   1.364 @@ -812,8 +801,8 @@
   1.365  
   1.366  primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
   1.367    "member Empty x \<longleftrightarrow> False"
   1.368 -  | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
   1.369 -  | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
   1.370 +| "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
   1.371 +| "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
   1.372  
   1.373  lemma eval_member:
   1.374    "member xq = eval (pred_of_seq xq)"
   1.375 @@ -973,23 +962,21 @@
   1.376     (auto simp add: Seq_def the_only_singleton is_empty_def
   1.377        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
   1.378  
   1.379 -definition not_unique :: "'a pred => 'a"
   1.380 -where
   1.381 -  [code del]: "not_unique A = (THE x. eval A x)"
   1.382 -
   1.383 -definition the :: "'a pred => 'a"
   1.384 -where
   1.385 +definition the :: "'a pred \<Rightarrow> 'a" where
   1.386    "the A = (THE x. eval A x)"
   1.387  
   1.388  lemma the_eqI:
   1.389    "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   1.390    by (simp add: the_def)
   1.391  
   1.392 +definition not_unique :: "'a pred \<Rightarrow> 'a" where
   1.393 +  [code del]: "not_unique A = (THE x. eval A x)"
   1.394 +
   1.395 +code_abort not_unique
   1.396 +
   1.397  lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
   1.398    by (rule the_eqI) (simp add: singleton_def not_unique_def)
   1.399  
   1.400 -code_abort not_unique
   1.401 -
   1.402  code_reflect Predicate
   1.403    datatypes pred = Seq and seq = Empty | Insert | Join
   1.404    functions map