author  haftmann 
Sun, 26 Feb 2012 20:43:33 +0100  
changeset 46692  1f8b766224f6 
parent 46691  72d81e789106 
child 46694  0988b22e2626 
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 

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

5 
header {* Relations – as sets of pairs, and binary predicates *} 
12905  6 

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

10 

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

11 
subsection {* Classical rules for reasoning on predicates *} 
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 

46689  13 
(* CANDIDATE declare predicate1I [Pure.intro!, 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

14 
declare predicate1D [Pure.dest?, dest?] 
46689  15 
(* CANDIDATE declare predicate1D [Pure.dest, dest] *) 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

16 
declare predicate2I [Pure.intro!, intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

17 
declare predicate2D [Pure.dest, dest] 
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 bot1E [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 bot2E [elim!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

20 
declare top1I [intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

21 
declare top2I [intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

22 
declare inf1I [intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

23 
declare inf2I [intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

24 
declare inf1E [elim!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

25 
declare inf2E [elim!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

26 
declare sup1I1 [intro?] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

27 
declare sup2I1 [intro?] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

28 
declare sup1I2 [intro?] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

29 
declare sup2I2 [intro?] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

30 
declare sup1E [elim!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

31 
declare sup2E [elim!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

32 
declare sup1CI [intro!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

33 
declare sup2CI [intro!] 
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!] 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

35 
declare INF2_I [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

36 
declare INF1_D [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

37 
declare INF2_D [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

38 
declare INF1_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

39 
declare INF2_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

40 
declare SUP1_I [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

41 
declare SUP2_I [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

42 
declare SUP1_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

43 
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

44 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

45 

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 
subsection {* Conversions between set and predicate relations *} 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

47 

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 
lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = 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

49 
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

50 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

51 
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = 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

52 
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

53 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

54 
lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> 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

55 
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

56 

1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

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

58 
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

59 

46689  60 
lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})" 
61 
by (auto simp add: fun_eq_iff) 

62 

63 
lemma bot_empty_eq2 (* CANDIDATE [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

64 
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

65 

46689  66 
(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)" 
67 
by (auto simp add: fun_eq_iff) *) 

68 

69 
(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)" 

70 
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

71 

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

72 
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

73 
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

74 

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

75 
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

76 
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

77 

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

78 
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

79 
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

80 

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

81 
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

82 
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

83 

46689  84 
lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))" 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

85 
by (simp add: INF_apply 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

86 

46689  87 
lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))" 
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 (simp add: INF_apply 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 

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

90 
lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

91 
by (simp add: SUP_apply fun_eq_iff) 
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

92 

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

93 
lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" 
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

94 
by (simp add: SUP_apply 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

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 

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 
subsection {* Relations as sets of pairs *} 
12913  98 

46372  99 
type_synonym 'a rel = "('a * 'a) set" 
100 

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

101 
lemma subrelI:  {* Version of @{thm [source] subsetI} for binary relations *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

102 
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

103 
by auto 
7912  104 

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

105 
lemma lfp_induct2:  {* Version of @{thm [source] lfp_induct} for binary relations *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

106 
"(a, b) \<in> lfp f \<Longrightarrow> mono f \<Longrightarrow> 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

107 
(\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

108 
using lfp_induct_set [of "(a, b)" f "prod_case P"] by auto 
12913  109 

5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

110 

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

111 
subsubsection {* Reflexivity *} 
10786  112 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

113 
definition 
30198  114 
refl_on :: "['a set, ('a * 'a) set] => bool" where  {* reflexivity over a set *} 
45137  115 
"refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

116 

26297  117 
abbreviation 
30198  118 
refl :: "('a * 'a) set => bool" where  {* reflexivity over a type *} 
45137  119 
"refl \<equiv> refl_on UNIV" 
26297  120 

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

121 
lemma refl_onI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

123 

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

124 
lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

126 

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

127 
lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

129 

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

130 
lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

132 

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

133 
lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

135 

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

136 
lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

138 

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

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

140 
"ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

142 

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

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

144 
"ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

146 

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

147 
lemma refl_on_empty[simp]: "refl_on {} {}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

149 

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

150 
lemma refl_on_def' [nitpick_unfold, code]: 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

151 
"refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

152 
by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

153 

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

154 

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

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

156 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

157 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

158 
antisym :: "('a * 'a) set => bool" where  {* antisymmetry predicate *} 
45137  159 
"antisym r \<longleftrightarrow> (ALL x y. (x,y):r > (y,x):r > x=y)" 
6806
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
5978
diff
changeset

160 

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

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

162 
"(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

164 

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

165 
lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

167 

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

168 
lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

170 

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

171 
lemma antisym_empty [simp]: "antisym {}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

173 

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

174 

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

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

176 

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

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

178 
sym :: "('a * 'a) set => bool" where  {* symmetry predicate *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

179 
"sym r \<longleftrightarrow> (ALL x y. (x,y): r > (y,x): r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

180 

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

181 
lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

182 
by (unfold sym_def) iprover 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

183 

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

184 
lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

186 

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

187 
lemma sym_Int: "sym r ==> sym s ==> sym (r \<inter> s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

188 
by (fast intro: symI dest: symD) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

189 

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

190 
lemma sym_Un: "sym r ==> sym s ==> sym (r \<union> s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

191 
by (fast intro: symI dest: symD) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

192 

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

193 
lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

194 
by (fast intro: symI dest: symD) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

195 

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

196 
lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

197 
by (fast intro: symI dest: symD) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

198 

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

199 

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

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

201 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

202 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

203 
trans :: "('a * 'a) set => bool" where  {* transitivity predicate *} 
45137  204 
"trans r \<longleftrightarrow> (ALL x y z. (x,y):r > (y,z):r > (x,z):r)" 
5978
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5608
diff
changeset

205 

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

206 
lemma trans_join [code]: 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

207 
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

209 

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

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

211 
"(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

212 
by (unfold trans_def) iprover 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

213 

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

214 
lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

215 
by (unfold trans_def) iprover 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

216 

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

217 
lemma trans_Int: "trans r ==> trans s ==> trans (r \<inter> s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

219 

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

220 
lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

222 

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

223 

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

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

225 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

226 
definition 
45137  227 
irrefl :: "('a * 'a) set => bool" where 
228 
"irrefl r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r)" 

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

229 

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

230 
lemma irrefl_distinct [code]: 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

231 
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

233 

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

234 

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

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

236 

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

237 
definition 
45137  238 
total_on :: "'a set => ('a * 'a) set => bool" where 
239 
"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

240 

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

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

242 

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

243 
lemma total_on_empty[simp]: "total_on {} r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

244 
by(simp add:total_on_def) 
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 

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

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

248 

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

249 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

250 
single_valued :: "('a * 'b) set => bool" where 
45137  251 
"single_valued r \<longleftrightarrow> (ALL x y. (x,y):r > (ALL z. (x,z):r > y=z))" 
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
6806
diff
changeset

252 

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

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

254 
"ALL x y. (x,y):r > (ALL z. (x,z):r > y=z) ==> single_valued r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

256 

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

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

258 
"single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

260 

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

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

262 
"r \<subseteq> s ==> single_valued s ==> single_valued r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

263 
by (unfold single_valued_def) blast 
11136  264 

12905  265 

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

266 
subsubsection {* The identity relation *} 
12905  267 

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

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

269 
Id :: "('a * 'a) set" where  {* the identity relation *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

270 
"Id = {p. EX x. p = (x,x)}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

271 

12905  272 
lemma IdI [intro]: "(a, a) : Id" 
26271  273 
by (simp add: Id_def) 
12905  274 

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

26271  276 
by (unfold Id_def) (iprover elim: CollectE) 
12905  277 

278 
lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" 

26271  279 
by (unfold Id_def) blast 
12905  280 

30198  281 
lemma refl_Id: "refl Id" 
282 
by (simp add: refl_on_def) 

12905  283 

284 
lemma antisym_Id: "antisym Id" 

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

26271  286 
by (simp add: antisym_def) 
12905  287 

19228  288 
lemma sym_Id: "sym Id" 
26271  289 
by (simp add: sym_def) 
19228  290 

12905  291 
lemma trans_Id: "trans Id" 
26271  292 
by (simp add: trans_def) 
12905  293 

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

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

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

296 

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

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

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

299 

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

300 
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

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

302 

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

303 
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

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

305 

12905  306 

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

307 
subsubsection {* Diagonal: identity over a set *} 
12905  308 

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

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

310 
Id_on :: "'a set => ('a * 'a) set" where  {* diagonal: identity over a set *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

312 

30198  313 
lemma Id_on_empty [simp]: "Id_on {} = {}" 
314 
by (simp add: Id_on_def) 

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

315 

30198  316 
lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A" 
317 
by (simp add: Id_on_def) 

12905  318 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
33218
diff
changeset

319 
lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A" 
30198  320 
by (rule Id_on_eqI) (rule refl) 
12905  321 

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

12913  324 
 {* The general elimination rule. *} 
30198  325 
by (unfold Id_on_def) (iprover elim!: UN_E singletonE) 
12905  326 

30198  327 
lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" 
26271  328 
by blast 
12905  329 

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

331 
"Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
41792
diff
changeset

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

333 

30198  334 
lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" 
26271  335 
by blast 
12905  336 

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

337 
lemma refl_on_Id_on: "refl_on A (Id_on A)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

338 
by (rule refl_onI [OF Id_on_subset_Times Id_onI]) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

339 

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

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

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

342 

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

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

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

345 

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

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

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

348 

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

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

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

351 

12905  352 

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

353 
subsubsection {* Composition of two relations *} 
12905  354 

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

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

356 
rel_comp :: "[('a * 'b) set, ('b * 'c) set] => ('a * 'c) set" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

357 
(infixr "O" 75) where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

358 
"r O s = {(x,z). EX y. (x, y) : r & (y, z) : s}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

359 

12913  360 
lemma rel_compI [intro]: 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31011
diff
changeset

361 
"(a, b) : r ==> (b, c) : s ==> (a, c) : r O s" 
26271  362 
by (unfold rel_comp_def) blast 
12905  363 

12913  364 
lemma rel_compE [elim!]: "xz : r O s ==> 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31011
diff
changeset

365 
(!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s ==> P) ==> P" 
26271  366 
by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE) 
12905  367 

368 
lemma rel_compEpair: 

32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31011
diff
changeset

369 
"(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P" 
26271  370 
by (iprover elim: rel_compE Pair_inject ssubst) 
12905  371 

372 
lemma R_O_Id [simp]: "R O Id = R" 

26271  373 
by fast 
12905  374 

375 
lemma Id_O_R [simp]: "Id O R = R" 

26271  376 
by fast 
12905  377 

23185  378 
lemma rel_comp_empty1[simp]: "{} O R = {}" 
26271  379 
by blast 
23185  380 

381 
lemma rel_comp_empty2[simp]: "R O {} = {}" 

26271  382 
by blast 
23185  383 

12905  384 
lemma O_assoc: "(R O S) O T = R O (S O T)" 
26271  385 
by blast 
12905  386 

12913  387 
lemma trans_O_subset: "trans r ==> r O r \<subseteq> r" 
26271  388 
by (unfold trans_def) blast 
12905  389 

12913  390 
lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)" 
26271  391 
by blast 
12905  392 

393 
lemma rel_comp_subset_Sigma: 

32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31011
diff
changeset

394 
"r \<subseteq> A \<times> B ==> s \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C" 
26271  395 
by blast 
12905  396 

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

397 
lemma rel_comp_distrib[simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" 
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset

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

399 

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

400 
lemma rel_comp_distrib2[simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)" 
f945f8d9ad4d
added distributivity of relation composition over union [simp]
krauss
parents:
26297
diff
changeset

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

402 

36772  403 
lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)" 
404 
by auto 

405 

406 
lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)" 

407 
by auto 

408 

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

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

410 
"single_valued r ==> single_valued s ==> single_valued (r O s)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

411 
by (unfold single_valued_def) blast 
12905  412 

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

413 

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

414 
subsubsection {* Converse *} 
12913  415 

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

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

417 
converse :: "('a * 'b) set => ('b * 'a) set" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

418 
("(_^1)" [1000] 999) where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

419 
"r^1 = {(y, x). (x, y) : r}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

420 

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

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

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

423 

12913  424 
lemma converse_iff [iff]: "((a,b): r^1) = ((b,a) : r)" 
26271  425 
by (simp add: converse_def) 
12905  426 

13343  427 
lemma converseI[sym]: "(a, b) : r ==> (b, a) : r^1" 
26271  428 
by (simp add: converse_def) 
12905  429 

13343  430 
lemma converseD[sym]: "(a,b) : r^1 ==> (b, a) : r" 
26271  431 
by (simp add: converse_def) 
12905  432 

433 
lemma converseE [elim!]: 

434 
"yx : r^1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P" 

12913  435 
 {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} 
26271  436 
by (unfold converse_def) (iprover elim!: CollectE splitE bexE) 
12905  437 

438 
lemma converse_converse [simp]: "(r^1)^1 = r" 

26271  439 
by (unfold converse_def) blast 
12905  440 

441 
lemma converse_rel_comp: "(r O s)^1 = s^1 O r^1" 

26271  442 
by blast 
12905  443 

19228  444 
lemma converse_Int: "(r \<inter> s)^1 = r^1 \<inter> s^1" 
26271  445 
by blast 
19228  446 

447 
lemma converse_Un: "(r \<union> s)^1 = r^1 \<union> s^1" 

26271  448 
by blast 
19228  449 

450 
lemma converse_INTER: "(INTER S r)^1 = (INT x:S. (r x)^1)" 

26271  451 
by fast 
19228  452 

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

26271  454 
by blast 
19228  455 

12905  456 
lemma converse_Id [simp]: "Id^1 = Id" 
26271  457 
by blast 
12905  458 

30198  459 
lemma converse_Id_on [simp]: "(Id_on A)^1 = Id_on A" 
26271  460 
by blast 
12905  461 

30198  462 
lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" 
463 
by (unfold refl_on_def) auto 

12905  464 

19228  465 
lemma sym_converse [simp]: "sym (converse r) = sym r" 
26271  466 
by (unfold sym_def) blast 
19228  467 

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

26271  469 
by (unfold antisym_def) blast 
12905  470 

19228  471 
lemma trans_converse [simp]: "trans (converse r) = trans r" 
26271  472 
by (unfold trans_def) blast 
12905  473 

19228  474 
lemma sym_conv_converse_eq: "sym r = (r^1 = r)" 
26271  475 
by (unfold sym_def) fast 
19228  476 

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

26271  478 
by (unfold sym_def) blast 
19228  479 

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

26271  481 
by (unfold sym_def) blast 
19228  482 

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

483 
lemma total_on_converse[simp]: "total_on A (r^1) = total_on A r" 
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset

484 
by (auto simp: total_on_def) 
33bff35f1335
Moved Order_Relation into Library and moved some of it into Relation.
nipkow
parents:
29609
diff
changeset

485 

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

486 
lemma finite_converse [iff]: "finite (r^1) = finite r" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

487 
apply (subgoal_tac "r^1 = (%(x,y). (y,x))`r") 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

489 
apply (rule iffI) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

490 
apply (erule finite_imageD [unfolded inj_on_def]) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

491 
apply (simp split add: split_split) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

492 
apply (erule finite_imageI) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

493 
apply (simp add: converse_def image_def, auto) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

494 
apply (rule bexI) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

495 
prefer 2 apply assumption 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

497 
done 
12913  498 

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

499 

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

500 
subsubsection {* Domain, range and field *} 
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 
definition 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

503 
Domain :: "('a * 'b) set => 'a set" where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

504 
"Domain r = {x. EX y. (x,y):r}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

505 

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

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

507 
Range :: "('a * 'b) set => 'b set" where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

508 
"Range r = Domain(r^1)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

509 

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

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

511 
Field :: "('a * 'a) set => 'a set" where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

512 
"Field r = Domain r \<union> Range r" 
12905  513 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
33218
diff
changeset

514 
declare Domain_def [no_atp] 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

515 

12905  516 
lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)" 
26271  517 
by (unfold Domain_def) blast 
12905  518 

519 
lemma DomainI [intro]: "(a, b) : r ==> a : Domain r" 

26271  520 
by (iprover intro!: iffD2 [OF Domain_iff]) 
12905  521 

522 
lemma DomainE [elim!]: 

523 
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P" 

26271  524 
by (iprover dest!: iffD1 [OF Domain_iff]) 
12905  525 

46127  526 
lemma Domain_fst [code]: 
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

527 
"Domain r = fst ` r" 
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

528 
by (auto simp add: image_def Bex_def) 
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

529 

12905  530 
lemma Domain_empty [simp]: "Domain {} = {}" 
26271  531 
by blast 
12905  532 

32876  533 
lemma Domain_empty_iff: "Domain r = {} \<longleftrightarrow> r = {}" 
534 
by auto 

535 

12905  536 
lemma Domain_insert: "Domain (insert (a, b) r) = insert a (Domain r)" 
26271  537 
by blast 
12905  538 

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

26271  540 
by blast 
12905  541 

30198  542 
lemma Domain_Id_on [simp]: "Domain (Id_on A) = A" 
26271  543 
by blast 
12905  544 

13830  545 
lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)" 
26271  546 
by blast 
12905  547 

13830  548 
lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)" 
26271  549 
by blast 
12905  550 

12913  551 
lemma Domain_Diff_subset: "Domain(A)  Domain(B) \<subseteq> Domain(A  B)" 
26271  552 
by blast 
12905  553 

13830  554 
lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)" 
26271  555 
by blast 
556 

557 
lemma Domain_converse[simp]: "Domain(r^1) = Range r" 

558 
by(auto simp:Range_def) 

12905  559 

12913  560 
lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" 
26271  561 
by blast 
12905  562 

36729  563 
lemma fst_eq_Domain: "fst ` R = Domain R" 
44921  564 
by force 
22172  565 

29609  566 
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" 
567 
by auto 

568 

569 
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)" 

570 
by auto 

571 

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

572 
lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

573 
by auto 
12905  574 

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

575 
lemma finite_Domain: "finite r ==> finite (Domain r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

576 
by (induct set: finite) (auto simp add: Domain_insert) 
12905  577 

578 
lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" 

26271  579 
by (simp add: Domain_def Range_def) 
12905  580 

581 
lemma RangeI [intro]: "(a, b) : r ==> b : Range r" 

26271  582 
by (unfold Range_def) (iprover intro!: converseI DomainI) 
12905  583 

584 
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P" 

26271  585 
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD) 
12905  586 

46127  587 
lemma Range_snd [code]: 
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

588 
"Range r = snd ` r" 
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

589 
by (auto simp add: image_def Bex_def) 
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44921
diff
changeset

590 

12905  591 
lemma Range_empty [simp]: "Range {} = {}" 
26271  592 
by blast 
12905  593 

32876  594 
lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}" 
595 
by auto 

596 

12905  597 
lemma Range_insert: "Range (insert (a, b) r) = insert b (Range r)" 
26271  598 
by blast 
12905  599 

600 
lemma Range_Id [simp]: "Range Id = UNIV" 

26271  601 
by blast 
12905  602 

30198  603 
lemma Range_Id_on [simp]: "Range (Id_on A) = A" 
26271  604 
by auto 
12905  605 

13830  606 
lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)" 
26271  607 
by blast 
12905  608 

13830  609 
lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)" 
26271  610 
by blast 
12905  611 

12913  612 
lemma Range_Diff_subset: "Range(A)  Range(B) \<subseteq> Range(A  B)" 
26271  613 
by blast 
12905  614 

13830  615 
lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" 
26271  616 
by blast 
617 

618 
lemma Range_converse[simp]: "Range(r^1) = Domain r" 

619 
by blast 

12905  620 

36729  621 
lemma snd_eq_Range: "snd ` R = Range R" 
44921  622 
by force 
26271  623 

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

624 
lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

625 
by auto 
26271  626 

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

627 
lemma finite_Range: "finite r ==> finite (Range r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

628 
by (induct set: finite) (auto simp add: Range_insert) 
26271  629 

630 
lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s" 

631 
by(auto simp:Field_def Domain_def Range_def) 

632 

633 
lemma Field_empty[simp]: "Field {} = {}" 

634 
by(auto simp:Field_def) 

635 

636 
lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r" 

637 
by(auto simp:Field_def) 

638 

639 
lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s" 

640 
by(auto simp:Field_def) 

641 

642 
lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)" 

643 
by(auto simp:Field_def) 

644 

645 
lemma Field_converse[simp]: "Field(r^1) = Field r" 

646 
by(auto simp:Field_def) 

22172  647 

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

648 
lemma finite_Field: "finite r ==> finite (Field r)" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

649 
 {* A finite relation has a finite field (@{text "= domain \<union> range"}. *} 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

650 
apply (induct set: finite) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

651 
apply (auto simp add: Field_def Domain_insert Range_insert) 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

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

653 

12905  654 

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

655 
subsubsection {* Image of a set under a relation *} 
12905  656 

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

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

658 
Image :: "[('a * 'b) set, 'a set] => 'b set" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

659 
(infixl "``" 90) where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

660 
"r `` s = {y. EX x:s. (x,y):r}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

661 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
33218
diff
changeset

662 
declare Image_def [no_atp] 
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23709
diff
changeset

663 

12913  664 
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" 
26271  665 
by (simp add: Image_def) 
12905  666 

12913  667 
lemma Image_singleton: "r``{a} = {b. (a, b) : r}" 
26271  668 
by (simp add: Image_def) 
12905  669 

12913  670 
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)" 
26271  671 
by (rule Image_iff [THEN trans]) simp 
12905  672 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
33218
diff
changeset

673 
lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A" 
26271  674 
by (unfold Image_def) blast 
12905  675 

676 
lemma ImageE [elim!]: 

12913  677 
"b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P" 
26271  678 
by (unfold Image_def) (iprover elim!: CollectE bexE) 
12905  679 

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

681 
 {* This version's more effective when we already have the required @{text a} *} 

26271  682 
by blast 
12905  683 

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

26271  685 
by blast 
12905  686 

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

26271  688 
by blast 
12905  689 

30198  690 
lemma Image_Id_on [simp]: "Id_on A `` B = A \<inter> B" 
26271  691 
by blast 
13830  692 

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

26271  694 
by blast 
12905  695 

13830  696 
lemma Image_Int_eq: 
697 
"single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B" 

26271  698 
by (simp add: single_valued_def, blast) 
12905  699 

13830  700 
lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B" 
26271  701 
by blast 
12905  702 

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

703 
lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A" 
26271  704 
by blast 
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13639
diff
changeset

705 

12913  706 
lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B" 
26271  707 
by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) 
12905  708 

13830  709 
lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})" 
12905  710 
 {* NOT suitable for rewriting *} 
26271  711 
by blast 
12905  712 

12913  713 
lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)" 
26271  714 
by blast 
12905  715 

13830  716 
lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))" 
26271  717 
by blast 
13830  718 

719 
lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))" 

26271  720 
by blast 
12905  721 

13830  722 
text{*Converse inclusion requires some assumptions*} 
723 
lemma Image_INT_eq: 

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

725 
apply (rule equalityI) 

726 
apply (rule Image_INT_subset) 

727 
apply (simp add: single_valued_def, blast) 

728 
done 

12905  729 

12913  730 
lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq>  ((r^1) `` (B)))" 
26271  731 
by blast 
12905  732 

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

733 
lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}" 
26271  734 
by auto 
12905  735 

736 

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

737 
subsubsection {* Inverse image *} 
12905  738 

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

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

740 
inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set" where 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

741 
"inv_image r f = {(x, y). (f x, f y) : r}" 
1f8b766224f6
tuned structure; dropped already existing syntax declarations
haftmann
parents:
46691
diff
changeset

742 

19228  743 
lemma sym_inv_image: "sym r ==> sym (inv_image r f)" 
26271  744 
by (unfold sym_def inv_image_def) blast 
19228  745 

12913  746 
lemma trans_inv_image: "trans r ==> trans (inv_image r f)" 
12905  747 
apply (unfold trans_def inv_image_def) 
748 
apply (simp (no_asm)) 

749 
apply blast 

750 
done 

751 

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

752 
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

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

754 

33218  755 
lemma converse_inv_image[simp]: "(inv_image R f)^1 = inv_image (R^1) f" 
756 
unfolding inv_image_def converse_def by auto 

757 

23709  758 

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

759 
subsection {* Relations as binary predicates *} 
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

760 

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

761 
subsubsection {* Composition *} 
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

762 

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

763 
inductive pred_comp :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75) 
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

764 
for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where 
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

765 
pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c" 
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

766 

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

767 
inductive_cases pred_compE [elim!]: "(r OO s) a c" 
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

768 

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

769 
lemma pred_comp_rel_comp_eq [pred_set_conv]: 
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

770 
"((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O 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

771 
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

772 

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

773 

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

774 
subsubsection {* Converse *} 
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

775 

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

776 
inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^1)" [1000] 1000) 
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

777 
for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where 
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

778 
conversepI: "r a b \<Longrightarrow> r^1 b 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

779 

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

780 
notation (xsymbols) 
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

781 
conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 
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

782 

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

783 
lemma conversepD: 
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

784 
assumes ab: "r^1 a b" 
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

785 
shows "r b a" using ab 
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

786 
by cases simp 
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

787 

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

788 
lemma conversep_iff [iff]: "r^1 a b = r b 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

789 
by (iprover intro: conversepI dest: conversepD) 
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

790 

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

791 
lemma conversep_converse_eq [pred_set_conv]: 
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

792 
"(\<lambda>x y. (x, y) \<in> r)^1 = (\<lambda>x y. (x, y) \<in> r^1)" 
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

793 
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

794 

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

795 
lemma conversep_conversep [simp]: "(r^1)^1 = r" 
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

796 
by (iprover intro: order_antisym conversepI dest: conversepD) 
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

797 

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

798 
lemma converse_pred_comp: "(r OO s)^1 = s^1 OO r^1" 
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

799 
by (iprover intro: order_antisym conversepI pred_compI 
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

800 
elim: pred_compE dest: conversepD) 
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

801 

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

802 
lemma converse_meet: "(r \<sqinter> s)^1 = r^1 \<sqinter> s^1" 
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

803 
by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) 
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

804 

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

805 
lemma converse_join: "(r \<squnion> s)^1 = r^1 \<squnion> s^1" 
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

806 
by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) 
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

807 

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

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

809 
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

810 

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

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

812 
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

813 

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

814 

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

815 
subsubsection {* Domain *} 
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

816 

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

817 
inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" 
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

818 
for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where 
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

819 
DomainPI [intro]: "r a b \<Longrightarrow> DomainP r 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

820 

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

821 
inductive_cases DomainPE [elim!]: "DomainP r 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

822 

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

823 
lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)" 
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

824 
by (blast intro!: Orderings.order_antisym predicate1I) 
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

825 

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

826 

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

827 
subsubsection {* Range *} 
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

828 

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

829 
inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" 
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

830 
for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where 
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

831 
RangePI [intro]: "r a b \<Longrightarrow> RangeP r b" 
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

832 

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

833 
inductive_cases RangePE [elim!]: "RangeP r b" 
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

834 

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

835 
lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)" 
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

836 
by (blast intro!: Orderings.order_antisym predicate1I) 
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

837 

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

838 

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

839 
subsubsection {* Inverse image *} 
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

840 

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

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

842 
"inv_imagep r f = (\<lambda>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

843 

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

844 
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" 
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

845 
by (simp add: inv_image_def 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

846 

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

847 
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

848 
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

849 

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

850 

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

851 
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

852 

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

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

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

855 

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

856 
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

857 
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

858 

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

859 
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

860 

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

861 

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

862 
subsubsection {* Properties of predicate relations *} 
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

863 

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

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

865 
"antisymP r \<equiv> antisym {(x, y). r x 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

866 

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

867 
abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where 
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

868 
"transP r \<equiv> trans {(x, y). r x 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

869 

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

870 
abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where 
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

871 
"single_valuedP r \<equiv> single_valued {(x, y). r x 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

872 

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

873 
(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*) 
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

874 

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

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

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

877 

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

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

879 
"symp r \<longleftrightarrow> sym {(x, y). r x 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

880 

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

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

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

883 

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

884 
lemma reflpI: 
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

885 
"(\<And>x. r x x) \<Longrightarrow> reflp r" 
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

886 
by (auto intro: refl_onI simp add: reflp_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

887 

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

888 
lemma reflpE: 
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

889 
assumes "reflp r" 
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

890 
obtains "r x 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

891 
using assms by (auto dest: refl_onD simp add: reflp_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

892 

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

893 
lemma sympI: 
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

894 
"(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r" 
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

895 
by (auto intro: symI simp add: symp_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

896 

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

897 
lemma sympE: 
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

898 
assumes "symp r" and "r x 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

899 
obtains "r y 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

900 
using assms by (auto dest: symD simp add: symp_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

901 

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

902 
lemma transpI: 
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

903 
"(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" 
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

904 
by (auto intro: transI simp add: transp_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

905 

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

906 
lemma transpE: 
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

907 
assumes "transp r" and "r x y" and "r y z" 
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

908 
obtains "r x z" 
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

909 
using assms by (auto dest: transD simp add: transp_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

910 

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

911 
end 
46689  912 