72 "set_of_rel (rel_of_set R) = R" |
73 "set_of_rel (rel_of_set R) = R" |
73 by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) |
74 by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) |
74 |
75 |
75 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] |
76 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] |
76 |
77 |
77 definition rel :: "'a set => ('a * 'a) set => 'a rel" |
78 quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done |
78 where |
|
79 "rel X R = rel_of_set (rel_raw X R)" |
|
80 |
79 |
81 subsubsection {* Constant definitions on relations *} |
80 subsubsection {* Constant definitions on relations *} |
82 |
81 |
83 hide_const (open) converse rel_comp rtrancl Image |
82 hide_const (open) converse rel_comp rtrancl Image |
84 |
83 |
85 quotient_definition member :: "'a * 'a => 'a rel => bool" where |
84 quotient_definition member :: "'a * 'a => 'a rel => bool" where |
86 "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" |
85 "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done |
87 |
86 |
88 quotient_definition converse :: "'a rel => 'a rel" |
87 quotient_definition converse :: "'a rel => 'a rel" |
89 where |
88 where |
90 "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" |
89 "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done |
91 |
90 |
92 quotient_definition union :: "'a rel => 'a rel => 'a rel" |
91 quotient_definition union :: "'a rel => 'a rel => 'a rel" |
93 where |
92 where |
94 "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" |
93 "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done |
95 |
94 |
96 quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel" |
95 quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel" |
97 where |
96 where |
98 "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" |
97 "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done |
99 |
98 |
100 quotient_definition rtrancl :: "'a rel => 'a rel" |
99 quotient_definition rtrancl :: "'a rel => 'a rel" |
101 where |
100 where |
102 "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" |
101 "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done |
103 |
102 |
104 quotient_definition Image :: "'a rel => 'a set => 'a set" |
103 quotient_definition Image :: "'a rel => 'a set => 'a set" |
105 where |
104 where |
106 "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" |
105 "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done |
107 |
106 |
108 subsubsection {* Code generation *} |
107 subsubsection {* Code generation *} |
109 |
108 |
110 code_datatype rel |
109 code_datatype rel |
111 |
110 |
112 lemma [code]: |
111 lemma [code]: |
113 "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)" |
112 "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)" |
114 unfolding rel_def member_def |
113 by (lifting member_raw) |
115 by (simp add: member_raw) |
|
116 |
114 |
117 lemma [code]: |
115 lemma [code]: |
118 "converse (rel X R) = rel X (R^-1)" |
116 "converse (rel X R) = rel X (R^-1)" |
119 unfolding rel_def converse_def |
117 by (lifting converse_raw) |
120 by (simp add: converse_raw) |
|
121 |
118 |
122 lemma [code]: |
119 lemma [code]: |
123 "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)" |
120 "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)" |
124 unfolding rel_def union_def |
121 by (lifting union_raw) |
125 by (simp add: union_raw) |
|
126 |
122 |
127 lemma [code]: |
123 lemma [code]: |
128 "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))" |
124 "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))" |
129 unfolding rel_def rel_comp_def |
125 by (lifting rel_comp_raw) |
130 by (simp add: rel_comp_raw) |
|
131 |
126 |
132 lemma [code]: |
127 lemma [code]: |
133 "rtrancl (rel X R) = rel UNIV (R^+)" |
128 "rtrancl (rel X R) = rel UNIV (R^+)" |
134 unfolding rel_def rtrancl_def |
129 by (lifting rtrancl_raw) |
135 by (simp add: rtrancl_raw) |
|
136 |
130 |
137 lemma [code]: |
131 lemma [code]: |
138 "Image (rel X R) S = (X Int S) Un (R `` S)" |
132 "Image (rel X R) S = (X Int S) Un (R `` S)" |
139 unfolding rel_def Image_def |
133 by (lifting Image_raw) |
140 by (simp add: Image_raw) |
|
141 |
134 |
142 quickcheck_generator rel constructors: rel |
135 quickcheck_generator rel constructors: rel |
143 |
136 |
144 lemma |
137 lemma |
145 "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))" |
138 "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))" |