author | nipkow |
Tue, 01 Jun 2021 19:46:34 +0200 | |
changeset 73832 | 9db620f007fa |
parent 71935 | 82b00b8f1871 |
child 74806 | ba59c691b3ee |
permissions | -rw-r--r-- |
10358 | 1 |
(* Title: HOL/Relation.thy |
63612 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Author: Stefan Berghofer, TU Muenchen |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
4 |
*) |
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
5 |
|
60758 | 6 |
section \<open>Relations -- as sets of pairs, and binary predicates\<close> |
12905 | 7 |
|
15131 | 8 |
theory Relation |
63612 | 9 |
imports Finite_Set |
15131 | 10 |
begin |
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset
|
11 |
|
60758 | 12 |
text \<open>A preliminary: classical rules for reasoning on predicates\<close> |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
13 |
|
46882 | 14 |
declare predicate1I [Pure.intro!, intro!] |
15 |
declare predicate1D [Pure.dest, dest] |
|
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
16 |
declare predicate2I [Pure.intro!, intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
17 |
declare predicate2D [Pure.dest, dest] |
63404 | 18 |
declare bot1E [elim!] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
19 |
declare bot2E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
20 |
declare top1I [intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
21 |
declare top2I [intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
22 |
declare inf1I [intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
23 |
declare inf2I [intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
24 |
declare inf1E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
25 |
declare inf2E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
26 |
declare sup1I1 [intro?] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
27 |
declare sup2I1 [intro?] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
28 |
declare sup1I2 [intro?] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
29 |
declare sup2I2 [intro?] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
30 |
declare sup1E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
31 |
declare sup2E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
32 |
declare sup1CI [intro!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
33 |
declare sup2CI [intro!] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
34 |
declare Inf1_I [intro!] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
35 |
declare INF1_I [intro!] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
36 |
declare Inf2_I [intro!] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
37 |
declare INF2_I [intro!] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
38 |
declare Inf1_D [elim] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
39 |
declare INF1_D [elim] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
40 |
declare Inf2_D [elim] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
41 |
declare INF2_D [elim] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
42 |
declare Inf1_E [elim] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
43 |
declare INF1_E [elim] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
44 |
declare Inf2_E [elim] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
45 |
declare INF2_E [elim] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
46 |
declare Sup1_I [intro] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
47 |
declare SUP1_I [intro] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
48 |
declare Sup2_I [intro] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
49 |
declare SUP2_I [intro] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
50 |
declare Sup1_E [elim!] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
51 |
declare SUP1_E [elim!] |
56742
678a52e676b6
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
haftmann
parents:
56545
diff
changeset
|
52 |
declare Sup2_E [elim!] |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
53 |
declare SUP2_E [elim!] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
54 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
55 |
|
60758 | 56 |
subsection \<open>Fundamental\<close> |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
57 |
|
60758 | 58 |
subsubsection \<open>Relations as sets of pairs\<close> |
46694 | 59 |
|
63404 | 60 |
type_synonym 'a rel = "('a \<times> 'a) set" |
46694 | 61 |
|
63404 | 62 |
lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s" |
63 |
\<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close> |
|
46694 | 64 |
by auto |
65 |
||
63404 | 66 |
lemma lfp_induct2: |
46694 | 67 |
"(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow> |
68 |
(\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b" |
|
63404 | 69 |
\<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close> |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55096
diff
changeset
|
70 |
using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto |
46694 | 71 |
|
72 |
||
60758 | 73 |
subsubsection \<open>Conversions between set and predicate relations\<close> |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
74 |
|
46833 | 75 |
lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
76 |
by (simp add: set_eq_iff fun_eq_iff) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
77 |
|
46833 | 78 |
lemma pred_equals_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R = S" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
79 |
by (simp add: set_eq_iff fun_eq_iff) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
80 |
|
46833 | 81 |
lemma pred_subset_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S) \<longleftrightarrow> R \<subseteq> S" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
82 |
by (simp add: subset_iff le_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
83 |
|
46833 | 84 |
lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
85 |
by (simp add: subset_iff le_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
86 |
|
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
87 |
lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})" |
46689 | 88 |
by (auto simp add: fun_eq_iff) |
89 |
||
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
90 |
lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
91 |
by (auto simp add: fun_eq_iff) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
92 |
|
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
93 |
lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)" |
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
94 |
by (auto simp add: fun_eq_iff) |
46689 | 95 |
|
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
96 |
lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)" |
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset
|
97 |
by (auto simp add: fun_eq_iff) |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
98 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
99 |
lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
100 |
by (simp add: inf_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
101 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
102 |
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)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
103 |
by (simp add: inf_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
104 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
105 |
lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
106 |
by (simp add: sup_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
107 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
108 |
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)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
109 |
by (simp add: sup_fun_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
110 |
|
46981 | 111 |
lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))" |
112 |
by (simp add: fun_eq_iff) |
|
113 |
||
114 |
lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))" |
|
115 |
by (simp add: fun_eq_iff) |
|
116 |
||
117 |
lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))" |
|
118 |
by (simp add: fun_eq_iff) |
|
119 |
||
120 |
lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))" |
|
121 |
by (simp add: fun_eq_iff) |
|
122 |
||
69275 | 123 |
lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> (\<Inter>(Collect ` S)))" |
46884 | 124 |
by (simp add: fun_eq_iff) |
46833 | 125 |
|
126 |
lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" |
|
46884 | 127 |
by (simp add: fun_eq_iff) |
46833 | 128 |
|
69275 | 129 |
lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> (\<Inter>(Collect ` case_prod ` S)))" |
46884 | 130 |
by (simp add: fun_eq_iff) |
46833 | 131 |
|
132 |
lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)" |
|
46884 | 133 |
by (simp add: fun_eq_iff) |
46833 | 134 |
|
69275 | 135 |
lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> \<Union>(Collect ` S))" |
46884 | 136 |
by (simp add: fun_eq_iff) |
46833 | 137 |
|
138 |
lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)" |
|
46884 | 139 |
by (simp add: fun_eq_iff) |
46833 | 140 |
|
69275 | 141 |
lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> (\<Union>(Collect ` case_prod ` S)))" |
46884 | 142 |
by (simp add: fun_eq_iff) |
46833 | 143 |
|
144 |
lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)" |
|
46884 | 145 |
by (simp add: fun_eq_iff) |
46833 | 146 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
147 |
|
60758 | 148 |
subsection \<open>Properties of relations\<close> |
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset
|
149 |
|
60758 | 150 |
subsubsection \<open>Reflexivity\<close> |
10786 | 151 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
152 |
definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
63404 | 153 |
where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)" |
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset
|
154 |
|
63404 | 155 |
abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close> |
156 |
where "refl \<equiv> refl_on UNIV" |
|
26297 | 157 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
158 |
definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
63404 | 159 |
where "reflp r \<longleftrightarrow> (\<forall>x. r x x)" |
46694 | 160 |
|
63404 | 161 |
lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
162 |
by (simp add: refl_on_def reflp_def) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
163 |
|
63404 | 164 |
lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r" |
165 |
unfolding refl_on_def by (iprover intro!: ballI) |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
166 |
|
63404 | 167 |
lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r" |
168 |
unfolding refl_on_def by blast |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
169 |
|
63404 | 170 |
lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A" |
171 |
unfolding refl_on_def by blast |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
172 |
|
63404 | 173 |
lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A" |
174 |
unfolding refl_on_def by blast |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
175 |
|
63404 | 176 |
lemma reflpI [intro?]: "(\<And>x. r x x) \<Longrightarrow> reflp r" |
46694 | 177 |
by (auto intro: refl_onI simp add: reflp_def) |
178 |
||
179 |
lemma reflpE: |
|
180 |
assumes "reflp r" |
|
181 |
obtains "r x x" |
|
182 |
using assms by (auto dest: refl_onD simp add: reflp_def) |
|
183 |
||
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
184 |
lemma reflpD [dest?]: |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47436
diff
changeset
|
185 |
assumes "reflp r" |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47436
diff
changeset
|
186 |
shows "r x x" |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47436
diff
changeset
|
187 |
using assms by (auto elim: reflpE) |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47436
diff
changeset
|
188 |
|
63404 | 189 |
lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)" |
190 |
unfolding refl_on_def by blast |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
191 |
|
63404 | 192 |
lemma reflp_inf: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
193 |
by (auto intro: reflpI elim: reflpE) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
194 |
|
63404 | 195 |
lemma refl_on_Un: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<union> B) (r \<union> s)" |
196 |
unfolding refl_on_def by blast |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
197 |
|
63404 | 198 |
lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
199 |
by (auto intro: reflpI elim: reflpE) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
200 |
|
69275 | 201 |
lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))" |
63404 | 202 |
unfolding refl_on_def by fast |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
203 |
|
69275 | 204 |
lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Union>(A ` S)) (\<Union>(r ` S))" |
63404 | 205 |
unfolding refl_on_def by blast |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
206 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
207 |
lemma refl_on_empty [simp]: "refl_on {} {}" |
63404 | 208 |
by (simp add: refl_on_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
209 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
210 |
lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}" |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
211 |
by (blast intro: refl_onI) |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
212 |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
213 |
lemma refl_on_def' [nitpick_unfold, code]: |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
214 |
"refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
215 |
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
216 |
|
67399 | 217 |
lemma reflp_equality [simp]: "reflp (=)" |
63404 | 218 |
by (simp add: reflp_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
219 |
|
63404 | 220 |
lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<longrightarrow> Q x y) \<Longrightarrow> reflp Q" |
221 |
by (auto intro: reflpI dest: reflpD) |
|
61630 | 222 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
223 |
|
60758 | 224 |
subsubsection \<open>Irreflexivity\<close> |
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset
|
225 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
226 |
definition irrefl :: "'a rel \<Rightarrow> bool" |
63404 | 227 |
where "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)" |
56545 | 228 |
|
229 |
definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
|
63404 | 230 |
where "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)" |
56545 | 231 |
|
63404 | 232 |
lemma irreflp_irrefl_eq [pred_set_conv]: "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" |
56545 | 233 |
by (simp add: irrefl_def irreflp_def) |
234 |
||
63404 | 235 |
lemma irreflI [intro?]: "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R" |
56545 | 236 |
by (simp add: irrefl_def) |
237 |
||
63404 | 238 |
lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R" |
56545 | 239 |
by (fact irreflI [to_pred]) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
240 |
|
63404 | 241 |
lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)" |
46694 | 242 |
by (auto simp add: irrefl_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
243 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
244 |
|
60758 | 245 |
subsubsection \<open>Asymmetry\<close> |
56545 | 246 |
|
247 |
inductive asym :: "'a rel \<Rightarrow> bool" |
|
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
248 |
where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" |
56545 | 249 |
|
250 |
inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
|
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
251 |
where asympI: "(\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R" |
56545 | 252 |
|
63404 | 253 |
lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" |
56545 | 254 |
by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) |
255 |
||
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
256 |
lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R" |
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
257 |
by (simp add: asym.simps) |
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
258 |
|
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
259 |
lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)" |
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
260 |
by (blast intro: asymI dest: asymD) |
56545 | 261 |
|
60758 | 262 |
subsubsection \<open>Symmetry\<close> |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
263 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
264 |
definition sym :: "'a rel \<Rightarrow> bool" |
63404 | 265 |
where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
266 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
267 |
definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
63404 | 268 |
where "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
269 |
|
63404 | 270 |
lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
271 |
by (simp add: sym_def symp_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
272 |
|
63404 | 273 |
lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
274 |
by (unfold sym_def) iprover |
46694 | 275 |
|
63404 | 276 |
lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
277 |
by (fact symI [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
278 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
279 |
lemma symE: |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
280 |
assumes "sym r" and "(b, a) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
281 |
obtains "(a, b) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
282 |
using assms by (simp add: sym_def) |
46694 | 283 |
|
284 |
lemma sympE: |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
285 |
assumes "symp r" and "r b a" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
286 |
obtains "r a b" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
287 |
using assms by (rule symE [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
288 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
289 |
lemma symD [dest?]: |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
290 |
assumes "sym r" and "(b, a) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
291 |
shows "(a, b) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
292 |
using assms by (rule symE) |
46694 | 293 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
294 |
lemma sympD [dest?]: |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
295 |
assumes "symp r" and "r b a" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
296 |
shows "r a b" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
297 |
using assms by (rule symD [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
298 |
|
63404 | 299 |
lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
300 |
by (fast intro: symI elim: symE) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
301 |
|
63404 | 302 |
lemma symp_inf: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
303 |
by (fact sym_Int [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
304 |
|
63404 | 305 |
lemma sym_Un: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
306 |
by (fast intro: symI elim: symE) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
307 |
|
63404 | 308 |
lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
309 |
by (fact sym_Un [to_pred]) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
310 |
|
69275 | 311 |
lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Inter>(r ` S))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
312 |
by (fast intro: symI elim: symE) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
313 |
|
69275 | 314 |
lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Sqinter>(r ` S))" |
46982 | 315 |
by (fact sym_INTER [to_pred]) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
316 |
|
69275 | 317 |
lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Union>(r ` S))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
318 |
by (fast intro: symI elim: symE) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
319 |
|
69275 | 320 |
lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Squnion>(r ` S))" |
46982 | 321 |
by (fact sym_UNION [to_pred]) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
322 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
323 |
|
60758 | 324 |
subsubsection \<open>Antisymmetry\<close> |
46694 | 325 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
326 |
definition antisym :: "'a rel \<Rightarrow> bool" |
63404 | 327 |
where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
328 |
|
64634 | 329 |
definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
330 |
where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)" |
|
63404 | 331 |
|
64634 | 332 |
lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r" |
333 |
by (simp add: antisym_def antisymp_def) |
|
334 |
||
335 |
lemma antisymI [intro?]: |
|
336 |
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" |
|
63404 | 337 |
unfolding antisym_def by iprover |
46694 | 338 |
|
64634 | 339 |
lemma antisympI [intro?]: |
340 |
"(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r" |
|
341 |
by (fact antisymI [to_pred]) |
|
342 |
||
343 |
lemma antisymD [dest?]: |
|
344 |
"antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" |
|
63404 | 345 |
unfolding antisym_def by iprover |
46694 | 346 |
|
64634 | 347 |
lemma antisympD [dest?]: |
348 |
"antisymp r \<Longrightarrow> r a b \<Longrightarrow> r b a \<Longrightarrow> a = b" |
|
349 |
by (fact antisymD [to_pred]) |
|
46694 | 350 |
|
64634 | 351 |
lemma antisym_subset: |
352 |
"r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" |
|
63404 | 353 |
unfolding antisym_def by blast |
46694 | 354 |
|
64634 | 355 |
lemma antisymp_less_eq: |
356 |
"r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r" |
|
357 |
by (fact antisym_subset [to_pred]) |
|
358 |
||
359 |
lemma antisym_empty [simp]: |
|
360 |
"antisym {}" |
|
361 |
unfolding antisym_def by blast |
|
46694 | 362 |
|
64634 | 363 |
lemma antisym_bot [simp]: |
364 |
"antisymp \<bottom>" |
|
365 |
by (fact antisym_empty [to_pred]) |
|
366 |
||
367 |
lemma antisymp_equality [simp]: |
|
368 |
"antisymp HOL.eq" |
|
369 |
by (auto intro: antisympI) |
|
370 |
||
371 |
lemma antisym_singleton [simp]: |
|
372 |
"antisym {x}" |
|
373 |
by (blast intro: antisymI) |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
374 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
375 |
|
60758 | 376 |
subsubsection \<open>Transitivity\<close> |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
377 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
378 |
definition trans :: "'a rel \<Rightarrow> bool" |
63404 | 379 |
where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
380 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
381 |
definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
63404 | 382 |
where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
383 |
|
63404 | 384 |
lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
385 |
by (simp add: trans_def transp_def) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
386 |
|
63404 | 387 |
lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
388 |
by (unfold trans_def) iprover |
46694 | 389 |
|
63404 | 390 |
lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
391 |
by (fact transI [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
392 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
393 |
lemma transE: |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
394 |
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
395 |
obtains "(x, z) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
396 |
using assms by (unfold trans_def) iprover |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
397 |
|
46694 | 398 |
lemma transpE: |
399 |
assumes "transp r" and "r x y" and "r y z" |
|
400 |
obtains "r x z" |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
401 |
using assms by (rule transE [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
402 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
403 |
lemma transD [dest?]: |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
404 |
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
405 |
shows "(x, z) \<in> r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
406 |
using assms by (rule transE) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
407 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
408 |
lemma transpD [dest?]: |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
409 |
assumes "transp r" and "r x y" and "r y z" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
410 |
shows "r x z" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
411 |
using assms by (rule transD [to_pred]) |
46694 | 412 |
|
63404 | 413 |
lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
414 |
by (fast intro: transI elim: transE) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
415 |
|
63404 | 416 |
lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
417 |
by (fact trans_Int [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
418 |
|
69275 | 419 |
lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (\<Inter>(r ` S))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
420 |
by (fast intro: transI elim: transD) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
421 |
|
69275 | 422 |
lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))" |
64584 | 423 |
by (fact trans_INTER [to_pred]) |
424 |
||
63404 | 425 |
lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
46694 | 426 |
by (auto simp add: trans_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
427 |
|
63404 | 428 |
lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
429 |
by (simp add: trans_def transp_def) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
430 |
|
67399 | 431 |
lemma transp_equality [simp]: "transp (=)" |
63404 | 432 |
by (auto intro: transpI) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
433 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
434 |
lemma trans_empty [simp]: "trans {}" |
63612 | 435 |
by (blast intro: transI) |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
436 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
437 |
lemma transp_empty [simp]: "transp (\<lambda>x y. False)" |
63612 | 438 |
using trans_empty[to_pred] by (simp add: bot_fun_def) |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
439 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
440 |
lemma trans_singleton [simp]: "trans {(a, a)}" |
63612 | 441 |
by (blast intro: transI) |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
442 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
443 |
lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)" |
63612 | 444 |
by (simp add: transp_def) |
445 |
||
66441 | 446 |
context preorder |
447 |
begin |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
64634
diff
changeset
|
448 |
|
67399 | 449 |
lemma transp_le[simp]: "transp (\<le>)" |
66441 | 450 |
by(auto simp add: transp_def intro: order_trans) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
64634
diff
changeset
|
451 |
|
67399 | 452 |
lemma transp_less[simp]: "transp (<)" |
66441 | 453 |
by(auto simp add: transp_def intro: less_trans) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
64634
diff
changeset
|
454 |
|
67399 | 455 |
lemma transp_ge[simp]: "transp (\<ge>)" |
66441 | 456 |
by(auto simp add: transp_def intro: order_trans) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
64634
diff
changeset
|
457 |
|
67399 | 458 |
lemma transp_gr[simp]: "transp (>)" |
66441 | 459 |
by(auto simp add: transp_def intro: less_trans) |
460 |
||
461 |
end |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
462 |
|
60758 | 463 |
subsubsection \<open>Totality\<close> |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
464 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
465 |
definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
63404 | 466 |
where "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)" |
29859
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset
|
467 |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
468 |
lemma total_onI [intro?]: |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
469 |
"(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r" |
63612 | 470 |
unfolding total_on_def by blast |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
471 |
|
29859
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset
|
472 |
abbreviation "total \<equiv> total_on UNIV" |
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset
|
473 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
474 |
lemma total_on_empty [simp]: "total_on {} r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
475 |
by (simp add: total_on_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
476 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
477 |
lemma total_on_singleton [simp]: "total_on {x} {(x, x)}" |
63612 | 478 |
unfolding total_on_def by blast |
479 |
||
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
480 |
|
60758 | 481 |
subsubsection \<open>Single valued relations\<close> |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
482 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
483 |
definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" |
63404 | 484 |
where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
485 |
|
64634 | 486 |
definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
487 |
where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))" |
|
488 |
||
489 |
lemma single_valuedp_single_valued_eq [pred_set_conv]: |
|
490 |
"single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r" |
|
491 |
by (simp add: single_valued_def single_valuedp_def) |
|
46694 | 492 |
|
71827 | 493 |
lemma single_valuedp_iff_Uniq: |
494 |
"single_valuedp r \<longleftrightarrow> (\<forall>x. \<exists>\<^sub>\<le>\<^sub>1y. r x y)" |
|
495 |
unfolding Uniq_def single_valuedp_def by auto |
|
496 |
||
64634 | 497 |
lemma single_valuedI: |
498 |
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (\<And>z. (x, z) \<in> r \<Longrightarrow> y = z)) \<Longrightarrow> single_valued r" |
|
499 |
unfolding single_valued_def by blast |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
500 |
|
64634 | 501 |
lemma single_valuedpI: |
502 |
"(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r" |
|
503 |
by (fact single_valuedI [to_pred]) |
|
504 |
||
505 |
lemma single_valuedD: |
|
506 |
"single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
507 |
by (simp add: single_valued_def) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
508 |
|
64634 | 509 |
lemma single_valuedpD: |
510 |
"single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z" |
|
511 |
by (fact single_valuedD [to_pred]) |
|
512 |
||
513 |
lemma single_valued_empty [simp]: |
|
514 |
"single_valued {}" |
|
63404 | 515 |
by (simp add: single_valued_def) |
52392 | 516 |
|
64634 | 517 |
lemma single_valuedp_bot [simp]: |
518 |
"single_valuedp \<bottom>" |
|
519 |
by (fact single_valued_empty [to_pred]) |
|
520 |
||
521 |
lemma single_valued_subset: |
|
522 |
"r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" |
|
63404 | 523 |
unfolding single_valued_def by blast |
11136 | 524 |
|
64634 | 525 |
lemma single_valuedp_less_eq: |
526 |
"r \<le> s \<Longrightarrow> single_valuedp s \<Longrightarrow> single_valuedp r" |
|
527 |
by (fact single_valued_subset [to_pred]) |
|
528 |
||
12905 | 529 |
|
60758 | 530 |
subsection \<open>Relation operations\<close> |
46694 | 531 |
|
60758 | 532 |
subsubsection \<open>The identity relation\<close> |
12905 | 533 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
534 |
definition Id :: "'a rel" |
69905 | 535 |
where "Id = {p. \<exists>x. p = (x, x)}" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
536 |
|
63404 | 537 |
lemma IdI [intro]: "(a, a) \<in> Id" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
538 |
by (simp add: Id_def) |
12905 | 539 |
|
63404 | 540 |
lemma IdE [elim!]: "p \<in> Id \<Longrightarrow> (\<And>x. p = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" |
541 |
unfolding Id_def by (iprover elim: CollectE) |
|
12905 | 542 |
|
63404 | 543 |
lemma pair_in_Id_conv [iff]: "(a, b) \<in> Id \<longleftrightarrow> a = b" |
544 |
unfolding Id_def by blast |
|
12905 | 545 |
|
30198 | 546 |
lemma refl_Id: "refl Id" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
547 |
by (simp add: refl_on_def) |
12905 | 548 |
|
549 |
lemma antisym_Id: "antisym Id" |
|
61799 | 550 |
\<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close> |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
551 |
by (simp add: antisym_def) |
12905 | 552 |
|
19228 | 553 |
lemma sym_Id: "sym Id" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
554 |
by (simp add: sym_def) |
19228 | 555 |
|
12905 | 556 |
lemma trans_Id: "trans Id" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
557 |
by (simp add: trans_def) |
12905 | 558 |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
559 |
lemma single_valued_Id [simp]: "single_valued Id" |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
560 |
by (unfold single_valued_def) blast |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
561 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
562 |
lemma irrefl_diff_Id [simp]: "irrefl (r - Id)" |
63404 | 563 |
by (simp add: irrefl_def) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
564 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
565 |
lemma trans_diff_Id: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)" |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
566 |
unfolding antisym_def trans_def by blast |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
567 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
568 |
lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r" |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
569 |
by (simp add: total_on_def) |
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
570 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
571 |
lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}" |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
572 |
by force |
12905 | 573 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
574 |
|
60758 | 575 |
subsubsection \<open>Diagonal: identity over a set\<close> |
12905 | 576 |
|
63612 | 577 |
definition Id_on :: "'a set \<Rightarrow> 'a rel" |
63404 | 578 |
where "Id_on A = (\<Union>x\<in>A. {(x, x)})" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
579 |
|
30198 | 580 |
lemma Id_on_empty [simp]: "Id_on {} = {}" |
63404 | 581 |
by (simp add: Id_on_def) |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset
|
582 |
|
63404 | 583 |
lemma Id_on_eqI: "a = b \<Longrightarrow> a \<in> A \<Longrightarrow> (a, b) \<in> Id_on A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
584 |
by (simp add: Id_on_def) |
12905 | 585 |
|
63404 | 586 |
lemma Id_onI [intro!]: "a \<in> A \<Longrightarrow> (a, a) \<in> Id_on A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
587 |
by (rule Id_on_eqI) (rule refl) |
12905 | 588 |
|
63404 | 589 |
lemma Id_onE [elim!]: "c \<in> Id_on A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> c = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" |
61799 | 590 |
\<comment> \<open>The general elimination rule.\<close> |
63404 | 591 |
unfolding Id_on_def by (iprover elim!: UN_E singletonE) |
12905 | 592 |
|
63404 | 593 |
lemma Id_on_iff: "(x, y) \<in> Id_on A \<longleftrightarrow> x = y \<and> x \<in> A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
594 |
by blast |
12905 | 595 |
|
63404 | 596 |
lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
597 |
by auto |
40923
be80c93ac0a2
adding a nice definition of Id_on for quickcheck and nitpick
bulwahn
parents:
36772
diff
changeset
|
598 |
|
30198 | 599 |
lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
600 |
by blast |
12905 | 601 |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
602 |
lemma refl_on_Id_on: "refl_on A (Id_on A)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
603 |
by (rule refl_onI [OF Id_on_subset_Times Id_onI]) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
604 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
605 |
lemma antisym_Id_on [simp]: "antisym (Id_on A)" |
63404 | 606 |
unfolding antisym_def by blast |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
607 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
608 |
lemma sym_Id_on [simp]: "sym (Id_on A)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
609 |
by (rule symI) clarify |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
610 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
611 |
lemma trans_Id_on [simp]: "trans (Id_on A)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
612 |
by (fast intro: transI elim: transD) |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
613 |
|
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
614 |
lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" |
63404 | 615 |
unfolding single_valued_def by blast |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
616 |
|
12905 | 617 |
|
60758 | 618 |
subsubsection \<open>Composition\<close> |
12905 | 619 |
|
63404 | 620 |
inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
621 |
for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" |
63404 | 622 |
where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
623 |
|
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset
|
624 |
notation relcompp (infixr "OO" 75) |
12905 | 625 |
|
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset
|
626 |
lemmas relcomppI = relcompp.intros |
12905 | 627 |
|
60758 | 628 |
text \<open> |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
629 |
For historic reasons, the elimination rules are not wholly corresponding. |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
630 |
Feel free to consolidate this. |
60758 | 631 |
\<close> |
46694 | 632 |
|
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
633 |
inductive_cases relcompEpair: "(a, c) \<in> r O s" |
47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset
|
634 |
inductive_cases relcomppE [elim!]: "(r OO s) a c" |
46694 | 635 |
|
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
636 |
lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
637 |
(\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" |
63404 | 638 |
apply (cases xz) |
639 |
apply simp |
|
640 |
apply (erule relcompEpair) |
|
641 |
apply iprover |
|
642 |
done |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
643 |
|
63404 | 644 |
lemma R_O_Id [simp]: "R O Id = R" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
645 |
by fast |
46694 | 646 |
|
63404 | 647 |
lemma Id_O_R [simp]: "Id O R = R" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
648 |
by fast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
649 |
|
63404 | 650 |
lemma relcomp_empty1 [simp]: "{} O R = {}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
651 |
by blast |
12905 | 652 |
|
63404 | 653 |
lemma relcompp_bot1 [simp]: "\<bottom> OO R = \<bottom>" |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
654 |
by (fact relcomp_empty1 [to_pred]) |
12905 | 655 |
|
63404 | 656 |
lemma relcomp_empty2 [simp]: "R O {} = {}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
657 |
by blast |
12905 | 658 |
|
63404 | 659 |
lemma relcompp_bot2 [simp]: "R OO \<bottom> = \<bottom>" |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
660 |
by (fact relcomp_empty2 [to_pred]) |
23185 | 661 |
|
63404 | 662 |
lemma O_assoc: "(R O S) O T = R O (S O T)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
663 |
by blast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
664 |
|
63404 | 665 |
lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
666 |
by (fact O_assoc [to_pred]) |
23185 | 667 |
|
63404 | 668 |
lemma trans_O_subset: "trans r \<Longrightarrow> r O r \<subseteq> r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
669 |
by (unfold trans_def) blast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
670 |
|
63404 | 671 |
lemma transp_relcompp_less_eq: "transp r \<Longrightarrow> r OO r \<le> r " |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
672 |
by (fact trans_O_subset [to_pred]) |
12905 | 673 |
|
63404 | 674 |
lemma relcomp_mono: "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
675 |
by blast |
12905 | 676 |
|
63404 | 677 |
lemma relcompp_mono: "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
678 |
by (fact relcomp_mono [to_pred]) |
12905 | 679 |
|
63404 | 680 |
lemma relcomp_subset_Sigma: "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
681 |
by blast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
682 |
|
63404 | 683 |
lemma relcomp_distrib [simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
684 |
by auto |
12905 | 685 |
|
63404 | 686 |
lemma relcompp_distrib [simp]: "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
687 |
by (fact relcomp_distrib [to_pred]) |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
688 |
|
63404 | 689 |
lemma relcomp_distrib2 [simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
690 |
by auto |
28008
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset
|
691 |
|
63404 | 692 |
lemma relcompp_distrib2 [simp]: "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" |
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset
|
693 |
by (fact relcomp_distrib2 [to_pred]) |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
694 |
|
69275 | 695 |
lemma relcomp_UNION_distrib: "s O \<Union>(r ` I) = (\<Union>i\<in>I. s O r i) " |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
696 |
by auto |
28008
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset
|
697 |
|
69275 | 698 |
lemma relcompp_SUP_distrib: "s OO \<Squnion>(r ` I) = (\<Squnion>i\<in>I. s OO r i)" |
64584 | 699 |
by (fact relcomp_UNION_distrib [to_pred]) |
700 |
||
69275 | 701 |
lemma relcomp_UNION_distrib2: "\<Union>(r ` I) O s = (\<Union>i\<in>I. r i O s) " |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
702 |
by auto |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
703 |
|
69275 | 704 |
lemma relcompp_SUP_distrib2: "\<Squnion>(r ` I) OO s = (\<Squnion>i\<in>I. r i OO s)" |
64584 | 705 |
by (fact relcomp_UNION_distrib2 [to_pred]) |
706 |
||
63404 | 707 |
lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" |
708 |
unfolding single_valued_def by blast |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
709 |
|
63404 | 710 |
lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
711 |
by (auto simp add: set_eq_iff) |
12905 | 712 |
|
58195 | 713 |
lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)" |
714 |
unfolding relcomp_unfold [to_pred] .. |
|
715 |
||
67399 | 716 |
lemma eq_OO: "(=) OO R = R" |
63404 | 717 |
by blast |
55083 | 718 |
|
67399 | 719 |
lemma OO_eq: "R OO (=) = R" |
63404 | 720 |
by blast |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
721 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
722 |
|
60758 | 723 |
subsubsection \<open>Converse\<close> |
12913 | 724 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
725 |
inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999) |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
726 |
for r :: "('a \<times> 'b) set" |
63404 | 727 |
where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
728 |
|
63404 | 729 |
notation conversep ("(_\<inverse>\<inverse>)" [1000] 1000) |
46694 | 730 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
731 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
732 |
converse ("(_^-1)" [1000] 999) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset
|
733 |
conversep ("(_^--1)" [1000] 1000) |
46694 | 734 |
|
63404 | 735 |
lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
736 |
by (fact converse.intros) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
737 |
|
63404 | 738 |
lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
739 |
by (fact conversep.intros) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
740 |
|
63404 | 741 |
lemma converseD [sym]: "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
742 |
by (erule converse.cases) iprover |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
743 |
|
63404 | 744 |
lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
745 |
by (fact converseD [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
746 |
|
63404 | 747 |
lemma converseE [elim!]: "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" |
61799 | 748 |
\<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close> |
63404 | 749 |
apply (cases yx) |
750 |
apply simp |
|
751 |
apply (erule converse.cases) |
|
752 |
apply iprover |
|
753 |
done |
|
46694 | 754 |
|
46882 | 755 |
lemmas conversepE [elim!] = conversep.cases |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
756 |
|
63404 | 757 |
lemma converse_iff [iff]: "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
758 |
by (auto intro: converseI) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
759 |
|
63404 | 760 |
lemma conversep_iff [iff]: "r\<inverse>\<inverse> a b = r b a" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
761 |
by (fact converse_iff [to_pred]) |
46694 | 762 |
|
63404 | 763 |
lemma converse_converse [simp]: "(r\<inverse>)\<inverse> = r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
764 |
by (simp add: set_eq_iff) |
46694 | 765 |
|
63404 | 766 |
lemma conversep_conversep [simp]: "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
767 |
by (fact converse_converse [to_pred]) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
768 |
|
53680 | 769 |
lemma converse_empty[simp]: "{}\<inverse> = {}" |
63404 | 770 |
by auto |
53680 | 771 |
|
772 |
lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV" |
|
63404 | 773 |
by auto |
53680 | 774 |
|
63404 | 775 |
lemma converse_relcomp: "(r O s)\<inverse> = s\<inverse> O r\<inverse>" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
776 |
by blast |
46694 | 777 |
|
63404 | 778 |
lemma converse_relcompp: "(r OO s)\<inverse>\<inverse> = s\<inverse>\<inverse> OO r\<inverse>\<inverse>" |
779 |
by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD) |
|
46694 | 780 |
|
63404 | 781 |
lemma converse_Int: "(r \<inter> s)\<inverse> = r\<inverse> \<inter> s\<inverse>" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
782 |
by blast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
783 |
|
63404 | 784 |
lemma converse_meet: "(r \<sqinter> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<sqinter> s\<inverse>\<inverse>" |
46694 | 785 |
by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) |
786 |
||
63404 | 787 |
lemma converse_Un: "(r \<union> s)\<inverse> = r\<inverse> \<union> s\<inverse>" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
788 |
by blast |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
789 |
|
63404 | 790 |
lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>" |
46694 | 791 |
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) |
792 |
||
69275 | 793 |
lemma converse_INTER: "(\<Inter>(r ` S))\<inverse> = (\<Inter>x\<in>S. (r x)\<inverse>)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
794 |
by fast |
19228 | 795 |
|
69275 | 796 |
lemma converse_UNION: "(\<Union>(r ` S))\<inverse> = (\<Union>x\<in>S. (r x)\<inverse>)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
797 |
by blast |
19228 | 798 |
|
63404 | 799 |
lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s" |
52749 | 800 |
by auto |
801 |
||
63404 | 802 |
lemma conversep_mono[simp]: "r\<inverse>\<inverse> \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<le> s" |
52749 | 803 |
by (fact converse_mono[to_pred]) |
804 |
||
63404 | 805 |
lemma converse_inject[simp]: "r\<inverse> = s \<inverse> \<longleftrightarrow> r = s" |
52730 | 806 |
by auto |
807 |
||
63404 | 808 |
lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s" |
52749 | 809 |
by (fact converse_inject[to_pred]) |
810 |
||
63612 | 811 |
lemma converse_subset_swap: "r \<subseteq> s \<inverse> \<longleftrightarrow> r \<inverse> \<subseteq> s" |
52749 | 812 |
by auto |
813 |
||
63612 | 814 |
lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<inverse>\<inverse> \<le> s" |
52749 | 815 |
by (fact converse_subset_swap[to_pred]) |
52730 | 816 |
|
63404 | 817 |
lemma converse_Id [simp]: "Id\<inverse> = Id" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
818 |
by blast |
12905 | 819 |
|
63404 | 820 |
lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
821 |
by blast |
12905 | 822 |
|
30198 | 823 |
lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" |
63404 | 824 |
by (auto simp: refl_on_def) |
12905 | 825 |
|
19228 | 826 |
lemma sym_converse [simp]: "sym (converse r) = sym r" |
63404 | 827 |
unfolding sym_def by blast |
19228 | 828 |
|
829 |
lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
|
63404 | 830 |
unfolding antisym_def by blast |
12905 | 831 |
|
19228 | 832 |
lemma trans_converse [simp]: "trans (converse r) = trans r" |
63404 | 833 |
unfolding trans_def by blast |
12905 | 834 |
|
63404 | 835 |
lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r" |
836 |
unfolding sym_def by fast |
|
19228 | 837 |
|
63404 | 838 |
lemma sym_Un_converse: "sym (r \<union> r\<inverse>)" |
839 |
unfolding sym_def by blast |
|
19228 | 840 |
|
63404 | 841 |
lemma sym_Int_converse: "sym (r \<inter> r\<inverse>)" |
842 |
unfolding sym_def by blast |
|
19228 | 843 |
|
63404 | 844 |
lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
845 |
by (auto simp: total_on_def) |
29859
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset
|
846 |
|
63404 | 847 |
lemma finite_converse [iff]: "finite (r\<inverse>) = finite r" |
68455 | 848 |
unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] |
849 |
by (auto elim: finite_imageD simp: inj_on_def) |
|
850 |
||
851 |
lemma card_inverse[simp]: "card (R\<inverse>) = card R" |
|
852 |
proof - |
|
853 |
have *: "\<And>R. prod.swap ` R = R\<inverse>" by auto |
|
854 |
{ |
|
855 |
assume "\<not>finite R" |
|
856 |
hence ?thesis |
|
857 |
by auto |
|
858 |
} moreover { |
|
859 |
assume "finite R" |
|
860 |
with card_image_le[of R prod.swap] card_image_le[of "R\<inverse>" prod.swap] |
|
861 |
have ?thesis by (auto simp: *) |
|
862 |
} ultimately show ?thesis by blast |
|
863 |
qed |
|
12913 | 864 |
|
67399 | 865 |
lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
866 |
by (auto simp add: fun_eq_iff) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
867 |
|
67399 | 868 |
lemma conversep_eq [simp]: "(=)\<inverse>\<inverse> = (=)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
869 |
by (auto simp add: fun_eq_iff) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
870 |
|
63404 | 871 |
lemma converse_unfold [code]: "r\<inverse> = {(y, x). (x, y) \<in> r}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
872 |
by (simp add: set_eq_iff) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
873 |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
874 |
|
60758 | 875 |
subsubsection \<open>Domain, range and field\<close> |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
876 |
|
63404 | 877 |
inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" for r :: "('a \<times> 'b) set" |
878 |
where DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" |
|
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
879 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
880 |
lemmas DomainPI = Domainp.DomainI |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
881 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
882 |
inductive_cases DomainE [elim!]: "a \<in> Domain r" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
883 |
inductive_cases DomainpE [elim!]: "Domainp r a" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
884 |
|
63404 | 885 |
inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" for r :: "('a \<times> 'b) set" |
886 |
where RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" |
|
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
887 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
888 |
lemmas RangePI = Rangep.RangeI |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
889 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
890 |
inductive_cases RangeE [elim!]: "b \<in> Range r" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
891 |
inductive_cases RangepE [elim!]: "Rangep r b" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
892 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
893 |
definition Field :: "'a rel \<Rightarrow> 'a set" |
63404 | 894 |
where "Field r = Domain r \<union> Range r" |
12905 | 895 |
|
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
896 |
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R" |
63612 | 897 |
unfolding Field_def by blast |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
898 |
|
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
899 |
lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
900 |
unfolding Field_def by auto |
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
901 |
|
63404 | 902 |
lemma Domain_fst [code]: "Domain r = fst ` r" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
903 |
by force |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
904 |
|
63404 | 905 |
lemma Range_snd [code]: "Range r = snd ` r" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
906 |
by force |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
907 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
908 |
lemma fst_eq_Domain: "fst ` R = Domain R" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
909 |
by force |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
910 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
911 |
lemma snd_eq_Range: "snd ` R = Range R" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
912 |
by force |
46694 | 913 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
914 |
lemma range_fst [simp]: "range fst = UNIV" |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
915 |
by (auto simp: fst_eq_Domain) |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
916 |
|
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
917 |
lemma range_snd [simp]: "range snd = UNIV" |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
918 |
by (auto simp: snd_eq_Range) |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset
|
919 |
|
46694 | 920 |
lemma Domain_empty [simp]: "Domain {} = {}" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
921 |
by auto |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
922 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
923 |
lemma Range_empty [simp]: "Range {} = {}" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
924 |
by auto |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
925 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
926 |
lemma Field_empty [simp]: "Field {} = {}" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
927 |
by (simp add: Field_def) |
46694 | 928 |
|
929 |
lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}" |
|
930 |
by auto |
|
931 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
932 |
lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
933 |
by auto |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
934 |
|
46882 | 935 |
lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
936 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
937 |
|
46882 | 938 |
lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
939 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
940 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
941 |
lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r" |
46884 | 942 |
by (auto simp add: Field_def) |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
943 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
944 |
lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
945 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
946 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
947 |
lemma Range_iff: "a \<in> Range r \<longleftrightarrow> (\<exists>y. (y, a) \<in> r)" |
46694 | 948 |
by blast |
949 |
||
950 |
lemma Domain_Id [simp]: "Domain Id = UNIV" |
|
951 |
by blast |
|
952 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
953 |
lemma Range_Id [simp]: "Range Id = UNIV" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
954 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
955 |
|
46694 | 956 |
lemma Domain_Id_on [simp]: "Domain (Id_on A) = A" |
957 |
by blast |
|
958 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
959 |
lemma Range_Id_on [simp]: "Range (Id_on A) = A" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
960 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
961 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
962 |
lemma Domain_Un_eq: "Domain (A \<union> B) = Domain A \<union> Domain B" |
46694 | 963 |
by blast |
964 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
965 |
lemma Range_Un_eq: "Range (A \<union> B) = Range A \<union> Range B" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
966 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
967 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
968 |
lemma Field_Un [simp]: "Field (r \<union> s) = Field r \<union> Field s" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
969 |
by (auto simp: Field_def) |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
970 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
971 |
lemma Domain_Int_subset: "Domain (A \<inter> B) \<subseteq> Domain A \<inter> Domain B" |
46694 | 972 |
by blast |
973 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
974 |
lemma Range_Int_subset: "Range (A \<inter> B) \<subseteq> Range A \<inter> Range B" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
975 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
976 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
977 |
lemma Domain_Diff_subset: "Domain A - Domain B \<subseteq> Domain (A - B)" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
978 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
979 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
980 |
lemma Range_Diff_subset: "Range A - Range B \<subseteq> Range (A - B)" |
46694 | 981 |
by blast |
982 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
983 |
lemma Domain_Union: "Domain (\<Union>S) = (\<Union>A\<in>S. Domain A)" |
46694 | 984 |
by blast |
985 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
986 |
lemma Range_Union: "Range (\<Union>S) = (\<Union>A\<in>S. Range A)" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
987 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
988 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
989 |
lemma Field_Union [simp]: "Field (\<Union>R) = \<Union>(Field ` R)" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
990 |
by (auto simp: Field_def) |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
991 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
992 |
lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r" |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
993 |
by auto |
46694 | 994 |
|
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
995 |
lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r" |
46694 | 996 |
by blast |
997 |
||
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
998 |
lemma Field_converse [simp]: "Field (r\<inverse>) = Field r" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
999 |
by (auto simp: Field_def) |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1000 |
|
63404 | 1001 |
lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. \<exists>y. P x y}" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1002 |
by auto |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1003 |
|
63404 | 1004 |
lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \<exists>x. P x y}" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1005 |
by auto |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1006 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1007 |
lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)" |
46884 | 1008 |
by (induct set: finite) auto |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1009 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1010 |
lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)" |
46884 | 1011 |
by (induct set: finite) auto |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1012 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1013 |
lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1014 |
by (simp add: Field_def finite_Domain finite_Range) |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1015 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1016 |
lemma Domain_mono: "r \<subseteq> s \<Longrightarrow> Domain r \<subseteq> Domain s" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1017 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1018 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1019 |
lemma Range_mono: "r \<subseteq> s \<Longrightarrow> Range r \<subseteq> Range s" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1020 |
by blast |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1021 |
|
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1022 |
lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s" |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1023 |
by (auto simp: Field_def Domain_def Range_def) |
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1024 |
|
63404 | 1025 |
lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}" |
46767
807a5d219c23
more fundamental pred-to-set conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset
|
1026 |
by blast |
46694 | 1027 |
|
63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOL-UNITY
Andreas Lochbihler
parents:
63561
diff
changeset
|
1028 |
lemma Field_square [simp]: "Field (x \<times> x) = x" |
63612 | 1029 |
unfolding Field_def by blast |
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset
|
1030 |
|
12905 | 1031 |
|
60758 | 1032 |
subsubsection \<open>Image of a set under a relation\<close> |
12905 | 1033 |
|
63404 | 1034 |
definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90) |
1035 |
where "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}" |
|
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
1036 |
|
63404 | 1037 |
lemma Image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. (x, b) \<in> r)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1038 |
by (simp add: Image_def) |
12905 | 1039 |
|
63404 | 1040 |
lemma Image_singleton: "r``{a} = {b. (a, b) \<in> r}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1041 |
by (simp add: Image_def) |
12905 | 1042 |
|
63404 | 1043 |
lemma Image_singleton_iff [iff]: "b \<in> r``{a} \<longleftrightarrow> (a, b) \<in> r" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1044 |
by (rule Image_iff [THEN trans]) simp |
12905 | 1045 |
|
63404 | 1046 |
lemma ImageI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> r``A" |
1047 |
unfolding Image_def by blast |
|
12905 | 1048 |
|
63404 | 1049 |
lemma ImageE [elim!]: "b \<in> r `` A \<Longrightarrow> (\<And>x. (x, b) \<in> r \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" |
1050 |
unfolding Image_def by (iprover elim!: CollectE bexE) |
|
12905 | 1051 |
|
63404 | 1052 |
lemma rev_ImageI: "a \<in> A \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> b \<in> r `` A" |
61799 | 1053 |
\<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close> |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1054 |
by blast |
12905 | 1055 |
|
68455 | 1056 |
lemma Image_empty1 [simp]: "{} `` X = {}" |
1057 |
by auto |
|
1058 |
||
1059 |
lemma Image_empty2 [simp]: "R``{} = {}" |
|
1060 |
by blast |
|
12905 | 1061 |
|
1062 |
lemma Image_Id [simp]: "Id `` A = A" |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1063 |
by blast |
12905 | 1064 |
|
30198 | 1065 |
lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1066 |
by blast |
13830 | 1067 |
|
1068 |
lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1069 |
by blast |
12905 | 1070 |
|
63404 | 1071 |
lemma Image_Int_eq: "single_valued (converse R) \<Longrightarrow> R `` (A \<inter> B) = R `` A \<inter> R `` B" |
63612 | 1072 |
by (auto simp: single_valued_def) |
12905 | 1073 |
|
13830 | 1074 |
lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1075 |
by blast |
12905 | 1076 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset
|
1077 |
lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1078 |
by blast |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset
|
1079 |
|
63404 | 1080 |
lemma Image_subset: "r \<subseteq> A \<times> B \<Longrightarrow> r``C \<subseteq> B" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1081 |
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) |
12905 | 1082 |
|
13830 | 1083 |
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" |
61799 | 1084 |
\<comment> \<open>NOT suitable for rewriting\<close> |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1085 |
by blast |
12905 | 1086 |
|
63404 | 1087 |
lemma Image_mono: "r' \<subseteq> r \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> (r' `` A') \<subseteq> (r `` A)" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1088 |
by blast |
12905 | 1089 |
|
69275 | 1090 |
lemma Image_UN: "r `` (\<Union>(B ` A)) = (\<Union>x\<in>A. r `` (B x))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1091 |
by blast |
13830 | 1092 |
|
54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1093 |
lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)" |
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1094 |
by auto |
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1095 |
|
69275 | 1096 |
lemma Image_INT_subset: "(r `` (\<Inter>(B ` A))) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1097 |
by blast |
12905 | 1098 |
|
63404 | 1099 |
text \<open>Converse inclusion requires some assumptions\<close> |
69275 | 1100 |
lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)" |
63404 | 1101 |
apply (rule equalityI) |
1102 |
apply (rule Image_INT_subset) |
|
1103 |
apply (auto simp add: single_valued_def) |
|
1104 |
apply blast |
|
1105 |
done |
|
12905 | 1106 |
|
63404 | 1107 |
lemma Image_subset_eq: "r``A \<subseteq> B \<longleftrightarrow> A \<subseteq> - ((r\<inverse>) `` (- B))" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1108 |
by blast |
12905 | 1109 |
|
63404 | 1110 |
lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. \<exists>x\<in>A. P x y}" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1111 |
by auto |
12905 | 1112 |
|
54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1113 |
lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)" |
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1114 |
by auto |
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1115 |
|
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1116 |
lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)" |
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset
|
1117 |
by auto |
12905 | 1118 |
|
68455 | 1119 |
lemma finite_Image[simp]: assumes "finite R" shows "finite (R `` A)" |
1120 |
by(rule finite_subset[OF _ finite_Range[OF assms]]) auto |
|
1121 |
||
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
1122 |
|
60758 | 1123 |
subsubsection \<open>Inverse image\<close> |
12905 | 1124 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1125 |
definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel" |
63404 | 1126 |
where "inv_image r f = {(x, y). (f x, f y) \<in> r}" |
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset
|
1127 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1128 |
definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
63404 | 1129 |
where "inv_imagep r f = (\<lambda>x y. r (f x) (f y))" |
46694 | 1130 |
|
1131 |
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" |
|
1132 |
by (simp add: inv_image_def inv_imagep_def) |
|
1133 |
||
63404 | 1134 |
lemma sym_inv_image: "sym r \<Longrightarrow> sym (inv_image r f)" |
1135 |
unfolding sym_def inv_image_def by blast |
|
19228 | 1136 |
|
63404 | 1137 |
lemma trans_inv_image: "trans r \<Longrightarrow> trans (inv_image r f)" |
1138 |
unfolding trans_def inv_image_def |
|
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69905
diff
changeset
|
1139 |
by (simp (no_asm)) blast |
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69905
diff
changeset
|
1140 |
|
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69905
diff
changeset
|
1141 |
lemma total_inv_image: "\<lbrakk>inj f; total r\<rbrakk> \<Longrightarrow> total (inv_image r f)" |
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69905
diff
changeset
|
1142 |
unfolding inv_image_def total_on_def by (auto simp: inj_eq) |
12905 | 1143 |
|
71935
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
1144 |
lemma asym_inv_image: "asym R \<Longrightarrow> asym (inv_image R f)" |
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
1145 |
by (simp add: inv_image_def asym_iff) |
82b00b8f1871
fixed the utterly weird definitions of asym / asymp, and added many asym lemmas
paulson <lp15@cam.ac.uk>
parents:
71827
diff
changeset
|
1146 |
|
63404 | 1147 |
lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r" |
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
69905
diff
changeset
|
1148 |
by (auto simp: inv_image_def) |
32463
3a0a65ca2261
moved lemma Wellfounded.in_inv_image to Relation.thy
krauss
parents:
32235
diff
changeset
|
1149 |
|
63404 | 1150 |
lemma converse_inv_image[simp]: "(inv_image R f)\<inverse> = inv_image (R\<inverse>) f" |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1151 |
unfolding inv_image_def converse_unfold by auto |
33218 | 1152 |
|
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1153 |
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1154 |
by (simp add: inv_imagep_def) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1155 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1156 |
|
60758 | 1157 |
subsubsection \<open>Powerset\<close> |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1158 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset
|
1159 |
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" |
63404 | 1160 |
where "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1161 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1162 |
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1163 |
by (auto simp add: Powp_def fun_eq_iff) |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1164 |
|
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1165 |
lemmas Powp_mono [mono] = Pow_mono [to_pred] |
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
1166 |
|
63376
4c0cc2b356f0
default one-step rules for predicates on relations;
haftmann
parents:
62343
diff
changeset
|
1167 |
|
69593 | 1168 |
subsubsection \<open>Expressing relation operations via \<^const>\<open>Finite_Set.fold\<close>\<close> |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1169 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1170 |
lemma Id_on_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1171 |
assumes "finite A" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1172 |
shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1173 |
proof - |
63404 | 1174 |
interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" |
1175 |
by standard auto |
|
1176 |
from assms show ?thesis |
|
1177 |
unfolding Id_on_def by (induct A) simp_all |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1178 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1179 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1180 |
lemma comp_fun_commute_Image_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1181 |
"comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1182 |
proof - |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1183 |
interpret comp_fun_idem Set.insert |
63404 | 1184 |
by (fact comp_fun_idem_insert) |
1185 |
show ?thesis |
|
63612 | 1186 |
by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split) |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1187 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1188 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1189 |
lemma Image_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1190 |
assumes "finite R" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1191 |
shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1192 |
proof - |
63404 | 1193 |
interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1194 |
by (rule comp_fun_commute_Image_fold) |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1195 |
have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))" |
52749 | 1196 |
by (force intro: rev_ImageI) |
63404 | 1197 |
show ?thesis |
1198 |
using assms by (induct R) (auto simp: *) |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1199 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1200 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1201 |
lemma insert_relcomp_union_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1202 |
assumes "finite S" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1203 |
shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1204 |
proof - |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1205 |
interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" |
63404 | 1206 |
proof - |
1207 |
interpret comp_fun_idem Set.insert |
|
1208 |
by (fact comp_fun_idem_insert) |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1209 |
show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" |
63404 | 1210 |
by standard (auto simp add: fun_eq_iff split: prod.split) |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1211 |
qed |
63404 | 1212 |
have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}" |
1213 |
by (auto simp: relcomp_unfold intro!: exI) |
|
1214 |
show ?thesis |
|
1215 |
unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split) |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1216 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1217 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1218 |
lemma insert_relcomp_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1219 |
assumes "finite S" |
63404 | 1220 |
shows "Set.insert x R O S = |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1221 |
Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1222 |
proof - |
63404 | 1223 |
have "Set.insert x R O S = ({x} O S) \<union> (R O S)" |
1224 |
by auto |
|
1225 |
then show ?thesis |
|
1226 |
by (auto simp: insert_relcomp_union_fold [OF assms]) |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1227 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1228 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1229 |
lemma comp_fun_commute_relcomp_fold: |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1230 |
assumes "finite S" |
63404 | 1231 |
shows "comp_fun_commute (\<lambda>(x,y) A. |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1232 |
Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1233 |
proof - |
63404 | 1234 |
have *: "\<And>a b A. |
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1235 |
Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A" |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1236 |
by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) |
63404 | 1237 |
show ?thesis |
1238 |
by standard (auto simp: *) |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1239 |
qed |
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1240 |
|
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1241 |
lemma relcomp_fold: |
63404 | 1242 |
assumes "finite R" "finite S" |
1243 |
shows "R O S = Finite_Set.fold |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1244 |
(\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R" |
73832 | 1245 |
proof - |
1246 |
interpret commute_relcomp_fold: comp_fun_commute |
|
1247 |
"(\<lambda>(x, y) A. Finite_Set.fold (\<lambda>(w, z) A'. if y = w then insert (x, z) A' else A') A S)" |
|
1248 |
by (fact comp_fun_commute_relcomp_fold[OF \<open>finite S\<close>]) |
|
1249 |
from assms show ?thesis |
|
1250 |
by (induct R) (auto simp: comp_fun_commute_relcomp_fold insert_relcomp_fold cong: if_cong) |
|
1251 |
qed |
|
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset
|
1252 |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
1253 |
end |