- Moved infrastructure for converting between sets and predicates
authorberghofe
Wed Jul 11 11:07:57 2007 +0200 (2007-07-11)
changeset 237411801a921df13
parent 23740 d7f18c837ce7
child 23742 d6349ac8b153
- Moved infrastructure for converting between sets and predicates
to Tools/inductive_set_package.ML
- Adapted conversion rules to new format (now use standard op :
and Collect operators rather than Collect2 and member(2))
- Removed bounded quantifiers for predicates
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Wed Jul 11 11:04:39 2007 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Jul 11 11:07:57 2007 +0200
     1.3 @@ -9,202 +9,46 @@
     1.4  imports Inductive Relation
     1.5  begin
     1.6  
     1.7 -subsection {* Converting between predicates and sets *}
     1.8 -
     1.9 -definition
    1.10 -  member :: "'a set => 'a => bool" where
    1.11 -  "member == %S x. x : S"
    1.12 -
    1.13 -lemma memberI[intro!, Pure.intro!]: "x : S ==> member S x"
    1.14 -  by (simp add: member_def)
    1.15 -
    1.16 -lemma memberD[dest!, Pure.dest!]: "member S x ==> x : S"
    1.17 -  by (simp add: member_def)
    1.18 -
    1.19 -lemma member_eq[simp]: "member S x = (x : S)"
    1.20 -  by (simp add: member_def)
    1.21 -
    1.22 -lemma member_Collect_eq[simp]: "member (Collect P) = P"
    1.23 -  by (simp add: member_def)
    1.24 -
    1.25 -lemma Collect_member_eq[simp]: "Collect (member S) = S"
    1.26 -  by (simp add: member_def)
    1.27 -
    1.28 -lemma split_set: "(!!S. PROP P S) == (!!S. PROP P (Collect S))"
    1.29 -proof
    1.30 -  fix S
    1.31 -  assume "!!S. PROP P S"
    1.32 -  then show "PROP P (Collect S)" .
    1.33 -next
    1.34 -  fix S
    1.35 -  assume "!!S. PROP P (Collect S)"
    1.36 -  then have "PROP P {x. x : S}" .
    1.37 -  thus "PROP P S" by simp
    1.38 -qed
    1.39 -
    1.40 -lemma split_predicate: "(!!S. PROP P S) == (!!S. PROP P (member S))"
    1.41 -proof
    1.42 -  fix S
    1.43 -  assume "!!S. PROP P S"
    1.44 -  then show "PROP P (member S)" .
    1.45 -next
    1.46 -  fix S
    1.47 -  assume "!!S. PROP P (member S)"
    1.48 -  then have "PROP P (member {x. S x})" .
    1.49 -  thus "PROP P S" by simp
    1.50 -qed
    1.51 -
    1.52 -lemma member_right_eq: "(x == member y) == (Collect x == y)"
    1.53 -  by (rule equal_intr_rule, simp, drule symmetric, simp)
    1.54 -
    1.55 -definition
    1.56 -  member2 :: "('a * 'b) set => 'a => 'b \<Rightarrow> bool" where
    1.57 -  "member2 == %S x y. (x, y) : S"
    1.58 -
    1.59 -definition
    1.60 -  Collect2 :: "('a => 'b => bool) => ('a * 'b) set" where
    1.61 -  "Collect2 == %P. {(x, y). P x y}"
    1.62 -
    1.63 -lemma member2I[intro!, Pure.intro!]: "(x, y) : S ==> member2 S x y"
    1.64 -  by (simp add: member2_def)
    1.65 -
    1.66 -lemma member2D[dest!, Pure.dest!]: "member2 S x y ==> (x, y) : S"
    1.67 -  by (simp add: member2_def)
    1.68 -
    1.69 -lemma member2_eq[simp]: "member2 S x y = ((x, y) : S)"
    1.70 -  by (simp add: member2_def)
    1.71 -
    1.72 -lemma Collect2I: "P x y ==> (x, y) : Collect2 P"
    1.73 -  by (simp add: Collect2_def)
    1.74 -
    1.75 -lemma Collect2D: "(x, y) : Collect2 P ==> P x y"
    1.76 -  by (simp add: Collect2_def)
    1.77 -
    1.78 -lemma member2_Collect2_eq[simp]: "member2 (Collect2 P) = P"
    1.79 -  by (simp add: member2_def Collect2_def)
    1.80 -
    1.81 -lemma Collect2_member2_eq[simp]: "Collect2 (member2 S) = S"
    1.82 -  by (auto simp add: member2_def Collect2_def)
    1.83 -
    1.84 -lemma mem_Collect2_eq[iff]: "((x, y) : Collect2 P) = P x y"
    1.85 -  by (iprover intro: Collect2I dest: Collect2D)
    1.86 -
    1.87 -lemma member2_Collect_split_eq [simp]: "member2 (Collect (split P)) = P"
    1.88 -  by (simp add: expand_fun_eq)
    1.89 +subsection {* Equality and Subsets *}
    1.90  
    1.91 -lemma split_set2: "(!!S. PROP P S) == (!!S. PROP P (Collect2 S))"
    1.92 -proof
    1.93 -  fix S
    1.94 -  assume "!!S. PROP P S"
    1.95 -  then show "PROP P (Collect2 S)" .
    1.96 -next
    1.97 -  fix S
    1.98 -  assume "!!S. PROP P (Collect2 S)"
    1.99 -  then have "PROP P (Collect2 (member2 S))" .
   1.100 -  thus "PROP P S" by simp
   1.101 -qed
   1.102 -
   1.103 -lemma split_predicate2: "(!!S. PROP P S) == (!!S. PROP P (member2 S))"
   1.104 -proof
   1.105 -  fix S
   1.106 -  assume "!!S. PROP P S"
   1.107 -  then show "PROP P (member2 S)" .
   1.108 -next
   1.109 -  fix S
   1.110 -  assume "!!S. PROP P (member2 S)"
   1.111 -  then have "PROP P (member2 (Collect2 S))" .
   1.112 -  thus "PROP P S" by simp
   1.113 -qed
   1.114 -
   1.115 -lemma member2_right_eq: "(x == member2 y) == (Collect2 x == y)"
   1.116 -  by (rule equal_intr_rule, simp, drule symmetric, simp)
   1.117 -
   1.118 -ML_setup {*
   1.119 -local
   1.120 -
   1.121 -fun vars_of b (v as Var _) = if b then [] else [v]
   1.122 -  | vars_of b (t $ u) = vars_of true t union vars_of false u
   1.123 -  | vars_of b (Abs (_, _, t)) = vars_of false t
   1.124 -  | vars_of _ _ = [];
   1.125 -
   1.126 -fun rew ths1 ths2 th = Drule.forall_elim_vars 0
   1.127 -  (rewrite_rule ths2 (rewrite_rule ths1 (Drule.forall_intr_list
   1.128 -    (map (cterm_of (theory_of_thm th)) (vars_of false (prop_of th))) th)));
   1.129 -
   1.130 -val get_eq = Simpdata.mk_eq o thm;
   1.131 +lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
   1.132 +  by (auto simp add: expand_fun_eq)
   1.133  
   1.134 -val split_predicate = get_eq "split_predicate";
   1.135 -val split_predicate2 = get_eq "split_predicate2";
   1.136 -val split_set = get_eq "split_set";
   1.137 -val split_set2 = get_eq "split_set2";
   1.138 -val member_eq = get_eq "member_eq";
   1.139 -val member2_eq = get_eq "member2_eq";
   1.140 -val member_Collect_eq = get_eq "member_Collect_eq";
   1.141 -val member2_Collect2_eq = get_eq "member2_Collect2_eq";
   1.142 -val mem_Collect2_eq = get_eq "mem_Collect2_eq";
   1.143 -val member_right_eq = thm "member_right_eq";
   1.144 -val member2_right_eq = thm "member2_right_eq";
   1.145 -
   1.146 -val rew' = Thm.symmetric o rew [split_set2] [split_set,
   1.147 -  member_right_eq, member2_right_eq, member_Collect_eq, member2_Collect2_eq];
   1.148 -
   1.149 -val rules1 = [split_predicate, split_predicate2, member_eq, member2_eq];
   1.150 -val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
   1.151 -
   1.152 -structure PredSetConvData = GenericDataFun
   1.153 -(
   1.154 -  type T = thm list;
   1.155 -  val empty = [];
   1.156 -  val extend = I;
   1.157 -  fun merge _ = Drule.merge_rules;
   1.158 -);
   1.159 -
   1.160 -fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
   1.161 -  Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
   1.162 -    (ths @ PredSetConvData.get ctxt) @ ths2))));
   1.163 -
   1.164 -val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute
   1.165 -  (Drule.add_rule #> PredSetConvData.map));
   1.166 -
   1.167 -in
   1.168 -
   1.169 -val _ = ML_Context.>> (
   1.170 -  Attrib.add_attributes
   1.171 -    [("pred_set_conv", pred_set_conv_att,
   1.172 -        "declare rules for converting between predicate and set notation"),
   1.173 -     ("to_set", mk_attr [] rules1 I, "convert rule to set notation"),
   1.174 -     ("to_pred", mk_attr [split_set2] rules2 rew',
   1.175 -        "convert rule to predicate notation")])
   1.176 -
   1.177 -end;
   1.178 -*}
   1.179 -
   1.180 -lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)"
   1.181 +lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
   1.182    by (auto simp add: expand_fun_eq)
   1.183  
   1.184 -lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)"
   1.185 -  by (auto simp add: expand_fun_eq)
   1.186 -
   1.187 -lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)"
   1.188 +lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
   1.189    by fast
   1.190  
   1.191 -lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)"
   1.192 +lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
   1.193    by fast
   1.194  
   1.195 -lemma member_empty [pred_set_conv]: "(%x. False) = member {}"
   1.196 -  by (simp add: expand_fun_eq)
   1.197 +
   1.198 +subsection {* Top and bottom elements *}
   1.199 +
   1.200 +lemma top1I [intro!]: "top x"
   1.201 +  by (simp add: top_fun_eq top_bool_eq)
   1.202  
   1.203 -lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}"
   1.204 -  by (simp add: expand_fun_eq)
   1.205 +lemma top2I [intro!]: "top x y"
   1.206 +  by (simp add: top_fun_eq top_bool_eq)
   1.207 +
   1.208 +lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
   1.209 +  by (simp add: bot_fun_eq bot_bool_eq)
   1.210 +
   1.211 +lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
   1.212 +  by (simp add: bot_fun_eq bot_bool_eq)
   1.213  
   1.214  
   1.215 -subsubsection {* Binary union *}
   1.216 +subsection {* The empty set *}
   1.217 +
   1.218 +lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   1.219 +  by (auto simp add: expand_fun_eq)
   1.220  
   1.221 -lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)"
   1.222 -  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
   1.223 +lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
   1.224 +  by (auto simp add: expand_fun_eq)
   1.225  
   1.226 -lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)"
   1.227 -  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
   1.228 +
   1.229 +subsection {* Binary union *}
   1.230  
   1.231  lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
   1.232    by (simp add: sup_fun_eq sup_bool_eq)
   1.233 @@ -212,16 +56,22 @@
   1.234  lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
   1.235    by (simp add: sup_fun_eq sup_bool_eq)
   1.236  
   1.237 +lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   1.238 +  by (simp add: expand_fun_eq)
   1.239 +
   1.240 +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.241 +  by (simp add: expand_fun_eq)
   1.242 +
   1.243  lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
   1.244    by simp
   1.245  
   1.246  lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
   1.247    by simp
   1.248  
   1.249 -lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   1.250 +lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   1.251    by simp
   1.252  
   1.253 -lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   1.254 +lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   1.255    by simp
   1.256  
   1.257  text {*
   1.258 @@ -242,13 +92,7 @@
   1.259    by simp iprover
   1.260  
   1.261  
   1.262 -subsubsection {* Binary intersection *}
   1.263 -
   1.264 -lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)"
   1.265 -  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
   1.266 -
   1.267 -lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)"
   1.268 -  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
   1.269 +subsection {* Binary intersection *}
   1.270  
   1.271  lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
   1.272    by (simp add: inf_fun_eq inf_bool_eq)
   1.273 @@ -256,6 +100,12 @@
   1.274  lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
   1.275    by (simp add: inf_fun_eq inf_bool_eq)
   1.276  
   1.277 +lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   1.278 +  by (simp add: expand_fun_eq)
   1.279 +
   1.280 +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.281 +  by (simp add: expand_fun_eq)
   1.282 +
   1.283  lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
   1.284    by simp
   1.285  
   1.286 @@ -281,13 +131,7 @@
   1.287    by simp
   1.288  
   1.289  
   1.290 -subsubsection {* Unions of families *}
   1.291 -
   1.292 -lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
   1.293 -  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
   1.294 -
   1.295 -lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
   1.296 -  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
   1.297 +subsection {* Unions of families *}
   1.298  
   1.299  lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
   1.300    by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
   1.301 @@ -307,14 +151,14 @@
   1.302  lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
   1.303    by auto
   1.304  
   1.305 -
   1.306 -subsubsection {* Intersections of families *}
   1.307 +lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
   1.308 +  by (simp add: expand_fun_eq)
   1.309  
   1.310 -lemma member_INF: "(INF i. member (r i)) = member (INT i. r i)"
   1.311 -  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
   1.312 +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.313 +  by (simp add: expand_fun_eq)
   1.314  
   1.315 -lemma member2_INF: "(INF i. member2 (r i)) = member2 (INT i. r i)"
   1.316 -  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
   1.317 +
   1.318 +subsection {* Intersections of families *}
   1.319  
   1.320  lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
   1.321    by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
   1.322 @@ -340,26 +184,32 @@
   1.323  lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
   1.324    by auto
   1.325  
   1.326 +lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
   1.327 +  by (simp add: expand_fun_eq)
   1.328 +
   1.329 +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.330 +  by (simp add: expand_fun_eq)
   1.331 +
   1.332  
   1.333  subsection {* Composition of two relations *}
   1.334  
   1.335 -inductive2
   1.336 +inductive
   1.337    pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
   1.338      (infixr "OO" 75)
   1.339    for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
   1.340  where
   1.341    pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
   1.342  
   1.343 -inductive_cases2 pred_compE [elim!]: "(r OO s) a c"
   1.344 +inductive_cases pred_compE [elim!]: "(r OO s) a c"
   1.345  
   1.346  lemma pred_comp_rel_comp_eq [pred_set_conv]:
   1.347 -  "(member2 r OO member2 s) = member2 (r O s)"
   1.348 +  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   1.349    by (auto simp add: expand_fun_eq elim: pred_compE)
   1.350  
   1.351  
   1.352  subsection {* Converse *}
   1.353  
   1.354 -inductive2
   1.355 +inductive
   1.356    conversep :: "('a => 'b => bool) => 'b => 'a => bool"
   1.357      ("(_^--1)" [1000] 1000)
   1.358    for r :: "'a => 'b => bool"
   1.359 @@ -378,7 +228,7 @@
   1.360    by (iprover intro: conversepI dest: conversepD)
   1.361  
   1.362  lemma conversep_converse_eq [pred_set_conv]:
   1.363 -  "(member2 r)^--1 = member2 (r^-1)"
   1.364 +  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   1.365    by (auto simp add: expand_fun_eq)
   1.366  
   1.367  lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   1.368 @@ -405,29 +255,29 @@
   1.369  
   1.370  subsection {* Domain *}
   1.371  
   1.372 -inductive2
   1.373 +inductive
   1.374    DomainP :: "('a => 'b => bool) => 'a => bool"
   1.375    for r :: "'a => 'b => bool"
   1.376  where
   1.377    DomainPI [intro]: "r a b ==> DomainP r a"
   1.378  
   1.379 -inductive_cases2 DomainPE [elim!]: "DomainP r a"
   1.380 +inductive_cases DomainPE [elim!]: "DomainP r a"
   1.381  
   1.382 -lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)"
   1.383 +lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
   1.384    by (blast intro!: Orderings.order_antisym)
   1.385  
   1.386  
   1.387  subsection {* Range *}
   1.388  
   1.389 -inductive2
   1.390 +inductive
   1.391    RangeP :: "('a => 'b => bool) => 'b => bool"
   1.392    for r :: "'a => 'b => bool"
   1.393  where
   1.394    RangePI [intro]: "r a b ==> RangeP r b"
   1.395  
   1.396 -inductive_cases2 RangePE [elim!]: "RangeP r b"
   1.397 +inductive_cases RangePE [elim!]: "RangeP r b"
   1.398  
   1.399 -lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)"
   1.400 +lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
   1.401    by (blast intro!: Orderings.order_antisym)
   1.402  
   1.403  
   1.404 @@ -437,77 +287,31 @@
   1.405    inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
   1.406    "inv_imagep r f == %x y. r (f x) (f y)"
   1.407  
   1.408 -lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)"
   1.409 +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.410    by (simp add: inv_image_def inv_imagep_def)
   1.411  
   1.412  lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   1.413    by (simp add: inv_imagep_def)
   1.414  
   1.415  
   1.416 +subsection {* The Powerset operator *}
   1.417 +
   1.418 +definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.419 +  "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
   1.420 +
   1.421 +lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   1.422 +  by (auto simp add: Powp_def expand_fun_eq)
   1.423 +
   1.424 +
   1.425  subsection {* Properties of relations - predicate versions *}
   1.426  
   1.427  abbreviation antisymP :: "('a => 'a => bool) => bool" where
   1.428 -  "antisymP r == antisym (Collect2 r)"
   1.429 +  "antisymP r == antisym {(x, y). r x y}"
   1.430  
   1.431  abbreviation transP :: "('a => 'a => bool) => bool" where
   1.432 -  "transP r == trans (Collect2 r)"
   1.433 +  "transP r == trans {(x, y). r x y}"
   1.434  
   1.435  abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   1.436 -  "single_valuedP r == single_valued (Collect2 r)"
   1.437 -
   1.438 -
   1.439 -subsection {* Bounded quantifiers for predicates *}
   1.440 -
   1.441 -text {*
   1.442 -Bounded existential quantifier for predicates (executable).
   1.443 -*}
   1.444 -
   1.445 -inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.446 -  for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool"
   1.447 -where
   1.448 -  bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q"
   1.449 -
   1.450 -lemmas bexpE [elim!] = bexp.cases
   1.451 -
   1.452 -syntax
   1.453 -  Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10)
   1.454 -
   1.455 -translations
   1.456 -  "\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)"
   1.457 -
   1.458 -constdefs
   1.459 -  ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.460 -  "ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x"
   1.461 -
   1.462 -syntax
   1.463 -  Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10)
   1.464 -
   1.465 -translations
   1.466 -  "\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)"
   1.467 -
   1.468 -(* To avoid eta-contraction of body: *)
   1.469 -print_translation {*
   1.470 -let
   1.471 -  fun btr' syn [A,Abs abs] =
   1.472 -    let val (x,t) = atomic_abs_tr' abs
   1.473 -    in Syntax.const syn $ x $ A $ t end
   1.474 -in
   1.475 -[("ballp", btr' "Ballp"),("bexp", btr' "Bexp")]
   1.476 -end
   1.477 -*}
   1.478 -
   1.479 -lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x"
   1.480 -  by (simp add: ballp_def)
   1.481 -
   1.482 -lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x"
   1.483 -  by (simp add: ballp_def)
   1.484 -
   1.485 -lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q"
   1.486 -  by (unfold ballp_def) blast
   1.487 -
   1.488 -lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))"
   1.489 -  by (blast dest: bspecp)
   1.490 -
   1.491 -declare ballp_not_bexp_eq [THEN eq_reflection, code unfold]
   1.492 +  "single_valuedP r == single_valued {(x, y). r x y}"
   1.493  
   1.494  end