New theory for converting between predicates and sets.
authorberghofe
Wed Feb 07 17:25:39 2007 +0100 (2007-02-07)
changeset 22259476604be7d88
parent 22258 0967b03844b5
child 22260 45f01828cb69
New theory for converting between predicates and sets.
src/HOL/Predicate.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Predicate.thy	Wed Feb 07 17:25:39 2007 +0100
     1.3 @@ -0,0 +1,482 @@
     1.4 +(*  Title:      HOL/Predicate.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Predicates *}
    1.10 +
    1.11 +theory Predicate
    1.12 +imports Inductive
    1.13 +begin
    1.14 +
    1.15 +subsection {* Converting between predicates and sets *}
    1.16 +
    1.17 +definition
    1.18 +  member :: "'a set => 'a => bool" where
    1.19 +  "member == %S x. x : S"
    1.20 +
    1.21 +lemma memberI[intro!, Pure.intro!]: "x : S ==> member S x"
    1.22 +  by (simp add: member_def)
    1.23 +
    1.24 +lemma memberD[dest!, Pure.dest!]: "member S x ==> x : S"
    1.25 +  by (simp add: member_def)
    1.26 +
    1.27 +lemma member_eq[simp]: "member S x = (x : S)"
    1.28 +  by (simp add: member_def)
    1.29 +
    1.30 +lemma member_Collect_eq[simp]: "member (Collect P) = P"
    1.31 +  by (simp add: member_def)
    1.32 +
    1.33 +lemma Collect_member_eq[simp]: "Collect (member S) = S"
    1.34 +  by (simp add: member_def)
    1.35 +
    1.36 +lemma split_set: "(!!S. PROP P S) == (!!S. PROP P (Collect S))"
    1.37 +proof
    1.38 +  fix S
    1.39 +  assume "!!S. PROP P S"
    1.40 +  show "PROP P (Collect S)" .
    1.41 +next
    1.42 +  fix S
    1.43 +  assume "!!S. PROP P (Collect S)"
    1.44 +  have "PROP P {x. x : S}" .
    1.45 +  thus "PROP P S" by simp
    1.46 +qed
    1.47 +
    1.48 +lemma split_predicate: "(!!S. PROP P S) == (!!S. PROP P (member S))"
    1.49 +proof
    1.50 +  fix S
    1.51 +  assume "!!S. PROP P S"
    1.52 +  show "PROP P (member S)" .
    1.53 +next
    1.54 +  fix S
    1.55 +  assume "!!S. PROP P (member S)"
    1.56 +  have "PROP P (member {x. S x})" .
    1.57 +  thus "PROP P S" by simp
    1.58 +qed
    1.59 +
    1.60 +lemma member_right_eq: "(x == member y) == (Collect x == y)"
    1.61 +  by (rule equal_intr_rule, simp, drule symmetric, simp)
    1.62 +
    1.63 +definition
    1.64 +  member2 :: "('a * 'b) set => 'a => 'b \<Rightarrow> bool" where
    1.65 +  "member2 == %S x y. (x, y) : S"
    1.66 +
    1.67 +definition
    1.68 +  Collect2 :: "('a => 'b => bool) => ('a * 'b) set" where
    1.69 +  "Collect2 == %P. {(x, y). P x y}"
    1.70 +
    1.71 +lemma member2I[intro!, Pure.intro!]: "(x, y) : S ==> member2 S x y"
    1.72 +  by (simp add: member2_def)
    1.73 +
    1.74 +lemma member2D[dest!, Pure.dest!]: "member2 S x y ==> (x, y) : S"
    1.75 +  by (simp add: member2_def)
    1.76 +
    1.77 +lemma member2_eq[simp]: "member2 S x y = ((x, y) : S)"
    1.78 +  by (simp add: member2_def)
    1.79 +
    1.80 +lemma Collect2I: "P x y ==> (x, y) : Collect2 P"
    1.81 +  by (simp add: Collect2_def)
    1.82 +
    1.83 +lemma Collect2D: "(x, y) : Collect2 P ==> P x y"
    1.84 +  by (simp add: Collect2_def)
    1.85 +
    1.86 +lemma member2_Collect2_eq[simp]: "member2 (Collect2 P) = P"
    1.87 +  by (simp add: member2_def Collect2_def)
    1.88 +
    1.89 +lemma Collect2_member2_eq[simp]: "Collect2 (member2 S) = S"
    1.90 +  by (auto simp add: member2_def Collect2_def)
    1.91 +
    1.92 +lemma mem_Collect2_eq[iff]: "((x, y) : Collect2 P) = P x y"
    1.93 +  by (iprover intro: Collect2I dest: Collect2D)
    1.94 +
    1.95 +lemma member2_Collect_split_eq [simp]: "member2 (Collect (split P)) = P"
    1.96 +  by (simp add: expand_fun_eq)
    1.97 +
    1.98 +lemma split_set2: "(!!S. PROP P S) == (!!S. PROP P (Collect2 S))"
    1.99 +proof
   1.100 +  fix S
   1.101 +  assume "!!S. PROP P S"
   1.102 +  show "PROP P (Collect2 S)" .
   1.103 +next
   1.104 +  fix S
   1.105 +  assume "!!S. PROP P (Collect2 S)"
   1.106 +  have "PROP P (Collect2 (member2 S))" .
   1.107 +  thus "PROP P S" by simp
   1.108 +qed
   1.109 +
   1.110 +lemma split_predicate2: "(!!S. PROP P S) == (!!S. PROP P (member2 S))"
   1.111 +proof
   1.112 +  fix S
   1.113 +  assume "!!S. PROP P S"
   1.114 +  show "PROP P (member2 S)" .
   1.115 +next
   1.116 +  fix S
   1.117 +  assume "!!S. PROP P (member2 S)"
   1.118 +  have "PROP P (member2 (Collect2 S))" .
   1.119 +  thus "PROP P S" by simp
   1.120 +qed
   1.121 +
   1.122 +lemma member2_right_eq: "(x == member2 y) == (Collect2 x == y)"
   1.123 +  by (rule equal_intr_rule, simp, drule symmetric, simp)
   1.124 +
   1.125 +ML_setup {*
   1.126 +local
   1.127 +
   1.128 +fun vars_of b (v as Var _) = if b then [] else [v]
   1.129 +  | vars_of b (t $ u) = vars_of true t union vars_of false u
   1.130 +  | vars_of b (Abs (_, _, t)) = vars_of false t
   1.131 +  | vars_of _ _ = [];
   1.132 +
   1.133 +fun rew ths1 ths2 th = Drule.forall_elim_vars 0
   1.134 +  (rewrite_rule ths2 (rewrite_rule ths1 (Drule.forall_intr_list
   1.135 +    (map (cterm_of (theory_of_thm th)) (vars_of false (prop_of th))) th)));
   1.136 +
   1.137 +val get_eq = Simpdata.mk_eq o thm;
   1.138 +
   1.139 +val split_predicate = get_eq "split_predicate";
   1.140 +val split_predicate2 = get_eq "split_predicate2";
   1.141 +val split_set = get_eq "split_set";
   1.142 +val split_set2 = get_eq "split_set2";
   1.143 +val member_eq = get_eq "member_eq";
   1.144 +val member2_eq = get_eq "member2_eq";
   1.145 +val member_Collect_eq = get_eq "member_Collect_eq";
   1.146 +val member2_Collect2_eq = get_eq "member2_Collect2_eq";
   1.147 +val mem_Collect2_eq = get_eq "mem_Collect2_eq";
   1.148 +val member_right_eq = thm "member_right_eq";
   1.149 +val member2_right_eq = thm "member2_right_eq";
   1.150 +
   1.151 +val rew' = Thm.symmetric o rew [split_set2] [split_set,
   1.152 +  member_right_eq, member2_right_eq, member_Collect_eq, member2_Collect2_eq];
   1.153 +
   1.154 +val rules1 = [split_predicate, split_predicate2, member_eq, member2_eq];
   1.155 +val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
   1.156 +
   1.157 +structure PredSetConvData = GenericDataFun
   1.158 +(struct
   1.159 +  val name = "HOL/pred_set_conv";
   1.160 +  type T = thm list;
   1.161 +  val empty = [];
   1.162 +  val extend = I;
   1.163 +  fun merge _ = Drule.merge_rules;
   1.164 +  fun print _ _ = ()
   1.165 +end)
   1.166 +
   1.167 +fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
   1.168 +  Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
   1.169 +    (ths @ PredSetConvData.get ctxt) @ ths2))));
   1.170 +
   1.171 +val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute
   1.172 +  (Drule.add_rule #> PredSetConvData.map));
   1.173 +
   1.174 +in
   1.175 +
   1.176 +val _ = ML_Context.>> (PredSetConvData.init #>
   1.177 +  Attrib.add_attributes
   1.178 +    [("pred_set_conv", pred_set_conv_att,
   1.179 +        "declare rules for converting between predicate and set notation"),
   1.180 +     ("to_set", mk_attr [] rules1 I, "convert rule to set notation"),
   1.181 +     ("to_pred", mk_attr [split_set2] rules2 rew',
   1.182 +        "convert rule to predicate notation")])
   1.183 +
   1.184 +end;
   1.185 +*}
   1.186 +
   1.187 +lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)"
   1.188 +  by (auto simp add: expand_fun_eq)
   1.189 +
   1.190 +lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)"
   1.191 +  by (auto simp add: expand_fun_eq)
   1.192 +
   1.193 +lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)"
   1.194 +  by fast
   1.195 +
   1.196 +lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)"
   1.197 +  by fast
   1.198 +
   1.199 +lemma member_empty [pred_set_conv]: "(%x. False) = member {}"
   1.200 +  by (simp add: expand_fun_eq)
   1.201 +
   1.202 +lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}"
   1.203 +  by (simp add: expand_fun_eq)
   1.204 +
   1.205 +
   1.206 +subsubsection {* Binary union *}
   1.207 +
   1.208 +lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)"
   1.209 +  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
   1.210 +
   1.211 +lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)"
   1.212 +  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
   1.213 +
   1.214 +lemma join1_iff [simp]: "(join A B x) = (A x | B x)"
   1.215 +  by (simp add: join_fun_eq join_bool_eq)
   1.216 +
   1.217 +lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)"
   1.218 +  by (simp add: join_fun_eq join_bool_eq)
   1.219 +
   1.220 +lemma join1I1 [elim?]: "A x ==> join A B x"
   1.221 +  by simp
   1.222 +
   1.223 +lemma join2I1 [elim?]: "A x y ==> join A B x y"
   1.224 +  by simp
   1.225 +
   1.226 +lemma join1I2 [elim?]: "B x ==> join A B x"
   1.227 +  by simp
   1.228 +
   1.229 +lemma join2I2 [elim?]: "B x y ==> join A B x y"
   1.230 +  by simp
   1.231 +
   1.232 +text {*
   1.233 +  \medskip Classical introduction rule: no commitment to @{text A} vs
   1.234 +  @{text B}.
   1.235 +*}
   1.236 +
   1.237 +lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x"
   1.238 +  by auto
   1.239 +
   1.240 +lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y"
   1.241 +  by auto
   1.242 +
   1.243 +lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   1.244 +  by simp iprover
   1.245 +
   1.246 +lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   1.247 +  by simp iprover
   1.248 +
   1.249 +
   1.250 +subsubsection {* Binary intersection *}
   1.251 +
   1.252 +lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)"
   1.253 +  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
   1.254 +
   1.255 +lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)"
   1.256 +  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
   1.257 +
   1.258 +lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)"
   1.259 +  by (simp add: meet_fun_eq meet_bool_eq)
   1.260 +
   1.261 +lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)"
   1.262 +  by (simp add: meet_fun_eq meet_bool_eq)
   1.263 +
   1.264 +lemma meet1I [intro!]: "A x ==> B x ==> meet A B x"
   1.265 +  by simp
   1.266 +
   1.267 +lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y"
   1.268 +  by simp
   1.269 +
   1.270 +lemma meet1D1: "meet A B x ==> A x"
   1.271 +  by simp
   1.272 +
   1.273 +lemma meet2D1: "meet A B x y ==> A x y"
   1.274 +  by simp
   1.275 +
   1.276 +lemma meet1D2: "meet A B x ==> B x"
   1.277 +  by simp
   1.278 +
   1.279 +lemma meet2D2: "meet A B x y ==> B x y"
   1.280 +  by simp
   1.281 +
   1.282 +lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P"
   1.283 +  by simp
   1.284 +
   1.285 +lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P"
   1.286 +  by simp
   1.287 +
   1.288 +
   1.289 +subsubsection {* Unions of families *}
   1.290 +
   1.291 +lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
   1.292 +  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
   1.293 +
   1.294 +lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
   1.295 +  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
   1.296 +
   1.297 +lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)"
   1.298 +  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
   1.299 +
   1.300 +lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)"
   1.301 +  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
   1.302 +
   1.303 +lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b"
   1.304 +  by auto
   1.305 +
   1.306 +lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c"
   1.307 +  by auto
   1.308 +
   1.309 +lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R"
   1.310 +  by simp iprover
   1.311 +
   1.312 +lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R"
   1.313 +  by simp iprover
   1.314 +
   1.315 +
   1.316 +subsection {* Composition of two relations *}
   1.317 +
   1.318 +inductive2
   1.319 +  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
   1.320 +    (infixr "OO" 75)
   1.321 +  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
   1.322 +where
   1.323 +  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
   1.324 +
   1.325 +inductive_cases2 pred_compE [elim!]: "(r OO s) a c"
   1.326 +
   1.327 +lemma pred_comp_rel_comp_eq [pred_set_conv]:
   1.328 +  "(member2 r OO member2 s) = member2 (r O s)"
   1.329 +  by (auto simp add: expand_fun_eq elim: pred_compE)
   1.330 +
   1.331 +
   1.332 +subsection {* Converse *}
   1.333 +
   1.334 +inductive2
   1.335 +  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
   1.336 +    ("(_^--1)" [1000] 1000)
   1.337 +  for r :: "'a => 'b => bool"
   1.338 +where
   1.339 +  conversepI: "r a b ==> r^--1 b a"
   1.340 +
   1.341 +notation (xsymbols)
   1.342 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   1.343 +
   1.344 +lemma conversepD:
   1.345 +  assumes ab: "r^--1 a b"
   1.346 +  shows "r b a" using ab
   1.347 +  by cases simp
   1.348 +
   1.349 +lemma conversep_iff [iff]: "r^--1 a b = r b a"
   1.350 +  by (iprover intro: conversepI dest: conversepD)
   1.351 +
   1.352 +lemma conversep_converse_eq [pred_set_conv]:
   1.353 +  "(member2 r)^--1 = member2 (r^-1)"
   1.354 +  by (auto simp add: expand_fun_eq)
   1.355 +
   1.356 +lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   1.357 +  by (iprover intro: order_antisym conversepI dest: conversepD)
   1.358 +
   1.359 +lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
   1.360 +  by (iprover intro: order_antisym conversepI pred_compI
   1.361 +    elim: pred_compE dest: conversepD)
   1.362 +
   1.363 +lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1"
   1.364 +  by (simp add: meet_fun_eq meet_bool_eq)
   1.365 +    (iprover intro: conversepI ext dest: conversepD)
   1.366 +
   1.367 +lemma converse_join: "(join r s)^--1 = join r^--1 s^--1"
   1.368 +  by (simp add: join_fun_eq join_bool_eq)
   1.369 +    (iprover intro: conversepI ext dest: conversepD)
   1.370 +
   1.371 +lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
   1.372 +  by (auto simp add: expand_fun_eq)
   1.373 +
   1.374 +lemma conversep_eq [simp]: "(op =)^--1 = op ="
   1.375 +  by (auto simp add: expand_fun_eq)
   1.376 +
   1.377 +
   1.378 +subsection {* Domain *}
   1.379 +
   1.380 +inductive2
   1.381 +  DomainP :: "('a => 'b => bool) => 'a => bool"
   1.382 +  for r :: "'a => 'b => bool"
   1.383 +where
   1.384 +  DomainPI [intro]: "r a b ==> DomainP r a"
   1.385 +
   1.386 +inductive_cases2 DomainPE [elim!]: "DomainP r a"
   1.387 +
   1.388 +lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)"
   1.389 +  by (blast intro!: Orderings.order_antisym)
   1.390 +
   1.391 +
   1.392 +subsection {* Range *}
   1.393 +
   1.394 +inductive2
   1.395 +  RangeP :: "('a => 'b => bool) => 'b => bool"
   1.396 +  for r :: "'a => 'b => bool"
   1.397 +where
   1.398 +  RangePI [intro]: "r a b ==> RangeP r b"
   1.399 +
   1.400 +inductive_cases2 RangePE [elim!]: "RangeP r b"
   1.401 +
   1.402 +lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)"
   1.403 +  by (blast intro!: Orderings.order_antisym)
   1.404 +
   1.405 +
   1.406 +subsection {* Inverse image *}
   1.407 +
   1.408 +definition
   1.409 +  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
   1.410 +  "inv_imagep r f == %x y. r (f x) (f y)"
   1.411 +
   1.412 +lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)"
   1.413 +  by (simp add: inv_image_def inv_imagep_def)
   1.414 +
   1.415 +lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
   1.416 +  by (simp add: inv_imagep_def)
   1.417 +
   1.418 +
   1.419 +subsection {* Properties of relations - predicate versions *}
   1.420 +
   1.421 +abbreviation antisymP :: "('a => 'a => bool) => bool" where
   1.422 +  "antisymP r == antisym (Collect2 r)"
   1.423 +
   1.424 +abbreviation transP :: "('a => 'a => bool) => bool" where
   1.425 +  "transP r == trans (Collect2 r)"
   1.426 +
   1.427 +abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   1.428 +  "single_valuedP r == single_valued (Collect2 r)"
   1.429 +
   1.430 +
   1.431 +subsection {* Bounded quantifiers for predicates *}
   1.432 +
   1.433 +text {*
   1.434 +Bounded existential quantifier for predicates (executable).
   1.435 +*}
   1.436 +
   1.437 +inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.438 +  for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool"
   1.439 +where
   1.440 +  bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q"
   1.441 +
   1.442 +lemmas bexpE [elim!] = bexp.cases
   1.443 +
   1.444 +syntax
   1.445 +  Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10)
   1.446 +
   1.447 +translations
   1.448 +  "\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)"
   1.449 +
   1.450 +constdefs
   1.451 +  ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.452 +  "ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x"
   1.453 +
   1.454 +syntax
   1.455 +  Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10)
   1.456 +
   1.457 +translations
   1.458 +  "\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)"
   1.459 +
   1.460 +(* To avoid eta-contraction of body: *)
   1.461 +print_translation {*
   1.462 +let
   1.463 +  fun btr' syn [A,Abs abs] =
   1.464 +    let val (x,t) = atomic_abs_tr' abs
   1.465 +    in Syntax.const syn $ x $ A $ t end
   1.466 +in
   1.467 +[("ballp", btr' "Ballp"),("bexp", btr' "Bexp")]
   1.468 +end
   1.469 +*}
   1.470 +
   1.471 +lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x"
   1.472 +  by (simp add: ballp_def)
   1.473 +
   1.474 +lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x"
   1.475 +  by (simp add: ballp_def)
   1.476 +
   1.477 +lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q"
   1.478 +  by (unfold ballp_def) blast
   1.479 +
   1.480 +lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))"
   1.481 +  by (blast dest: bspecp)
   1.482 +
   1.483 +declare ballp_not_bexp_eq [THEN eq_reflection, code unfold]
   1.484 +
   1.485 +end