|
1 (* Title: HOL/Predicate.thy |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Predicates *} |
|
7 |
|
8 theory Predicate |
|
9 imports Inductive |
|
10 begin |
|
11 |
|
12 subsection {* Converting between predicates and sets *} |
|
13 |
|
14 definition |
|
15 member :: "'a set => 'a => bool" where |
|
16 "member == %S x. x : S" |
|
17 |
|
18 lemma memberI[intro!, Pure.intro!]: "x : S ==> member S x" |
|
19 by (simp add: member_def) |
|
20 |
|
21 lemma memberD[dest!, Pure.dest!]: "member S x ==> x : S" |
|
22 by (simp add: member_def) |
|
23 |
|
24 lemma member_eq[simp]: "member S x = (x : S)" |
|
25 by (simp add: member_def) |
|
26 |
|
27 lemma member_Collect_eq[simp]: "member (Collect P) = P" |
|
28 by (simp add: member_def) |
|
29 |
|
30 lemma Collect_member_eq[simp]: "Collect (member S) = S" |
|
31 by (simp add: member_def) |
|
32 |
|
33 lemma split_set: "(!!S. PROP P S) == (!!S. PROP P (Collect S))" |
|
34 proof |
|
35 fix S |
|
36 assume "!!S. PROP P S" |
|
37 show "PROP P (Collect S)" . |
|
38 next |
|
39 fix S |
|
40 assume "!!S. PROP P (Collect S)" |
|
41 have "PROP P {x. x : S}" . |
|
42 thus "PROP P S" by simp |
|
43 qed |
|
44 |
|
45 lemma split_predicate: "(!!S. PROP P S) == (!!S. PROP P (member S))" |
|
46 proof |
|
47 fix S |
|
48 assume "!!S. PROP P S" |
|
49 show "PROP P (member S)" . |
|
50 next |
|
51 fix S |
|
52 assume "!!S. PROP P (member S)" |
|
53 have "PROP P (member {x. S x})" . |
|
54 thus "PROP P S" by simp |
|
55 qed |
|
56 |
|
57 lemma member_right_eq: "(x == member y) == (Collect x == y)" |
|
58 by (rule equal_intr_rule, simp, drule symmetric, simp) |
|
59 |
|
60 definition |
|
61 member2 :: "('a * 'b) set => 'a => 'b \<Rightarrow> bool" where |
|
62 "member2 == %S x y. (x, y) : S" |
|
63 |
|
64 definition |
|
65 Collect2 :: "('a => 'b => bool) => ('a * 'b) set" where |
|
66 "Collect2 == %P. {(x, y). P x y}" |
|
67 |
|
68 lemma member2I[intro!, Pure.intro!]: "(x, y) : S ==> member2 S x y" |
|
69 by (simp add: member2_def) |
|
70 |
|
71 lemma member2D[dest!, Pure.dest!]: "member2 S x y ==> (x, y) : S" |
|
72 by (simp add: member2_def) |
|
73 |
|
74 lemma member2_eq[simp]: "member2 S x y = ((x, y) : S)" |
|
75 by (simp add: member2_def) |
|
76 |
|
77 lemma Collect2I: "P x y ==> (x, y) : Collect2 P" |
|
78 by (simp add: Collect2_def) |
|
79 |
|
80 lemma Collect2D: "(x, y) : Collect2 P ==> P x y" |
|
81 by (simp add: Collect2_def) |
|
82 |
|
83 lemma member2_Collect2_eq[simp]: "member2 (Collect2 P) = P" |
|
84 by (simp add: member2_def Collect2_def) |
|
85 |
|
86 lemma Collect2_member2_eq[simp]: "Collect2 (member2 S) = S" |
|
87 by (auto simp add: member2_def Collect2_def) |
|
88 |
|
89 lemma mem_Collect2_eq[iff]: "((x, y) : Collect2 P) = P x y" |
|
90 by (iprover intro: Collect2I dest: Collect2D) |
|
91 |
|
92 lemma member2_Collect_split_eq [simp]: "member2 (Collect (split P)) = P" |
|
93 by (simp add: expand_fun_eq) |
|
94 |
|
95 lemma split_set2: "(!!S. PROP P S) == (!!S. PROP P (Collect2 S))" |
|
96 proof |
|
97 fix S |
|
98 assume "!!S. PROP P S" |
|
99 show "PROP P (Collect2 S)" . |
|
100 next |
|
101 fix S |
|
102 assume "!!S. PROP P (Collect2 S)" |
|
103 have "PROP P (Collect2 (member2 S))" . |
|
104 thus "PROP P S" by simp |
|
105 qed |
|
106 |
|
107 lemma split_predicate2: "(!!S. PROP P S) == (!!S. PROP P (member2 S))" |
|
108 proof |
|
109 fix S |
|
110 assume "!!S. PROP P S" |
|
111 show "PROP P (member2 S)" . |
|
112 next |
|
113 fix S |
|
114 assume "!!S. PROP P (member2 S)" |
|
115 have "PROP P (member2 (Collect2 S))" . |
|
116 thus "PROP P S" by simp |
|
117 qed |
|
118 |
|
119 lemma member2_right_eq: "(x == member2 y) == (Collect2 x == y)" |
|
120 by (rule equal_intr_rule, simp, drule symmetric, simp) |
|
121 |
|
122 ML_setup {* |
|
123 local |
|
124 |
|
125 fun vars_of b (v as Var _) = if b then [] else [v] |
|
126 | vars_of b (t $ u) = vars_of true t union vars_of false u |
|
127 | vars_of b (Abs (_, _, t)) = vars_of false t |
|
128 | vars_of _ _ = []; |
|
129 |
|
130 fun rew ths1 ths2 th = Drule.forall_elim_vars 0 |
|
131 (rewrite_rule ths2 (rewrite_rule ths1 (Drule.forall_intr_list |
|
132 (map (cterm_of (theory_of_thm th)) (vars_of false (prop_of th))) th))); |
|
133 |
|
134 val get_eq = Simpdata.mk_eq o thm; |
|
135 |
|
136 val split_predicate = get_eq "split_predicate"; |
|
137 val split_predicate2 = get_eq "split_predicate2"; |
|
138 val split_set = get_eq "split_set"; |
|
139 val split_set2 = get_eq "split_set2"; |
|
140 val member_eq = get_eq "member_eq"; |
|
141 val member2_eq = get_eq "member2_eq"; |
|
142 val member_Collect_eq = get_eq "member_Collect_eq"; |
|
143 val member2_Collect2_eq = get_eq "member2_Collect2_eq"; |
|
144 val mem_Collect2_eq = get_eq "mem_Collect2_eq"; |
|
145 val member_right_eq = thm "member_right_eq"; |
|
146 val member2_right_eq = thm "member2_right_eq"; |
|
147 |
|
148 val rew' = Thm.symmetric o rew [split_set2] [split_set, |
|
149 member_right_eq, member2_right_eq, member_Collect_eq, member2_Collect2_eq]; |
|
150 |
|
151 val rules1 = [split_predicate, split_predicate2, member_eq, member2_eq]; |
|
152 val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq]; |
|
153 |
|
154 structure PredSetConvData = GenericDataFun |
|
155 (struct |
|
156 val name = "HOL/pred_set_conv"; |
|
157 type T = thm list; |
|
158 val empty = []; |
|
159 val extend = I; |
|
160 fun merge _ = Drule.merge_rules; |
|
161 fun print _ _ = () |
|
162 end) |
|
163 |
|
164 fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths => |
|
165 Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq) |
|
166 (ths @ PredSetConvData.get ctxt) @ ths2)))); |
|
167 |
|
168 val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute |
|
169 (Drule.add_rule #> PredSetConvData.map)); |
|
170 |
|
171 in |
|
172 |
|
173 val _ = ML_Context.>> (PredSetConvData.init #> |
|
174 Attrib.add_attributes |
|
175 [("pred_set_conv", pred_set_conv_att, |
|
176 "declare rules for converting between predicate and set notation"), |
|
177 ("to_set", mk_attr [] rules1 I, "convert rule to set notation"), |
|
178 ("to_pred", mk_attr [split_set2] rules2 rew', |
|
179 "convert rule to predicate notation")]) |
|
180 |
|
181 end; |
|
182 *} |
|
183 |
|
184 lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)" |
|
185 by (auto simp add: expand_fun_eq) |
|
186 |
|
187 lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)" |
|
188 by (auto simp add: expand_fun_eq) |
|
189 |
|
190 lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)" |
|
191 by fast |
|
192 |
|
193 lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)" |
|
194 by fast |
|
195 |
|
196 lemma member_empty [pred_set_conv]: "(%x. False) = member {}" |
|
197 by (simp add: expand_fun_eq) |
|
198 |
|
199 lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}" |
|
200 by (simp add: expand_fun_eq) |
|
201 |
|
202 |
|
203 subsubsection {* Binary union *} |
|
204 |
|
205 lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)" |
|
206 by (simp add: expand_fun_eq join_fun_eq join_bool_eq) |
|
207 |
|
208 lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)" |
|
209 by (simp add: expand_fun_eq join_fun_eq join_bool_eq) |
|
210 |
|
211 lemma join1_iff [simp]: "(join A B x) = (A x | B x)" |
|
212 by (simp add: join_fun_eq join_bool_eq) |
|
213 |
|
214 lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)" |
|
215 by (simp add: join_fun_eq join_bool_eq) |
|
216 |
|
217 lemma join1I1 [elim?]: "A x ==> join A B x" |
|
218 by simp |
|
219 |
|
220 lemma join2I1 [elim?]: "A x y ==> join A B x y" |
|
221 by simp |
|
222 |
|
223 lemma join1I2 [elim?]: "B x ==> join A B x" |
|
224 by simp |
|
225 |
|
226 lemma join2I2 [elim?]: "B x y ==> join A B x y" |
|
227 by simp |
|
228 |
|
229 text {* |
|
230 \medskip Classical introduction rule: no commitment to @{text A} vs |
|
231 @{text B}. |
|
232 *} |
|
233 |
|
234 lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x" |
|
235 by auto |
|
236 |
|
237 lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y" |
|
238 by auto |
|
239 |
|
240 lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" |
|
241 by simp iprover |
|
242 |
|
243 lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" |
|
244 by simp iprover |
|
245 |
|
246 |
|
247 subsubsection {* Binary intersection *} |
|
248 |
|
249 lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)" |
|
250 by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq) |
|
251 |
|
252 lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)" |
|
253 by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq) |
|
254 |
|
255 lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)" |
|
256 by (simp add: meet_fun_eq meet_bool_eq) |
|
257 |
|
258 lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)" |
|
259 by (simp add: meet_fun_eq meet_bool_eq) |
|
260 |
|
261 lemma meet1I [intro!]: "A x ==> B x ==> meet A B x" |
|
262 by simp |
|
263 |
|
264 lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y" |
|
265 by simp |
|
266 |
|
267 lemma meet1D1: "meet A B x ==> A x" |
|
268 by simp |
|
269 |
|
270 lemma meet2D1: "meet A B x y ==> A x y" |
|
271 by simp |
|
272 |
|
273 lemma meet1D2: "meet A B x ==> B x" |
|
274 by simp |
|
275 |
|
276 lemma meet2D2: "meet A B x y ==> B x y" |
|
277 by simp |
|
278 |
|
279 lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P" |
|
280 by simp |
|
281 |
|
282 lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P" |
|
283 by simp |
|
284 |
|
285 |
|
286 subsubsection {* Unions of families *} |
|
287 |
|
288 lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)" |
|
289 by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast |
|
290 |
|
291 lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)" |
|
292 by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast |
|
293 |
|
294 lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)" |
|
295 by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast |
|
296 |
|
297 lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)" |
|
298 by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast |
|
299 |
|
300 lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b" |
|
301 by auto |
|
302 |
|
303 lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c" |
|
304 by auto |
|
305 |
|
306 lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R" |
|
307 by simp iprover |
|
308 |
|
309 lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R" |
|
310 by simp iprover |
|
311 |
|
312 |
|
313 subsection {* Composition of two relations *} |
|
314 |
|
315 inductive2 |
|
316 pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool" |
|
317 (infixr "OO" 75) |
|
318 for r :: "'b => 'c => bool" and s :: "'a => 'b => bool" |
|
319 where |
|
320 pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c" |
|
321 |
|
322 inductive_cases2 pred_compE [elim!]: "(r OO s) a c" |
|
323 |
|
324 lemma pred_comp_rel_comp_eq [pred_set_conv]: |
|
325 "(member2 r OO member2 s) = member2 (r O s)" |
|
326 by (auto simp add: expand_fun_eq elim: pred_compE) |
|
327 |
|
328 |
|
329 subsection {* Converse *} |
|
330 |
|
331 inductive2 |
|
332 conversep :: "('a => 'b => bool) => 'b => 'a => bool" |
|
333 ("(_^--1)" [1000] 1000) |
|
334 for r :: "'a => 'b => bool" |
|
335 where |
|
336 conversepI: "r a b ==> r^--1 b a" |
|
337 |
|
338 notation (xsymbols) |
|
339 conversep ("(_\<inverse>\<inverse>)" [1000] 1000) |
|
340 |
|
341 lemma conversepD: |
|
342 assumes ab: "r^--1 a b" |
|
343 shows "r b a" using ab |
|
344 by cases simp |
|
345 |
|
346 lemma conversep_iff [iff]: "r^--1 a b = r b a" |
|
347 by (iprover intro: conversepI dest: conversepD) |
|
348 |
|
349 lemma conversep_converse_eq [pred_set_conv]: |
|
350 "(member2 r)^--1 = member2 (r^-1)" |
|
351 by (auto simp add: expand_fun_eq) |
|
352 |
|
353 lemma conversep_conversep [simp]: "(r^--1)^--1 = r" |
|
354 by (iprover intro: order_antisym conversepI dest: conversepD) |
|
355 |
|
356 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1" |
|
357 by (iprover intro: order_antisym conversepI pred_compI |
|
358 elim: pred_compE dest: conversepD) |
|
359 |
|
360 lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1" |
|
361 by (simp add: meet_fun_eq meet_bool_eq) |
|
362 (iprover intro: conversepI ext dest: conversepD) |
|
363 |
|
364 lemma converse_join: "(join r s)^--1 = join r^--1 s^--1" |
|
365 by (simp add: join_fun_eq join_bool_eq) |
|
366 (iprover intro: conversepI ext dest: conversepD) |
|
367 |
|
368 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~=" |
|
369 by (auto simp add: expand_fun_eq) |
|
370 |
|
371 lemma conversep_eq [simp]: "(op =)^--1 = op =" |
|
372 by (auto simp add: expand_fun_eq) |
|
373 |
|
374 |
|
375 subsection {* Domain *} |
|
376 |
|
377 inductive2 |
|
378 DomainP :: "('a => 'b => bool) => 'a => bool" |
|
379 for r :: "'a => 'b => bool" |
|
380 where |
|
381 DomainPI [intro]: "r a b ==> DomainP r a" |
|
382 |
|
383 inductive_cases2 DomainPE [elim!]: "DomainP r a" |
|
384 |
|
385 lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)" |
|
386 by (blast intro!: Orderings.order_antisym) |
|
387 |
|
388 |
|
389 subsection {* Range *} |
|
390 |
|
391 inductive2 |
|
392 RangeP :: "('a => 'b => bool) => 'b => bool" |
|
393 for r :: "'a => 'b => bool" |
|
394 where |
|
395 RangePI [intro]: "r a b ==> RangeP r b" |
|
396 |
|
397 inductive_cases2 RangePE [elim!]: "RangeP r b" |
|
398 |
|
399 lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)" |
|
400 by (blast intro!: Orderings.order_antisym) |
|
401 |
|
402 |
|
403 subsection {* Inverse image *} |
|
404 |
|
405 definition |
|
406 inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where |
|
407 "inv_imagep r f == %x y. r (f x) (f y)" |
|
408 |
|
409 lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)" |
|
410 by (simp add: inv_image_def inv_imagep_def) |
|
411 |
|
412 lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" |
|
413 by (simp add: inv_imagep_def) |
|
414 |
|
415 |
|
416 subsection {* Properties of relations - predicate versions *} |
|
417 |
|
418 abbreviation antisymP :: "('a => 'a => bool) => bool" where |
|
419 "antisymP r == antisym (Collect2 r)" |
|
420 |
|
421 abbreviation transP :: "('a => 'a => bool) => bool" where |
|
422 "transP r == trans (Collect2 r)" |
|
423 |
|
424 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where |
|
425 "single_valuedP r == single_valued (Collect2 r)" |
|
426 |
|
427 |
|
428 subsection {* Bounded quantifiers for predicates *} |
|
429 |
|
430 text {* |
|
431 Bounded existential quantifier for predicates (executable). |
|
432 *} |
|
433 |
|
434 inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
435 for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool" |
|
436 where |
|
437 bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q" |
|
438 |
|
439 lemmas bexpE [elim!] = bexp.cases |
|
440 |
|
441 syntax |
|
442 Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10) |
|
443 |
|
444 translations |
|
445 "\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)" |
|
446 |
|
447 constdefs |
|
448 ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
449 "ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x" |
|
450 |
|
451 syntax |
|
452 Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10) |
|
453 |
|
454 translations |
|
455 "\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)" |
|
456 |
|
457 (* To avoid eta-contraction of body: *) |
|
458 print_translation {* |
|
459 let |
|
460 fun btr' syn [A,Abs abs] = |
|
461 let val (x,t) = atomic_abs_tr' abs |
|
462 in Syntax.const syn $ x $ A $ t end |
|
463 in |
|
464 [("ballp", btr' "Ballp"),("bexp", btr' "Bexp")] |
|
465 end |
|
466 *} |
|
467 |
|
468 lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x" |
|
469 by (simp add: ballp_def) |
|
470 |
|
471 lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x" |
|
472 by (simp add: ballp_def) |
|
473 |
|
474 lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q" |
|
475 by (unfold ballp_def) blast |
|
476 |
|
477 lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))" |
|
478 by (blast dest: bspecp) |
|
479 |
|
480 declare ballp_not_bexp_eq [THEN eq_reflection, code unfold] |
|
481 |
|
482 end |