author  haftmann 
Wed, 21 Dec 2016 21:26:26 +0100  
changeset 64633  5ebcf6c525f1 
parent 64632  9df24b8b6c0a 
child 64634  5bd30359e46e 
permissions  rwrr 
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 onestep 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 

46833  123 
lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)" 
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 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55096
diff
changeset

129 
lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)" 
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 

135 
lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)" 

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 

55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55096
diff
changeset

141 
lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)" 
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 onestep 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 predtoset 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 predtoset 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 predtoset 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 predtoset 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 onestep 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 predtoset 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 predtoset 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 predtoset 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 predtoset 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 

63404  201 
lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (INTER S A) (INTER S r)" 
202 
unfolding refl_on_def by fast 

46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

203 

63404  204 
lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)" 
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 predtoset 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 HOLUNITY
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 predtoset 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 predtoset 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 

60057  217 
lemma reflp_equality [simp]: "reflp op =" 
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 onestep 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 predtoset 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" 

63404  248 
where asymI: "irrefl R \<Longrightarrow> (\<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" 

63404  251 
where asympI: "irreflp R \<Longrightarrow> (\<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 

256 

60758  257 
subsubsection \<open>Symmetry\<close> 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

258 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

259 
definition sym :: "'a rel \<Rightarrow> bool" 
63404  260 
where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

261 

e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

262 
definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
63404  263 
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

264 

63404  265 
lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

266 
by (simp add: sym_def symp_def) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

267 

63404  268 
lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

269 
by (unfold sym_def) iprover 
46694  270 

63404  271 
lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

272 
by (fact symI [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

273 

e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

274 
lemma symE: 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

275 
assumes "sym r" and "(b, a) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

276 
obtains "(a, b) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

277 
using assms by (simp add: sym_def) 
46694  278 

279 
lemma sympE: 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

280 
assumes "symp r" and "r b a" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

281 
obtains "r a b" 
e9e7209eb375
more fundamental predtoset 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 (rule symE [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

283 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

284 
lemma symD [dest?]: 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

285 
assumes "sym r" and "(b, a) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

286 
shows "(a, b) \<in> r" 
e9e7209eb375
more fundamental predtoset 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) 
46694  288 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

289 
lemma sympD [dest?]: 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

290 
assumes "symp r" and "r b a" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

291 
shows "r a b" 
e9e7209eb375
more fundamental predtoset 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 symD [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

293 

63404  294 
lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

295 
by (fast intro: symI elim: symE) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

296 

63404  297 
lemma symp_inf: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

298 
by (fact sym_Int [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

299 

63404  300 
lemma sym_Un: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

301 
by (fast intro: symI elim: symE) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

302 

63404  303 
lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

304 
by (fact sym_Un [to_pred]) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

305 

63404  306 
lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

307 
by (fast intro: symI elim: symE) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

308 

63404  309 
lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)" 
46982  310 
by (fact sym_INTER [to_pred]) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

311 

63404  312 
lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

313 
by (fast intro: symI elim: symE) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

314 

63404  315 
lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)" 
46982  316 
by (fact sym_UNION [to_pred]) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

317 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

318 

60758  319 
subsubsection \<open>Antisymmetry\<close> 
46694  320 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

321 
definition antisym :: "'a rel \<Rightarrow> bool" 
63404  322 
where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

323 

e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

324 
abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
63404  325 
where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *) 
326 

327 
lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" 

328 
unfolding antisym_def by iprover 

46694  329 

63404  330 
lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" 
331 
unfolding antisym_def by iprover 

46694  332 

63404  333 
lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" 
334 
unfolding antisym_def by blast 

46694  335 

336 
lemma antisym_empty [simp]: "antisym {}" 

63404  337 
unfolding antisym_def by blast 
46694  338 

60057  339 
lemma antisymP_equality [simp]: "antisymP op =" 
63404  340 
by (auto intro: antisymI) 
46694  341 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

342 
lemma antisym_singleton [simp]: "antisym {x}" 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

343 
by (blast intro: antisymI) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

344 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

345 

60758  346 
subsubsection \<open>Transitivity\<close> 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

347 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

348 
definition trans :: "'a rel \<Rightarrow> bool" 
63404  349 
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 predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

350 

e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

351 
definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
63404  352 
where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

353 

63404  354 
lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

355 
by (simp add: trans_def transp_def) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

356 

63404  357 
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 predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

358 
by (unfold trans_def) iprover 
46694  359 

63404  360 
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 predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

361 
by (fact transI [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

362 

e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

363 
lemma transE: 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

364 
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

365 
obtains "(x, z) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

366 
using assms by (unfold trans_def) iprover 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

367 

46694  368 
lemma transpE: 
369 
assumes "transp r" and "r x y" and "r y z" 

370 
obtains "r x z" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

371 
using assms by (rule transE [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

372 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

373 
lemma transD [dest?]: 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

374 
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

375 
shows "(x, z) \<in> r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

376 
using assms by (rule transE) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

377 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

378 
lemma transpD [dest?]: 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

379 
assumes "transp r" and "r x y" and "r y z" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

380 
shows "r x z" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

381 
using assms by (rule transD [to_pred]) 
46694  382 

63404  383 
lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

384 
by (fast intro: transI elim: transE) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

385 

63404  386 
lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

387 
by (fact trans_Int [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

388 

63404  389 
lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

390 
by (fast intro: transI elim: transD) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

391 

64584  392 
lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (INFIMUM S r)" 
393 
by (fact trans_INTER [to_pred]) 

394 

63404  395 
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  396 
by (auto simp add: trans_def) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

397 

63404  398 
lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

399 
by (simp add: trans_def transp_def) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

400 

59518  401 
lemma transp_equality [simp]: "transp op =" 
63404  402 
by (auto intro: transpI) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

403 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

404 
lemma trans_empty [simp]: "trans {}" 
63612  405 
by (blast intro: transI) 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

406 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

407 
lemma transp_empty [simp]: "transp (\<lambda>x y. False)" 
63612  408 
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

409 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

410 
lemma trans_singleton [simp]: "trans {(a, a)}" 
63612  411 
by (blast intro: transI) 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

412 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

413 
lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)" 
63612  414 
by (simp add: transp_def) 
415 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

416 

60758  417 
subsubsection \<open>Totality\<close> 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

418 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

419 
definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" 
63404  420 
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

421 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

422 
lemma total_onI [intro?]: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

423 
"(\<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  424 
unfolding total_on_def by blast 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

425 

29859
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset

426 
abbreviation "total \<equiv> total_on UNIV" 
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset

427 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

428 
lemma total_on_empty [simp]: "total_on {} r" 
e9e7209eb375
more fundamental predtoset 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: total_on_def) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

430 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

431 
lemma total_on_singleton [simp]: "total_on {x} {(x, x)}" 
63612  432 
unfolding total_on_def by blast 
433 

46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

434 

60758  435 
subsubsection \<open>Single valued relations\<close> 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

436 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

437 
definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" 
63404  438 
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

439 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

440 
abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 
63404  441 
where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *) 
46694  442 

63404  443 
lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r" 
444 
unfolding single_valued_def . 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

445 

63404  446 
lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

447 
by (simp add: single_valued_def) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

448 

57111  449 
lemma single_valued_empty[simp]: "single_valued {}" 
63404  450 
by (simp add: single_valued_def) 
52392  451 

63404  452 
lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" 
453 
unfolding single_valued_def by blast 

11136  454 

12905  455 

60758  456 
subsection \<open>Relation operations\<close> 
46694  457 

60758  458 
subsubsection \<open>The identity relation\<close> 
12905  459 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

460 
definition Id :: "'a rel" 
63404  461 
where [code del]: "Id = {p. \<exists>x. p = (x, x)}" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

462 

63404  463 
lemma IdI [intro]: "(a, a) \<in> Id" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

464 
by (simp add: Id_def) 
12905  465 

63404  466 
lemma IdE [elim!]: "p \<in> Id \<Longrightarrow> (\<And>x. p = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" 
467 
unfolding Id_def by (iprover elim: CollectE) 

12905  468 

63404  469 
lemma pair_in_Id_conv [iff]: "(a, b) \<in> Id \<longleftrightarrow> a = b" 
470 
unfolding Id_def by blast 

12905  471 

30198  472 
lemma refl_Id: "refl Id" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

473 
by (simp add: refl_on_def) 
12905  474 

475 
lemma antisym_Id: "antisym Id" 

61799  476 
\<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close> 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

477 
by (simp add: antisym_def) 
12905  478 

19228  479 
lemma sym_Id: "sym Id" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

480 
by (simp add: sym_def) 
19228  481 

12905  482 
lemma trans_Id: "trans Id" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

483 
by (simp add: trans_def) 
12905  484 

46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

485 
lemma single_valued_Id [simp]: "single_valued Id" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

486 
by (unfold single_valued_def) blast 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

487 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

488 
lemma irrefl_diff_Id [simp]: "irrefl (r  Id)" 
63404  489 
by (simp add: irrefl_def) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

490 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

491 
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

492 
unfolding antisym_def trans_def by blast 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

493 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

494 
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

495 
by (simp add: total_on_def) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

496 

62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

497 
lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}" 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

498 
by force 
12905  499 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

500 

60758  501 
subsubsection \<open>Diagonal: identity over a set\<close> 
12905  502 

63612  503 
definition Id_on :: "'a set \<Rightarrow> 'a rel" 
63404  504 
where "Id_on A = (\<Union>x\<in>A. {(x, x)})" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

505 

30198  506 
lemma Id_on_empty [simp]: "Id_on {} = {}" 
63404  507 
by (simp add: Id_on_def) 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

508 

63404  509 
lemma Id_on_eqI: "a = b \<Longrightarrow> a \<in> A \<Longrightarrow> (a, b) \<in> Id_on A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

510 
by (simp add: Id_on_def) 
12905  511 

63404  512 
lemma Id_onI [intro!]: "a \<in> A \<Longrightarrow> (a, a) \<in> Id_on A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

513 
by (rule Id_on_eqI) (rule refl) 
12905  514 

63404  515 
lemma Id_onE [elim!]: "c \<in> Id_on A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> c = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" 
61799  516 
\<comment> \<open>The general elimination rule.\<close> 
63404  517 
unfolding Id_on_def by (iprover elim!: UN_E singletonE) 
12905  518 

63404  519 
lemma Id_on_iff: "(x, y) \<in> Id_on A \<longleftrightarrow> x = y \<and> x \<in> A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

520 
by blast 
12905  521 

63404  522 
lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

523 
by auto 
40923
be80c93ac0a2
adding a nice definition of Id_on for quickcheck and nitpick
bulwahn
parents:
36772
diff
changeset

524 

30198  525 
lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

526 
by blast 
12905  527 

46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

528 
lemma refl_on_Id_on: "refl_on A (Id_on A)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

529 
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

530 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

531 
lemma antisym_Id_on [simp]: "antisym (Id_on A)" 
63404  532 
unfolding antisym_def by blast 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

533 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

534 
lemma sym_Id_on [simp]: "sym (Id_on A)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

535 
by (rule symI) clarify 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

536 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

537 
lemma trans_Id_on [simp]: "trans (Id_on A)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

538 
by (fast intro: transI elim: transD) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

539 

1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

540 
lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" 
63404  541 
unfolding single_valued_def by blast 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

542 

12905  543 

60758  544 
subsubsection \<open>Composition\<close> 
12905  545 

63404  546 
inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

547 
for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" 
63404  548 
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

549 

47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset

550 
notation relcompp (infixr "OO" 75) 
12905  551 

47434
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset

552 
lemmas relcomppI = relcompp.intros 
12905  553 

60758  554 
text \<open> 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

555 
For historic reasons, the elimination rules are not wholly corresponding. 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

556 
Feel free to consolidate this. 
60758  557 
\<close> 
46694  558 

47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

559 
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

560 
inductive_cases relcomppE [elim!]: "(r OO s) a c" 
46694  561 

47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

562 
lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

563 
(\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" 
63404  564 
apply (cases xz) 
565 
apply simp 

566 
apply (erule relcompEpair) 

567 
apply iprover 

568 
done 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

569 

63404  570 
lemma R_O_Id [simp]: "R O Id = R" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

571 
by fast 
46694  572 

63404  573 
lemma Id_O_R [simp]: "Id O R = R" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

574 
by fast 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

575 

63404  576 
lemma relcomp_empty1 [simp]: "{} O R = {}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

577 
by blast 
12905  578 

63404  579 
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

580 
by (fact relcomp_empty1 [to_pred]) 
12905  581 

63404  582 
lemma relcomp_empty2 [simp]: "R O {} = {}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

583 
by blast 
12905  584 

63404  585 
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

586 
by (fact relcomp_empty2 [to_pred]) 
23185  587 

63404  588 
lemma O_assoc: "(R O S) O T = R O (S O T)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

589 
by blast 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

590 

63404  591 
lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

592 
by (fact O_assoc [to_pred]) 
23185  593 

63404  594 
lemma trans_O_subset: "trans r \<Longrightarrow> r O r \<subseteq> r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

595 
by (unfold trans_def) blast 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

596 

63404  597 
lemma transp_relcompp_less_eq: "transp r \<Longrightarrow> r OO r \<le> r " 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

598 
by (fact trans_O_subset [to_pred]) 
12905  599 

63404  600 
lemma relcomp_mono: "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

601 
by blast 
12905  602 

63404  603 
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

604 
by (fact relcomp_mono [to_pred]) 
12905  605 

63404  606 
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 predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

607 
by blast 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

608 

63404  609 
lemma relcomp_distrib [simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

610 
by auto 
12905  611 

63404  612 
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

613 
by (fact relcomp_distrib [to_pred]) 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

614 

63404  615 
lemma relcomp_distrib2 [simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

616 
by auto 
28008
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset

617 

63404  618 
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

619 
by (fact relcomp_distrib2 [to_pred]) 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

620 

63404  621 
lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) " 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

622 
by auto 
28008
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset

623 

64584  624 
lemma relcompp_SUP_distrib: "s OO SUPREMUM I r = (\<Squnion>i\<in>I. s OO r i)" 
625 
by (fact relcomp_UNION_distrib [to_pred]) 

626 

63404  627 
lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) " 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

628 
by auto 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

629 

64584  630 
lemma relcompp_SUP_distrib2: "SUPREMUM I r OO s = (\<Squnion>i\<in>I. r i OO s)" 
631 
by (fact relcomp_UNION_distrib2 [to_pred]) 

632 

63404  633 
lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" 
634 
unfolding single_valued_def by blast 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

635 

63404  636 
lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

637 
by (auto simp add: set_eq_iff) 
12905  638 

58195  639 
lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)" 
640 
unfolding relcomp_unfold [to_pred] .. 

641 

63612  642 
lemma eq_OO: "op = OO R = R" 
63404  643 
by blast 
55083  644 

61630  645 
lemma OO_eq: "R OO op = = R" 
63404  646 
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

647 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

648 

60758  649 
subsubsection \<open>Converse\<close> 
12913  650 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

651 
inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999) 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

652 
for r :: "('a \<times> 'b) set" 
63404  653 
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

654 

63404  655 
notation conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 
46694  656 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

657 
notation (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

658 
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

659 
conversep ("(_^1)" [1000] 1000) 
46694  660 

63404  661 
lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

662 
by (fact converse.intros) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

663 

63404  664 
lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

665 
by (fact conversep.intros) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

666 

63404  667 
lemma converseD [sym]: "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

668 
by (erule converse.cases) iprover 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

669 

63404  670 
lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

671 
by (fact converseD [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

672 

63404  673 
lemma converseE [elim!]: "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" 
61799  674 
\<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close> 
63404  675 
apply (cases yx) 
676 
apply simp 

677 
apply (erule converse.cases) 

678 
apply iprover 

679 
done 

46694  680 

46882  681 
lemmas conversepE [elim!] = conversep.cases 
46752
e9e7209eb375
more fundamental predtoset 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 converse_iff [iff]: "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

684 
by (auto intro: converseI) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

685 

63404  686 
lemma conversep_iff [iff]: "r\<inverse>\<inverse> a b = r b a" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

687 
by (fact converse_iff [to_pred]) 
46694  688 

63404  689 
lemma converse_converse [simp]: "(r\<inverse>)\<inverse> = r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

690 
by (simp add: set_eq_iff) 
46694  691 

63404  692 
lemma conversep_conversep [simp]: "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

693 
by (fact converse_converse [to_pred]) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

694 

53680  695 
lemma converse_empty[simp]: "{}\<inverse> = {}" 
63404  696 
by auto 
53680  697 

698 
lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV" 

63404  699 
by auto 
53680  700 

63404  701 
lemma converse_relcomp: "(r O s)\<inverse> = s\<inverse> O r\<inverse>" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

702 
by blast 
46694  703 

63404  704 
lemma converse_relcompp: "(r OO s)\<inverse>\<inverse> = s\<inverse>\<inverse> OO r\<inverse>\<inverse>" 
705 
by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD) 

46694  706 

63404  707 
lemma converse_Int: "(r \<inter> s)\<inverse> = r\<inverse> \<inter> s\<inverse>" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

708 
by blast 
e9e7209eb375
more fundamental predtoset 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 converse_meet: "(r \<sqinter> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<sqinter> s\<inverse>\<inverse>" 
46694  711 
by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) 
712 

63404  713 
lemma converse_Un: "(r \<union> s)\<inverse> = r\<inverse> \<union> s\<inverse>" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

714 
by blast 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

715 

63404  716 
lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>" 
46694  717 
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) 
718 

63404  719 
lemma converse_INTER: "(INTER S r)\<inverse> = (INT x:S. (r x)\<inverse>)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

720 
by fast 
19228  721 

63404  722 
lemma converse_UNION: "(UNION S r)\<inverse> = (UN x:S. (r x)\<inverse>)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

723 
by blast 
19228  724 

63404  725 
lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s" 
52749  726 
by auto 
727 

63404  728 
lemma conversep_mono[simp]: "r\<inverse>\<inverse> \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<le> s" 
52749  729 
by (fact converse_mono[to_pred]) 
730 

63404  731 
lemma converse_inject[simp]: "r\<inverse> = s \<inverse> \<longleftrightarrow> r = s" 
52730  732 
by auto 
733 

63404  734 
lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s" 
52749  735 
by (fact converse_inject[to_pred]) 
736 

63612  737 
lemma converse_subset_swap: "r \<subseteq> s \<inverse> \<longleftrightarrow> r \<inverse> \<subseteq> s" 
52749  738 
by auto 
739 

63612  740 
lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<inverse>\<inverse> \<le> s" 
52749  741 
by (fact converse_subset_swap[to_pred]) 
52730  742 

63404  743 
lemma converse_Id [simp]: "Id\<inverse> = Id" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

744 
by blast 
12905  745 

63404  746 
lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

747 
by blast 
12905  748 

30198  749 
lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" 
63404  750 
by (auto simp: refl_on_def) 
12905  751 

19228  752 
lemma sym_converse [simp]: "sym (converse r) = sym r" 
63404  753 
unfolding sym_def by blast 
19228  754 

755 
lemma antisym_converse [simp]: "antisym (converse r) = antisym r" 

63404  756 
unfolding antisym_def by blast 
12905  757 

19228  758 
lemma trans_converse [simp]: "trans (converse r) = trans r" 
63404  759 
unfolding trans_def by blast 
12905  760 

63404  761 
lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r" 
762 
unfolding sym_def by fast 

19228  763 

63404  764 
lemma sym_Un_converse: "sym (r \<union> r\<inverse>)" 
765 
unfolding sym_def by blast 

19228  766 

63404  767 
lemma sym_Int_converse: "sym (r \<inter> r\<inverse>)" 
768 
unfolding sym_def by blast 

19228  769 

63404  770 
lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

771 
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

772 

63404  773 
lemma finite_converse [iff]: "finite (r\<inverse>) = finite r" 
54611
31afce809794
set_comprehension_pointfree simproc causes to many surprises if enabled by default
traytel
parents:
54555
diff
changeset

774 
unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] 
31afce809794
set_comprehension_pointfree simproc causes to many surprises if enabled by default
traytel
parents:
54555
diff
changeset

775 
by (auto elim: finite_imageD simp: inj_on_def) 
12913  776 

63404  777 
lemma conversep_noteq [simp]: "(op \<noteq>)\<inverse>\<inverse> = op \<noteq>" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

778 
by (auto simp add: fun_eq_iff) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

779 

63404  780 
lemma conversep_eq [simp]: "(op =)\<inverse>\<inverse> = op =" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

781 
by (auto simp add: fun_eq_iff) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

782 

63404  783 
lemma converse_unfold [code]: "r\<inverse> = {(y, x). (x, y) \<in> r}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

784 
by (simp add: set_eq_iff) 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

785 

46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

786 

60758  787 
subsubsection \<open>Domain, range and field\<close> 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

788 

63404  789 
inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" for r :: "('a \<times> 'b) set" 
790 
where DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

791 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

792 
lemmas DomainPI = Domainp.DomainI 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

793 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

794 
inductive_cases DomainE [elim!]: "a \<in> Domain r" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

795 
inductive_cases DomainpE [elim!]: "Domainp r a" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

796 

63404  797 
inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" for r :: "('a \<times> 'b) set" 
798 
where RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

799 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

800 
lemmas RangePI = Rangep.RangeI 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

801 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

802 
inductive_cases RangeE [elim!]: "b \<in> Range r" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

803 
inductive_cases RangepE [elim!]: "Rangep r b" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

804 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

805 
definition Field :: "'a rel \<Rightarrow> 'a set" 
63404  806 
where "Field r = Domain r \<union> Range r" 
12905  807 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

808 
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R" 
63612  809 
unfolding Field_def by blast 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

810 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

811 
lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

812 
unfolding Field_def by auto 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

813 

63404  814 
lemma Domain_fst [code]: "Domain r = fst ` r" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

815 
by force 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

816 

63404  817 
lemma Range_snd [code]: "Range r = snd ` r" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

818 
by force 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

819 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

820 
lemma fst_eq_Domain: "fst ` R = Domain R" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

821 
by force 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

822 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

823 
lemma snd_eq_Range: "snd ` R = Range R" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

824 
by force 
46694  825 

62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

826 
lemma range_fst [simp]: "range fst = UNIV" 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

827 
by (auto simp: fst_eq_Domain) 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

828 

44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

829 
lemma range_snd [simp]: "range snd = UNIV" 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

830 
by (auto simp: snd_eq_Range) 
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61955
diff
changeset

831 

46694  832 
lemma Domain_empty [simp]: "Domain {} = {}" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

833 
by auto 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

834 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

835 
lemma Range_empty [simp]: "Range {} = {}" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

836 
by auto 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

837 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

838 
lemma Field_empty [simp]: "Field {} = {}" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

839 
by (simp add: Field_def) 
46694  840 

841 
lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}" 

842 
by auto 

843 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

844 
lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

845 
by auto 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

846 

46882  847 
lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

848 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

849 

46882  850 
lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

851 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

852 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

853 
lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r" 
46884  854 
by (auto simp add: Field_def) 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

855 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

856 
lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

857 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

858 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

859 
lemma Range_iff: "a \<in> Range r \<longleftrightarrow> (\<exists>y. (y, a) \<in> r)" 
46694  860 
by blast 
861 

862 
lemma Domain_Id [simp]: "Domain Id = UNIV" 

863 
by blast 

864 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

865 
lemma Range_Id [simp]: "Range Id = UNIV" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

866 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

867 

46694  868 
lemma Domain_Id_on [simp]: "Domain (Id_on A) = A" 
869 
by blast 

870 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

871 
lemma Range_Id_on [simp]: "Range (Id_on A) = A" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

872 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

873 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

874 
lemma Domain_Un_eq: "Domain (A \<union> B) = Domain A \<union> Domain B" 
46694  875 
by blast 
876 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

877 
lemma Range_Un_eq: "Range (A \<union> B) = Range A \<union> Range B" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

878 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

879 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

880 
lemma Field_Un [simp]: "Field (r \<union> s) = Field r \<union> Field s" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

881 
by (auto simp: Field_def) 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

882 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

883 
lemma Domain_Int_subset: "Domain (A \<inter> B) \<subseteq> Domain A \<inter> Domain B" 
46694  884 
by blast 
885 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

886 
lemma Range_Int_subset: "Range (A \<inter> B) \<subseteq> Range A \<inter> Range B" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

887 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

888 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

889 
lemma Domain_Diff_subset: "Domain A  Domain B \<subseteq> Domain (A  B)" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

890 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

891 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

892 
lemma Range_Diff_subset: "Range A  Range B \<subseteq> Range (A  B)" 
46694  893 
by blast 
894 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

895 
lemma Domain_Union: "Domain (\<Union>S) = (\<Union>A\<in>S. Domain A)" 
46694  896 
by blast 
897 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

898 
lemma Range_Union: "Range (\<Union>S) = (\<Union>A\<in>S. Range A)" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

899 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

900 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

901 
lemma Field_Union [simp]: "Field (\<Union>R) = \<Union>(Field ` R)" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

902 
by (auto simp: Field_def) 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

903 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

904 
lemma Domain_converse [simp]: "Domain (r\<inverse>) = Range r" 
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

905 
by auto 
46694  906 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

907 
lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r" 
46694  908 
by blast 
909 

46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

910 
lemma Field_converse [simp]: "Field (r\<inverse>) = Field r" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

911 
by (auto simp: Field_def) 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

912 

63404  913 
lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. \<exists>y. P x y}" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

914 
by auto 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

915 

63404  916 
lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \<exists>x. P x y}" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

917 
by auto 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

918 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

919 
lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)" 
46884  920 
by (induct set: finite) auto 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

921 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

922 
lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)" 
46884  923 
by (induct set: finite) auto 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

924 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

925 
lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

926 
by (simp add: Field_def finite_Domain finite_Range) 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

927 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

928 
lemma Domain_mono: "r \<subseteq> s \<Longrightarrow> Domain r \<subseteq> Domain s" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

929 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

930 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

931 
lemma Range_mono: "r \<subseteq> s \<Longrightarrow> Range r \<subseteq> Range s" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

932 
by blast 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

933 

807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

934 
lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

935 
by (auto simp: Field_def Domain_def Range_def) 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

936 

63404  937 
lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}" 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

938 
by blast 
46694  939 

63563
0bcd79da075b
prefer [simp] over [iff] as [iff] break HOLUNITY
Andreas Lochbihler
parents:
63561
diff
changeset

940 
lemma Field_square [simp]: "Field (x \<times> x) = x" 
63612  941 
unfolding Field_def by blast 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63404
diff
changeset

942 

12905  943 

60758  944 
subsubsection \<open>Image of a set under a relation\<close> 
12905  945 

63404  946 
definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90) 
947 
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

948 

63404  949 
lemma Image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. (x, b) \<in> r)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

950 
by (simp add: Image_def) 
12905  951 

63404  952 
lemma Image_singleton: "r``{a} = {b. (a, b) \<in> r}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

953 
by (simp add: Image_def) 
12905  954 

63404  955 
lemma Image_singleton_iff [iff]: "b \<in> r``{a} \<longleftrightarrow> (a, b) \<in> r" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

956 
by (rule Image_iff [THEN trans]) simp 
12905  957 

63404  958 
lemma ImageI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> r``A" 
959 
unfolding Image_def by blast 

12905  960 

63404  961 
lemma ImageE [elim!]: "b \<in> r `` A \<Longrightarrow> (\<And>x. (x, b) \<in> r \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" 
962 
unfolding Image_def by (iprover elim!: CollectE bexE) 

12905  963 

63404  964 
lemma rev_ImageI: "a \<in> A \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> b \<in> r `` A" 
61799  965 
\<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close> 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

966 
by blast 
12905  967 

968 
lemma Image_empty [simp]: "R``{} = {}" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

969 
by blast 
12905  970 

971 
lemma Image_Id [simp]: "Id `` A = A" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

972 
by blast 
12905  973 

30198  974 
lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

975 
by blast 
13830  976 

977 
lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

978 
by blast 
12905  979 

63404  980 
lemma Image_Int_eq: "single_valued (converse R) \<Longrightarrow> R `` (A \<inter> B) = R `` A \<inter> R `` B" 
63612  981 
by (auto simp: single_valued_def) 
12905  982 

13830  983 
lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

984 
by blast 
12905  985 

13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

986 
lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

987 
by blast 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

988 

63404  989 
lemma Image_subset: "r \<subseteq> A \<times> B \<Longrightarrow> r``C \<subseteq> B" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

990 
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 
12905  991 

13830  992 
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" 
61799  993 
\<comment> \<open>NOT suitable for rewriting\<close> 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

994 
by blast 
12905  995 

63404  996 
lemma Image_mono: "r' \<subseteq> r \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> (r' `` A') \<subseteq> (r `` A)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

997 
by blast 
12905  998 

13830  999 
lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1000 
by blast 
13830  1001 

54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset

1002 
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

1003 
by auto 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset

1004 

13830  1005 
lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1006 
by blast 
12905  1007 

63404  1008 
text \<open>Converse inclusion requires some assumptions\<close> 
1009 
lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)" 

1010 
apply (rule equalityI) 

1011 
apply (rule Image_INT_subset) 

1012 
apply (auto simp add: single_valued_def) 

1013 
apply blast 

1014 
done 

12905  1015 

63404  1016 
lemma Image_subset_eq: "r``A \<subseteq> B \<longleftrightarrow> A \<subseteq>  ((r\<inverse>) `` ( B))" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1017 
by blast 
12905  1018 

63404  1019 
lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. \<exists>x\<in>A. P x y}" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1020 
by auto 
12905  1021 

54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset

1022 
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

1023 
by auto 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset

1024 

0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
54147
diff
changeset

1025 
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

1026 
by auto 
12905  1027 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

1028 

60758  1029 
subsubsection \<open>Inverse image\<close> 
12905  1030 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1031 
definition inv_image :: "'b rel \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a rel" 
63404  1032 
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

1033 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1034 
definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
63404  1035 
where "inv_imagep r f = (\<lambda>x y. r (f x) (f y))" 
46694  1036 

1037 
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" 

1038 
by (simp add: inv_image_def inv_imagep_def) 

1039 

63404  1040 
lemma sym_inv_image: "sym r \<Longrightarrow> sym (inv_image r f)" 
1041 
unfolding sym_def inv_image_def by blast 

19228  1042 

63404  1043 
lemma trans_inv_image: "trans r \<Longrightarrow> trans (inv_image r f)" 
1044 
unfolding trans_def inv_image_def 

12905  1045 
apply (simp (no_asm)) 
1046 
apply blast 

1047 
done 

1048 

63404  1049 
lemma in_inv_image[simp]: "(x, y) \<in> inv_image r f \<longleftrightarrow> (f x, f y) \<in> r" 
32463
3a0a65ca2261
moved lemma Wellfounded.in_inv_image to Relation.thy
krauss
parents:
32235
diff
changeset

1050 
by (auto simp:inv_image_def) 
3a0a65ca2261
moved lemma Wellfounded.in_inv_image to Relation.thy
krauss
parents:
32235
diff
changeset

1051 

63404  1052 
lemma converse_inv_image[simp]: "(inv_image R f)\<inverse> = inv_image (R\<inverse>) f" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1053 
unfolding inv_image_def converse_unfold by auto 
33218  1054 

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

1055 
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

1056 
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

1057 

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

1058 

60758  1059 
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

1060 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46696
diff
changeset

1061 
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" 
63404  1062 
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

1063 

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

1064 
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

1065 
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

1066 

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

1067 
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

1068 

63376
4c0cc2b356f0
default onestep rules for predicates on relations;
haftmann
parents:
62343
diff
changeset

1069 

60758  1070 
subsubsection \<open>Expressing relation operations via @{const Finite_Set.fold}\<close> 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1071 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1072 
lemma Id_on_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1073 
assumes "finite A" 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1074 
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

1075 
proof  
63404  1076 
interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" 
1077 
by standard auto 

1078 
from assms show ?thesis 

1079 
unfolding Id_on_def by (induct A) simp_all 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1080 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1081 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1082 
lemma comp_fun_commute_Image_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1083 
"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

1084 
proof  
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1085 
interpret comp_fun_idem Set.insert 
63404  1086 
by (fact comp_fun_idem_insert) 
1087 
show ?thesis 

63612  1088 
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

1089 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1090 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1091 
lemma Image_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1092 
assumes "finite R" 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1093 
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

1094 
proof  
63404  1095 
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

1096 
by (rule comp_fun_commute_Image_fold) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1097 
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  1098 
by (force intro: rev_ImageI) 
63404  1099 
show ?thesis 
1100 
using assms by (induct R) (auto simp: *) 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1101 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1102 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1103 
lemma insert_relcomp_union_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1104 
assumes "finite S" 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1105 
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

1106 
proof  
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1107 
interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" 
63404  1108 
proof  
1109 
interpret comp_fun_idem Set.insert 

1110 
by (fact comp_fun_idem_insert) 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1111 
show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" 
63404  1112 
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

1113 
qed 
63404  1114 
have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}" 
1115 
by (auto simp: relcomp_unfold intro!: exI) 

1116 
show ?thesis 

1117 
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

1118 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1119 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1120 
lemma insert_relcomp_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1121 
assumes "finite S" 
63404  1122 
shows "Set.insert x R O S = 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1123 
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

1124 
proof  
63404  1125 
have "Set.insert x R O S = ({x} O S) \<union> (R O S)" 
1126 
by auto 

1127 
then show ?thesis 

1128 
by (auto simp: insert_relcomp_union_fold [OF assms]) 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1129 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1130 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1131 
lemma comp_fun_commute_relcomp_fold: 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1132 
assumes "finite S" 
63404  1133 
shows "comp_fun_commute (\<lambda>(x,y) A. 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1134 
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

1135 
proof  
63404  1136 
have *: "\<And>a b A. 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1137 
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

1138 
by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) 
63404  1139 
show ?thesis 
1140 
by standard (auto simp: *) 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1141 
qed 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1142 

fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1143 
lemma relcomp_fold: 
63404  1144 
assumes "finite R" "finite S" 
1145 
shows "R O S = Finite_Set.fold 

48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1146 
(\<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" 
63404  1147 
using assms 
1148 
by (induct R) 

52749  1149 
(auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1150 
cong: if_cong) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1151 

1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

1152 
end 