author  Andreas Lochbihler 
Wed, 11 Feb 2015 14:07:28 +0100  
changeset 59518  28cfc60dea7a 
parent 58889  5b7a9633cfa8 
child 60057  86fa63ce8156 
permissions  rwrr 
10358  1 
(* Title: HOL/Relation.thy 
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

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen 
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset

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

4 

58889  5 
section {* Relations  as sets of pairs, and binary predicates *} 
12905  6 

15131  7 
theory Relation 
54555  8 
imports Finite_Set 
15131  9 
begin 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

10 

46694  11 
text {* A preliminary: classical rules for reasoning on predicates *} 
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

12 

46882  13 
declare predicate1I [Pure.intro!, intro!] 
14 
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

15 
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

16 
declare predicate2D [Pure.dest, dest] 
46767
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

17 
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

18 
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

19 
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

20 
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

21 
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

22 
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

23 
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

24 
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

25 
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

26 
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

27 
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

28 
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

29 
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

30 
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

31 
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

32 
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

33 
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

34 
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

35 
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

36 
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

37 
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

38 
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

39 
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

40 
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

41 
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

42 
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

43 
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

44 
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

45 
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

46 
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

47 
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

48 
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

49 
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

50 
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

51 
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

52 
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

53 

46694  54 
subsection {* Fundamental *} 
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

55 

46694  56 
subsubsection {* Relations as sets of pairs *} 
57 

58 
type_synonym 'a rel = "('a * 'a) set" 

59 

60 
lemma subrelI:  {* Version of @{thm [source] subsetI} for binary relations *} 

61 
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s" 

62 
by auto 

63 

64 
lemma lfp_induct2:  {* Version of @{thm [source] lfp_induct} for binary relations *} 

65 
"(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow> 

66 
(\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b" 

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

67 
using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto 
46694  68 

69 

70 
subsubsection {* Conversions between set and predicate relations *} 

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

71 

46833  72 
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

73 
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

74 

46833  75 
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

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_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

79 
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

80 

46833  81 
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

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 

46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset

84 
lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})" 
46689  85 
by (auto simp add: fun_eq_iff) 
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_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

88 
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

89 

46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset

90 
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

91 
by (auto simp add: fun_eq_iff) 
46689  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_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

94 
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

95 

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

96 
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

97 
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

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_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

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

103 
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

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_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

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 

46981  108 
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))" 
109 
by (simp add: fun_eq_iff) 

110 

111 
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))" 

112 
by (simp add: fun_eq_iff) 

113 

114 
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))" 

115 
by (simp add: fun_eq_iff) 

116 

117 
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))" 

118 
by (simp add: fun_eq_iff) 

119 

46833  120 
lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)" 
46884  121 
by (simp add: fun_eq_iff) 
46833  122 

123 
lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" 

46884  124 
by (simp add: fun_eq_iff) 
46833  125 

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

126 
lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)" 
46884  127 
by (simp add: fun_eq_iff) 
46833  128 

129 
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  130 
by (simp add: fun_eq_iff) 
46833  131 

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

46884  133 
by (simp add: fun_eq_iff) 
46833  134 

135 
lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)" 

46884  136 
by (simp add: fun_eq_iff) 
46833  137 

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

138 
lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)" 
46884  139 
by (simp add: fun_eq_iff) 
46833  140 

141 
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  142 
by (simp add: fun_eq_iff) 
46833  143 

46694  144 
subsection {* Properties of relations *} 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

145 

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

146 
subsubsection {* Reflexivity *} 
10786  147 

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

148 
definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" 
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

149 
where 
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

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

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 
abbreviation refl :: "'a rel \<Rightarrow> bool" 
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

153 
where  {* reflexivity over a type *} 
45137  154 
"refl \<equiv> refl_on UNIV" 
26297  155 

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

156 
definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
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

157 
where 
47375
8e6a45f1bf8f
define reflp directly, in the manner of symp and transp
huffman
parents:
47087
diff
changeset

158 
"reflp r \<longleftrightarrow> (\<forall>x. r x x)" 
46694  159 

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

160 
lemma reflp_refl_eq [pred_set_conv]: 
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

161 
"reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl 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

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 

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

164 
lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_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

165 
by (unfold refl_on_def) (iprover intro!: ballI) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

166 

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

167 
lemma refl_onD: "refl_on A r ==> a : A ==> (a, 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

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

169 

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

170 
lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : 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

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

172 

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

173 
lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : 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

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

175 

46694  176 
lemma reflpI: 
177 
"(\<And>x. r x x) \<Longrightarrow> reflp r" 

178 
by (auto intro: refl_onI simp add: reflp_def) 

179 

180 
lemma reflpE: 

181 
assumes "reflp r" 

182 
obtains "r x x" 

183 
using assms by (auto dest: refl_onD simp add: reflp_def) 

184 

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 
lemma reflpD: 
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 
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

187 
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

188 
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

189 

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

190 
lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (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

191 
by (unfold refl_on_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

192 

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 
lemma reflp_inf: 
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

194 
"reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" 
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

195 
by (auto intro: reflpI elim: reflpE) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

196 

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

197 
lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (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

198 
by (unfold refl_on_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

199 

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

200 
lemma reflp_sup: 
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

201 
"reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)" 
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

202 
by (auto intro: reflpI elim: reflpE) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

203 

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

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

205 
"ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (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

206 
by (unfold refl_on_def) fast 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

207 

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

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

209 
"ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (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

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

211 

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

212 
lemma refl_on_empty [simp]: "refl_on {} {}" 
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

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

214 

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

215 
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

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

217 
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

218 

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

219 

46694  220 
subsubsection {* Irreflexivity *} 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

221 

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

222 
definition irrefl :: "'a rel \<Rightarrow> bool" 
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

223 
where 
56545  224 
"irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)" 
225 

226 
definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 

227 
where 

228 
"irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)" 

229 

230 
lemma irreflp_irrefl_eq [pred_set_conv]: 

231 
"irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" 

232 
by (simp add: irrefl_def irreflp_def) 

233 

234 
lemma irreflI: 

235 
"(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R" 

236 
by (simp add: irrefl_def) 

237 

238 
lemma irreflpI: 

239 
"(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R" 

240 
by (fact irreflI [to_pred]) 

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

241 

46694  242 
lemma irrefl_distinct [code]: 
56545  243 
"irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)" 
46694  244 
by (auto simp add: irrefl_def) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

245 

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

246 

56545  247 
subsubsection {* Asymmetry *} 
248 

249 
inductive asym :: "'a rel \<Rightarrow> bool" 

250 
where 

251 
asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" 

252 

253 
inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 

254 
where 

255 
asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R" 

256 

257 
lemma asymp_asym_eq [pred_set_conv]: 

258 
"asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" 

259 
by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) 

260 

261 

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

262 
subsubsection {* Symmetry *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

263 

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

264 
definition sym :: "'a rel \<Rightarrow> bool" 
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

265 
where 
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 
"sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, 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

267 

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

268 
definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
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 
where 
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

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

271 

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 
lemma symp_sym_eq [pred_set_conv]: 
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 
"symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym 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

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

275 

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

276 
lemma symI: 
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 
"(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym 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

278 
by (unfold sym_def) iprover 
46694  279 

280 
lemma sympI: 

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

281 
"(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp 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

282 
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

283 

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

284 
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

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

287 
using assms by (simp add: sym_def) 
46694  288 

289 
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

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

292 
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

293 

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

294 
lemma symD: 
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 
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

296 
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

297 
using assms by (rule symE) 
46694  298 

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

299 
lemma sympD: 
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

300 
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

301 
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

302 
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

303 

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 
lemma sym_Int: 
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

305 
"sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" 
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

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

307 

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

308 
lemma symp_inf: 
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

309 
"symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" 
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

310 
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

311 

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

312 
lemma sym_Un: 
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 
"sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" 
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 
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

315 

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

316 
lemma symp_sup: 
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

317 
"symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" 
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

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

319 

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

320 
lemma sym_INTER: 
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 
"\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S 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

322 
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

323 

46982  324 
lemma symp_INF: 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56085
diff
changeset

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

327 

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

328 
lemma sym_UNION: 
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

329 
"\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S 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

330 
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

331 

46982  332 
lemma symp_SUP: 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56085
diff
changeset

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

335 

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

336 

46694  337 
subsubsection {* Antisymmetry *} 
338 

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

339 
definition antisym :: "'a rel \<Rightarrow> bool" 
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

340 
where 
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

341 
"antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" 
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

342 

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

343 
abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
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

344 
where 
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

345 
"antisymP r \<equiv> antisym {(x, y). r x y}" 
46694  346 

347 
lemma antisymI: 

348 
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym 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

349 
by (unfold antisym_def) iprover 
46694  350 

351 
lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : 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

352 
by (unfold antisym_def) iprover 
46694  353 

354 
lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym 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 (unfold antisym_def) blast 
46694  356 

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

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 antisym_def) blast 
46694  359 

360 

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

361 
subsubsection {* Transitivity *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

362 

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

363 
definition trans :: "'a rel \<Rightarrow> bool" 
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 
where 
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 
"trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (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 

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 
definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
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

368 
where 
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

369 
"transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> 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

370 

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 
lemma transp_trans_eq [pred_set_conv]: 
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 
"transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans 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

373 
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

374 

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 
abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 
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 
where  {* FIXME drop *} 
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 
"transP r \<equiv> trans {(x, y). r x y}" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

378 

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

379 
lemma transI: 
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

380 
"(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans 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

381 
by (unfold trans_def) iprover 
46694  382 

383 
lemma transpI: 

384 
"(\<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

385 
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

386 

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

388 
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

389 
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

390 
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

391 

46694  392 
lemma transpE: 
393 
assumes "transp r" and "r x y" and "r y z" 

394 
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

395 
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

396 

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

397 
lemma 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

398 
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

399 
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

400 
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

401 

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

402 
lemma transpD: 
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

403 
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

404 
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

405 
using assms by (rule transD [to_pred]) 
46694  406 

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

407 
lemma trans_Int: 
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

408 
"trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" 
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

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

410 

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

411 
lemma transp_inf: 
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

412 
"transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" 
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

413 
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

414 

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

415 
lemma trans_INTER: 
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

416 
"\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S 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

417 
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

418 

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 
(* FIXME thm trans_INTER [to_pred] *) 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

420 

46694  421 
lemma trans_join [code]: 
422 
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" 

423 
by (auto simp add: trans_def) 

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

424 

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

425 
lemma transp_trans: 
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

426 
"transp r \<longleftrightarrow> trans {(x, y). r x y}" 
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

427 
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

428 

59518  429 
lemma transp_equality [simp]: "transp op =" 
430 
by(auto intro: transpI) 

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

431 

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

432 
subsubsection {* Totality *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

433 

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

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

435 
where 
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

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

437 

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

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

439 

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

440 
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

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

442 

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

443 

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

444 
subsubsection {* Single valued relations *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

445 

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

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

449 

46694  450 
abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where 
451 
"single_valuedP r \<equiv> single_valued {(x, y). r x y}" 

452 

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

453 
lemma single_valuedI: 
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

454 
"ALL x y. (x,y):r > (ALL z. (x,z):r > y=z) ==> single_valued 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

455 
by (unfold 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

456 

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

457 
lemma single_valuedD: 
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

458 
"single_valued r ==> (x, y) : r ==> (x, z) : 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

459 
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

460 

57111  461 
lemma single_valued_empty[simp]: "single_valued {}" 
52392  462 
by(simp add: single_valued_def) 
463 

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

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

465 
"r \<subseteq> s ==> single_valued s ==> single_valued 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

466 
by (unfold single_valued_def) blast 
11136  467 

12905  468 

46694  469 
subsection {* Relation operations *} 
470 

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

471 
subsubsection {* The identity relation *} 
12905  472 

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 
definition Id :: "'a rel" 
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

474 
where 
48253
4410a709913c
a first guess to avoid the Codegenerator_Test to loop infinitely
bulwahn
parents:
47937
diff
changeset

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

476 

12905  477 
lemma IdI [intro]: "(a, a) : 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

478 
by (simp add: Id_def) 
12905  479 

480 
lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" 

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

481 
by (unfold Id_def) (iprover elim: CollectE) 
12905  482 

483 
lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (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

484 
by (unfold Id_def) blast 
12905  485 

30198  486 
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

487 
by (simp add: refl_on_def) 
12905  488 

489 
lemma antisym_Id: "antisym Id" 

490 
 {* A strange result, since @{text Id} is also symmetric. *} 

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

491 
by (simp add: antisym_def) 
12905  492 

19228  493 
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

494 
by (simp add: sym_def) 
19228  495 

12905  496 
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

497 
by (simp add: trans_def) 
12905  498 

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

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

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

501 

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

502 
lemma irrefl_diff_Id [simp]: "irrefl (r  Id)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

504 

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

505 
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

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

507 

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

508 
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

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

510 

12905  511 

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

512 
subsubsection {* Diagonal: identity over a set *} 
12905  513 

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

514 
definition Id_on :: "'a set \<Rightarrow> 'a rel" 
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

515 
where 
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

516 
"Id_on A = (\<Union>x\<in>A. {(x, x)})" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

517 

30198  518 
lemma Id_on_empty [simp]: "Id_on {} = {}" 
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

519 
by (simp add: Id_on_def) 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

520 

30198  521 
lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : 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

522 
by (simp add: Id_on_def) 
12905  523 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53680
diff
changeset

524 
lemma Id_onI [intro!]: "a : A ==> (a, 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

525 
by (rule Id_on_eqI) (rule refl) 
12905  526 

30198  527 
lemma Id_onE [elim!]: 
528 
"c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" 

12913  529 
 {* The general elimination rule. *} 
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

530 
by (unfold Id_on_def) (iprover elim!: UN_E singletonE) 
12905  531 

30198  532 
lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : 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

533 
by blast 
12905  534 

45967  535 
lemma Id_on_def' [nitpick_unfold]: 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
41792
diff
changeset

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

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

538 

30198  539 
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

540 
by blast 
12905  541 

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

542 
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

543 
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

544 

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

545 
lemma antisym_Id_on [simp]: "antisym (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

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

547 

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

548 
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

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

550 

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

551 
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

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

553 

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

554 
lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

556 

12905  557 

46694  558 
subsubsection {* Composition *} 
12905  559 

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

560 
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

561 
for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" 
46694  562 
where 
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

563 
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

564 

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

565 
notation relcompp (infixr "OO" 75) 
12905  566 

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

567 
lemmas relcomppI = relcompp.intros 
12905  568 

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 
text {* 
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

570 
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

571 
Feel free to consolidate this. 
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

572 
*} 
46694  573 

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

574 
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

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

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

577 
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

578 
(\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" 
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

579 
by (cases xz) (simp, erule relcompEpair, iprover) 
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

580 

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

581 
lemma R_O_Id [simp]: 
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

582 
"R O Id = 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

583 
by fast 
46694  584 

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

585 
lemma Id_O_R [simp]: 
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

586 
"Id O R = 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

587 
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

588 

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

589 
lemma relcomp_empty1 [simp]: 
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

590 
"{} O 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

591 
by blast 
12905  592 

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

593 
lemma relcompp_bot1 [simp]: 
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset

594 
"\<bottom> OO R = \<bottom>" 
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

595 
by (fact relcomp_empty1 [to_pred]) 
12905  596 

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

597 
lemma relcomp_empty2 [simp]: 
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 
"R O {} = {}" 
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

599 
by blast 
12905  600 

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

601 
lemma relcompp_bot2 [simp]: 
46883
eec472dae593
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
noschinl
parents:
46882
diff
changeset

602 
"R OO \<bottom> = \<bottom>" 
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
47087
diff
changeset

603 
by (fact relcomp_empty2 [to_pred]) 
23185  604 

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

605 
lemma O_assoc: 
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

606 
"(R O S) O T = R O (S O T)" 
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 

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

609 
lemma relcompp_assoc: 
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 
"(r OO s) OO t = r OO (s OO t)" 
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

611 
by (fact O_assoc [to_pred]) 
23185  612 

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

613 
lemma trans_O_subset: 
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 
"trans r \<Longrightarrow> r O r \<subseteq> 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

615 
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

616 

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

617 
lemma transp_relcompp_less_eq: 
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

618 
"transp r \<Longrightarrow> r OO r \<le> 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

619 
by (fact trans_O_subset [to_pred]) 
12905  620 

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

621 
lemma relcomp_mono: 
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 
"r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" 
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

623 
by blast 
12905  624 

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

625 
lemma relcompp_mono: 
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

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

627 
by (fact relcomp_mono [to_pred]) 
12905  628 

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

629 
lemma relcomp_subset_Sigma: 
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

630 
"r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" 
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

631 
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

632 

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

633 
lemma relcomp_distrib [simp]: 
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

634 
"R O (S \<union> T) = (R O S) \<union> (R O T)" 
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 
by auto 
12905  636 

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

637 
lemma relcompp_distrib [simp]: 
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

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

639 
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

640 

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

641 
lemma relcomp_distrib2 [simp]: 
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

642 
"(S \<union> T) O R = (S O R) \<union> (T O 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

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

644 

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

645 
lemma relcompp_distrib2 [simp]: 
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

646 
"(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

647 
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

648 

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

649 
lemma relcomp_UNION_distrib: 
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

650 
"s O UNION I r = (\<Union>i\<in>I. s O r i) " 
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

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

652 

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

653 
(* FIXME thm relcomp_UNION_distrib [to_pred] *) 
36772  654 

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

655 
lemma relcomp_UNION_distrib2: 
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

656 
"UNION I r O s = (\<Union>i\<in>I. r i O s) " 
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

657 
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

658 

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

659 
(* FIXME thm relcomp_UNION_distrib2 [to_pred] *) 
36772  660 

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

661 
lemma single_valued_relcomp: 
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 
"single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" 
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 
by (unfold single_valued_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

664 

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

665 
lemma relcomp_unfold: 
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

666 
"r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" 
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

667 
by (auto simp add: set_eq_iff) 
12905  668 

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

671 

55083  672 
lemma eq_OO: "op= OO R = R" 
673 
by blast 

674 

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

675 

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

676 
subsubsection {* Converse *} 
12913  677 

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

678 
inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^1)" [1000] 999) 
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

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

680 
where 
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

681 
"(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r^1" 
46692
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

682 

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

683 
notation (xsymbols) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

684 
converse ("(_\<inverse>)" [1000] 999) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

685 

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

686 
notation 
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 
conversep ("(_^1)" [1000] 1000) 
46694  688 

689 
notation (xsymbols) 

690 
conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 

691 

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

692 
lemma converseI [sym]: 
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 
"(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" 
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 
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

695 

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

696 
lemma conversepI (* CANDIDATE [sym] *): 
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

697 
"r a b \<Longrightarrow> r\<inverse>\<inverse> 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

698 
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

699 

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

700 
lemma converseD [sym]: 
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

701 
"(a, b) \<in> r\<inverse> \<Longrightarrow> (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

702 
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

703 

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

704 
lemma conversepD (* CANDIDATE [sym] *): 
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

705 
"r\<inverse>\<inverse> b a \<Longrightarrow> 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

706 
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

707 

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 
lemma converseE [elim!]: 
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 
 {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} 
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

710 
"yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" 
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

711 
by (cases yx) (simp, erule converse.cases, iprover) 
46694  712 

46882  713 
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

714 

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 
lemma converse_iff [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

716 
"(a, b) \<in> r\<inverse> \<longleftrightarrow> (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

717 
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

718 

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

719 
lemma conversep_iff [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

720 
"r\<inverse>\<inverse> a b = 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

721 
by (fact converse_iff [to_pred]) 
46694  722 

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 
lemma converse_converse [simp]: 
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

724 
"(r\<inverse>)\<inverse> = 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

725 
by (simp add: set_eq_iff) 
46694  726 

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

727 
lemma conversep_conversep [simp]: 
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

728 
"(r\<inverse>\<inverse>)\<inverse>\<inverse> = 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

729 
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

730 

53680  731 
lemma converse_empty[simp]: "{}\<inverse> = {}" 
732 
by auto 

733 

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

735 
by auto 

736 

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

737 
lemma converse_relcomp: "(r O s)^1 = s^1 O r^1" 
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

738 
by blast 
46694  739 

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

740 
lemma converse_relcompp: "(r OO s)^1 = s^1 OO r^1" 
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset

741 
by (iprover intro: order_antisym conversepI relcomppI 
b75ce48a93ee
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
griff
parents:
47433
diff
changeset

742 
elim: relcomppE dest: conversepD) 
46694  743 

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 
lemma converse_Int: "(r \<inter> s)^1 = r^1 \<inter> s^1" 
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

745 
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

746 

46694  747 
lemma converse_meet: "(r \<sqinter> s)^1 = r^1 \<sqinter> s^1" 
748 
by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) 

749 

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

750 
lemma converse_Un: "(r \<union> s)^1 = r^1 \<union> s^1" 
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

751 
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

752 

46694  753 
lemma converse_join: "(r \<squnion> s)^1 = r^1 \<squnion> s^1" 
754 
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) 

755 

19228  756 
lemma converse_INTER: "(INTER S r)^1 = (INT x:S. (r x)^1)" 
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

757 
by fast 
19228  758 

759 
lemma converse_UNION: "(UNION S r)^1 = (UN x:S. (r x)^1)" 

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

760 
by blast 
19228  761 

52749  762 
lemma converse_mono[simp]: "r^1 \<subseteq> s ^1 \<longleftrightarrow> r \<subseteq> s" 
763 
by auto 

764 

765 
lemma conversep_mono[simp]: "r^1 \<le> s ^1 \<longleftrightarrow> r \<le> s" 

766 
by (fact converse_mono[to_pred]) 

767 

768 
lemma converse_inject[simp]: "r^1 = s ^1 \<longleftrightarrow> r = s" 

52730  769 
by auto 
770 

52749  771 
lemma conversep_inject[simp]: "r^1 = s ^1 \<longleftrightarrow> r = s" 
772 
by (fact converse_inject[to_pred]) 

773 

774 
lemma converse_subset_swap: "r \<subseteq> s ^1 = (r ^1 \<subseteq> s)" 

775 
by auto 

776 

777 
lemma conversep_le_swap: "r \<le> s ^1 = (r ^1 \<le> s)" 

778 
by (fact converse_subset_swap[to_pred]) 

52730  779 

12905  780 
lemma converse_Id [simp]: "Id^1 = 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

781 
by blast 
12905  782 

30198  783 
lemma converse_Id_on [simp]: "(Id_on A)^1 = 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

784 
by blast 
12905  785 

30198  786 
lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_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

787 
by (unfold refl_on_def) auto 
12905  788 

19228  789 
lemma sym_converse [simp]: "sym (converse r) = 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

790 
by (unfold sym_def) blast 
19228  791 

792 
lemma antisym_converse [simp]: "antisym (converse r) = antisym 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

793 
by (unfold antisym_def) blast 
12905  794 

19228  795 
lemma trans_converse [simp]: "trans (converse r) = 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

796 
by (unfold trans_def) blast 
12905  797 

19228  798 
lemma sym_conv_converse_eq: "sym r = (r^1 = 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

799 
by (unfold sym_def) fast 
19228  800 

801 
lemma sym_Un_converse: "sym (r \<union> r^1)" 

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

802 
by (unfold sym_def) blast 
19228  803 

804 
lemma sym_Int_converse: "sym (r \<inter> r^1)" 

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 
by (unfold sym_def) blast 
19228  806 

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

807 
lemma total_on_converse [simp]: "total_on A (r^1) = total_on A 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

808 
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

809 

52749  810 
lemma finite_converse [iff]: "finite (r^1) = finite r" 
54611
31afce809794
set_comprehension_pointfree simproc causes to many surprises if enabled by default
traytel
parents:
54555
diff
changeset

811 
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

812 
by (auto elim: finite_imageD simp: inj_on_def) 
12913  813 

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

814 
lemma conversep_noteq [simp]: "(op \<noteq>)^1 = op \<noteq>" 
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

815 
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

816 

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

817 
lemma conversep_eq [simp]: "(op =)^1 = op =" 
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

818 
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

819 

53680  820 
lemma converse_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

821 
"r\<inverse> = {(y, x). (x, y) \<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

822 
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

823 

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

824 

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

825 
subsubsection {* Domain, range and field *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

826 

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

827 
inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

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

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

830 
DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

831 

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

832 
abbreviation (input) "DomainP \<equiv> Domainp" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

833 

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

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

835 

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

836 
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

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

838 

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

839 
inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

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

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

842 
RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

843 

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

844 
abbreviation (input) "RangeP \<equiv> Rangep" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

845 

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

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

847 

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

848 
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

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

850 

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

851 
definition Field :: "'a rel \<Rightarrow> 'a set" 
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

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

853 
"Field r = Domain r \<union> Range r" 
12905  854 

46694  855 
lemma Domain_fst [code]: 
856 
"Domain r = fst ` r" 

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

857 
by force 
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_snd [code]: 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

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

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

862 

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

863 
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

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

865 

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

866 
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

867 
by force 
46694  868 

869 
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

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

871 

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

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

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

874 

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

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

876 
by (simp add: Field_def) 
46694  877 

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

879 
by auto 

880 

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

881 
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

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

883 

46882  884 
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

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

886 

46882  887 
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

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

889 

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

890 
lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r" 
46884  891 
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

892 

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

893 
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

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

895 

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

896 
lemma Range_iff: "a \<in> Range r \<longleftrightarrow> (\<exists>y. (y, a) \<in> r)" 
46694  897 
by blast 
898 

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

900 
by blast 

901 

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

902 
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

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

904 

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

907 

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

908 
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

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

910 

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

911 
lemma Domain_Un_eq: "Domain (A \<union> B) = Domain A \<union> Domain B" 
46694  912 
by blast 
913 

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

914 
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

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

916 

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

917 
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

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

919 

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

920 
lemma Domain_Int_subset: "Domain (A \<inter> B) \<subseteq> Domain A \<inter> Domain B" 
46694  921 
by blast 
922 

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

923 
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

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

925 

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

926 
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

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

928 

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

929 
lemma Range_Diff_subset: "Range A  Range B \<subseteq> Range (A  B)" 
46694  930 
by blast 
931 

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

932 
lemma Domain_Union: "Domain (\<Union>S) = (\<Union>A\<in>S. Domain A)" 
46694  933 
by blast 
934 

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

935 
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

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

937 

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

938 
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

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

940 

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

941 
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

942 
by auto 
46694  943 

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

944 
lemma Range_converse [simp]: "Range (r\<inverse>) = Domain r" 
46694  945 
by blast 
946 

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

947 
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

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

949 

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

950 
lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

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

952 

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

953 
lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

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

955 

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

956 
lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)" 
46884  957 
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

958 

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

959 
lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)" 
46884  960 
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

961 

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

962 
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

963 
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

964 

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

965 
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

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

967 

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

968 
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

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

970 

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

971 
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

972 
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

973 

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

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

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

976 
by blast 
46694  977 

12905  978 

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

979 
subsubsection {* Image of a set under a relation *} 
12905  980 

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

982 
where 
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

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

984 

12913  985 
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : 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

986 
by (simp add: Image_def) 
12905  987 

12913  988 
lemma Image_singleton: "r``{a} = {b. (a, b) : 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

989 
by (simp add: Image_def) 
12905  990 

12913  991 
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : 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

992 
by (rule Image_iff [THEN trans]) simp 
12905  993 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53680
diff
changeset

994 
lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : 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

995 
by (unfold Image_def) blast 
12905  996 

997 
lemma ImageE [elim!]: 

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

998 
"b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" 
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

999 
by (unfold Image_def) (iprover elim!: CollectE bexE) 
12905  1000 

1001 
lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A" 

1002 
 {* This version's more effective when we already have the required @{text 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

1003 
by blast 
12905  1004 

1005 
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

1006 
by blast 
12905  1007 

1008 
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

1009 
by blast 
12905  1010 

30198  1011 
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

1012 
by blast 
13830  1013 

1014 
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

1015 
by blast 
12905  1016 

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

1018 
"single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B" 
807a5d219c23
more fundamental predtoset conversions for range and domain by means of inductive_set
haftmann
parents:
46752
diff
changeset

1019 
by (simp add: single_valued_def, blast) 
12905  1020 

13830  1021 
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

1022 
by blast 
12905  1023 

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

1024 
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

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

1026 

12913  1027 
lemma Image_subset: "r \<subseteq> A \<times> B ==> 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

1028 
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 
12905  1029 

13830  1030 
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" 
12905  1031 
 {* NOT suitable for rewriting *} 
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

1032 
by blast 
12905  1033 

12913  1034 
lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (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

1035 
by blast 
12905  1036 

13830  1037 
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

1038 
by blast 
13830  1039 

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

1040 
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

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

1042 

13830  1043 
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

1044 
by blast 
12905  1045 

13830  1046 
text{*Converse inclusion requires some assumptions*} 
1047 
lemma Image_INT_eq: 

1048 
"[single_valued (r\<inverse>); A\<noteq>{}] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)" 

1049 
apply (rule equalityI) 

1050 
apply (rule Image_INT_subset) 

1051 
apply (simp add: single_valued_def, blast) 

1052 
done 

12905  1053 

12913  1054 
lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq>  ((r^1) `` (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

1055 
by blast 
12905  1056 

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

1057 
lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x: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

1058 
by auto 
12905  1059 

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

1060 
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

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

1062 

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

1063 
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

1064 
by auto 
12905  1065 

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

1066 
subsubsection {* Inverse image *} 
12905  1067 

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

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

1069 
where 
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

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

1071 

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

1072 
definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
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

1073 
where 
46694  1074 
"inv_imagep r f = (\<lambda>x y. r (f x) (f y))" 
1075 

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

1077 
by (simp add: inv_image_def inv_imagep_def) 

1078 

19228  1079 
lemma sym_inv_image: "sym r ==> sym (inv_image r 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

1080 
by (unfold sym_def inv_image_def) blast 
19228  1081 

12913  1082 
lemma trans_inv_image: "trans r ==> trans (inv_image r f)" 
12905  1083 
apply (unfold trans_def inv_image_def) 
1084 
apply (simp (no_asm)) 

1085 
apply blast 

1086 
done 

1087 

32463
3a0a65ca2261
moved lemma Wellfounded.in_inv_image to Relation.thy
krauss
parents:
32235
diff
changeset

1088 
lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" 
3a0a65ca2261
moved lemma Wellfounded.in_inv_image to Relation.thy
krauss
parents:
32235
diff
changeset

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

1090 

33218  1091 
lemma converse_inv_image[simp]: "(inv_image R f)^1 = inv_image (R^1) 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

1092 
unfolding inv_image_def converse_unfold by auto 
33218  1093 

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

1094 
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

1095 
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

1096 

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

1097 

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

1098 
subsubsection {* Powerset *} 
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

1099 

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

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

1101 
where 
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

1102 
"Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" 
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

1103 

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

1104 
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

1105 
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

1106 

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

1107 
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

1108 

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

1109 
subsubsection {* Expressing relation operations via @{const Finite_Set.fold} *} 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1110 

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

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

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

1113 
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

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

1115 
interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by default auto 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1116 
show ?thesis using assms unfolding Id_on_def by (induct A) simp_all 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1118 

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

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

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

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

1122 
interpret comp_fun_idem Set.insert 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1123 
by (fact comp_fun_idem_insert) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1124 
show ?thesis 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1125 
by default (auto simp add: fun_eq_iff comp_fun_commute split:prod.split) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1127 

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

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

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

1130 
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

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

1132 
interpret 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

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

1134 
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  1135 
by (force intro: rev_ImageI) 
48620
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1136 
show ?thesis using assms by (induct R) (auto simp: *) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1138 

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

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

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

1141 
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

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

1143 
interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1145 
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1146 
show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1147 
by default (auto simp add: fun_eq_iff split:prod.split) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1149 
have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1150 
show ?thesis unfolding * 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1151 
using `finite S` by (induct S) (auto split: prod.split) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1153 

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

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

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

1156 
shows "Set.insert x R O S = 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1157 
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

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

1159 
have "Set.insert x R O S = ({x} O S) \<union> (R O S)" by auto 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1160 
then show ?thesis by (auto simp: insert_relcomp_union_fold[OF assms]) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1162 

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

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

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

1165 
shows "comp_fun_commute (\<lambda>(x,y) A. 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1166 
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

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

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

1169 
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

1170 
by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1171 
show ?thesis by default (auto simp: *) 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

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

1173 

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

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

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

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

1177 
shows "R O S = Finite_Set.fold 
fc9be489e2fb
more relation operations expressed by Finite_Set.fold
kuncar
parents:
48253
diff
changeset

1178 
(\<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" 
52749  1179 
using assms by (induct R) 
1180 
(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

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

1182 

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

1183 
end 