author berghofe Wed Feb 07 17:25:39 2007 +0100 (2007-02-07) changeset 22259 476604be7d88 parent 22258 0967b03844b5 child 22260 45f01828cb69
New theory for converting between predicates and sets.
 src/HOL/Predicate.thy file | annotate | diff | revisions
```     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.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.173 +
1.174 +in
1.175 +
1.176 +val _ = ML_Context.>> (PredSetConvData.init #>
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)
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)
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
```